[isabelle-dev] AFP devel broken

Lars Noschinski noschinl at in.tum.de
Wed Dec 5 15:37:56 CET 2012


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



More information about the isabelle-dev mailing list