[isabelle-dev] Failure semantics for isabelle sessions

Alexander Krauss krauss at in.tum.de
Wed Oct 19 22:34:34 CEST 2011


Hi all,

Many of us have already seen isatest and other failures with of the 
following form:

/tmp/mira/workbench/26748-140130062513920/Isabelle/lib/scripts/run-polyml: 
line 77: 13588 Killed                  "$POLY" -q $ML_OPTIONS

...

make: *** 
[/tmp/mira/workbench/26748-140130062513920/Isabelle/heaps/polyml-5.4.0_x86_64-linux/log/HOL-Regular-Sets.gz] 
Error 137

or

/tmp/mira/workbench/42947-139804334458624/Isabelle/lib/scripts/run-polyml: 
line 77: 58024 Aborted                 "$POLY" -q $ML_OPTIONS

...

make: *** 
[/tmp/mira/workbench/42947-139804334458624/Isabelle/heaps/polyml-5.4.0_x86_64-linux/log/HOL-Word-JinjaThreads.gz] 
Error 134


Does anybody know if there is a straightforward translation of the error 
codes 134/137 into English?

It would be really useful if we had a table of the most common failure 
situations, and I wonder if some of this knowledge is already floating 
around somewhere...

Alex


More information about the isabelle-dev mailing list