Re: [isabelle] Problem installing on an intel mac



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= at 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


Le 15 sept. 06 à 15:20, Stephanie Weirich a écrit :

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.








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