Email Gateway (Aug 22 2022 at 18:28): Email Gateway (Aug 22 2022 at 18:28):From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
I run:
isabelle build -b HOL-Library
and find that a heap image for HOL-Library is saved under my
$HOME/.isabelle. But when I launch the Isabelle IDE, create a new theory
and import the theory HOL-Library.Library in the new theory, it looks like
Isabelle re-loads and re-checks all theories in HOL-Library, since those
theories show up in the theory panel of the IDE and have colored progress
bars.
However, after I change the default theory in the theory panel to
HOL-Library, quit the IDE and then re-launch it, a window pops up showing
that Isabelle is re-building HOL-Library, whose heap image is saved under
the Isabelle installation's directory. (On my Mac, it is
/Applications/Isabelle2018.app.) Furthermore, if I quit the IDE and then
come back and open the theory which imports HOL-Library.Library, Isabelle
does not re-load and re-check HOL-Library.
My questions are:
What caused the difference between the two scenarios, in particular
regarding whether the previously saved session is re-checked?
My goal is to create the heap images of large sessions like
HOL-Analysis. Is there a command-line method of doing this?
Thanks!
Email Gateway (Aug 22 2022 at 18:28):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Ching Tsun,
the default session heap image (or "default logic") that is used when
starting Isabelle/jEdit is "HOL". Which is why, even when you already
built a heap image for HOL-Library, the corresponding theories are
loaded again.
You can tell Isabelle/jEdit explicitly on the command line, which heap
image to use (setting the default logic in the theory panel, should
basically be equivalent, but you avoid a restart):
isabelle jedit -l HOL-Library
should build the heap image HOL-Library if necessary (and otherwise
reuse the existing heap image).
Concerning the other part of your question, why HOL-Libary was rebuilt
by Isabelle/jEdit even though you already did
isabelle build -b HOL-Library
on the command line, I am not 100% sure, but I think this is due to the
fact that Isabelle has two different "build modes": system build mode,
and "user" build mode. See also the -s option for "isabelle build".
With the former session heap images are located below the installation
directory of Isabelle ( $ISABELLE_HOME ) and with the latter below
the user's home directory ( $ISABELLE_HOME_USER ).
I think what happened is the following:
"isabelle build -b HOL-Library" produced a heap image below
ISABELLE_HOME_USER
but setting HOL-Library as default logic in Isabelle/jEdit looks for
the heap image below ISABELLE_HOME (I am not sure about this point)
thus after the first restart of Isabelle/jEdit the image was produced
below ISABELLE_HOME and the next time no rebuilt was necessary
cheers
chris
Email Gateway (Aug 22 2022 at 18:28):From: Dominique Unruh <unruh@ut.ee>
To add what Christian said:
This is due to different defaults in the isabelle-command (command line),
and the Isabelle2018.app (under its different names on different OSs).
Roughly speaking, Isabelle2018.app runs "isabelle jedit -s", hence the
image will be in the Isabelle installation directory.
While "isabelle jedit" and "isabelle build" uses the user directory by
default.
So there are three ways to avoid the duplication of heaps:
- Always use the -s option when running the "isabelle" command (e.g., in
"isabelle build").
- Avoid using Isabelle2018.app, use "isabelle jedit" instead
- Use symlinks to make the two heap directories point to the same place.
Personally, I think it would be best if the Isabelle distro would switch to
using the same default in both tools but I don't know if there are any
reasons against this that I am not aware of.
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 18:29):From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Thanks a lot for all the explanations!
Last updated: Apr 19 2024 at 16:20 UTC