metamath / metamath-exe

Metamath program - source code for the Metamath executable
GNU General Public License v2.0
75 stars 25 forks source link

Attempting to fix the curly brackets bug #166

Closed GinoGiotto closed 8 months ago

GinoGiotto commented 9 months ago

This is my attempt to fix issue #129. The solution I proposed in https://github.com/metamath/metamath-exe/issues/129#issuecomment-1404255591 is actually not very practical because latex translations get merged togheter pretty early and this makes it difficult to take advantage of that information. So I changed my mind and implemented @david-a-wheeler proposal instead https://github.com/metamath/metamath-exe/issues/129#issuecomment-1435743413. I took inspiration from an analogous functionality already present for HTML: https://github.com/metamath/metamath-exe/blob/ae35c1b2931be8f9683f8bf66d1d10c9b56db706/src/mminou.c#L549-L588

With this change the generated TeX of my minimal example seems to work as intended:

% This LaTeX file was created by Metamath on 22-Oct-2023 9:40 PM.
\documentclass{article}
\usepackage{amssymb} % amssymb must be loaded before phonetic
\usepackage{phonetic} % for \riota
\usepackage{mathrsfs} % for \mathscr
\usepackage{mathtools} % loads package amsmath
\usepackage{amsthm} % amsthm must be loaded after amsmath
\usepackage{accents} % accents should be loaded after mathtools
\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 }
    \notag \\ && & \qquad \text{ A A A A A A A A A A }
    \notag \\ && & \qquad \text{ A A A A A A A A A A }
\text{ A A A A A A A A A A }&(\mbox{\ref{eq:ax-1}})\notag
\end{align}
\end{proof}

\end{document}

I'm somewhat surprised by how simple this solution looks, and this makes me wonder whether it might be a false friend due to my own ignorance. So it most likely needs to be overhauled by an expert eye.

tirix commented 9 months ago

Maybe one (last?) remark would be to integrate your minimal example into an additional test in the tests directory, with an additional issue129.in, issue129.mm and issue129.expected.

Unfortunately I don't have the rights to merge, I guess @digama0 does.

GinoGiotto commented 8 months ago

My only question is whether issue129.tex should be included as well, since in this case that's the file we are interested verifying. But run_test.sh doesn't seem to be designed to check the generated tex tho.

tirix commented 8 months ago

Oh right, of course I have not thought so far. That would have been a nice to have, I'm sorry I feel I have made you add a quite useless test.

digama0 commented 8 months ago

There is another test which has to check the result of an auxiliary file, and uses a trick calling cat inside metamath to get it to be validated. See the underscores test.

GinoGiotto commented 8 months ago

I don't understand what's wrong. On my computer both attempts pass. Maybe it doesn't like backslashes?

tirix commented 8 months ago

Based on this SO answer, line 113 of run_tests.sh, I would try replacing the cat "$result" with printf '%s' "$result" so that the backslashes are not interpreted.

GinoGiotto commented 8 months ago

(Accidentally pressed the close button)

Thanks for making it work, should be good to merge now.

I wonder if there is any difference between using more or cat in issue129.in

GinoGiotto commented 8 months ago

Btw sorry @tirix I superficially read your suggestion and made a mess.

tirix commented 8 months ago

The final one looks good! I already approved, I think only @digama0 can merge now.