Re: [isabelle] Fresh Install?



On 29.02.2012 11:44, Jens Doll wrote:
--------------------------------------------------------------------------------------------
msg ----------------------------------------------------
$ isabelle make
cygpath: can't convert empty path
Running HOL-Theorien ...
Unknown logic "HOL" -- no heap file found in:
/home/Jens/.isabelle/Isabelle2011-1/heaps/polyml-undefined_x86-cygwin
/Isabelle2011-1/heaps/polyml-undefined_x86-cygwin
HOL-Theorien FAILED
(see also
/home/Jens/.isabelle/Isabelle2011-1/heaps/polyml-undefined_x86-cygwin/log/HOL-Theorien)
---------------------------------------------------------------------------------------------------
end msg ----------------------------------------------------

This error message strikes me a bit odd. The precompiled heaps are somewhere under $ISABELLE_HOME/heaps (i.e. somewhere in the installation directory), not under $ISABELLE_HOME_USER/heaps (i.e. your .isabelle directory). $ISABELLE_PATH should contain both.

If you (or your makefile) does not specify paths explicitly (check with 'isabelle getenv ISABELLE_PATH'), HOL should be found.

If you cannot / don't want to change your makefile, as a workaround you can rebuild HOL as a user by executing 'isabelle make' in $ISABELLE_HOME/src/HOL -- this puts the heap image into $ISABELLE_HOME_USER/heaps, where your makefile is looking for it.

  -- Lars.





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