[isabelle] Document preparation hints

Dear Isabelle users,

with the deadline of ITP2014 approaching, there is a good chance that several people are writing papers with the Isabelle document preparation system as usual. (Raw Latex became out of use for that almost 15 years ago.)

For historic reasons, the document build process works in batch mode, and is still not integrated into the Prover IDE. This incurs slightly awkward overhead when invoking the whole stack of sub-systems again and again on the command line. See also the explanation of "isabelle mkroot" with subsequent "isabelle build -D." in the Isabelle System manual.

Since Isabelle/Scala is the actual system programming interface, not the command line shell, some time can be saved by working continously within "isabelle scala" like this:

  $ isabelle scala
  scala> import isabelle._
  scala> Build.build(options = Options.init, progress = new Build.Console_Progress(verbose = false), more_dirs = List((true, Path.current)))

This imitates "isabelle build -D." from the system manual. The invocation of Build.build is repeated every time the document sources have been edited and saved to the file-system. The above avoids repeated re-booting and re-warming of the JVM to run Isabelle/Scala, and considerably speeds up the exploration of source dependencies.

Further time may be saved by reducing the underlying session in the ROOT file to the bare minimum. Full "HOL" is quite bulky -- sometimes "Pure" is sufficient, or one may compose a suitable base image on the spot starting with the HOL theory Main, instead of Complex_Main.

Hopefully, this is the last season that we are doing this archaic batch-processing of Isabelle documents ...


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