Email Gateway (Aug 18 2022 at 10:02): Email Gateway (Aug 18 2022 at 10:02):From: Thomas Bleher <bleher@informatik.uni-muenchen.de>
I can get polyml to dump core using the attached files.
polyml crashes on the "apply (erule_tac [!] SLE66.transs.elims,
simp_all)" in SLE66.thy (right at the bottom).
The actual error message is (from isabelle):
catchSEGV; &context = 0x8088304, in_run_time_system=1, context.trapno=14
/home/thomas/local/opt/Isabelle2005/lib/scripts/run-polyml: line 126: 9984 Segmentation fault (core dumped) "$POLY" $ML_OPTIONS "$(fixpath "$DB")"
I'm using Isabelle2005, polyml 4.1.4 (downloaded from the Isabelle home
page) and AWE 0.4 (downloaded from
http://www.informatik.uni-bremen.de/~cxl/awe/)
Seems like it's some interaction with AWE, because it works fine if I
remove the "use_thy ...AWE.thy" from SLE66.thy.
However, I currently use AWE in another theory just fine, so in general
the system is working, it just blows up on this specific command.
I didn't know where best to post this bug; if this is the wrong place
please let me know.
Any help appreciated,
Thomas
Basis.thy
ISM.thy
ISM_package.thy
SLE66.thy
Email Gateway (Aug 18 2022 at 10:03):From: Makarius <makarius@sketis.net>
This looks like a genuine problem of Poly/ML 4.1.4 (which is just 4.2.0
with a few back-patches). You may want to report this on the polyml
mailing list, or just try the forthcoming Poly/ML 5.0 right now:
http://www.polyml.org/Version5Beta.html
Then you will also need proper ML compatibility wrappers for Isabelle2005:
http://www4.in.tum.de/~wenzelm/test/Isabelle2005-polyml-5.0.tar.gz
Makarius
Last updated: May 03 2024 at 01:09 UTC