Re: [isabelle] THY path



On Fri, 17 Sep 2010, Andreas Lochbihler wrote:

Another option to get started quickly is to use writeable heaps, where you can start right where you had stopped before. I used to work with these, but my heaps got so large that shutting down Isabelle and writing the heap back to the disk exceeded all emacs timeouts. Makarius might be able to tell you more about writeable heaps.

These persistent heap images used to be very commonplace until everybody started using Proof General, because the basic usage of isabelle-process was forgotten. The Isabelle system explains this in section 1.2 with a small example near the end.

Proof General makes it traditionally a bit hard to work with the result, also due to the default time out -- it can be changed on the Proof General side using one of these huge option menus, or better by injecting some elisp into $HOME/.emacs like this:

  (custom-set-variables '(proof-shell-quit-timeout 45))


	Makarius





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