Email Gateway (Aug 18 2022 at 16:35): Email Gateway (Aug 18 2022 at 16:35):From: Walther Neuper <wneuper@ist.tugraz.at>
Hi,
for certain reasons we need to install Isabelle2002 once again, and are
not familiar with the old setup anymore.
After having installed polyml-4.1.3 we proceeded with
neuper@neuper:~/proto3-sml/Isabelle2002$ sudo ./build Pure
*********
* Welcome to Isabelle build * *********
Please check /home/neuper/proto3-sml/Isabelle2002/etc/settings
to make sure that Isabelle's ML system settings and compilation options
are appropriate.
The current values are:
ML_SYSTEM=polyml
ML_HOME=/usr/local/polyisac/unknown-platform
ML_OPTIONS=-h 15000
ML_PLATFORM=unknown-platform
ISABELLE_USEDIR_OPTIONS=-i true
Press RETURN to compilation of
Pure
Started at Tue Dec 21 11:24:28 CET 2010 (polyml_unknown-platform on neuper)
Building Pure ...
Pure FAILED
(see also /home/neuper/proto3-sml/Isabelle2002/heaps/polyml_unknown-platform/log/Pure)
/home/neuper/proto3-sml/Isabelle2002/bin/../lib/scripts/run-polyml: line 97: 15426 Done echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();"
15427 Segmentation fault | "$POLY" -r "$INFILE"
Unable to create output heap file: "/home/neuper/proto3-sml/Isabelle2002/heaps/polyml_unknown-platform/Pure"
make: *** [/home/neuper/proto3-sml/Isabelle2002/heaps/polyml_unknown-platform/Pure] Error 2
Finished at Tue Dec 21 11:24:28 CET 2010
0:00:00 total elapsed time
neuper@neuper:~/proto3-sml/Isabelle2002$
Is there somebody with long memory to help us ?
Walther
Email Gateway (Aug 18 2022 at 16:35):From: Jeremy Dawson <jlcaadawson@netspeed.com.au>
Walther,
I assume you're using the default generation of settings which (I
gather) sort of tries to guess them, which is great when it works. When
it doesn't I've always found it far too complicated to analyse and
troubleshoot the guessing process, but rather I ("manually") set the
right values.
As for working out the right values, here is what I used for
Isabelle2005 and polyml 4.1.4 (which are both installed just below my
home directory):
# Poly/ML 4.1.4 JED
ML_PLATFORM=x86-linux
ML_HOME=/home/users/jeremy/polyml-4.1.4/x86-linux
ML_SYSTEM=polyml-4.1.4
ML_OPTIONS="-H 80"
However Isabelle2002 may not be the same, I seem to recall that
occasionally Isabelle's way of naming relevant directories has changed.
Regards,
Jeremy
Email Gateway (Aug 18 2022 at 16:36):From: Walther Neuper <wneuper@ist.tugraz.at>
Jeremy,
due to your hints we made it run again --- a great Christmas present for
us, thanks a lot !
Walther
Last updated: Apr 24 2024 at 01:07 UTC