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:
(see also
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.