Latex curly brackets bug

[GinoGiotto]

Hello, so I wanted to show a proof in a .tex file, to do this I executed the following commands in Metamath:

Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> read set.mm
Reading source file "set.mm"... 42839696 bytes
42839696 bytes were read into the source buffer.
The source has 203558 statements; 2716 are $a and 40625 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> VERIFY PROOF *
0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
..................................................
All proofs in the database were verified in 27.72 s.
MM> open tex proof-example.tex
Created LaTeX output file "proof-example.tex".
Reading definitions from $t statement of set.mm...
1643 typesetting statements were read from "set.mm".
MM> show proof rankidn /tex
Outputting proof of "rankidn"...
The LaTeX source was written to "proof-example.tex".
MM> close tex
The LaTeX output file "proof-example.tex" has been closed.
MM>

These commands create THIS file called "proof-example.tex" (I changed the format to .txt) containing the proof of the "rankidn" theorem.

Now, when I compile the .tex file with a latex editor (I tested it with TeXstudio, TeXworks and Texmaker) it shows some errors such as:

Missing } inserted. \end{align}
Missing { inserted. \end{align}
Missing \endgroup inserted. \end{align}
Misplaced \omit. \end{align}

It also shows some warnings regarding missing references (latex commands such as \ref{eq:rankr1c} mention theorems and axioms that are not present in the .tex file so it shows (??) in the generated pdf). This is more of an aesthetic issue and it's not the main theme of this bug report.

Now regarding the errors here what I think is happening:

I think they all have one single cause, and the cause is that curly brackets cannot be opened and closed in separate lines. More specifically none of these symbols: \\ && & should appear in some text enclosed in curly brackets.

It's possible to test my hypothesis with the example I provided: If you edit the second step of "proof-example.tex" from:

\\ 2 &&  & \vdash ( A \in \bigcup ( R_1 `` {\rm On} ) \rightarrow ( ( {\rm
    \notag \\ && & \qquad rank} ` A ) = ( {\rm rank} ` A ) \leftrightarrow (
    \notag \\ && & \qquad \lnot A \in ( R_1 ` ( {\rm rank} ` A ) ) \wedge A \in
    \notag \\ && & \qquad ( R_1 ` {\rm suc} ( {\rm rank} ` A ) ) ) )
    \notag \\ && & \qquad )&(\mbox{\ref{eq:rankr1c}})\notag

to:

\\ 2 &&  & \vdash ( A \in \bigcup ( R_1 `` {\rm On} ) \rightarrow ( ( {\rm
    \notag \qquad rank} ` A ) = ( {\rm rank} ` A ) \leftrightarrow (
    \notag \\ && & \qquad \lnot A \in ( R_1 ` ( {\rm rank} ` A ) ) \wedge A \in
    \notag \\ && & \qquad ( R_1 ` {\rm suc} ( {\rm rank} ` A ) ) ) )
    \notag \\ && & \qquad )&(\mbox{\ref{eq:rankr1c}})\notag

Then all errors disappear.

I should mention that even though I think I understood the issue, I have no idea how to fix it, I'm still a beginner in Metamath and I don't know how its inner programming works.

I purposely chose the theorem "rankidn" because it has a short proof (only 4 steps) and so it shouldn't be too painful to look at its corresponding tex proof.

Regards

Gino

[tirix]

Hi Gino,

I've never tried to work with TeX output from Metamath.exe, and I have not tested my hypotheses, but here are my 2 cents anyway:
Just by looking at the exported TeX file, it looks like it is formatted with a line width of 80 characters. I believe this is a default Metamath.exe behaviour, which also applies to Metamath files.

If your issue comes from these line breaks, I think a command SET WIDTH would allow you to increase that width and remove the line breaks. Maybe setting a "very big" value, like SET WIDTH 99999, might rid you of all line breaks and allow the TeX generation to succeed. This assumes that this setting applies to all output, not just MM files output, but it looks like it is a reasonable assumption to make.

I don't know if there is a setting to remove this line width altogether - that would be even better.

[GinoGiotto]

Yes, I used the default width, which is setted at 79. The problem of setting a big value is that the text goes outside of the pdf document, which I think it's the reason why lew lines were put in the first place. This would require to manually adjust the length of steps that are too long, which is quite unpractical for long proofs.

Now I looked it up a little and maybe there is a way to fix it. Metamath tex translation doesn't have expressions that depend on the surrounding symbols, so all curly brackets derive from the translation of an unicode symbol sequence from the $t comment. For the example I provided before there is the line latexdef "rank" as "{\rm rank}"; which translates "rank" into {\rm rank}, so the translator just placed \notag \\ && & \qquad inside it, generating {\rm \notag \\ && & \qquad rank}, which produces an error. So one approach could be to change the code so that it put line breaks always between latex translations and never inside one. I guess Metamath just counts the characters up to 79 for each line and then it places a linebreak before the next word passes that treshold. So instead of separating the latex text by words, it could work separating it by translations.

Let me know if I made mistakes, I've written this just by empirical observations, but I don't really know how the code works.

[benjub]

(\mbox{\ref{eq:rankr1c}})\notag

I guess that here, \ref is meant to be \tag. It makes no sense to enclose \ref in an mbox (nor to put it in a displayed equation, generally): \ref points to the element with the corresponding \label. Insteead, \tag will put what it encloses as a tag (while \notag deactivates the standard tagging, generally numerical tagging, global or within the chapter/section...).

[benjub]

latexdef "rank" as "{\rm rank}";

The LaTeX code should be \mathrm{rank}. And this happens to solve your present problem.

[david-a-wheeler]

@benjub - thanks for working that out.

In the longer term, I think the problem is that we don't have an automated test suite for metamath-exe that checks TeX generation. Once we fix that problems, we should add that (and other tests) to prevent recurrence.

[benjub]

@david-a-wheeler : A naive test could be to have a python/sed/AWK script transform each new/modified substring of the mm files of the form

latexdef "XXX" as "YYY"

into \( YYY \), remove the rest and add "\documentclass{article}\usepackage{mathtools} [and whatnot]\begin{document}" at the beginning and "\end{document}" at the end and see if pdflatex compiles...

[digama0]

I think we should just have test cases that exercise the HTML/TeX part. I don't think we need to also test the TeX files to ensure they compile as long as the checked in tests are okay.

[david-a-wheeler]

Fair enough.

In this case the problem is a problem in set.mm, not really in metamath-exe. That should also be tested, but probably in the set.mm test suite (once we're sure it's working).

[digama0]

No, I think this is a metamath-exe bug - it is clearly wrong to be putting so much weight on the line breaking that it produces incorrect TeX. The {\rm rank} expression is not wrong at all, and the same issue would happen whenever there are any spaces in a TeX substitution.

[benjub]

Yes: the test I proposed above tests the mm files and should be in the "databases" repository (currently called "set.mm"). It tests only single latexdefs independently.

The question of arranging them together is the role of metamath.c (or any transcription program), and should be tested here. Both the TeX generation and the test suites here are much harder to come with.

[david-a-wheeler]

So one approach could be to change the code so that it put line breaks always between latex translations and never inside one.

This seems like the best course. We could try to be clever and count braces, but the code would have to be smart enough to notice the various escape mechanisms, and it would look the same either way.

[GinoGiotto]

The example I initially provided doesn't work anymore because in the meantime {\rm rank} has been converted into \mathrm{rank} which has no spaces between curly braces. To ensure that this issue remains independent from future set.mm updates, I provide new a minimal test case below:

$c A $.

ax-1 $a A A A A A $.

th1 $p A A A A A $= ax-1 $.

$( $t
    latexdef "A" as "\text{ A A A A A A A A A A }";
$)

Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> read issue129.mm
Reading source file "issue129.mm"... 121 bytes
121 bytes were read into the source buffer.
The source has 3 statements; 1 are $a and 1 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> open tex issue129.tex
Created LaTeX output file "issue129.tex".
Reading definitions from $t statement of issue129.mm...
1 typesetting statements were read from "issue129.mm".
MM> show proof th1 /tex
Outputting proof of "th1"...
The LaTeX source was written to "issue129.tex".
MM> close tex
The LaTeX output file "issue129.tex" has been closed.
MM>

Generated file:

% This LaTeX file was created by Metamath on 16-Oct-2023 3:21 PM.
\documentclass{article}
\usepackage{graphicx} % For rotated iota
\usepackage{amssymb}
\usepackage{amsmath} % For \begin{align}...
\usepackage{amsthm}
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{definition}[theorem]{Definition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{axiom}{Axiom}
\allowdisplaybreaks[1] % Allow page breaks in {align}
\usepackage[plainpages=false,pdfpagelabels]{hyperref}
\hypersetup{colorlinks} % Get rid of boxes around links
\begin{document}

\begin{proof}
\begin{align}
  1 &&  & \text{ A A A A A A A A A A } \text{ A A A A A A A A A A } \text{ A A
    \notag \\ && & \qquad A A A A A A A A } \text{ A A A A A A A A A A } \text{
    \notag \\ && & \qquad A A A A A A A A A A }&(\mbox{\ref{eq:ax-1}})\notag
\end{align}
\end{proof}

\end{document}

Short recap: the LaTeX compiler generates an error because \notag \\ && & \qquad appears inside curly braces. As a solution I proposed to forbid the placement of \notag \\ && & \qquad inside TeX substitutions. I don't think metamath-exe allows other ways to generate curly braces with spaces inside, therefore I believe this approach is a sensible way to solve the issue.

[GinoGiotto]

PR #166 fixes this bug, so I can close this issue now.

[GinoGiotto]

Thanks everyone for your partecipation and contributions.