Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] help!!

view this post on Zulip Email Gateway (Aug 18 2022 at 11:15):

From: "jwang whu.edu.cn (jwang)" <jwang@whu.edu.cn>
Hello, Now Isabelle was installed in linux OS by the installation
instructions.When I start the Isabelle and open a theroy file (in
/isabelle2007/src/HOL/)to run by "use" button, I get the following error
message:
unknown logic "HOL"--no heap file found in:
/root/isabelle/heaps/Isabelle2007/polyml_x86-linux
/usr/local/isabelle/heaps/Isabelle2007/polyml_x86-linux.
Anyone have the same problem when Isabelle was installed?

view this post on Zulip Email Gateway (Aug 18 2022 at 11:15):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Jwanf,

You need HOL precompiled in order to use it immediately. You can get a
precompiled image for Linux according to the installation instructions
at http://isabelle.in.tum.de/installation.html

If this fails again, inspect your file system where the HOL file from
the HOL_x86-linux.tar.gz archive has found its place. Then move it to
one of the locations mentioned above.

Hope this helps
Florian
florian.haftmann.vcf
signature.asc

Last updated: May 03 2024 at 08:18 UTC