[isabelle-dev] "build" name
makarius at sketis.net
Fri Dec 14 13:06:00 CET 2012
On Wed, 12 Dec 2012, Jasmin Christian Blanchette wrote:
> The new "isabelle build" tool is really a joy to work with -- thanks Makarius! :-) But one of the mistakes I find myself doing over and over is typing
> isabelle build HOL
> when I really meant
> isabelle build -b HOL
> Sometimes I don't even notice my mistake and find myself using an old
> version, with old bugs, and can't understand what they're doing there.
> The problem also occurs with other theories, e.g. "HOL-Probability".
It used to happen to me as well, and somehow I also get -a vs. -b
occasionally wrong due to layers of old habits that I cannot fully
One of the reasons why the re-implementation of the build tool has taken
so long is that it was unclear how to call it and how to name the ROOT
files. (There were also some technical problems, of course.) Over many
years I intended to call it "session", because it is the tool to manage
This naming issue is not just an odd joke: the French colleages had a
discussion how to call the "project" files of a future version of CoqIde.
Then someone proposed to introduce an option such that everyone can choose
his own name. But how to call that option? So they are still stuck with
makefiles that are getting more and more complicated.
Anyway, the name of the isabelle build tool and its broad spectrum of
options from -n no build, default build with images as required, and -b to
really build an image as a side-effect, is the result of working on all
that a long time this summer. Further reforms need to look more deeply at
Note that the image is just one thing that might get built, the
browser_info or log content will become more and more important over the
years, as it becomes more formal. In some sense the traditional heap
image is just an optimization to accelarate startup.
Just practically, the confusion of forgetting "-b" for HOL in everyday
testing is already obsolete, since Isabelle/jEdit has this implicit build
mode on startup: you specify a logic session and the Prover IDE takes that
the corresponding image will be there up-to-date when th editor comes up.
This feels a bit like hand-holding to me right now, but it is probably a
matter of getting used to it -- and of further fine-tuning of the build
dialog. I was already tempted to remove the "isabelle build -b HOL" line
from the quickstart in README_REPOSITORY, but left it there for now as an
important intermediate step that is worth knowing.
The main question on this thread for me is if it is worthwhile to add a
similar build_dialog wrapper to the "isabelle emacs" startup script like
In fact, I made the build_dialog tool in a way that it could be re-used
for non-jedit front-ends. Otherwise I could have done it more directly,
and more efficiently on startup, using just one JVM process instead of
More information about the isabelle-dev