[isabelle-dev] segmentation faults

[Tobias Nipkow]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5059 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20150116/501b171e/attachment.p7s>