<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
</head>
<body style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">
<div style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">
Dear <span style="color: rgba(0, 0, 0, 0.85); font-family: "Helvetica Neue";">isabelle-dev</span>
<div><span style="color: rgba(0, 0, 0, 0.85); font-family: "Helvetica Neue";"><br>
</span></div>
<div><font face="Helvetica Neue"><span style="caret-color: rgba(0, 0, 0, 0.85); color: rgba(0, 0, 0, 0.85);">I tried to update the Paraconsistency entry of AFP to be as shown here: </span></font><a href="https://foss.heptapod.net/isa-afp/afp-devel/-/tree/851994a5d75d634876f75e47eca2d45f4b6fbee5/thys/Paraconsistency">https://foss.heptapod.net/isa-afp/afp-devel/-/tree/851994a5d75d634876f75e47eca2d45f4b6fbee5/thys/Paraconsistency</a></div>
<div><font face="Helvetica Neue"><span style="caret-color: rgba(0, 0, 0, 0.85); color: rgba(0, 0, 0, 0.85);"><br>
</span></font></div>
<div><font face="Helvetica Neue"><span style="caret-color: rgba(0, 0, 0, 0.85); color: rgba(0, 0, 0, 0.85);">However, when I pushed it to the repository, then the AFP build failed: </span></font><a href="https://ci.isabelle.systems/jenkins/job/isabelle-all/4580/consoleFull">https://ci.isabelle.systems/jenkins/job/isabelle-all/4580/consoleFull</a></div>
<div><br>
</div>
<div>The errors look like this:</div>
<div>
<pre style="overflow-wrap: break-word; white-space: pre-wrap;">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@ ...</pre>
</div>
<div>And keep going for many more lines.</div>
<div><br>
</div>
<div>(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.)</div>
<div><br>
</div>
<div><br>
</div>
<div>The problem seems to be with the generation by latex of the pdf-document for the entry.</div>
<div><br>
</div>
<div><br>
</div>
<div>I do not know how to reproduce that error on my machine even though I have tried as follows:</div>
<div><br>
</div>
<div>I go into the Paraconsistency folder and run</div>
<div><br>
</div>
<div>
<div style="margin: 0px; font-style: normal; font-variant-caps: normal; font-stretch: normal; line-height: normal; font-family: Menlo; font-size-adjust: none; font-kerning: auto; font-variant-alternates: normal; font-variant-ligatures: normal; font-variant-numeric: normal; font-variant-east-asian: normal; font-variant-position: normal; font-feature-settings: normal; font-optical-sizing: auto; font-variation-settings: normal;">
<span style="font-variant-ligatures: no-common-ligatures">isabelle build -f -o document=pdf -o document_output=output_folder -D .</span></div>
<div style="margin: 0px; font-style: normal; font-variant-caps: normal; font-stretch: normal; line-height: normal; font-family: Menlo; font-size-adjust: none; font-kerning: auto; font-variant-alternates: normal; font-variant-ligatures: normal; font-variant-numeric: normal; font-variant-east-asian: normal; font-variant-position: normal; font-feature-settings: normal; font-optical-sizing: auto; font-variation-settings: normal;">
<span style="font-variant-ligatures: no-common-ligatures"><br>
</span></div>
<div style="margin: 0px; font-style: normal; font-variant-caps: normal; font-stretch: normal; line-height: normal; font-size-adjust: none; font-kerning: auto; font-variant-alternates: normal; font-variant-ligatures: normal; font-variant-numeric: normal; font-variant-east-asian: normal; font-variant-position: normal; font-feature-settings: normal; font-optical-sizing: auto; font-variation-settings: normal;">
<span style="font-variant-ligatures: no-common-ligatures;">And then Isabelle generates a pdf without error.</span></div>
<div style="margin: 0px; font-style: normal; font-variant-caps: normal; font-stretch: normal; line-height: normal; font-size-adjust: none; font-kerning: auto; font-variant-alternates: normal; font-variant-ligatures: normal; font-variant-numeric: normal; font-variant-east-asian: normal; font-variant-position: normal; font-feature-settings: normal; font-optical-sizing: auto; font-variation-settings: normal;">
<span style="font-variant-ligatures: no-common-ligatures;"><br>
</span></div>
<div style="margin: 0px; font-style: normal; font-variant-caps: normal; font-stretch: normal; line-height: normal; font-size-adjust: none; font-kerning: auto; font-variant-alternates: normal; font-variant-ligatures: normal; font-variant-numeric: normal; font-variant-east-asian: normal; font-variant-position: normal; font-feature-settings: normal; font-optical-sizing: auto; font-variation-settings: normal;">
<br>
</div>
<div style="margin: 0px; font-style: normal; font-variant-caps: normal; font-stretch: normal; line-height: normal; font-size-adjust: none; font-kerning: auto; font-variant-alternates: normal; font-variant-ligatures: normal; font-variant-numeric: normal; font-variant-east-asian: normal; font-variant-position: normal; font-feature-settings: normal; font-optical-sizing: auto; font-variation-settings: normal;">
Does anyone have a suggestion of how I can proceed to solve this problem?</div>
<div style="margin: 0px; font-style: normal; font-variant-caps: normal; font-stretch: normal; line-height: normal; font-size-adjust: none; font-kerning: auto; font-variant-alternates: normal; font-variant-ligatures: normal; font-variant-numeric: normal; font-variant-east-asian: normal; font-variant-position: normal; font-feature-settings: normal; font-optical-sizing: auto; font-variation-settings: normal;">
<br>
</div>
<div style="margin: 0px; font-style: normal; font-variant-caps: normal; font-stretch: normal; line-height: normal; font-size-adjust: none; font-kerning: auto; font-variant-alternates: normal; font-variant-ligatures: normal; font-variant-numeric: normal; font-variant-east-asian: normal; font-variant-position: normal; font-feature-settings: normal; font-optical-sizing: auto; font-variation-settings: normal;">
Cheers,</div>
<div style="margin: 0px; font-style: normal; font-variant-caps: normal; font-stretch: normal; line-height: normal; font-size-adjust: none; font-kerning: auto; font-variant-alternates: normal; font-variant-ligatures: normal; font-variant-numeric: normal; font-variant-east-asian: normal; font-variant-position: normal; font-feature-settings: normal; font-optical-sizing: auto; font-variation-settings: normal;">
Anders</div>
<div style="margin: 0px; font-style: normal; font-variant-caps: normal; font-stretch: normal; line-height: normal; font-size-adjust: none; font-kerning: auto; font-variant-alternates: normal; font-variant-ligatures: normal; font-variant-numeric: normal; font-variant-east-asian: normal; font-variant-position: normal; font-feature-settings: normal; font-optical-sizing: auto; font-variation-settings: normal;">
<br>
</div>
</div>
</div>
</body>
</html>