[isabelle-dev] Latex problem on the AFP

[Achim D. Brucker]

Hi Anders,
Only a vague idea to help you debugging the issues:

To the best of my knowledge, the current AFP build infrastructure uses
TexLive 2019 on Ubuntu 20.04. This might be older than what you have
on your machine (I had some troubles with an entry currently in the
submission queue).

If you are familar with containers (e.g., docker, podman) or VMs, it
might be an idea to try to build the PDF by running latex in a TexLive 2019
container (e.g., docker HUB provides "listx/texlive:2019"). You can
use LaTeX files generated by Isabelle on your development machine.
No need to install Isabelle in a container ...

Best,
        Achim 





On Fri, Aug 25, 2023 at 09:13:55AM +0000, Anders Schlichtkrull wrote:
> 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
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev


-- 
Prof. Achim Brucker | Chair in Cybersecurity & Head of Group | University of Exeter
           https://www.brucker.ch | https://logicalhacking.com/blog
                         @adbrucker | @logicalhacking