Stream: Mirror: Isabelle Development Mailing List

Topic: Changed behaviour of (*<*) ... (*>*)

Email Gateway (Aug 27 2026 at 09:32):

From: "Achim D. Brucker" <adbrucker@0x5f.org>

Hi,

While trying to address a build failure of one of our AFP entries, I
spotted  (<) ... (>) does not seem to exclude parts from being
included in the generated LaTeX/PDF document. For instance, generating a
PDF from the the theory

theory Ex imports Main begin
(<)text\<open>Should this be included in the generated PDF?\<close>(>)
end

does not include the text "Should this be included in the generated
PDF?" in the generated PDF when using Isabelle 2025-2 but is included
when using the latest version from the repository (TIP:
85327:dc45b445012a).

By quickly skimming over the NEWS entries an the hg log messages, I
could not find out whether this is intentional or not.

I would appreciate any advise on how I should upgrade my theories to
make them ready for the future.

Thanks a lot!

Best,

Achim

Email Gateway (Sep 05 2026 at 18:56):

From: "Achim D. Brucker" <adbrucker@0x5f.org>

Hi,
I did some bisection. The changset that introduced the new behaviour is
"85275:e50cdc94cf5d".

Starting with this changeset, text enclosed in (<) ... (>) is no
longer excluded from the LaTeX/PDF generation. I assume this results in
a "silent" change for most applications (i.e., some text is now included
in the PDF that was not intended to be excluded). For one of the AFP
entries (Isabelle_DOF) I co-authored, this is resulting in a hard
compilation error, as some invalid LateX code is intentionally excluded
from the final LaTeX/PDF generation using (<) ... (>).

Best,
Achim

On 27/08/2026 10:32, Achim D. Brucker wrote:

Hi,

While trying to address a build failure of one of our AFP entries, I
spotted  (<) ... (>) does not seem to exclude parts from being
included in the generated LaTeX/PDF document. For instance, generating
a PDF from the the theory

theory Ex imports Main begin
(<)text\<open>Should this be included in the generated
PDF?\<close>(>)
end

does not include the text "Should this be included in the generated
PDF?" in the generated PDF when using Isabelle 2025-2 but is included
when using the latest version from the repository (TIP:
85327:dc45b445012a).

By quickly skimming over the NEWS entries an the hg log messages, I
could not find out whether this is intentional or not.

I would appreciate any advise on how I should upgrade my theories to
make them ready for the future.

Thanks a lot!

Best,

Achim

]

Email Gateway (Sep 05 2026 at 20:45):

From: Makarius <makarius@sketis.net>

On 05/09/2026 20:55, Achim D. Brucker wrote:

Hi,
I did some bisection. The changset that introduced the new behaviour is
"85275:e50cdc94cf5d".

Starting with this changeset, text enclosed in (<) ... (>) is no longer
excluded from the LaTeX/PDF generation. I assume this results in a "silent"
change for most applications (i.e., some text is now included in the PDF that
was not intended to be excluded). For one of the AFP entries (Isabelle_DOF) I
co-authored, this is resulting in a hard compilation error, as some invalid
LateX code is intentionally excluded from the final LaTeX/PDF generation using
(<) ... (>).

Hi Achim,

there is definitely something wrong in my side, but I did not find time yet to
figure out the details. Presently, the next defined snapshot will be
Isabelle2026-RC1. In between, many things can be wrong in many ways.

Makarius

Last updated: Sep 15 2026 at 09:19 UTC