Email Gateway (Nov 11 2021 at 15:26): Email Gateway (Nov 11 2021 at 15:26):From: Martin Desharnais <martin.desharnais@posteo.de>
Dear Isabelle developers,
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. Maybe I am
not the only one in this situation.
Consider the following example markup command.
text ‹Compactness of @{term entails} implies that Red_I and Red_F are
equivalent to ...›
No warning or error in Isabelle/jEdit nor when building the (AFP in this
case) entry with "isabelle build -c -d $AFP -B Entry_Name". Only later
when building the corresponding document with "-o document" option does
an error is (rightfully) reported. e.g.
Latex error (line N of "File.thy"):
Missing $ inserted.
<inserted text>
$
...harparenright}{\kern0pt}} implies that Red_
Latex error (line N of "File.thy"):
Missing $ inserted.
<inserted text>
$
\end{isamarkuptext}
Knowing that there is an error on this line, I immediately noticed that
I used unescaped underscores, which is now allowed in LaTeX. Here, the
solution was, as often, to use proper antiquotation, i.e., @{const
Red_I} and @{const Red_F}.
I believe that reporting this situation as soon as possible would be
beneficial for the user experience and could help minimize unfortunate
mistakes such as inadvertently pushing changesets that fail when
building documents. One could also argue that it wastes CPU cycles and
time to build the full entry, fail building the document, correct the
text, rebuild the entry, and finally build the full document.
Would it be possible for Isabelle to check for unescaped underscores in
markup commands and report a warning of incompatibility with LaTeX?
Regards,
Martin Desharnais
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 13 2021 at 15:41):From: Makarius <makarius@sketis.net>
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.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Apr 18 2024 at 20:16 UTC