Re: [isabelle] Isabelle on a Mac running linux
I had the same problem a few days ago. You need to change the file
etc/settings so that in the first section (# Poly/ML 4.x/5.x
(automated settings)) one of the options is the directory of Poly/ML;
the automated settings are not correct. For instance, in my system,
everything lives in /usr/local (i.e. Isabelle directory, ProofGeneral
directory, Poly/ML directory are all in this folder), so I added the
as one of the places it looks for ML_HOME. Then it should work
fine. (NOTE I run my Mac under OSX, but I don't think it should make
a difference, since it's the exact same error message I got)
On 31 Oct 2007, at 23:06, C. Menon wrote:
I'm trying to install Isabelle on an Apple Powerbook running linux.
I've got a working copy of Poly/ML from the polyml site, but when I
run Isabelle I get the following:
Exception Io raised while writing to stdOut.
Unknown logic "HOL" -- no heap file found in:
When I try to build HOL I get the following error:
Started at Thu Nov 1 09:32:39 EST 2007 (polyml_ppc-linux on cmenon)
make: Entering directory `/usr/local/Isabelle2005/src/Pure'
Building Pure ...
(see also /usr/local/Isabelle2005/heaps/polyml_ppc-linux/log/Pure)
/usr/local/Isabelle2005/lib/scripts/run-polyml: line 50: cd: ../lib/
poly: No such file or directory
Unable to locate /usr/local/bin/ML_dbase
Please check your ML system settings!
make: *** [/usr/local/Isabelle2005/heaps/polyml_ppc-linux/Pure]
make: Leaving directory `/usr/local/Isabelle2005/src/Pure'
make: *** [Pure] Error 2
Finished at Thu Nov 1 09:32:40 EST 2007
0:00:01 total elapsed time
My Poly/ML version seems to be working fine, as I can use it
separately from Isabelle. Has anyone else had this problem?
Thanks in advance!
This archive was generated by a fusion of
Pipermail (Mailman edition) and