Re: [isabelle-dev] NEWS: Latex errors

2017-12-14 Thread Makarius 
On 14/12/17 13:45, Lars Hupel wrote:
> 
> 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"

That is a mistake on my side. See now:

changeset:   67201:4cffa4791ef7
user:wenzelm
date:Thu Dec 14 14:28:27 2017 +0100
files:   src/Pure/Thy/present.scala
description:
proper \isakeeptag (amending 13b5c3ff1954);


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: Latex errors

2017-12-14 Thread Lars Hupel 
> * 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.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: Latex errors

2017-12-14 Thread Florian Haftmann 
> *** 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.

That explicit error reporting is a great thing missed for so long!

Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] NEWS: Latex errors

2017-12-14 Thread Makarius 
*** 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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev