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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
