[isabelle-dev] "build" name

[Tobias Nipkow]

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
>