Email Gateway (Aug 18 2022 at 09:39): Email Gateway (Aug 18 2022 at 09:39):From: Walid Taha <taha@cs.rice.edu>
I just tried to install Isabelle on an Intel Mac by following the
instructions for MacOS X on the web. The first problem that I ran into
was getting the following error message when I used isatool
|> This is the error message that I get:
|>
|> Building GradualTyping ...
|> Unknown logic "HOL" -- no heap file found in:
|> /Users/taha/isabelle/heaps/polyml_unknown-platform
|> /usr/local/Isabelle2005/heaps/polyml_unknown-platform
|> GradualTyping FAILED
|> (see also
|> /Users/taha/isabelle/heaps/polyml_unknown-platform/log/GradualTyping)
In an attempt to fix this problem, I moved ...heaps/polyml-ppc to
.../heaps/polyml_unknown-platorm. This let things move forward a bit
(polyml does work, it seems). But now I get this error:
dhcp-7-144:~/work/papers/Conference/gradual-typing/proofs/GradualTyping
taha$ isatool usedir -b HOL GradualTyping
Building GradualTyping ...
Unable to locate /opt/polyml/unknown-platform/poly
Please check your ML system settings!
GradualTyping FAILED
(see also
/Users/taha/isabelle/heaps/polyml_unknown-platform/log/GradualTyping)
Any idea why (or what) is looking in this /opt/... directory? Currently,
there is no such directory on my machine (and I don't know what, if
anything, should have created it).
May thanks in advance.
Walid.
Email Gateway (Aug 18 2022 at 09:39):From: Martin Klebermass <martin@klebermass.de>
Hello,
polyml does not work on intel mac at the moment.
Install SMLNJ http://www.smlnj.org/ on your Intel mac, and use smlnj
instead of polyml (you have to change the isabelle configuration).
Somewhere in the list archive there have to be some other mails
regarding this question.
If you have any problems installing smlnj with isabelle send me an
email with your problems.
Martin
Quoting Walid Taha <taha@cs.rice.edu>:
Email Gateway (Aug 18 2022 at 09:39):From: Stephanie Weirich <sweirich@cis.upenn.edu>
Hi Walid,
I installed Isabelle on my Intel Mac just yesterday.
The problem is that you need a SML compiler, and I believe that there
isn't a version of polyml for the Intel Mac. So I downloaded SML/NJ
from the smlnj website (don't use the one in Fink), and edited
Isabelle2005/etc/settings as follows:
(dirname "$POLY_HOME")"
# ML_HOME=$(choosefrom \
# "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \
# "$ISABELLE_HOME/../polyml/$ML_PLATFORM" \
# "/usr/local/polyml/$ML_PLATFORM" \
# "/usr/share/polyml/$ML_PLATFORM" \
# "/opt/polyml/$ML_PLATFORM" \
#SMLNJ_CYGWIN_RUNTIME=1
ML_SYSTEM=smlnj-110
ML_HOME="/usr/local/smlnj-110.59/bin"
ML_OPTIONS="@SMLdebug=/dev/null"
ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo
"$HEAP_SUFFIX")
(This file also explains the /opt directory....) After doing this you
should be able to compile HOL.
Good luck,
Stephanie
smime.p7s
Email Gateway (Aug 18 2022 at 10:02):From: UdS <julien.schmaltz@googlemail.com>
Hi All,
I have installed smlnj from their website.
Now, when I start Isabelle I have:
Unknown logic "HOL" -- no heap file found in:
/Users/julien/isabelle/heaps/smlnj-110_x86-darwin
/usr/local/Isabelle2005/heaps/smlnj-110_x86-darwin
I am now trying to build HOL (does it seem to be the right thing to
do ?)
but it does not work:
135:/usr/local/Isabelle2005 julien$ ./build HOL
*********
* Welcome to Isabelle build * *********
Please check /usr/local/Isabelle2005/etc/settings
to make sure that Isabelle's ML system settings and compilation options
are appropriate.
The current values are:
ML_SYSTEM=smlnj-110
ML_HOME=/usr/local/smlnj-110.60/bin
ML_OPTIONS=@SMLdebug=/dev/null
ML_PLATFORM=x86-darwin
ISABELLE_USEDIR_OPTIONS=-v true -V outline=/proof,/ML
HOL_USEDIR_OPTIONS=
Press RETURN to compilation of
HOL
Started at Fri Dec 22 14:19:18 CET 2006 (smlnj-110_x86-darwin on
135.8.98-84.rev.gaoland.net)
/usr/local/Isabelle2005/lib/Tools/make: line 27: exec: make: not found
Finished at Fri Dec 22 14:19:18 CET 2006
0:00:01 total elapsed time
Does anyone have a hint why I do not have this "exec" ? where can I
get it ?
Thanks !
Julien
Email Gateway (Aug 18 2022 at 10:02):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Julien,
The "exec" refers to the POSIX system call "exec" - what you are really
missing is a GNU make.
Hope this helps
Florian
signature.asc
Last updated: May 03 2024 at 04:19 UTC