[isabelle-dev] "build" name

[Makarius]

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 
explain.


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 
Isabelle sessions.

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 
all that.

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 
here: 
http://isabelle.in.tum.de/repos/isabelle/annotate/2e1b47e22fc6/src/Tools/jEdit/lib/Tools/jedit#l323

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 
two.


 	Makarius