Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Document preparation from within Isabelle/jEdit


view this post on Zulip Email Gateway (Nov 06 2020 at 16:59):

From: David Kretzmer <david.k@posteo.de>
Dear all,

is there a way to do PDF generation from within Isabelle/jEdit in a way
that avoids rebuilding the whole session? In the documentation it only
says how to preview the generated HTML, but not how to generate a PDF.
Currently I simply run isabelle build ..., but if I do this then I
have to close Isabelle/jEdit because I don't have enough RAM for both.

Best regards,
David

view this post on Zulip Email Gateway (Nov 06 2020 at 20:59):

From: Makarius <makarius@sketis.net>
This is certainly desirable, but still not supported. For now you can save
some time and space like this:

* Edit $ISABELLE_HOME_USER/etc/settings and restrict the ML heap, depending
on your total RAM and the size of your Isabelle/HOL application:

ML_OPTIONS="--minheap 500 --maxheap 2g"

(Restart the Isabelle/jEdit afterwards.)

* Open the Console/Scala plugin in Isabelle/jEdit and run the Isabelle build
tool within the Java process of Isabelle/jEdit:

Build.build(PIDE.options.value, progress = new Console_Progress, select_dirs
= List(Path.explode("~/tmp/Test")))

The arguments for Build.build may be seen here:
https://isabelle.sketis.net/repos/isabelle/file/Isabelle2020/src/Pure/Tools/build.scala#l392
and the mapping of command-line options to arguments here:
https://isabelle.sketis.net/repos/isabelle/file/Isabelle2020/src/Pure/Tools/build.scala#l726

Makarius

view this post on Zulip Email Gateway (Nov 06 2020 at 22:17):

From: David Kretzmer <david.k@posteo.de>
Hello Makarius,

thanks, it's still tight, but it does seem to just fit into main memory.
When I saw the -P option for isabelle build I had hoped that this
would somehow reuse the current session from Isabelle/jEdit, but this
does not seem to be the case.

Anyway, thanks for the help!

Best regards,
David

view this post on Zulip Email Gateway (Nov 06 2020 at 22:29):

From: Makarius <makarius@sketis.net>
In Isabelle2020, "isabelle build -P" will make a batch-build with a PIDE
session for that process --- it was somewhat experimental and unused back then.

In Isabelle2021 (presumably Feb-2021), "isabelle build" will always do this
and generally require more resources.

So you might run into resource problems again. How much memory do you actually
have?

As a spin-off from this unification --- PIDE sessions always used in
batch-mode and interaction --- it has now become more feasible to integrate
document preparation into Isabelle/jEdit. I was considering to do it some
weeks ago, but it is still a bit unclear if I manage for the coming release.

Makarius

view this post on Zulip Email Gateway (Nov 06 2020 at 22:50):

From: David Kretzmer <david.k@posteo.de>
On 06.11.20 23:29, Makarius wrote:> In Isabelle2021 (presumably
Feb-2021), "isabelle build" will always do this

and generally require more resources.

So you might run into resource problems again. How much memory do you actually
have?

I have 12GB in total, where roughly 2/3 are used when running
Build.build(...) in the Scala console inside Isabelle/jEdit, and 1/3
are used by other applications. So if I close some of the other
applications I still have some breathing room.

As a spin-off from this unification --- PIDE sessions always used in
batch-mode and interaction --- it has now become more feasible to integrate
document preparation into Isabelle/jEdit. I was considering to do it some
weeks ago, but it is still a bit unclear if I manage for the coming release.

If that becomes possible it would definitely be great!

Best regards,
David


Last updated: Dec 05 2021 at 22:18 UTC