[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