[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
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