Re: [isabelle] How to build a heap image
On Mon, 13 Jan 2014, Christian Maeder wrote:
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.
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
http://isabelle.in.tum.de/installation.html for "further technical
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