Email Gateway (Aug 18 2022 at 12:51): Email Gateway (Aug 18 2022 at 12:51):From: Benedikt.AHRENS@unice.fr
hello,
during the installation of isabelle following the instructions on
http://isabelle.in.tum.de/installation.html
i ran into the following problem:
after starting Isabelle, when trying to charge the first lines
'
theory Vect
begin
'
i had the error message
Unknown logic "HOL" -- no heap file found in:
/home/gp/ahrens/isabelle/heaps/Isabelle2008/polyml_x86-linux
/usr/local/Isabelle2008/heaps/polyml_x86-linux
the reason was a missing pointer polyml_x86-linux to the directory
polyml-<version>_x86-linux (version 5.2).
is this meant to be like that ? if yes, there should be a hint in the
INSTALL notes. if not, you might want to repair it.
i am not subscribed to the list, so please put me in CC if there is any
question/answer.
greetings
ben
Email Gateway (Aug 18 2022 at 12:53):From: Makarius <makarius@sketis.net>
I have just checked again: the link is part of the polyml tar, also for
ProofGeneral, as required.
Which tool did you use to unpack the archives?
Makarius
Email Gateway (Aug 18 2022 at 12:53):From: Benedikt.AHRENS@unice.fr
hello,
on the machine there is ubuntu 8.04 installed, we used the commandline
tool gnu tar 1.19.
other links have been created properly, like
Isabelle -> Isabelle2008.
i am not the administrator of the machine, so i cannot try to reproduce
the problem. considered that this seems to be the first time this
problem appears, i will assign it a problem of the machine.
thanks for your efforts.
ben
Makarius wrote:
Last updated: May 03 2024 at 04:19 UTC