[isabelle-dev] AFP Entries failing

Makarius makarius at sketis.net
Mon Sep 26 20:59:25 CEST 2022

On 26/09/2022 16:15, Fabian Huch wrote:
> No, the Jenkins / Testboard setup and the ML compiler works. However, the 
> latex setup of those two entries does not.

Trying it manually with "isabelle build -o document ..." the error is actually 

*** 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
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.


More information about the isabelle-dev mailing list