[isabelle-dev] "build" name
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Wed Dec 12 22:49:56 CET 2012
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?
More information about the isabelle-dev