[isabelle-dev] Wish for warning of unescaped underscores in markup commands

Makarius makarius at sketis.net
Sat Nov 13 16:40:53 CET 2021

On 10/11/2021 09:20, Martin Desharnais wrote:
> I was just found guilty of repeating a mistake that I sadly perpetrate every
> now and then when writing markup commands in Isabelle theories. This is not
> intentional of my part and I would like to start a discussion about ways this
> could be avoided in the future.

The problem can be avoided by not thinking in terms of "guilt", "mistake" or
"perpretration". LaTeX is a very fragile language and no amount of precautions
nor tests will change the situation substantially.

Too much testing can also become a problem on its own account, being neither
necessary nor sufficient for a "good" situation. (We have too many
"uninformative green lights" on the planet, and too much obsession in
producing them.)

In your change e5eeaaf2bd5b you claim to have "fixed" a LaTeX failure, but you
also turned the unchecked formal text \<open>wlog_non_Red_F\<close> into
checked @{thm wlog_non_Red_F}, with different output: the thm statement (with
schematic variables) instead of the thm name. You probably intended to say
@{thm [source] ...} here.

Typical LaTeX document errors are actually of that kind, and often remain
undetected for years. There are also situations where gradual changes in the
LaTeX system give a different appearance of the document at a later stage.

In retrospect, I regret to have given so much weight to LaTeX in 1999, when
the Isabelle document system emerged for the first time.


More information about the isabelle-dev mailing list