Email Gateway (Aug 18 2022 at 16:16): Email Gateway (Aug 18 2022 at 16:16):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
I'm trying to build Isabelle 2005 under PolyML 5.1 and get the following
error:
*********
* Welcome to Isabelle build * *********
Please check /home/users/jeremy/Isabelle2005/etc/settings
to make sure that Isabelle's ML system settings and compilation options
are appropriate.
The current values are:
ML_SYSTEM=polyml-5.1
ML_HOME=/home/users/jeremy/polyml-5.1/x86-linux
ML_OPTIONS=-H 500
ML_PLATFORM=x86-linux
ISABELLE_USEDIR_OPTIONS=-v true -V outline=/proof,/ML
HOL_USEDIR_OPTIONS=
Press RETURN to compilation of
HOL
Started at Mon Oct 25 16:00:34 EST 2010 (polyml-5.1_x86-linux on stiletto)
make[1]: Entering directory `/home/users/jeremy/Isabelle2005/src/Pure'
Building Pure ...
Pure FAILED
(see also
/home/users/jeremy/Isabelle2005/heaps/polyml-5.1_x86-linux/log/Pure)
Unable to locate /home/users/jeremy/polyml-5.1/x86-linux/ML_dbase
Please check your ML system settings!
make[1]: ***
[/home/users/jeremy/Isabelle2005/heaps/polyml-5.1_x86-linux/Pure] Error 2
make[1]: Leaving directory `/home/users/jeremy/Isabelle2005/src/Pure'
make: *** [Pure] Error 2
Finished at Mon Oct 25 16:00:34 EST 2010
0:00:00 total elapsed time
But I have built Isabelle2007 under polyml-5.1 successfully.
In etc/settings I put the following (copied from Isabelle2007/etc/settings)
ML_PLATFORM=x86-linux
ML_HOME=/home/users/jeremy/polyml-5.1/x86-linux
ML_SYSTEM=polyml-5.1
ML_OPTIONS="-H 500"
Have I got these settings wrong ? How do I fix this ?
Jeremy
Email Gateway (Aug 18 2022 at 16:16):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Jeremy Dawson wrote:
Further to the above, I've tried to build Isabelle 2007 - under Polyml
5.1 it seems to work fine, but under PolyML 5.2 it gives the following
error
*********
Please check /home/users/jeremy/Isabelle2007/etc/settings
to make sure that Isabelle's ML system settings and compilation options
are appropriate.
The current values are:
ML_SYSTEM=polyml-5.2
ML_HOME=/home/users/jeremy/polyml-5.2/x86-linux
ML_OPTIONS=-H 500
ML_PLATFORM=x86-linux
ISABELLE_USEDIR_OPTIONS=-p 1 -v true -V outline=/proof,/ML
HOL_USEDIR_OPTIONS=
Press RETURN to compilation of
FOL
Started at Tue Oct 26 18:24:01 EST 2010 (polyml-5.2_x86-linux on stiletto)
make[1]: Entering directory `/home/users/jeremy/Isabelle2007/src/Pure'
Building Pure ...
Pure FAILED
(see also
/home/users/jeremy/Isabelle2007/heaps/polyml-5.2_x86-linux/log/Pure)
Unable to locate /home/users/jeremy/polyml-5.2/x86-linux/ML_dbase
Please check your ML system settings!
make[1]: ***
[/home/users/jeremy/Isabelle2007/heaps/polyml-5.2_x86-linux/Pure] Error 2
make[1]: Leaving directory `/home/users/jeremy/Isabelle2007/src/Pure'
make: *** [Pure] Error 2
In fact so far as I can tell, PolyML-5.x doesn't have an ML_dbase, why
does the Isabelle build process want one ?
If I'm to check my ML system settings, what particular things should
they point to ?
thanks
Jeremy
Email Gateway (Aug 18 2022 at 16:16):From: Alexander Krauss <krauss@in.tum.de>
Hi Jeremy,
Combining Isabelle releases with versions of polyml that are much
younger normally does not work, unless you are lucky.
Looking at our local installations of old Isabelle versions, it seems
that Isabelle 2005 came with polyml 4.1.3, and Isabelle 2007 with polyml
5.1.
I vaguely remember a patch for Isabelle2005 floating around that made it
work with polyml 5. You might find it if you search the mailing list
archives.
Alex
Email Gateway (Aug 18 2022 at 16:17):From: Makarius <makarius@sketis.net>
BTW, the general solution to this kind of problem was invented by IBM in
the 1970-ies or so: hardware virtualisation. With something like
Virtualbox you can keep old versions of Linux, Poly/ML, and Isabelle
running for many more years.
Makarius
Email Gateway (Aug 18 2022 at 16:17):From: Jeremy Dawson <jlcaadawson@netspeed.com.au>
Thanks Alex, I've found a reference to the fact that Makarius had done
this, but no patch.
If each version of Isabelle only works with a specific (or sufficiently
old) version of PolyML, then
the old versions of PolyMl also need to be made available on the website
together with the old Isabelle releases.
Regards,
Jeremy
Email Gateway (Aug 18 2022 at 16:23):From: Makarius <makarius@sketis.net>
Full distributions in this sense are archived at
http://isabelle.in.tum.de/download_past.html -- starting with Isabelle2008
only.
Really old Isabelle versions can be easily compiled using SML/NJ, instead
of Poly/ML. While Poly/ML is still young and evolving fast, SML/NJ did
never really change in the past 15 years. The only incompatibilty is the
update of the basis library definition in 2004.
Just a few days ago, I managed to get Isabelle98 work with current SML/NJ
110.72 on Mac OS X (Intel 64bit), which was easy due to the lack of Proof
General in the 98 version. For the historical record, the relevant
src/Pure/ML-Systems/smlnj.ML is included here.
Makarius
smlnj.ML
Last updated: Nov 21 2024 at 12:39 UTC