[isabelle-dev] "build" name
makarius at sketis.net
Mon Dec 17 21:04:24 CET 2012
On Fri, 14 Dec 2012, Makarius wrote:
>> 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
> 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
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
More information about the isabelle-dev