[isabelle-dev] NEWS: Latex errors

Lars Hupel hupel at in.tum.de
Thu Dec 14 13:45:22 CET 2017


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

Featherweight_OCL now fails to build:

isabelle document -d
/home/lars/.isabelle/browser_info/AFP/Featherweight_OCL/outline -o pdf
-n outline -t -annexa\,afp\,/proof\,/ML
*** Latex error (line 183 of
"/home/lars/.isabelle/browser_info/AFP/Featherweight_OCL/annex-a/root.tex"):
***   LaTeX Error: No \title given.
*** Failed to build document in
"/home/lars/.isabelle/browser_info/AFP/Featherweight_OCL/annex-a"

I wonder if this error is genuine and just got swallowed before, or if
it's a side effect of the change.



More information about the isabelle-dev mailing list