Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle 2005 (Instalation problems) (Needed f...

view this post on Zulip Email Gateway (Aug 18 2022 at 12:51):

From: Alfio Ricardo de B Martini <alfio.martini@pucrs.br>
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@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@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

view this post on Zulip Email Gateway (Aug 18 2022 at 12:51):

From: Alfio Ricardo de B Martini <alfio.martini@pucrs.br>
Hi to everyone,

I was able to solve the problem with SML NJ, version 110.67.

Cheers

|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

Last updated: May 03 2024 at 12:27 UTC