Re: [isabelle] Problem installing on an intel mac



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 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.


Attachment: smime.p7s
Description: S/MIME cryptographic signature



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