[isabelle-dev] "build" name

[Lawrence Paulson]

Is there a "verbose" option where it says what it's going to do first?
Larry

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