Re: [isabelle] Latex without proofs

On Mon, 24 Jun 2013, Joachim Breitner wrote:

Am Montag, den 24.06.2013, 14:46 +0200 schrieb Makarius:
At some point I also hope to see document preparation as part of the
Prover IDE.  Only nostalgy associates latex documents with some batch
build job, there are no particular technical reasons (apart from
historical legacy getting in the way as usual).

does this mean that in the future it will not be possible to have a
script or makefile that will, say, create Isabelle course task and
solutions PDFs from Isabelle sources automatically and without firing up
a GUI program? Or are you merely stating that batch builds should not be
the _only_ way to create documents from Isabelle sources?

The two things that are "current" in Isabelle2013 are the batch build and the Prover IDE document interaction model. I am trying to converge both to use more and more the same technology (for some years already). So batch mode is definitely not going to disappear, just odd historic things that used to be batch-mode only in the past.

Anything apart from proper "build" and "document editing" is more or less legacy. Better forget that "isabelle usedir" with ROOT.ML or "isabelle make" with IsaMakefile ever existed.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.