[isabelle-dev] "build" name

[Christian Sternagel]

On 12/13/2012 06:49 AM, Jasmin Christian Blanchette wrote:
> 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".
Just as another data point. The same thing happened to me quite 
frequently (I seem to have adapted in the meanwhile, but in the 
beginning it happened regularly). I'm not sure, however, whether this is 
just due to the name. Apart from document preparation (which I think 
usually comes later in the life of an Isabelle user), heap images are 
the central thing to build/make. In fact only after stumbling across the 
above problem I realized (after years of using Isabelle) that it was 
possible to prepare documents without building a heap image (which sped 
up the generation of all my Isabelle related documents significantly).

cheers

chris

PS: "isabelle build" (whatever the name) is really great!