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 <[email protected]> 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
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
