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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
