[isabelle-dev] segmentation faults

[Makarius]

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
> HOL-IMPP FAILED

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


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


 	Makarius