[isabelle-dev] AFP devel broken
nipkow at in.tum.de
Wed Dec 5 08:31:59 CET 2012
I believe Gerwin already reported this in some email, and I can confirm it: the
afp test hangs even on my own laptop. The trace:
lapbroy100:AFP nipkow$ isabelle afp_build -A
Building Jinja ...
Finished Jinja (0:05:06 elapsed time, 0:15:28 cpu time, factor 3.03)
Building LatticeProperties ...
Finished LatticeProperties (0:00:13 elapsed time, 0:00:22 cpu time, factor 1.69)
Building HOL-Probability ...
Finished HOL-Probability (0:01:47 elapsed time, 0:05:10 cpu time, factor 2.89)
Building Group-Ring-Module ...
Finished Group-Ring-Module (0:02:50 elapsed time, 0:08:24 cpu time, factor 2.96)
Building Simpl ...
Finished Simpl (0:02:05 elapsed time, 0:05:35 cpu time, factor 2.68)
Building Collections ...
Finished Collections (0:04:51 elapsed time, 0:11:08 cpu time, factor 2.29)
Building Refine_Monadic ...
And this is where it ends. No more activity: CPU usage: 0.23% user
Can anybody still build the AFP on some machine?
Am 03/12/2012 06:38, schrieb Gerwin Klein:
> After looking at this over the weekend, the problem still escapes me.
> On macbroy2 when using the installation in ~/afp/isadist/Isabelle (basically the last built development snapshot), the session HOL-Probability with a high probability just hangs. This can be confirmed interactively:
> macbroy2:Probability isatest$ pwd
> macbroy2:Probability isatest$ ~/afp/isadist/Isabelle/bin/isabelle tty -l HOL-Multivariate_Analysis
>> val it = (): unit
> val commit = fn: unit -> bool
> Unofficial version of Isabelle/HOL-Multivariate_Analysis (Isabelle repository snapshot 38870ee59311 02-Dec-2012)
>> use_thy "Probability";
> just hangs (also doesn't react to Ctrl-C). Copying the isadist directory to my laptop and linking it with the corresponding contrib directory built that session just fine in under 2 min.
> Any ideas anyone?
> I'm tempted to move the whole AFP test to a different machine just to get things going again, it's been quite a while since we've had any solid test results.
> On 29/11/2012, at 11:47 PM, Christian Sternagel <c-sterna at jaist.ac.jp> wrote:
>> On 11/09/2012 12:26 AM, Christian Sternagel wrote:
>>> Just follow the "Browse theories" link of any devel entry, e.g.,
>> As far as I can tell the problem still remains. Is it known in the meantime what the problem is?
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev