Re: [isabelle] Problem installing on an intel mac



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









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