[isabelle-dev] Latex problem on the AFP

[Anders Schlichtkrull]

Hi Achim and isabelle-dev

Thanks Achim! I followed your idea of trying with different versions of TexLive and also with Docker, to try it also on different versions Ubuntu.

My conclusion is that the problem is essentially that in Paraconsistency.thy we have the following:

text
‹
Theorem valid_in_valid is a kind of the reverse of valid_valid_in (or its transfer variant).
›

In the generated LaTeX this becomes
  Theorem valid_in_valid is a kind of the reverse of valid_valid_in (or its transfer variant).

The underscore is a reserved character in LaTeX, and cannot be used in textmode.
However, we "solved" that "problem" by importing the underscore package.
That package's documentation states: "A simple “_” acts just like “\_” in text mode"

However, that package's documentation also states: 

You must avoid “_” in file names and in cite or ref tags, or you must use the babel package, with its active-character controls, or you must give the [strings] option, which attempts to redefine several commands (and may not work perfectly). Even without the [strings] option or babel, you can use occasional underscores like: “\include{file\string_name}”.

And this must be the problem we encounter now that we have introduced the file "Paraconsistency_Validity_Infinite.tex". 

What is peculiar that when I try with a docker container with Ubuntu 20.10 and texlive 2019 it results in lualatex/pdflatex giving an error, but none of the following systems give that error and they all build the pdf without problems:
* macOS with texlive 2019
* macOS with texlive 2023
* a docker container with Ubuntu 23.10 and texlive 2022.

The documentation of the underscore package suggests some solutions: 

  You must avoid “_” in file names and in cite or ref tags, or you must use the babel package, with its active-character controls, or you must give the [strings] option, 
  which attempts to redefine several commands (and may not work perfectly). Even without the [strings] option or babel, you can use occasional underscores like: “\include{file\string_name}”.

Using the [strings] option makes building the pdf work on all the mentioned platforms, so I will go with that solution.

I will try to push this to afp-devel to see what happens :-)

Cheers,
Anders

> On 25 Aug 2023, at 11.28, Achim D. Brucker <adbrucker at 0x5f.org> wrote:
> 
> 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