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
"Welcome to Isabelle/HOL (Isabelle2014-RC0: July 2014)
bad chunk (unexpected EOF after 0 of 7314 bytes)
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and