Re: [isabelle] Problem installing on an intel mac


polyml does not work on intel mac at the moment.

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


Quoting Walid Taha <taha at>:

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:

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

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.


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