[isabelle-dev] segmentation faults

Makarius makarius at sketis.net
Sat Jan 17 15:26:18 CET 2015

On Fri, 16 Jan 2015, Tobias Nipkow wrote:

> The AFP test has been failing for random entries with segmentation fault
> over the last few days. Now the same thing is happening when I test HOL
> locally on my Mac. My latest test run yielded
> Running HOL-IMPP ...
> /Users/nipkow/isabelle/lib/scripts/run-polyml-5.5.2: line 82:   473 
> Segmentation fault: 11  "$POLY" -q -i $ML_OPTIONS --eval "$(perl 
> "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" --error-exit < /dev/null

I have seen such core dumps only very sporadically so far.  If there is a 
known configuration where it happens reliably, it would help to figure out 
the reasons.  Where is the AFP test configuration formalized?

> Moreover, when I rerun the build I get
> Running HOL-IMPP ...
> Finished HOL-IMPP (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.16)
> Given the short execution times: have those theories really been tested?

Probably not.  The log.gz files should contain some information what 
really happened -- it might actually provide further clues about the above 

As a quick workaround it might also help to use ML_OPTIONS="-H 1500" or 
even ML_OPTIONS="-H 2000".


More information about the isabelle-dev mailing list