[isabelle] Problem installing on an intel mac




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.