Fixing some LaTeX definitions

[benjub]

This is an update on #3037. Some LaTeX definitions should be fixed in all the databases in this repository with LaTeX definitions. These are: set.mm, iset.mm, hol.mm, ql.mm, nf.mm.

The commands on the LHS below are deprecated, and here are some proposed replacements:

1. [x] {\rm xxx} --> \mathrm{xxx} (see #3054 for the only remaining cases)
2. [x] {\cal xxx} --> \mathcal{xxx}
3. [x] {\sf xxx} --> \mathsf{xxx}
4. [x] {\Bbb xxx} --> \mathbb{xxx}
5. [x] {\bb xxx} --> \mathrm{xxx}
6. [x] \tt --> depends; often \mathtt{...}
7. [x] \it, \bf, \sc, \sl: check that they do not occur in any of the databases (if they do, there is \mathsc{...}, etc.)
8. [x] \atop --> depends: \frac \genfrac \overset \stackrel...

(note that the expressions on the LHS above are not always surrounded by braces).

9. [ ] many \mathrm{...} should actually be \operatorname{...}
10. [x] \mbox{...} should generally be \text{...}

See @GinoGiotto's comment https://github.com/metamath/set.mm/issues/3067#issuecomment-1450875967 for an advancement step.

[GinoGiotto]

I believe most of these checks can be solved if the following few latexdefs are fixed:

 latexdef "-1-1->" as
    "\raisebox{.5ex}{${\textstyle{\:}_{\mbox{\footnotesize\rm 1" +
    "\tt -\rm 1}}}\atop{\textstyle{" +
    "\longrightarrow}\atop{\textstyle{}^{\mbox{\footnotesize\rm {\ }}}}}$}";

latexdef "-onto->" as
    "\raisebox{.5ex}{${\textstyle{\:}_{\mbox{\footnotesize\mathrm{\:}}}}" +
    "\atop{\textstyle{" +
    "\longrightarrow}\atop{\textstyle{}^" +
    "{\mbox{\footnotesize\mathrm{onto}}}}}$}";

latexdef "-1-1-onto->" as
    "\raisebox{.5ex}{${\textstyle{\:}_{\mbox{\footnotesize\mathrm{1}" +
    "\tt -\mathrm{1}}}}\atop{\textstyle{" +
    "\longrightarrow}\atop{\textstyle{}^" +
    "{\mbox{\footnotesize\mathrm{onto}}}}}$}";

 latexdef "-cn->" as
    "\raisebox{.5ex}{${\textstyle{\:}_{\mbox{\footnotesize\mathrm{cn}" +
    "}}}\atop{\textstyle{" +
    "\longrightarrow}\atop{\textstyle{}^{\mbox{\footnotesize\mathrm{\:}}}}}$}";

I'm not confident enough to provide a solution for these, I might integrate them in my pull request if someone knows how to fix them.

[benjub]

I can think of several solutions, but best in my opinion is #3054. Since there is not much discussion, I'll implement it soon..ish.

[avekens]

Should the following LaTeX definitions also be changed?

• latexdef "..^" as " \,..\hat{}\, ";
• latexdef "gcd" as "\,{\rm gcd}\,";
• latexdef "lcm" as "\,{\rm lcm}\,";
• latexdef "pCnt" as "\,{\rm pCnt}\,";
• latexdef "_d" as "\,{\rm d}";,

See discussion in #3066, @benjub`s comment:

For instance, \,{\rm gcd}\, is an example of what not to do. Since gcd is used in set.mm as a binary operation, it should be \mathbin{\operatorname{gcd}}.

What about other (binary) operation names? For example, is the following LaTeX definition acceptable?

• latexdef "eval" as " {\rm eval} ";

[benjub]

We should use the commands provided by LaTeX /AMSTeX for these cases (for spacing reasons, and for clarity too):

• (prefix) operators: \operatorname{mycosine}
• (infix) binary operators: \mathbin{\operatorname{mod}} (if a symbol is used, there is no need to change the font shape, so things like \mathbin{\hat{+}} should suffice).
• (infix) binary relations: \mathrel{\operatorname{parallel}}

There are other commands too: for opening and closing symbols, you have \mathopen, \mathclose. Some symbols are recognized by LaTeX to be of the correct "type", e.g., (, +, = are recognized respectively as being an opening symbol, a binary operator, a binary relation, so they do not need the above commands. So I don't have a complete answer, but the above should already deal with many cases.

A problem is that work is duplicated with (i)set.mm. Since the latex output functionality seems to be not much used, I'm not sure what priority this work should be given.

[david-a-wheeler]

@avekens Should the following LaTeX definitions also be changed? ...

• latexdef "gcd" as "\,{\rm gcd}\,";

No! First of all, we're trying eliminate all uses of \rm ... because that is deprecated in TeX. Use \mathrm{...} instead. The \mathrm{...} only works in TeX "math mode", but all formula expressions should be in math mode already. (There are a very few LaTeX definitions that presume you're not in math mode, leading to TeX failures. We're fixing those right now.)

Second of all, I encourage people to not use embedded spaces in TeX. Use, e.g., \: if you must. Metamath-exe breaks spaces oddly in TeX, and while we do need to fix that, having no spaces in generated formulas eliminates oddities until we do and ensures people will get the "whole expression" on copy/paste.

[GinoGiotto]

• latexdef "gcd" as "\,{\rm gcd}\,";
• latexdef "lcm" as "\,{\rm lcm}\,";
• latexdef "pCnt" as "\,{\rm pCnt}\,";
• latexdef "_d" as "\,{\rm d}";,

These ones are already in \mathrm form.

I believe that after https://github.com/metamath/set.mm/pull/3071#issue-1600936896 will be merged, there won't be any occurrence of \rm left in any database except for these three: latexdef "-1-1->" latexdef "-onto->" latexdef "-1-1-onto->".

I'll write a more detailed report after merge, if there are mistakes or inaccuracies in https://github.com/metamath/set.mm/pull/3071#issue-1600936896, please report them there and I will commit those changes.

[GinoGiotto]

As promised in https://github.com/metamath/set.mm/pull/3071#issue-1600936896 here is a more specific report of what I think is done and what I think is left:

1. I wasn't able to find any occurrence of \rm left in any database.

2. I wasn't able to find any occurrence of \cal left in any database.

3. I wasn't able to find any occurrence of \sf left in any database.

4. I wasn't able to find any occurrence of \Bbb left in any database.

5. I wasn't able to find any occurrence of \bb left in any database.

6. I wasn't able to find any occurrence of \tt left in any database.

7. I wasn't able to find any occurrence of \it \bf \sc \sl left in any database.

8. I wasn't able to find any occurrence of \atop left in any database.

9. I checked a few of them, but there is still a lot to do. I'm not planning to check them again in the future.

10. I wasn't able to find any occurrence of \mbox left in any database.

So basically I think that all checks except 9 are done.

[benjub]

Thanks @GinoGiotto. I updated the description and checked some boxes. Thanks for the list of exceptions in 8. I see several ways to deal with them, similar to #3054 and with e.g. \overset{\mathrm{cn}}{\longrightarrow}:

$f \colon A \overset{\mathrm{cn}}{\longrightarrow} B$

[GinoGiotto]

Thanks @GinoGiotto. I updated the description and checked some boxes. Thanks for the list of exceptions in 8. I see several ways to deal with them, similar to #3054 and with e.g. \overset{\mathrm{cn}}{\longrightarrow}:

I like this solution, it is a quick fix that would work to solve the remaining deprecated TeX and the errors generated by those substitutions. I could implement this soon, and then they could be replaced with https://github.com/metamath/set.mm/issues/3054 if it's desired. The reason I'm proposing this path is because the solution in https://github.com/metamath/set.mm/issues/3054 seems a bit long since the intention there is to replace the tokens too, so with this temporary fix I would at least quickly eliminate them from my list of malfunctioning latexdefs.

[GinoGiotto]

I updated https://github.com/metamath/set.mm/issues/3067#issuecomment-1450875967 since https://github.com/metamath/set.mm/pull/3075 is now merged. You can still consult the original report in the edit history of the comment.

[GinoGiotto]

@benjub Isn't check 8 completed? I cannot edit someone else's comment.

[benjub]

@benjub Isn't check 8 completed? I cannot edit someone else's comment.

what about 9 ?

[GinoGiotto]

what about 9 ?

As I said in https://github.com/metamath/set.mm/pull/3099#issue-1627987886 I made some progress towards it, but I only checked a few occurrences, I'm not planning to check them all in the future.