Re: [isabelle] Document preparation hints

On Tue, 7 Jan 2014, Timothy Bourke wrote:

What is the best way to skip proofs when generating .tex files in this way? I was using "ML {* Toplevel.skip_proofs := true *}" but it seems to have stopped working with Isabelle 2013-x (or I have started making a mistake).

This is none of the things that were broken in Isabelle2013-1 with nobody taking notice, but it is just a standard renovation of old-style ML reference variables. For several years these have a tendency to get an official status as "configuration options" or (more recently) as persistent "system option".

Unlike "skip_proofs", the better-known option "quick_and_dirty" has a NEWS entry about that in Isabelle2013-1:

* Uniform management of "quick_and_dirty" as system option (see also
"isabelle options"), configuration option within the context (see also
Config.get in Isabelle/ML), and attribute in Isabelle/Isar.  Minor
INCOMPATIBILITY, need to use more official Isabelle means to access
quick_and_dirty, instead of historical poking into mutable reference.

The "more official Isabelle means" to access such options are manifold, e.g. in a session ROOT file:

  options [skip_proofs]

or for some particular theories within it:

  theories [skip_proofs]

or globally on the isabelle build command line:

  isabelle build -o skip_proofs -D.

Since this thread is about eliminating the command shell, the latter form works in isabelle scala like this:

  val options = Options.init().bool("skip_proofs") = true, progress = new Build.Console_Progress(verbose = false), more_dirs = List((true, Path.current)))

Doing Options.init() only once also saves 50-100ms each time the build is invoked :-)


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