Email Gateway (Aug 19 2022 at 11:50): Email Gateway (Aug 19 2022 at 11:50):From: Ognjen Maric <ognjen.maric@gmail.com>
Hello all,
I'm having some problems transferring heap images between different
machines. My ROOT file looks like this:
session Full_Ref = "HOL" +
options [
document = false]
theories
Full_Ref
session Snippets = "Full_Ref" +
options [
document = "pdf",
document_output = "generated"]
theories
Snippets
files
"document/build"
On fast-machine, I build the heap using:
isabelle build -b -d . -o threads=16 Full_Ref
I can now copy the resulting heap image from
fast-machine:~user/.isabelle to the corresponding location on
slow-machine, and use it with:
isabelle emacs -l Full_Ref Snippets.thy
This works fine, so there should not be any problems with mismatched
PolyML versions or anything of the sort (I'm using the same release
tarball on both machines).
However, trying either of:
isabelle jedit -d . -l Full_Ref Snippets.thy
or
isabelle build -d . Snippets
on slow-machine results in Isabelle trying to (re)build Full_Ref on
slow-machine, while it happily uses uses the generated heap if ran on on
fast-machine.
Any help is appreciated.
Thanks,
Ognjen
Email Gateway (Aug 19 2022 at 11:50):From: Makarius <makarius@sketis.net>
On Thu, 26 Sep 2013, Ognjen Maric wrote:
I can now copy the resulting heap image from
fast-machine:~user/.isabelle to the corresponding location on
slow-machine
How do you make the copy? You need to preserve the modification time of
the heap files here.
, and use it with:
isabelle emacs -l Full_Ref Snippets.thy
This works fine, so there should not be any problems with mismatched
PolyML versions or anything of the sort (I'm using the same release
tarball on both machines).However, trying either of:
isabelle jedit -d . -l Full_Ref Snippets.thy
or
isabelle build -d . Snippets
on slow-machine results in Isabelle trying to (re)build Full_Ref on
slow-machine, while it happily uses uses the generated heap if ran on on
fast-machine.
isabelle jedit and build check the sources according to SHA1 and the heaps
according to size + modification time, and rebuild if anything has
changed.
The legacy mode of isabelle tty and emacs omits the integrity check, which
is why it happens to work by accident.
Just out of curiosity: What is the fast and the slow machine like? I have
recently started to think again about reintroducing remote connection to
the prover in Isabelle/Scala/jEdit, as was very common > 10 years ago.
The asymmetry of local vs. remote hardware is coming back ...
Makarius
Email Gateway (Aug 19 2022 at 11:50):From: Ognjen Maric <ognjen.maric@gmail.com>
Mistakingly took the reply off the list, posting back in case it's
useful to somebody else.
Thanks Makarius, this clears it up. I did not copy the log files.
Additionally, while my Full_Ref images were the same, the HOL and Pure
images on the two machines were different (the parent image fingerprint
is also present in the log file).
Ognjen
Last updated: Nov 21 2024 at 12:39 UTC