Email Gateway (Aug 18 2022 at 10:57): Email Gateway (Aug 18 2022 at 10:57):From: "C. Menon" <cmenon@ics.mq.edu.au>
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
Email Gateway (Aug 18 2022 at 10:58):From: kahl@cas.mcmaster.ca
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
Which version?
For Isabelle2005, you really need to use PolyML 4.14,
as far as I could find out.
If the PolyML provided on the Isabelle website works for you,
it is probably best to stick with that.
(The same may apply to ProofGeneral.)
(I just finished a series of experiments on a PowerMac running linux,
and your error looks similar to one I had at some point in time...)
Wolfram
Email Gateway (Aug 18 2022 at 10:59):From: kahl@cas.mcmaster.ca
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
I somehow overlooked that you are on linux, too.
(Now I have my coffee...)
I tried this on my home machine and don't remember how far I got
with Isabelle2005 -- I am afraid it failed in the end,
since PolyML 4.14 would actually require some porting effort
to be able to mmap() the ``database'' to a fixed address.
(To get all files for PolyML 4.14,
you have to dive more deeply into the PolyML (download) website.)
I did get the development snapshot to work with PolyML 5, though.
(Are you running a 32bit userland on a ppc64?
Then you possibly either have to run it within a linux32'' shell,
or (better) you have to manually set the system identifier in etc/settings
to the variant without 64''.)
Wolfram
Email Gateway (Aug 18 2022 at 11:00):From: Peter Chapman <pc@cs.st-and.ac.uk>
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
Email Gateway (Aug 18 2022 at 11:04):From: Makarius <makarius@sketis.net>
Here the 4.x version of run-polyml fails on Poly/ML 5.x (the one from the
current CVS). Using the compatibility wrappers for 5.0 from
http://www4.in.tum.de/~wenzelm/test/Isabelle2005-polyml-5.0.tar.gz you
should be able to run Isabelle2005 on the latest Poly/ML, even though that
version announces itself as "5.1". Just make sure your isabelle/settings
force it back to "5.0".
I haven't seen this working on ppc-linux yet, as there are very few such
systems available these days. In principle it should work, though.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC