Re: [isabelle] Transferring heap images between machines
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
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
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
isabelle jedit and build check the sources according to SHA1 and the heaps
according to size + modification time, and rebuild if anything has
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 ...
This archive was generated by a fusion of
Pipermail (Mailman edition) and