[isabelle-dev] "build" name

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Wed Dec 12 22:49:56 CET 2012

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?


More information about the isabelle-dev mailing list