Re: [isabelle] Isabelle2002



On 12/21/2010 09:40 PM, Walther Neuper wrote:
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 at 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 at neuper:~/proto3-sml/Isabelle2002$


Is there somebody with long memory to help us ?
Walther




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









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