[isabelle-dev] AFP Entries failing

[Fabian Huch]

No, the Jenkins / Testboard setup and the ML compiler works. However, 
the latex setup of those two entries does not.

I can look at that later.


Fabian

On 9/26/22 16:04, Makarius wrote:
> 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
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev