[isabelle-dev] NEWS: Latex errors

Makarius makarius at sketis.net
Thu Dec 14 11:49:22 CET 2017

*** Document preparation ***

* Command-line tool "isabelle document" has been re-implemented in
Isabelle/Scala, with simplified arguments and explicit errors from the
latex process. Minor INCOMPATIBILITY.

*** System ***

* ISABELLE_LATEX and ISABELLE_PDFLATEX now include platform-specific
options for improved error reporting. Potential INCOMPATIBILITY with
unusual LaTeX installations, may have to adapt these settings.

This refers to Isabelle/93600ca0c8d9. It turned out much more
complicated than anticipated: the TeX engine is a dark pit from a
different era, when parsers and sane error output did not exist yet.

Early adopters should keep an eye on it: whenever there is a need to
inspect root.log manually for errors, please report it.


More information about the isabelle-dev mailing list