On Fri, 14 Dec 2012, Makarius wrote:
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.
Actually this should not happen. When you update accidentally via "build
HOL" without requesting a heap image, the old HOL image should be deleted.
So there might be a time penalty to build the image again, but you should
not see an old one, not even in Proof General.
Trying it again in Isabelle/0eaefd4306d7 seems to work according to this
description.
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.
I've tuned this again a few times. In 345b25cf2e4f it really insists in
having an image that is up-to-date -- it was not correct before.
The command line also changed slightly again to follow the "-l LOGIC" form
of isabelle jedit, emacs, tty. Right now, only isabelle jedit has this
build_dialog wrapper; it can be bypassed via option -n.
For isabelle tty it looks wrong to have a GUI dialog -- so it could be
changed into a non-dialog, but that is all a bit odd for low-level prover
process startup.
For isabelle emacs it definitely makes sense to have the implicit
build_dialog as well, although guessing the right logic name might not be
as easy. Isabelle/Scala shares the options environment with
Isabelle/jEdit, but not with Emacs for its own settings. Nonetheless, it
should work for explicit -l LOGIC on the command line, or implicit
$ISABELLE_LOGIC.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
