Re: [isabelle] How to build a heap image

On Mon, 13 Jan 2014, Christian Maeder wrote:

Well, I called


as described at

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.

We have a bit too many manuals, and getting attention of users into the right corner is difficult.

For Isabelle2013-2 all defaults are for Isabelle/jEdit, there is also the new "jedit" manual (accessible in the Documentation panel of Isabelle/jEdit), which has near the start the following item:

  The logic image of the prover session may be specified within
  Isabelle/jEdit. The new image is provided automatically by the Isabelle
  build tool after restart of the application.

Anything beyond selecting a logic image in Plugin Options / Isabelle (or the Theories) panel is subsumed by the "system" manual, which is linked at for "further technical background information".

The assumption (and the hope) is that users invest time in getting acqainted with the current generation of the Prover IDE, instead of finding quick-paths to do it like in old times.

In fact, I've not tried yet if

 isabelle tty -l HOLCF

works like older versions did.

No change here in recent releases. The "isabelle build -b" requirement was the same in Isabelle2012 and Isabelle2013, if you really want to bypass Isabelle/jEdit. Note that isabelle-process is really low-level, normally you have your session ROOT files and use "isabelle build" as explained in the "system" manual.

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

The basic assumption is that people who are still using Proof General have some extra time to tinker with shell scripts etc. I used to maintain special tricks to get Proof General / Emacs run for most people out of the box, but that is long past.

Now the remaining tricks are for the Java Runtime Environment on various platforms, and Linux is not the best right now, especially various recent forks of desktop environments. Windows and Mac OS X are more friendly to users of Java. Hopefully Linux recovers eventually, when more and more "free people" realize that there is a problem


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