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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
