[isabelle-dev] "build" name

[Makarius]

On Thu, 13 Dec 2012, Christian Sternagel wrote:

> 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).

I wonder where this idea of requiring a heap image was coming from. 
Maybe from the build process of .c -> .o?  The Coq guys always think in 
such terms, because OCaml does it.  Occasionally, some non-ML people have 
pointed out that Poly/ML looks so strange to them, because its compilation 
model is not centered around object files. (You can do that now, but we 
don't use it, because it does not solve any problems, but introduces new 
ones.)

Back to Isabelle document preparation today, and the anticipated state for 
the next release: writing a bit of text for papers and manuals in the past 
few months, I found the edit-build-view cycle very heavy and slow.  It 
reminds me of how it was around 2000, when all this was introduced.  In 
the next big reform -- not the the coming release -- I will try harder to 
get document preparation work during interaction.  So you can feed parts 
of your formal theories directly to latex and preview the results on the 
spot, without any build process getting in between.


 	Makarius