[isabelle] Failing afp-2015 build
while trying to run some performance tests on potential future Jenkins
servers, I've encountered a ? in my opinion ? severe problem. The setup is
$ isabelle version
Isabelle2015: May 2015
$ uname -a
Linux lars-demon 4.2.3-1-ARCH #1 SMP PREEMPT Sat Oct 3 18:52:50 CEST 2015
$ hg id # afp-2015 repository
If I now run the session "ConcurrentGC", this happens:
$ isabelle build -bv -d thys -o threads=1 ConcurrentGC
*** A total of 104 subgoals...
*** At command "by" (line 130 of "~/proj/afp-2015/thys/ConcurrentGC/TSO.thy")
Unfinished session(s): ConcurrentGC
Exactly the same error occurs with the following settings:
I have managed to reproduce this behaviour on three different machines.
However, now comes the worrying part: If I load the failing theory in
Isabelle/jEdit, it goes through just fine! Same goes for building without
"-o threads=1" *. This is a real problem, because I was actually planning
to run each session of the AFP with "-o threads=1". Can anybody reproduce
this behaviour? I'm scared ...
* it's still running on my machine, but the build has progressed well
This archive was generated by a fusion of
Pipermail (Mailman edition) and