Re: [isabelle] Unknown logic "HOL"



On Tue, 9 Apr 2013, Paqui Lucio Carrasco wrote:

I?ve installed Isabelle2013 on Windows. After started the system, I get the
message:

Unknown logic "HOL" -- no heap file found in:
 /cygdrive/d/Documents and
Settings/Paqui/.isabelle/Isabelle2013/heaps/polyml-5.5.0_x86-cygwin
 /cygdrive/c/Isabelle2013/heaps/polyml-5.5.0_x86-cygwin
Return code: 127

Does "started the system" mean running the Isabelle2013.exe within the main Isabelle2013 directory? If so, it should start some build dialog to produce the required HOL heap file on the spot -- this takes 2-3min on hardware that is not too old.

A failure in the build process should prevent the main application (Isabelle/jEdit) from coming up in the first place, so the system should stop before the above error can appear.

Anyway, the above error reveals that you have moved the main Isabelle2013 directory to the root of drive C:\ -- this can cause some confusion in file permissions. It should basically run, but might cause other problems later.


	Makarius




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