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
now called:

 isabelle build -b -s HOLCF

Have you tried starting the top-level "Isabelle" executable instead?

Well, I called

  Isabelle2013-2/Isabelle2013-2

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".)

http://trac.informatik.uni-bremen.de:8080/hets/ticket/1042

Cheers Christian

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.


     Makarius







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