Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Unknown logic "HOL"


view this post on Zulip Email Gateway (Aug 19 2022 at 10:50):

From: Paqui Lucio Carrasco <paqui.lucio@ehu.es>
Hi,
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

Could someone tell me what to do to fix this problem?

Thanks,
Paqui


Paqui Lucio
Dpto de Lenguajes y Sistemas Informáticos
Facultad de Informática
Paseo Manuel de Lardizabal, 1
20018-San Sebastián
SPAIN


e-mail: paqui.lucio@ehu.es
Tfn: (+34) (9)43 015049
Fax: (+34) (9)43 015590
Web: http://www.sc.ehu.es/paqui


view this post on Zulip Email Gateway (Aug 19 2022 at 10:50):

From: Makarius <makarius@sketis.net>
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


Last updated: Apr 26 2024 at 01:06 UTC