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:
### Comment out Polyml # Poly/ML 4.x# POLY_HOME="$(type -p poly)"; [ -n "$POLY_HOME" ] && POLY_HOME="$ (dirname "$POLY_HOME")"
# ML_PLATFORM=$("$ISABELLE_HOME/lib/scripts/polyml-platform") # 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" \ # $POLY_HOME) # ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version") # ML_OPTIONS="-H 80" # ML_DBASE="" # Standard ML of New Jersey 110 or later #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 On Sep 14, 2006, at 9:24 PM, Walid Taha wrote:
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 GradualTypingBuilding 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.
Description: S/MIME cryptographic signature