From f92ee1ad93ba4d692cca718b35e2c517bbd3e1c5 Mon Sep 17 00:00:00 2001 From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com> Date: Sun, 22 Oct 2023 21:16:04 +0200 Subject: [PATCH 01/11] fixed curly brackets bug --- src/mminou.c | 33 +++++++++++++++++++++++++++------ 1 file changed, 27 insertions(+), 6 deletions(-) diff --git a/src/mminou.c b/src/mminou.c index a36d60e3..26e8468a 100644 --- a/src/mminou.c +++ b/src/mminou.c @@ -501,7 +501,7 @@ void printLongLine(const char *line, const char *startNextLine, const char *brea vstring_def(prefix); vstring_def(startNextLine1); vstring_def(breakMatch1); - long i, j, p; + long i, j, p, k; long startNextLineLen; flag firstLine; flag tildeFlag = 0; @@ -546,6 +546,12 @@ void printLongLine(const char *line, const char *startNextLine, const char *brea breakMatch1[0] = ' '; // Change to a space (the real break character) } + // Do a bug check to make sure no real ASCII 3's are ever printed + j = (long)strlen(multiLine); + for (i = 0; i < j; i++) { + if (multiLine[i] == QUOTED_SPACE) bug(1514); // Should never be the case + } + // HTML mode // The HTML mode is intended not to break inside quoted HTML tag // strings. All HTML output should be called with this mode. @@ -559,11 +565,6 @@ void printLongLine(const char *line, const char *startNextLine, const char *brea // where all ASCII 3's are converted back to space. // Note added 20-Oct-02: tidy.exe breaks HREF quotes with new line. // Check HTML spec - do we really need this code? - j = (long)strlen(multiLine); - // Do a bug check to make sure no real ASCII 3's are ever printed - for (i = 0; i < j; i++) { - if (multiLine[i] == QUOTED_SPACE) bug(1514); // Should never be the case - } if (breakMatch1[0] == '\"') { breakMatch1[0] = ' '; // Change to a space (the real break character) // Scan string for quoted strings @@ -587,6 +588,26 @@ void printLongLine(const char *line, const char *startNextLine, const char *brea } } // if (breakMatch1[0] == '\"') + // TeX mode + // The TeX mode is intended not to break inside curly brace scopes. + // Whenever we are inside a scope of curly braces, we change a space to + // ASCII 3 to prevent matching it. The reverse is done in the print2() + // function, where all ASCII 3's are converted back to space. + if (breakMatch1[0] == ' ') { + i = 0; + // k counts the scope level we are in. + k = 0; + while (multiLine[i]) { + // We enter a non "\{" scope. + if (multiLine[i] == '{' && multiLine[i - 1] != '\\') k++; + // We escape a non "\}" scope. + if (multiLine[i] == '}' && multiLine[i - 1] != '\\') k--; + // If k > 0 then we are inside a scope. + if (multiLine[i] == ' ' && k > 0) multiLine[i] = QUOTED_SPACE; + i++; + } + } + // The tilde is a special flag for printLongLine to print a // tilde before the carriage return in a split line, not after. if (startNextLine1[0] == '~') { From 9c6e88eea71360e7fcb7b72051a4a9b7511ada46 Mon Sep 17 00:00:00 2001 From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com> Date: Wed, 25 Oct 2023 23:16:28 +0200 Subject: [PATCH 02/11] moved counting algorithm to mmwtex.c --- src/mminou.c | 28 +--------- src/mmwtex.c | 147 ++++++++++++++++++++++++++++++++++----------------- 2 files changed, 99 insertions(+), 76 deletions(-) diff --git a/src/mminou.c b/src/mminou.c index 26e8468a..e6c8579a 100644 --- a/src/mminou.c +++ b/src/mminou.c @@ -501,7 +501,7 @@ void printLongLine(const char *line, const char *startNextLine, const char *brea vstring_def(prefix); vstring_def(startNextLine1); vstring_def(breakMatch1); - long i, j, p, k; + long i, p; long startNextLineLen; flag firstLine; flag tildeFlag = 0; @@ -546,12 +546,6 @@ void printLongLine(const char *line, const char *startNextLine, const char *brea breakMatch1[0] = ' '; // Change to a space (the real break character) } - // Do a bug check to make sure no real ASCII 3's are ever printed - j = (long)strlen(multiLine); - for (i = 0; i < j; i++) { - if (multiLine[i] == QUOTED_SPACE) bug(1514); // Should never be the case - } - // HTML mode // The HTML mode is intended not to break inside quoted HTML tag // strings. All HTML output should be called with this mode. @@ -588,26 +582,6 @@ void printLongLine(const char *line, const char *startNextLine, const char *brea } } // if (breakMatch1[0] == '\"') - // TeX mode - // The TeX mode is intended not to break inside curly brace scopes. - // Whenever we are inside a scope of curly braces, we change a space to - // ASCII 3 to prevent matching it. The reverse is done in the print2() - // function, where all ASCII 3's are converted back to space. - if (breakMatch1[0] == ' ') { - i = 0; - // k counts the scope level we are in. - k = 0; - while (multiLine[i]) { - // We enter a non "\{" scope. - if (multiLine[i] == '{' && multiLine[i - 1] != '\\') k++; - // We escape a non "\}" scope. - if (multiLine[i] == '}' && multiLine[i - 1] != '\\') k--; - // If k > 0 then we are inside a scope. - if (multiLine[i] == ' ' && k > 0) multiLine[i] = QUOTED_SPACE; - i++; - } - } - // The tilde is a special flag for printLongLine to print a // tilde before the carriage return in a split line, not after. if (startNextLine1[0] == '~') { diff --git a/src/mmwtex.c b/src/mmwtex.c index 60d9f34d..43e84213 100644 --- a/src/mmwtex.c +++ b/src/mmwtex.c @@ -59,6 +59,15 @@ pntrString_def(g_mathboxUser); // User name vs. mathbox # // in a math string in a comment to be removed for HTML output. #define CLOSING_PUNCTUATION ".,;)?!:]'\"_-" +/*! + * \def QUOTED_SPACE + * The general line wrapping algorithm looks out for spaces as break positions. + * To prevent a quote delimited by __"__ be broken down, spaces are temporarily + * replaced with 0x03 (ETX, end of transmission), hopefully never used in + * text in this application. + */ +#define QUOTED_SPACE 3 // ASCII 3 that temporarily zaps a space + // Tex output file FILE *g_texFilePtr = NULL; flag g_texFileOpenFlag = 0; @@ -2806,10 +2815,11 @@ void printTexLongMath(nmbrString *mathString, long indentationLevel) { #define INDENTATION_OFFSET 1 - long i; + long i, j, k, n; long pos; vstring_def(tex); vstring_def(texLine); + vstring_def(texFull); vstring_def(sPrefix); vstring_def(htmStep); vstring_def(htmStepTag); @@ -3047,55 +3057,94 @@ void printTexLongMath(nmbrString *mathString, if (!g_oldTexFlag) { if (refType == 'e' || refType == 'f') { // A hypothesis - don't include \ref{} - printLongLine(cat(" ", - // If not first step, so print "\\" LaTeX line break - !strcmp(htmStep, "1") ? "" : "\\\\ ", - htmStep, // Step number - " && ", - " & ", - texLine, - // Don't put space to help prevent bad line break - "&\\text{Hyp~", - // The following puts a hypothesis number such as "2" if - // $e label is "abc.2"; if no ".", will be whole label. - right(htmRef, instr(1, htmRef, ".") + 1), - "}\\notag%", - // Add full label as LaTeX comment - note lack of space after - // "%" above to prevent bad line break. - htmRef, NULL), - " \\notag \\\\ && & \\qquad ", // Continuation line prefix - " "); + texFull = cat(" ", // texFull[0] should not be a "{" character. + // If not first step, so print "\\" LaTeX line break + !strcmp(htmStep, "1") ? "" : "\\\\ ", + htmStep, // Step number + " && ", + " & ", + texLine, + // Don't put space to help prevent bad line break + "&\\text{Hyp~", + // The following puts a hypothesis number such as "2" if + // $e label is "abc.2"; if no ".", will be whole label. + right(htmRef, instr(1, htmRef, ".") + 1), + "}\\notag%", + // Add full label as LaTeX comment - note lack of space after + // "%" above to prevent bad line break. + htmRef, NULL), + + // To avoid generating incorrect TeX, line breaking is forbidden inside + // scopes of curly braces. However breaking between '\{' and '\}' is + // allowed. + // The spaces that should not be matched with 'breakMatch' are + // temporarily changed to ASCII 3 before the 'printLongLine' procedure + // is called. The procedure rewraps the 'line' argument matching the + // unchanged spaces only, thus ensuring bad breaks will be avoided. + // The reverse is done in the 'print2()' function, where all ASCII 3's + // are converted back to spaces. + // k counts the scope level we are in. + k = 0; + n = (long)strlen(texFull); + for (j = 1; j < n; j++) { // We don't need to check texFull[0]. + // We enter a non "\{" scope. + if (texFull[j] == '{' && texFull[j - 1] != '\\') k++; + // We escape a non "\}" scope. + if (texFull[j] == '}' && texFull[j - 1] != '\\') k--; + // If k > 0 then we are inside a scope. + if (texFull[j] == ' ' && k > 0) texFull[j] = QUOTED_SPACE; + } + printLongLine(texFull, " \\notag \\\\ && & \\qquad ", /* Continuation line prefix */ " "); } else { - printLongLine(cat(" ", - // If not first step, so print "\\" LaTeX line break - !strcmp(htmStep, "1") ? "" : "\\\\ ", - htmStep, // Step number - " && ", - - // Local label if any e.g. "@2:" - (htmLocLab[0] != 0) ? cat(htmLocLab, "\\ ", NULL) : "", - - " & ", - texLine, - // Don't put space to help prevent bad line break - - // Surround \ref with \mbox for non-math-mode - // symbolic labels (due to \tag{..} in mmcmds.c). Also, - // move hypotheses to after referenced label. - "&", - "(", - - // Don't make local label a \ref - (htmRef[0] != '@') ? - cat("\\mbox{\\ref{eq:", htmRef, "}}", NULL) - : htmRef, - - htmHyp[0] ? "," : "", - htmHyp, - ")\\notag", NULL), - - " \\notag \\\\ && & \\qquad ", // Continuation line prefix - " "); + texFull = cat(" ", // texFull[0] should not be a "{" character. + // If not first step, so print "\\" LaTeX line break + !strcmp(htmStep, "1") ? "" : "\\\\ ", + htmStep, // Step number + " && ", + + // Local label if any e.g. "@2:" + (htmLocLab[0] != 0) ? cat(htmLocLab, "\\ ", NULL) : "", + + " & ", + texLine, + // Don't put space to help prevent bad line break + + // Surround \ref with \mbox for non-math-mode + // symbolic labels (due to \tag{..} in mmcmds.c). Also, + // move hypotheses to after referenced label. + "&", + "(", + + // Don't make local label a \ref + (htmRef[0] != '@') ? + cat("\\mbox{\\ref{eq:", htmRef, "}}", NULL) + : htmRef, + + htmHyp[0] ? "," : "", + htmHyp, + ")\\notag", NULL), + + // To avoid generating incorrect TeX, line breaking is forbidden inside + // scopes of curly braces. However breaking between '\{' and '\}' is + // allowed. + // The spaces that should not be matched with 'breakMatch' are + // temporarily changed to ASCII 3 before the 'printLongLine' procedure + // is called. The procedure rewraps the 'line' argument matching the + // unchanged spaces only, thus ensuring bad breaks will be avoided. + // The reverse is done in the 'print2()' function, where all ASCII 3's + // are converted back to spaces. + // k counts the scope level we are in. + k = 0; + n = (long)strlen(texFull); + for (j = 1; j < n; j++) { // We don't need to check texFull[0]. + // We enter a non "\{" scope. + if (texFull[j] == '{' && texFull[j - 1] != '\\') k++; + // We escape a non "\}" scope. + if (texFull[j] == '}' && texFull[j - 1] != '\\') k--; + // If k > 0 then we are inside a scope. + if (texFull[j] == ' ' && k > 0) texFull[j] = QUOTED_SPACE; + } + printLongLine(texFull, " \\notag \\\\ && & \\qquad ", /* Continuation line prefix */ " "); } } else { printLongLine(texLine, "", "\\"); From 85d6951d268ef8a5fa34b97fe464e5bd48a95bcd Mon Sep 17 00:00:00 2001 From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com> Date: Thu, 26 Oct 2023 20:39:30 +0200 Subject: [PATCH 03/11] unduplicate counting algorithm + printLongLine --- src/mmwtex.c | 69 ++++++++++++++++++---------------------------------- 1 file changed, 23 insertions(+), 46 deletions(-) diff --git a/src/mmwtex.c b/src/mmwtex.c index 43e84213..96f5063f 100644 --- a/src/mmwtex.c +++ b/src/mmwtex.c @@ -3072,29 +3072,7 @@ void printTexLongMath(nmbrString *mathString, "}\\notag%", // Add full label as LaTeX comment - note lack of space after // "%" above to prevent bad line break. - htmRef, NULL), - - // To avoid generating incorrect TeX, line breaking is forbidden inside - // scopes of curly braces. However breaking between '\{' and '\}' is - // allowed. - // The spaces that should not be matched with 'breakMatch' are - // temporarily changed to ASCII 3 before the 'printLongLine' procedure - // is called. The procedure rewraps the 'line' argument matching the - // unchanged spaces only, thus ensuring bad breaks will be avoided. - // The reverse is done in the 'print2()' function, where all ASCII 3's - // are converted back to spaces. - // k counts the scope level we are in. - k = 0; - n = (long)strlen(texFull); - for (j = 1; j < n; j++) { // We don't need to check texFull[0]. - // We enter a non "\{" scope. - if (texFull[j] == '{' && texFull[j - 1] != '\\') k++; - // We escape a non "\}" scope. - if (texFull[j] == '}' && texFull[j - 1] != '\\') k--; - // If k > 0 then we are inside a scope. - if (texFull[j] == ' ' && k > 0) texFull[j] = QUOTED_SPACE; - } - printLongLine(texFull, " \\notag \\\\ && & \\qquad ", /* Continuation line prefix */ " "); + htmRef, NULL); } else { texFull = cat(" ", // texFull[0] should not be a "{" character. // If not first step, so print "\\" LaTeX line break @@ -3122,30 +3100,29 @@ void printTexLongMath(nmbrString *mathString, htmHyp[0] ? "," : "", htmHyp, - ")\\notag", NULL), - - // To avoid generating incorrect TeX, line breaking is forbidden inside - // scopes of curly braces. However breaking between '\{' and '\}' is - // allowed. - // The spaces that should not be matched with 'breakMatch' are - // temporarily changed to ASCII 3 before the 'printLongLine' procedure - // is called. The procedure rewraps the 'line' argument matching the - // unchanged spaces only, thus ensuring bad breaks will be avoided. - // The reverse is done in the 'print2()' function, where all ASCII 3's - // are converted back to spaces. - // k counts the scope level we are in. - k = 0; - n = (long)strlen(texFull); - for (j = 1; j < n; j++) { // We don't need to check texFull[0]. - // We enter a non "\{" scope. - if (texFull[j] == '{' && texFull[j - 1] != '\\') k++; - // We escape a non "\}" scope. - if (texFull[j] == '}' && texFull[j - 1] != '\\') k--; - // If k > 0 then we are inside a scope. - if (texFull[j] == ' ' && k > 0) texFull[j] = QUOTED_SPACE; - } - printLongLine(texFull, " \\notag \\\\ && & \\qquad ", /* Continuation line prefix */ " "); + ")\\notag", NULL); + } + // To avoid generating incorrect TeX, line breaking is forbidden inside + // scopes of curly braces. However breaking between '\{' and '\}' is + // allowed. + // The spaces that should not be matched with 'breakMatch' are + // temporarily changed to ASCII 3 before the 'printLongLine' procedure + // is called. The procedure rewraps the 'line' argument matching the + // unchanged spaces only, thus ensuring bad breaks will be avoided. + // The reverse is done in the 'print2()' function, where all ASCII 3's + // are converted back to spaces. + // k counts the scope level we are in. + k = 0; + n = (long)strlen(texFull); + for (j = 1; j < n; j++) { // We don't need to check texFull[0]. + // We enter a non "\{" scope. + if (texFull[j] == '{' && texFull[j - 1] != '\\') k++; + // We escape a non "\}" scope. + if (texFull[j] == '}' && texFull[j - 1] != '\\') k--; + // If k > 0 then we are inside a scope. + if (texFull[j] == ' ' && k > 0) texFull[j] = QUOTED_SPACE; } + printLongLine(texFull, " \\notag \\\\ && & \\qquad ", /* Continuation line prefix */ " "); } else { printLongLine(texLine, "", "\\"); print2("\\endm\n"); From eb6541f02f6e537b071c9b860bca7352b0e23a16 Mon Sep 17 00:00:00 2001 From: Gino Giotto Date: Tue, 31 Oct 2023 16:23:42 +0100 Subject: [PATCH 04/11] add test case --- tests/issue129.expected | 13 +++++++++++++ tests/issue129.in | 3 +++ tests/issue129.mm | 9 +++++++++ 3 files changed, 25 insertions(+) create mode 100644 tests/issue129.expected create mode 100644 tests/issue129.in create mode 100644 tests/issue129.mm diff --git a/tests/issue129.expected b/tests/issue129.expected new file mode 100644 index 00000000..63b94a52 --- /dev/null +++ b/tests/issue129.expected @@ -0,0 +1,13 @@ +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> Continuous scrolling is now in effect. +MM> Created LaTeX output file "issue129.tex". +Reading definitions from $t statement of issue129.mm... +1 typesetting statements were read from "issue129.mm". +MM> Outputting proof of "th1"... +The LaTeX source was written to "issue129.tex". +MM> The LaTeX output file "issue129.tex" has been closed. diff --git a/tests/issue129.in b/tests/issue129.in new file mode 100644 index 00000000..056dfbaf --- /dev/null +++ b/tests/issue129.in @@ -0,0 +1,3 @@ +open tex issue129.tex +show proof th1 /tex +close tex \ No newline at end of file diff --git a/tests/issue129.mm b/tests/issue129.mm new file mode 100644 index 00000000..5ef3b6d4 --- /dev/null +++ b/tests/issue129.mm @@ -0,0 +1,9 @@ +$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 }"; +$) From 40bdc509989d90423c231741042eba98f47fdb94 Mon Sep 17 00:00:00 2001 From: Gino Giotto Date: Thu, 2 Nov 2023 20:49:04 +0100 Subject: [PATCH 05/11] updated test case --- tests/.gitignore | 1 + tests/issue129.expected | 31 +++++++++++++++++++++++++++++++ tests/issue129.in | 6 +++++- 3 files changed, 37 insertions(+), 1 deletion(-) diff --git a/tests/.gitignore b/tests/.gitignore index 43f7c2e6..74bcd279 100644 --- a/tests/.gitignore +++ b/tests/.gitignore @@ -1,2 +1,3 @@ +issue129.tex issue134.tex underscores.html \ No newline at end of file diff --git a/tests/issue129.expected b/tests/issue129.expected index 63b94a52..1e109f83 100644 --- a/tests/issue129.expected +++ b/tests/issue129.expected @@ -11,3 +11,34 @@ Reading definitions from $t statement of issue129.mm... MM> Outputting proof of "th1"... The LaTeX source was written to "issue129.tex". MM> The LaTeX output file "issue129.tex" has been closed. +MM> Entering the Text Tools utilities. Type HELP for help, EXIT to exit. +TOOLS> The input had 28 lines, the output has 27 lines. First output line: +\documentclass{article} +TOOLS> Exiting the Text Tools. Type EXIT again to exit Metamath. +MM> \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} diff --git a/tests/issue129.in b/tests/issue129.in index 056dfbaf..01769ea7 100644 --- a/tests/issue129.in +++ b/tests/issue129.in @@ -1,3 +1,7 @@ open tex issue129.tex show proof th1 /tex -close tex \ No newline at end of file +close tex +tools +match issue129.tex "% This LaTeX file was created by Metamath on " N +exit +more issue129.tex From 0f7bcef927dc2a2f71acc9f420e8d3ff264f3419 Mon Sep 17 00:00:00 2001 From: Gino Giotto Date: Thu, 2 Nov 2023 21:40:17 +0100 Subject: [PATCH 06/11] maybe fix --- tests/issue129.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/issue129.in b/tests/issue129.in index 01769ea7..6078bc29 100644 --- a/tests/issue129.in +++ b/tests/issue129.in @@ -4,4 +4,4 @@ close tex tools match issue129.tex "% This LaTeX file was created by Metamath on " N exit -more issue129.tex +"cat issue129.tex" From 93a80c7bfc7c68fc654b797a1a58e453c44bf0e2 Mon Sep 17 00:00:00 2001 From: Gino Giotto Date: Fri, 3 Nov 2023 21:13:58 +0100 Subject: [PATCH 07/11] edited run_test.sh --- tests/run_test.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/run_test.sh b/tests/run_test.sh index 052782f1..0bce10eb 100755 --- a/tests/run_test.sh +++ b/tests/run_test.sh @@ -130,7 +130,7 @@ for test in "$@"; do echo "$test.expected missing, $test.produced:" fi echo -n "---------------------------------------\n${green}" - cat "$test.produced" + printf '%s' "$test.produced" echo "${off}---------------------------------------\n" # call diff and put the diff output in $diff_result elif diff_result=$(diff "$test.expected" "$outfile" --color=always); then From 86d98e26bf1e59d01ac327f0eb776967807e05ab Mon Sep 17 00:00:00 2001 From: Gino Giotto Date: Fri, 3 Nov 2023 21:25:53 +0100 Subject: [PATCH 08/11] attempting again --- tests/run_test.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/run_test.sh b/tests/run_test.sh index 0bce10eb..aa413ad3 100755 --- a/tests/run_test.sh +++ b/tests/run_test.sh @@ -97,7 +97,7 @@ for test in "$@"; do echo "${red}failed${off} (exit code = $result_code)"; exit_code=1 if [ "$outfile" != "/dev/null" ]; then echo "---------------------------------------" - cat "$test.produced" + printf '%s' "$test.produced" echo "---------------------------------------\n" fi continue From 5abdc38539174d9b4969523cf9601bc948c0d1b2 Mon Sep 17 00:00:00 2001 From: Gino Giotto Date: Fri, 3 Nov 2023 21:36:48 +0100 Subject: [PATCH 09/11] how about this --- tests/issue129.expected | 52 ++++++++++++++++++++--------------------- 1 file changed, 26 insertions(+), 26 deletions(-) diff --git a/tests/issue129.expected b/tests/issue129.expected index 1e109f83..a48bd55e 100644 --- a/tests/issue129.expected +++ b/tests/issue129.expected @@ -13,32 +13,32 @@ The LaTeX source was written to "issue129.tex". MM> The LaTeX output file "issue129.tex" has been closed. MM> Entering the Text Tools utilities. Type HELP for help, EXIT to exit. TOOLS> The input had 28 lines, the output has 27 lines. First output line: -\documentclass{article} +\\documentclass{article} TOOLS> Exiting the Text Tools. Type EXIT again to exit Metamath. -MM> \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} +MM> \\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} +\\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} +\\end{document} From c6b8b970e21434473842cba3ad998f3578a0beb5 Mon Sep 17 00:00:00 2001 From: Gino Giotto Date: Fri, 3 Nov 2023 21:45:48 +0100 Subject: [PATCH 10/11] doesn't work, restore original run_test.sh and issue129.expected --- tests/issue129.expected | 52 ++++++++++++++++++++--------------------- tests/run_test.sh | 4 ++-- 2 files changed, 28 insertions(+), 28 deletions(-) diff --git a/tests/issue129.expected b/tests/issue129.expected index a48bd55e..1e109f83 100644 --- a/tests/issue129.expected +++ b/tests/issue129.expected @@ -13,32 +13,32 @@ The LaTeX source was written to "issue129.tex". MM> The LaTeX output file "issue129.tex" has been closed. MM> Entering the Text Tools utilities. Type HELP for help, EXIT to exit. TOOLS> The input had 28 lines, the output has 27 lines. First output line: -\\documentclass{article} +\documentclass{article} TOOLS> Exiting the Text Tools. Type EXIT again to exit Metamath. -MM> \\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} +MM> \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} +\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} +\end{document} diff --git a/tests/run_test.sh b/tests/run_test.sh index aa413ad3..052782f1 100755 --- a/tests/run_test.sh +++ b/tests/run_test.sh @@ -97,7 +97,7 @@ for test in "$@"; do echo "${red}failed${off} (exit code = $result_code)"; exit_code=1 if [ "$outfile" != "/dev/null" ]; then echo "---------------------------------------" - printf '%s' "$test.produced" + cat "$test.produced" echo "---------------------------------------\n" fi continue @@ -130,7 +130,7 @@ for test in "$@"; do echo "$test.expected missing, $test.produced:" fi echo -n "---------------------------------------\n${green}" - printf '%s' "$test.produced" + cat "$test.produced" echo "${off}---------------------------------------\n" # call diff and put the diff output in $diff_result elif diff_result=$(diff "$test.expected" "$outfile" --color=always); then From 74986e8cf25c1339fe980d449f889eb799003b8b Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Fri, 3 Nov 2023 20:25:52 -0400 Subject: [PATCH 11/11] fix test --- tests/run_test.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/run_test.sh b/tests/run_test.sh index 052782f1..d9e6afe3 100755 --- a/tests/run_test.sh +++ b/tests/run_test.sh @@ -110,7 +110,7 @@ for test in "$@"; do # a new version comes out. # The last line is always 'MM> EXIT' which is not relevant. # The sed is to redact timings, which are nondeterministic - echo "$result" | head -n -1 | tail -n +2 \ + printf "%s" "$result" | head -n -1 | tail -n +2 \ | sed -e 's/ \+[0-9]\+\.[0-9]\+ s/ x.xx s/g' \ > "$outfile"