Re: [isabelle] Isabelle2014-RC0 available for testing



On Mon, 7 Jul 2014, C. Diekmann wrote:

Finally, when I try to sledgehammer something in one of my thys, the
prover crashes.
"Welcome to Isabelle/HOL (Isabelle2014-RC0: July 2014)
Malformed message:
bad chunk (unexpected EOF after 0 of 7314 bytes)
message_output terminated
/home/diekmann/Downloads/Isabelle2014-RC0/lib/scripts/run-polyml-5.5.2:
line 84: 15324 Segmentation fault      (core dumped) "$POLY" -q -i
$ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl"
"$MLTEXT")" --error-exit < /dev/null

standard_error terminated
standard_output terminated
process terminated
command_input terminated
process_manager terminated
Return code: 139"
I will try to reproduce this in a minimal example

This is a total failure of existance of the ML runtime system, which is polyml-5.5.2 in Isabelle2014-R0.

In order to make some educated guesses what could be wrong, we need precise information about the hardware (CPU model and memory size), apart from the OS (which was Ubuntu 14.04 LTS here). Did you use x86 or x86_64 for Poly/ML? This depends on pre-installed C/C++ libraries.

If you know how to tinker with Isabelle components, you can also try with polyml-5.5.1-1 from the Isabelle component repository, e.g. claiming it via init_component in $ISABELLE_HOME_USER/etc/settings and using "isabelle components -a" as described in the "system" manual.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.