Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Generated document doesn't compile with recent...


view this post on Zulip Email Gateway (Aug 19 2022 at 14:25):

From: bnord <bnord01@gmail.com>
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

view this post on Zulip Email Gateway (Aug 19 2022 at 14:26):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Benedikt,

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

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-January/msg00142.html

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

Andreas

view this post on Zulip Email Gateway (Aug 19 2022 at 14:26):

From: bnord <bnord01@gmail.com>
Thanks!


Last updated: Apr 26 2024 at 16:20 UTC