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
> >24-182-155-65.dhcp.sllv.mo.charter.com)
> >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 
issue.


	Makarius





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