Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] AFP Entries failing


view this post on Zulip Email Gateway (Sep 26 2022 at 12:04):

From: Makarius <makarius@sketis.net>
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


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Sep 26 2022 at 14:15):

From: Fabian Huch <huch@in.tum.de>
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


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Sep 26 2022 at 19:08):

From: Makarius <makarius@sketis.net>
Trying it manually with "isabelle build -o document ..." the error is actually
this:

*** Latex error (line 24 of "PAC_Checker_MLton.tex"):
*** Undefined control sequence.
*** ...\isacharparenleft}{\kern0pt}\isactrlverbatim
*** Failed to build document "document"

So there is something missing in the Isabelle LaTeX styles, which I have now
amended here:

changeset: 76209:e44e044dadb3
user: wenzelm
date: Mon Sep 26 20:40:19 2022 +0200
files: lib/texinputs/isabellesym.sty
description:
provide missing LaTeX macro, e.g. for AFP/PAC_Checker;

The deeper reason for the omission is that \<^verbatim> in formal document
text produces verbatim LaTeX output without a separate macro \isactrlverbatim.

In contrast, the use in Isabelle/ML remains literally visible --- and it was
rarely used so far.

Now that feature of Isabelle/ML got some extra attention, so maybe it will be
used more often in the future.

It works even better than triple-quoted strings in Scala or Python.

Makarius


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev


Last updated: Mar 04 2024 at 10:08 UTC