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
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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.