[isabelle] Isabelle on a Mac running linux



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.