Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Easier quick PDF generation possible?

view this post on Zulip Email Gateway (Aug 19 2022 at 16:22):

From: Joachim Breitner <breitner@kit.edu>
Hi,

I just create a small theory to do a quick experiment, and I wanted to
share it with someone. Isabelle can create pretty PDF output, so I
wanted to share it as such, but this turns out to be a task that is
unnecessary complicated.

Here is my log:

  1. run "isabelle mkroot"
  2. notice that I ran it wrong, "rm ROOT"
  3. run "isabelle mkroot -d"

  4. add my theory to ROOT, removed the theories [document = false]
    section, because empty sections are not allowed

  5. run "isabelle build -D"

  6. noticed that a few other theories were pulled in that I did not want

  7. tried to add their theory names to the [document = false] section,
    for which I first had to look up the syntax in another ROOT file

  8. noticed that this did not work. Put in the theory path (i.e.
    "~~/src/HOL/Library/Extended_Real") in there

  9. adjusted document/root.txt to have a proper title and not disclose my
    local username

Here is what I would have liked to do:

  1. run "isabelle thy2pdf Foo.thy"

So if anyone agrees that this would be useful, and is able to implement
this minor feature suggestion, I’d appreciate that!

Thanks,
Joachim
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 16:22):

From: Andrew Butterfield <Andrew.Butterfield@scss.tcd.ie>
Joachim, all,

Gets +1 from me !

Regards, Andrew

Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204
Lero@TCD, Head of Foundations & Methods Research Group
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
http://www.scss.tcd.ie/Andrew.Butterfield/

view this post on Zulip Email Gateway (Aug 19 2022 at 16:22):

From: Gergely Buday <gbuday@gmail.com>
I could even imagine a button in Isabelle/JEdit to generate the
document and place it in the Document tab on the right.

And, isabelle build seems to be slow, does it use the information from
the continuous proof checking? I guess not. If it were part of
Isabelle/JEdit, it would be much different.

view this post on Zulip Email Gateway (Aug 19 2022 at 16:30):

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

view this post on Zulip Email Gateway (Aug 19 2022 at 16:36):

From: Makarius <makarius@sketis.net>
On Thu, 23 Oct 2014, Joachim Breitner wrote:

Here is my log:

  1. run "isabelle mkroot"
  2. notice that I ran it wrong, "rm ROOT"
  3. run "isabelle mkroot -d"
  4. add my theory to ROOT, removed the theories [document = false]
    section, because empty sections are not allowed
  5. run "isabelle build -D"
  6. noticed that a few other theories were pulled in that I did not want
  7. tried to add their theory names to the [document = false] section,
    for which I first had to look up the syntax in another ROOT file
  8. noticed that this did not work. Put in the theory path (i.e.
    "~~/src/HOL/Library/Extended_Real") in there
  9. adjusted document/root.txt to have a proper title and not disclose my
    local username

Here is what I would have liked to do:

  1. run "isabelle thy2pdf Foo.thy"

Note that Isabelle command-line tools are very old-fashioned, and many new
things don't have a shell wrapper anymore. The direct way is via
Isabelle/Scala. It is also possible to invoke Scala functionality in
Isabelle/jEdit with the Console/Scala plugin.

This older thread gives some hints about document preparation via
Build.build:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-January/msg00021.html
In Isabelle2014 this works a bit more smoothly, but there is still no
direct IDE support.

So if anyone agrees that this would be useful, and is able to implement
this minor feature suggestion

Above you describe too missing things in the current PIDE setup:

(1) management of "projects", i.e. sorting out ROOT files

(2) document-preparation within the IDE

These are not "minor" things, but quite important. Both of that is in the
pipeline for a long time. Last winter I tried hard to revisit point (2),
but got entangled in old TTY / Proof General features. Since the latter
has been cleared out at last, some more progress is to be expected
eventually.

Makarius

http://stop-ttip.org 777,071 people so far

view this post on Zulip Email Gateway (Aug 19 2022 at 16:37):

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

Of course, exploration of dependencies for document preparation is a bit
pointless in the first place. It is a left-over from the old times of
"make", and even until today people sometimes think they have to invoke
that ancient tool to make something, although it slows downs things a lot.

Makarius

http://stop-ttip.org 777,087 people so far

view this post on Zulip Email Gateway (Aug 19 2022 at 16:38):

From: Joachim Breitner <breitner@kit.edu>
Great! I’m looking forward to that.

Greetings,
Joachim
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC