Fix comment syntax in set.mm

[jkingdon]

The problem is that tests are now failing on develop/branches (UPDATE: intermittently, see CACHING NOTE below) because of the new checks in metamath/metamath-knife#127

The diff here fixes two small problems but most of the errors from metamath-knife seem to be from a metamath-knife bug/misfeature/problem as described in more detail at metamath/metamath-knife#128

Because this is blocking all set.mm changes (where "all" is to be interpreted in light of CACHING NOTE below), our choices for the moment would seem to be:

1. roll back the metamath-knife changes, at least the part which gives an error on single underscores
2. roll forward the metamath-knife code, that is find a solution for doubling underscores in URLs metamath-knife#128
3. stop running the metamath-knife checks for set.mm (seems like not a good option to me, but I list it for completeness)

I'd generally pick option 1 based on the general https://outage.party reasoning. But perhaps @tirix and @digama0 have more insight into this change.

CACHING NOTE: some test runs are getting the old metamath-knife, some the new one, see #3522 for more on that.

[tirix]

Wouldn't the better solution be to use "math mode" here?
I.e. put the formula within back tick escapes, and space out each symbol.

[jkingdon]

Maybe we should ask @avekens . There isn't a math symbol called :<-> and to be honest I'm not completely sure how well the concepts here map to set.mm notions of ordered pair, no-greater-than of extended reals, etc.

[tirix]

I guess this means "defined as", just like ":=" also sometimes means "defined as".
But yes, the best is to ask @avekens .

[avekens]

This should have been a semiformal definition of a lexicographical ordering. Maybe this "formula" can be replaced by <. a , b >. <_ <. x , y >. iff ( a < x \/ ( a = x /\ b <_ y ) ).

[jkingdon]

I've put that change into #3527

[tirix]

Thanks for all the actions (and sorry for the mess). Another action to avoid this in the future is to include a run of metamath-knife on the latest set.mm in its CI.
The changes have passed metamath-knife's CI, but it was run with an outdated version of set.mm.

[tirix]

The changes have passed metamath-knife's CI, but it was run with an outdated version of set.mm.

Actually, besides only running on set.mm's "master" branch, it seems that in its CI, metamath-knife does not run the "verify markup" and "verify typesetting" options.

[tirix]

Looking at the errors generated by metamath-knife, we have several different categories of issues:

• "unescaped" underscores in URL : see issue doubling underscores in URLs metamath-knife#128. This should be fixed by don't unescape _ in labels/URLs and in HTML mode metamath-knife#130.
• "unescaped" underscores in HTML : see issue Doubling underscores in HTML mode metamath-knife#131. This should be fixed by Underscores in comment's Html metamath-knife#129.
• "unescaped" underscores in math-like strings. Those should probably be corrected in set.mm
• "unescaped" underscores in file names. Those should probably be corrected in set.mm

[digama0]

metamath/metamath-knife#130 now also includes HTML mode fixes. Otherwise I think the summary is correct. I do think we should not silence the warning on undoubled _ in regular text, because this is a common cause of accidental subscripting so catching the issue whenever possible sounds like a good idea.

[jkingdon]

The changes have passed metamath-knife's CI, but it was run with an outdated version of set.mm.

Actually, besides only running on set.mm's "master" branch, it seems that in its CI, metamath-knife does not run the "verify markup" and "verify typesetting" options.

Ah, I suspected there must be something like that, since I don't think all of the markup in question in set.mm is recently added.

[tirix]

I've added some changes to fix underscores in the two last categories:

• "unescaped" underscores in math-like strings: I've mostly escaped the math string so that it is parsed in math mode. In some cases where metamath-exe also does not seem able to handle the subscript mode, like where there is no superscript to subscript to, as in <. A , B >. _1, I've doubled (= escaped) the underscores.
• "unescaped" underscores in file names: I've doubled (= escaped) the underscores.

After this change, there are still two cases not handled by the last metamath-knife version:

• the italics of the comments of constmap, which end in a dot . just before the end of the italics, whereas the "end of italics" test in metamath checks for alphanumeric characters only. The change most likely also has to be done in set.mm, but I was unsure.
• the italics of the comments of df-tsk, which starts with an ampersand & for the HTML codepoint for "Ü", Ü. It also has a dot immediately after the underscore marking the end of the italics mode, but that should not be an issue.

I believe these two cases are issues with metamath-knife, @digama0 .

Note that some of these changes affect mathboxes (at least @mazsa and @avekens)

[jkingdon]

This all looks good. I approve the changes by @tirix and I think we can merge this now.

If there is something remaining to be done (in set.mm, as opposed to metamath-knife), or we want to fix some of these in a different way, we can always make a follow up pull request.

[digama0]

@tirix metamath-knife is only following metamath-exe here. As the linked HTML pages should show, metamath-exe does not recognize either of these and uses underscores instead of italics, so metamath-knife is right to complain that it won't work.

[digama0]

+ ` <. A , B >. ` __2 ` = { { { A } , (/) } , { { B } } } ` , justified by
- ` <. A , B >. `_2 ` = { { { A } , (/) } , { { B } } } ` , justified by

It is possible to use subscript here, but you can't put a space after the quote.

[jkingdon]

+ ` <. A , B >. ` __2 ` = { { { A } , (/) } , { { B } } } ` , justified by
- ` <. A , B >. `_2 ` = { { { A } , (/) } , { { B } } } ` , justified by

It is possible to use subscript here, but you can't put a space after the quote.

Ah, nice. I didn't even realize that was the intention here, but it all makes sense now.

Fixed in #3527

[jkingdon]

@tirix metamath-knife is only following metamath-exe here. As the linked HTML pages should show, metamath-exe does not recognize either of these and uses underscores instead of italics, so metamath-knife is right to complain that it won't work.

Makes sense. I've adjusted the set.mm comment for both in #3527

[jkingdon]

The changes have passed metamath-knife's CI, but it was run with an outdated version of set.mm.

Actually, besides only running on set.mm's "master" branch, it seems that in its CI, metamath-knife does not run the "verify markup" and "verify typesetting" options.

See metamath/metamath-knife#135 regarding changing this.