Email Gateway (Nov 06 2020 at 16:59): 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
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
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
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
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: Jul 15 2022 at 23:21 UTC