Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Document preparation hints

view this post on Zulip Email Gateway (Aug 19 2022 at 13:26):

From: Makarius <makarius@sketis.net>
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 ...

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 13:27):

From: Timothy Bourke <tim@tbrk.org>

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).

Or do experts put their development in a base image and then avoid the
temptation to tune it while writing about it?

Tim.
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 13:27):

From: Makarius <makarius@sketis.net>
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:

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

options [skip_proofs]
theories
Foo
Bar
Baz

or for some particular theories within it:

theories [skip_proofs]
Foo
Bar
theories
Baz

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

Build.build(options, 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 :-)

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 13:27):

From: Timothy Bourke <tim@tbrk.org>

...

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

options [skip_proofs]
theories
Foo
Bar
Baz

or for some particular theories within it:

theories [skip_proofs]
Foo
Bar
theories
Baz

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

Build.build(options, progress = new Build.Console_Progress(verbose =
false), more_dirs = List((true, Path.current)))

Very nice. Thank you.

Tim.

(I must have only grepped in 2013-1...)
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 13:32):

From: Timothy Bourke <tim@tbrk.org>

...

or globally on the isabelle build command line:

isabelle build -o skip_proofs -D.

In fact, I find that this builds with skip_proofs are faster but that
no .tex file is generated. Is the latter expected?

Tim.
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 13:32):

From: Makarius <makarius@sketis.net>
Abstractly, skip_proofs falls under the "too many options" syndrome of
contempory Isabelle, so arbitrary behaviour can be expected in conjunction
with other options, like document preparation. Since skip_proofs was once
added as ad-hoc addition to the Isar top-level that was not exactly
well-defined until today, it has fluctuated back and forth quite a lot
over the years.

As far as I can see in Isabelle2013-2, skip_proofs now works with all Isar
commands (including diagnostic commands and antiquotations), but its
presence in some theory blanks-out the generated .tex file. (Document
prepration requires intermediate toplevel states, but skipped ones are
undefined.)

So for the purpose of this thread, "isabelle build -o skip_proofs" does
not make any sense with document preparation. The flag should be added to
individual theories within the session ROOT file, and the theories in
question won't appear in the document.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 09:50):

From: Mathias Fleury <mathias.fleury12@gmail.com>
(trying to revive an old thread from January 2014, see
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-January/msg00021.html[1]
for the mail exchange).

Dear list,

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
-bootingand re-warming of the JVM to run Isabelle/Scala, and
considerably
speeds up the exploration of source dependencies.

I am interested in doing the document preparation and the building
automatically in Isabelle 2015-RC4. After looking at the build.scala file, I
came up with:

scala > Build.build(options = Options.init, progress = new
Build.Console_Progress(verbose = false), select_dirs = List(Path.explode
("/path/to/directory")))

but this does not rebuild whenever a files is saved. Is there a way to
achieve this with Isabelle's upcoming version?

Thanks in advance,
Mathias

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
spotstarting 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 ...

Makarius

[1] https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-January/msg00021.html

view this post on Zulip Email Gateway (Aug 22 2022 at 09:50):

From: Makarius <makarius@sketis.net>
On Thu, 14 May 2015, Mathias Fleury wrote:

(trying to revive an old thread from January 2014, see
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-January/msg00021.html[1]
for the mail exchange).

Back in January 2014, I was expressing the hope that it would be the last
season with batch-mode document preparation, but it is still the situation
today.

There have been small improvementes in the meantime:

* The jEdit/Console/Scala plugin works better as a replacement for an
external terminal (already in Isabelle2014). This means there is no
need to have a separate "isabelle scala" process running.
Build.build() can be invoked directly in the JVM that runs jEdit as
Java application and Isabelle/Scala/PIDE infrastructure.

* In Isabelle2015-RC versions there is support for BibTeX files: context
menu, context-sensitive token marker, SideKick parser. See also the
Isabelle/jEdit manual.

More fundamental reforms are still in the pipeline. Here is a recent
wrap-up of the main things that could be done to warp into the year 2015:
http://sketis.net/2015/proposal-document-preparation-improvements

I am interested in doing the document preparation and the building
automatically in Isabelle 2015-RC4. After looking at the build.scala file, I
came up with:

scala > Build.build(options = Options.init, progress = new
Build.Console_Progress(verbose = false), select_dirs = List(Path.explode
("/path/to/directory")))

but this does not rebuild whenever a files is saved. Is there a way to
achieve this with Isabelle's upcoming version?

What exactly do you mean "whenever a files is saved"? Event-oriented
update based on file-system or editor changes?

The above invocation of Build.build() should check source dependencies
against the file-system each time it is invoked, but it has to be invoked
again and again explicitly. If that does not work, there is something
wrong elesewhere.

It should be also possible to define an editor macro or menu entry to
repeat the invocation above conveniently. I do it myself in a
minimalistic way via the command-line history of the jEdit/Console plugin.

A true reform would detach the document build from file-system state
altogether. In our fine PIDE world the file-system is out and state is
out.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 09:51):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Le 15/05/2015 15:15, Makarius a écrit :

On Thu, 14 May 2015, Mathias Fleury wrote:

(trying to revive an old thread from January 2014, see
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-January/msg00021.html[1]

for the mail exchange).

Back in January 2014, I was expressing the hope that it would be the
last season with batch-mode document preparation, but it is still the
situation today.

There have been small improvementes in the meantime:

* The jEdit/Console/Scala plugin works better as a replacement for an
external terminal (already in Isabelle2014). This means there is no
need to have a separate "isabelle scala" process running.
Build.build() can be invoked directly in the JVM that runs jEdit as
Java application and Isabelle/Scala/PIDE infrastructure.

* In Isabelle2015-RC versions there is support for BibTeX files:
context
menu, context-sensitive token marker, SideKick parser. See also the
Isabelle/jEdit manual.

More fundamental reforms are still in the pipeline. Here is a recent
wrap-up of the main things that could be done to warp into the year
2015: http://sketis.net/2015/proposal-document-preparation-improvements
Interesting plans.

I am interested in doing the document preparation and the building
automatically in Isabelle 2015-RC4. After looking at the build.scala
file, I
came up with:

scala > Build.build(options = Options.init, progress = new
Build.Console_Progress(verbose = false), select_dirs = List(Path.explode
("/path/to/directory")))

but this does not rebuild whenever a files is saved. Is there a way to
achieve this with Isabelle's upcoming version?

What exactly do you mean "whenever a files is saved"? Event-oriented
update based on file-system or editor changes?
Update based on file-system. I though the command you gave was already
doing it.

The above invocation of Build.build() should check source dependencies
against the file-system each time it is invoked, but it has to be
invoked again and again explicitly. If that does not work, there is
something wrong elesewhere.

It should be also possible to define an editor macro or menu entry to
repeat the invocation above conveniently. I do it myself in a
minimalistic way via the command-line history of the jEdit/Console
plugin.
Thanks for the advice,

Mathias

A true reform would detach the document build from file-system state
altogether. In our fine PIDE world the file-system is out and state
is out.

Makarius

Last updated: Apr 18 2024 at 20:16 UTC