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 Running HOL-TLA-Buffer .../Users/nipkow/isabelle/lib/scripts/run-polyml-5.5.2: line 82: 4075 Segmentation fault: 11 "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" --error-exit < /dev/null
HOL-TLA-Buffer FAILED Running ZF-Coind .../Users/nipkow/isabelle/lib/scripts/run-polyml-5.5.2: line 82: 6404 Segmentation fault: 11 "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" --error-exit < /dev/null
ZF-Coind FAILED parent: 59379:c7f6f01ede15 tip 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) Running HOL-TLA-Buffer ... Finished HOL-TLA-Buffer (0:00:05 elapsed time, 0:00:05 cpu time, factor 1.00) Running ZF-Coind ... Finished ZF-Coind (0:00:02 elapsed time, 0:00:02 cpu time) 0:00:21 elapsed time, 0:00:44 cpu time, factor 2.09 Given the short execution times: have those theories really been tested? Tobias
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
