Re: [isabelle] installing Isabelle under polyml-5



Jeremy Dawson wrote:

I'm trying to build Isabelle 2005 under PolyML 5.1 and get the following error:
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






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