Re: [isabelle] Generated document doesn't compile with recent TeX Live.

Hi Benedikt,

Jasmin had the same problem in January, see the following thread:

Makarius suggested to copy Isabelle's comment.sty in your document folder to overwrite the new one from TeXLive.


On 08/05/14 13:03, bnord wrote:
Hi there,

after installing a new TeX Live version I observed that none of my documents would compile
any more. I can still compile the generated latex files on another machine with an older
tex installation. See the error log below for a simple empty theory (it's the same for
every theory).

I could also reproduce the same error with a fresh TeX Live installation on another
(linux) machine (where it still works with the main tex installation). I also tested this
with a fresh Isabelle2013-2 version.

Best Benedikt

Error log:

$ isabelle build -D .
Running SimpleTest ...

SimpleTest FAILED
(see also /Users/bnord/.isabelle/Isabelle2013-2/heaps/polyml-5.5.1_x86-darwin/log/SimpleTest)

*** (/usr/local/texlive/2013/texmf-dist/tex/context/base/supp-pdf.mkii
*** [Loading MPS to PDF converter (version 2006.09.02).]
*** ) (/usr/local/texlive/2013/texmf-dist/tex/latex/hyperref/nameref.sty
*** (/usr/local/texlive/2013/texmf-dist/tex/generic/oberdiek/gettitlestring.sty))
*** (./session.tex (./SimpleTest.tex Including 'isadelimtheory' comment.)
*** Runaway argument?
*** ! File ended while scanning use of \next.
*** <inserted text>
***                 \par
*** l.1 \input{SimpleTest.tex}
*** ))
*** ! Emergency stop.
*** <*> \nonstopmode\input{root.tex}
*** !  ==> Fatal error occurred, no output PDF file produced!
*** Transcript written on root.log.
*** Document preparation failure in directory 'output/document'
*** Failed to build document "/Users/bnord/tests/SimpleTest/output/document.pdf"
Unfinished session(s): SimpleTest
0:00:19 elapsed time, 0:00:19 cpu time, factor 1.00

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.