[isabelle-dev] Latex problem on the AFP

[Anders Schlichtkrull]

Dear isabelle-dev

I tried to update the Paraconsistency entry of AFP to be as shown here: https://foss.heptapod.net/isa-afp/afp-devel/-/tree/851994a5d75d634876f75e47eca2d45f4b6fbee5/thys/Paraconsistency

However, when I pushed it to the repository, then the AFP build failed: https://ci.isabelle.systems/jenkins/job/isabelle-all/4580/consoleFull

The errors look like this:

07:46:21  Latex error (line 2 of "/tmp/isabelle-jenkins/document1954814550245541113/document/session.tex"):
07:46:21    Missing \endcsname inserted.
07:46:21    <to be read again>
07:46:21    unhbox
07:46:21    \input{Paraconsistency_Validity_Infinite.tex}
07:46:21  Latex error (line 2 of "/tmp/isabelle-jenkins/document1954814550245541113/document/session.tex"):
07:46:21    Undefined control sequence.
07:46:21    GenericError  ...
07:46:21                                                        #4  errhelp @err@       ...
07:46:21    \input{Paraconsistency_Validity_Infinite.tex}
07:46:21  Latex error (line 2 of "/tmp/isabelle-jenkins/document1954814550245541113/document/session.tex"):
07:46:21    Undefined control sequence.
07:46:21    GenericError  ...
07:46:21                                                      let @err@                 ...

And keep going for many more lines.

(I temporarily "solved" the problem before going on vacation by "reverting" to the old version of Paraconsistency, but I would now like to find out what happened, so that I can update the entry.)


The problem seems to be with the generation by latex of the pdf-document for the entry.


I do not know how to reproduce that error on my machine even though I have tried as follows:

I go into the Paraconsistency folder and run

isabelle build -f -o document=pdf -o document_output=output_folder -D .

And then Isabelle generates a pdf without error.


Does anyone have a suggestion of how I can proceed to solve this problem?

Cheers,
Anders

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20230825/3c32cad0/attachment.htm>