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
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
