[isabelle-dev] AFP Entries failing

[Makarius]

I am promiting this semi-private thread to isabelle-dev, because that is the 
canonical place to discuss problems with the Isabelle + AFP repositories.

My guess from a distance is that the Jenkins / Testboard setup is still 
lagging behind the change of Isabelle/d27ed188e0c4 that is cited in my log for 
AFP/10deeed51887.

There are further explanations on this isabelle-dev thread "NEWS: MLton 
compiler for x86_64-linux" 
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2022-September/017665.html


	Makarius

On 26/09/2022 11:32, Julian Brunner wrote:
> Hello,
> 
> I believe that this was initially triggered by commit
> https://foss.heptapod.net/isa-afp/afp-devel/-/commit/10deeed51887b7aa3b37f1c3e29eefb5b204b009
> where Makarius replaced "File.bash_path \<^path>" with "\<^verbatim>".
> I am assuming that this is the "\<^verbatim>", which corresponds to
> the "\isactrlverbatim" in the error message.
> 
> I have not touched this AFP entry in years and I do not know what
> Makarius' plans are with the verbatim control sequence. The initial
> change in 10deeed5 looked very intentional to me, so I was carelul not
> to interfere in series of events where I had no clue what was going
> on. If there is something I need to do here, please let me know.
> 
> Cheers,
>   Julian
> 
> 
> On Mon, Sep 26, 2022 at 10:18 AM Fabian Huch <huch at in.tum.de> wrote:
>>
>> Dear maintainers,
>>
>> the entries "Buchi_Complementation" and "PAC_Checker" both fail to build since Sep 17. You might not have been properly informed as the initial failure was induced by changes in the Isabelle SMLNJ component. The current failure is due to latex issues:
>>
>>
>> PAC_Checker FAILED
>>
>> 23:35:29 (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.9_x86_64_32-linux/log/PAC_Checker)
>>
>> 23:35:29 ./PAC_Checker_MLton.tex:45: Undefined control sequence.
>>
>> 23:35:29 l.45 ...\isacharparenleft}{\kern0pt}\isactrlverbatim
>>
>>
>>
>> 23:51:40 Buchi_Complementation FAILED
>>
>> 23:51:40 (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.9_x86_64_32-linux/log/Buchi_Complementation)
>>
>> 23:51:40 [57]) (./Complementation_Build.tex
>>
>> 23:51:40 ./Complementation_Build.tex:58: Undefined control sequence.
>>
>> 23:51:40 l.58 ...\isacharparenleft}{\kern0pt}\isactrlverbatim
>>
>> 23:51:40 {\isasymopen}{\isachardou...
>>
>>
>> Best,
>>
>> Fabian