Re: [isabelle] Isabelle on a Mac running linux



Hi Catherine

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 line

 "/usr/local/polyml/"

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)

Peter


On 31 Oct 2007, at 23:06, C. Menon wrote:

Hi all,
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:
  /home/cmenon/isabelle/heaps/polyml_ppc-linux
  /usr/local/Isabelle2005/heaps/polyml_ppc-linux

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[1]: Entering directory `/usr/local/Isabelle2005/src/Pure'
Building Pure ...
Pure FAILED
(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[1]: *** [/usr/local/Isabelle2005/heaps/polyml_ppc-linux/Pure] Error 2
make[1]: 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!
Catherine







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