[isabelle-dev] "build" name
c-sterna at jaist.ac.jp
Thu Dec 13 04:46:55 CET 2012
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).
PS: "isabelle build" (whatever the name) is really great!
More information about the isabelle-dev