[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.
Makarius
More information about the isabelle-dev
mailing list