[isabelle-dev] SML makeall fails

Lukas Bulwahn bulwahn at in.tum.de
Sun Feb 19 15:22:50 CET 2012


Hi all,


for three weeks, SML-makeall is continuously  failing with the following 
error message:

[/tmp/mira/workbench/15468-139692104476416/Isabelle/heaps/smlnj_x86-linux/HOL-Proofs] 
Error 152
[/tmp/mira/workbench/15468-139692104476416/Isabelle/heaps/smlnj_x86-linux/log/HOL-Metis_Examples.gz] 
Error 152
[/tmp/mira/workbench/15468-139692104476416/Isabelle/heaps/smlnj_x86-linux/HOL-IMP] 
Error 152

The error occured the first time on changeset 6d2af424d0f8 (cf. 
http://isabelle.in.tum.de/reports/Isabelle/rev/6d2af424d0f8) and 
SML-makeall still succeeded on fd21bbcbe61b.
In the time between those changesets, mainly three developers have been 
doing some changes.

We should look why the errors occur. Maybe we have to adjust the 
timeouts for these sessions.


Lukas


More information about the isabelle-dev mailing list