[isabelle-dev] AFP devel broken

[Tobias Nipkow]

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?

Tobias

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
> /home/isatest/afp/isadist/Isabelle/src/HOL/Probability
> 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.
> 
> Gerwin
> 
> 
> 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.,
>>> http://afp.sourceforge.net/browser_info/devel/HOL/Bondy/index.html
>> As far as I can tell the problem still remains. Is it known in the meantime what the problem is?
>>
>> cheers
>>
>> chris
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>