Re: [isabelle] pdflatex not found [SOLVED]

On Wed, 9 Jul 2014, Nils Jähnig wrote:

Pdf generation seems to work.

Is it now possible to get the pdf without the heap-file?

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._, 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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.