[isabelle-dev] "build" name
lp15 at cam.ac.uk
Thu Dec 13 11:45:48 CET 2012
Is there a "verbose" option where it says what it's going to do first?
On 13 Dec 2012, at 08:59, Tobias Nipkow <nipkow at in.tum.de> wrote:
> I suspect many people will have experienced the same confusion, and Makarius
> acknowledged this in some email when he spoke of the `joke' "build -b". Renaming
> "build" would make sense.
> Am 12/12/2012 22:49, schrieb Jasmin Christian Blanchette:
>> Hi all,
>> 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 occurred to me that the name "build" is simply misleading. What the tool does, first and foremost, is to "run" or "process" or "check" an Isabelle session (and, as a side effect, build intermediate images). If the command were to be called
>> isabelle run HOL-Probability
>> I wouldn't forget to pass -b if I wanted to actually build the image:
>> isabelle run -b HOL-Probability
>> The "build" name has not yet our users, but with the coming release the window of opportunity for changing it is rapidly closing.
>> What do you think?
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev