[isabelle-dev] "build" name

[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