Re: [isabelle] How to build a heap image
Am 13.01.2014 16:30, schrieb Makarius:
On Mon, 13 Jan 2014, Christian Maeder wrote:
whenever a new Isabelle version comes out, I need some time to find
out how to build a heap image i.e. for HOLCF.
After unpacking Isabelle2013-2_linux.tar.gz and extending my PATH I
isabelle build -b -s HOLCF
Have you tried starting the top-level "Isabelle" executable instead?
Well, I called
as described at http://isabelle.in.tum.de/installation.html
This made the Pure and HOL heaps (only). I ignored/closed all pop-ups as
I only wanted to use isabelle-process in batch mode to see if old .thy
files still go through.
In fact, I've not tried yet if
isabelle tty -l HOLCF
works like older versions did.
And yes, I still prefer Proof General for my (limited) uses, although I
once tried the jedit interface because of a Proof General / emacs
problem. (Also our hets tool still uses "isabelle emacs".)
Going to Plugin Options / Isabelle there, you can select a different
logic session name. After restart, the required heap image will be
built automatically. There is no need for any command line invocation.
In the past 2 year I've spent a lot of efforts to make such things work
without further ado. At the same time I have stopped maintaining
Isabelle Proof General, and nobody has jumped in, so that is legacy
since October 2011.
This archive was generated by a fusion of
Pipermail (Mailman edition) and