Re: [isabelle] Easier quick PDF generation possible?



On Mon, 3 Nov 2014, Makarius wrote:

The perceived slowness of invoking "isabelle build" from the command-line is mainly the JVM startup and warmup time (to have the just-in-time compiler go through the massive amounts of byte code).

It is much faster if invoked directly from the running PIDE in the Console/Scala plugin of Isabelle/jEdit. After 2-3 runs of Build.build the exploration of dependencies is actually quite fast.

This might require further explanations, apart from the small section "2.5 Scala console" in the Isabelle/jEdit manual.


The Scala toplevel is similar to really ancient ML toplevels, but to see the signature of some function one needs to provide some dummy argument. E.g. like this:

  Build.build _

The source for that is in $ISABELLE_HOME/src/Pure/Tools/build.scala which can be opened as plain-text file in Isabelle/jEdit precisely like that, but there is no particular IDE support. Here is the full signature for that function in the source:

  def build(
    options: Options,
    progress: Progress = Ignore_Progress,
    requirements: Boolean = false,
    all_sessions: Boolean = false,
    build_heap: Boolean = false,
    clean_build: Boolean = false,
    dirs: List[Path] = Nil,
    select_dirs: List[Path] = Nil,
    session_groups: List[String] = Nil,
    max_jobs: Int = 1,
    list_files: Boolean = false,
    no_build: Boolean = false,
    system_mode: Boolean = false,
    verbose: Boolean = false,
    sessions: List[String] = Nil): Int

Scala allows positional and named arguments with default. Here is a typical invocation:

  Build.build(PIDE.options.value, new Build.Console_Progress, select_dirs = List(Path.explode("~/Papers/Isabelle_Workshop_2014")))

PIDE.options.value refers to the options of the Prover IDE, which are edited in the Plugin Options / Isabelle dialog. It is also possible to provide separate options, taking Options.init() as a start.


Build.Progress objects need to be provided afresh for each invokation. Here it is connected to the enclosing console, which also allows to use the "Stop" button to interrupt the running job.

All other arguments are optional; select_dirs above corresponds to option -D in the shell command-line.


Bypassing the system shell and using the Scala loop directly saves some precious seconds in the edit-build cycle, which is particularly important to write papers, manuals, books etc. I have done that routinely for recenr manual updates, notable the Isabelle/jEdit itself. Together with the spell-checker in Isabelle2014 works already quite nicely.

In the next round of improvements, I hope to see full integration into the IDE: document preparation without funny build jobs, just some button to run Isabelle LaTeX on some theories.


	Makarius

----------------------------------------------------------------------------
                  http://stop-ttip.org  787,983 people so far
----------------------------------------------------------------------------




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