[isabelle-dev] "build" name

[Makarius]

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