Email Gateway (Aug 19 2022 at 15:16): Email Gateway (Aug 19 2022 at 15:16):From: Nils Jähnig <nils.jaehnig@tu-berlin.de>
Hi,
I am moving to Isabelle2013-2, and I had problem that build could not find
my pdflatex (though Isabelle2013 did).
I fixed this by reassigning ISABELLE_PDFLATEX in etc/settings to the
absolute path to pdflatex.
I post this here for reference, in case someone else has the same problems.
Best
Nils
Email Gateway (Aug 19 2022 at 15:17):From: Makarius <makarius@sketis.net>
Can you try http://isabelle.in.tum.de/website-Isabelle2014-RC0 as well?
I made some adjustments there, such that Mac OS X and Windows find their
pre-existing LaTeX more often. This only refers to the main application
entry point, i.e. the Prover IDE application bundle. Any command-line use
should find pdflatex from the normal shell PATH variable.
Makarius
Email Gateway (Aug 19 2022 at 15:17):From: Nils Jähnig <nils.jaehnig@tu-berlin.de>
Pdf generation seems to work.
Is it now possible to get the pdf without the heap-file?
(Because in my case, the heap file was not generated, as it still needs to
be adapted for Isabelle2014).
This is great news.
Email Gateway (Aug 19 2022 at 15:18):From: Makarius <makarius@sketis.net>
There was never a need to produce an output heap file together with the
document, but an input heap was (and still is) required to run the batch
session. The old plan to have document preparation without batch build
inside the Prover IDE is still not implemented.
Note that "isabelle mkroot -d" as explained in the "system" manual will do
most of the work to setup a session with document preparation according to
current standards. It works the same in Isabelle2013-2 and
Isabelle2014-RC0.
What changed in Isabelle2014-RC0 a little is the Console/Scala shell
inside the Prover IDE. It now allows to run the batch job
directly like this:
import isabelle._
Build.build(PIDE.options.value, new Build.Console_Progress,
select_dirs = List(Path.explode("~/Slides/Isabelle_Workshop_2014")))
Here you see that I am presently preparing slides for the huge VSL 2014
event next week.
Running directly from Isabelle/Scala inside the Prover IDE saves a few
seconds JVM warmup time. Scala is also a bit better as system programming
language than GNU bash, although there is sometimes more to type.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC