[isabelle-dev] AFP devel broken

[Tobias Nipkow]

I tried again (but after some hg fetches, and am now on 3ae4376cb739), and now
HOL still builds but HOLCF hangs. On the other hand Johannes (running Linux
rather than MacOS) is fine. Suspicion: I had to do isabelle components -a this
morning, and this may have done it.

Tobias

Am 05/12/2012 15:37, schrieb Lars Noschinski:
> On 05.12.2012 08:31, Tobias Nipkow wrote:
>> 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
> 
> This session builds for me. However, JinjaThreads (or Collections?) fails with a
> not so useful error message:
> 
> # isa afp_build -A -- -v -j2
> [...]
> Building Collections ...
> Running JinjaThreads ...
> I/O error: Stream closed
> Finished at Mi 5. Dez 15:21:29 CET 2012
> 0:22:18 elapsed time, 0:00:24 cpu time, factor 0.01
> 
> However, both log/JinjaThreads.gz, log/Collections.gz exist and don't record an
> error.
> 
>   -- Lars
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev