Re: [isabelle] Fwd: unexpected (for me) output using FOL
On Fri, 3 Nov 2006, clinton lefort wrote:
> >I got the message that when I did in
> >/clintonlefort/IsabelleHOME/bin/./Isabelle I got the message that it
> >couldn't find HOL. I I invoked isatool (after reading the SYSTEMS
> >manual) and tried to set up my makeall, but got this messsage: Pure
> >failed on all he logics.
> >24-182-155-65:~/Isabelle_HOME/bin clintonlefort$ ./isatool makeall
> >Started at Fri Nov 3 08:41:51 CST 2006 (polyml_ppc-darwin on
> >Building Pure ...
> >Pure FAILED
> >(see also /Users/clintonlefort/isabelle/heaps/polyml_ppc-darwin/log/Pure)
> >Unable to locate /opt/polyml/ppc-darwin/poly
> >Please check your ML system settings!
This looks like you don't have Poly/ML installed properly for your
platform. Since this is ppc-darwin we already provide precompiled
packages for HOL etc. on the Isabelle download site. Try to use these
before attempting to install any operation system packages for Poly/ML,
ProofGeneral etc. that occasionally show up elsewhere.
This should enable you to run plain isabelle tty sessions at the least.
Getting a version of (X)Emacs that works with ProofGeneral is a different
This archive was generated by a fusion of
Pipermail (Mailman edition) and