[isabelle] Isabelle 2005 (Instalation problems) (Needed for HOL-Z)



Dear Isabelle Users,

I have to install/use the HOL-Z system but it compiles/runs only under
Isabelle 2005. I have tried Isabelle 2008, but it does not work.
However,  when I run

./bin/isatool install -p /usr/local/bin I get the following error
message:

[root at localhost Isabelle]# ./bin/isatool install -p /usr/local/bin/
Exception Io raised while writing to stdOut.
referring to distribution at /home/alfio/Isabelle2005
installing /usr/local/bin//isatool
installing /usr/local/bin//isabelle-process
installing /usr/local/bin//isabelle-interface
installing /usr/local/bin//Isabelle
installing /usr/local/bin//isabelle
[root at localhost Isabelle]# ./build FOL
Exception Io raised while writing to stdOut.

Then, after this, I cannot longer compile the logics, as in:

./build FOL
Exception Io raised while writing to stdOut.

                *****************************
                * Welcome to Isabelle build *
                *****************************

Please check /home/alfio/Isabelle2005/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/bin
  ML_OPTIONS=-H 80
  ML_PLATFORM=x86-linux

  ISABELLE_USEDIR_OPTIONS=-v true -V outline=/proof,/ML
  HOL_USEDIR_OPTIONS=


since, the system no longer gets the right ML_HOME (the current value shown
above is wrong), which I always set at /etc/settings. This problem does
not arises if I install Isabelle 2008 instead. I wonder if this incompatibility
of Isabele 2005 has to do with Poly/ML 5.2.1, which I have installed. I even
tried to build the previous version (4.2) of Poly/ML, but I could not even
unpack the distribution file.

Many Thanks!

|Prof. Alfio Martini
|http://www.inf.pucrs.br/~alfio
|PUCRS - Pontificia Universidade Catolica do Rio Grande do Sul
|Faculty of Informatics -- Av. Ipiranga 6681
|Predio 32 -- 90619 - 900
|Porto Alegre - RS - Brasil
|Tel: +55 (051) 3320-8707
|Fax: +55 (051) 3320-3758 





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