[isabelle] Failing afp-2015 build



Dear list,

while trying to run some performance tests on potential future Jenkins
servers, I've encountered a ? in my opinion ? severe problem. The setup is
as follows:

$ 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
x86_64 GNU/Linux

$ hg id # afp-2015 repository
770bf7fe6d2b tip

If I now run the session "ConcurrentGC", this happens:

$ isabelle build -bv -d thys -o threads=1 ConcurrentGC
[...]
ML_PLATFORM="x86-linux"
ML_HOME="/opt/Isabelle2015/contrib/polyml-5.5.2-3/x86-linux"
ML_SYSTEM="polyml-5.5.2"
ML_OPTIONS="-H 500"
[...]
*** 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:

ML_PLATFORM="x86_64-linux"
ML_HOME="/opt/Isabelle2015/contrib/polyml-5.5.2-3/x86_64-linux"
ML_SYSTEM="polyml-5.5.2"
ML_OPTIONS="-H 2000"

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 ...

Best
Lars


* it's still running on my machine, but the build has progressed well
beyond "TSO"




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.