Hi All, I've been working on a reimplementation of metamath.exe's VERIFY MARKUP feature for metamath-knife, you can see the highlights at https://github.com/david-a-wheeler/metamath-knife/pull/70 . It's already started catching some bugs that will be PR'd to set.mm once the checker stabilizes, but I wanted to bring specific attention to two rules which have produced hundreds of new errors on set.mm:
- 23. The ~ and ` characters, when used as delimiters in markup, should have whitespace around them - 24. Characters [, ~ and ` must be doubled if they could not be interpreted as special in markup - Some of the violators have been highlighted at https://github.com/david-a-wheeler/metamath-knife/pull/70#issuecomment-1027601499 . - - The question is: Should these rules be kept? * The use of space after ~ was used to make it easier to find labels in comments for find/replace activities, and I think there are only a small handful of violators. - * Space *before* ~ seems to have a lot of violators, so unless we like the look of it I'm okay with relaxing this restriction. - * Space after the initial ` and before the final ` in a math string has no violators at a glance, I think VERIFY MARKUP was already checking this. * Space before the initial ` and after the final ` in a math string has lots of violators for things like (` e. `). Metamath will strip the surrounding spaces if it is a closing punctuation, but there are also examples like "I` /\ `2" in the description of natural deduction rules where the added spaces would be preserved, which is undesirable in this case (we want it to read I∧2). Using unicode html entities would be an alternative way to handle this. - * Non-doubled ~ inside a URL was already being warned against in metamath.exe, although arguably it's fine since it doesn't do anything and is interpreted literally. - * Non-doubled [ has lots of violators in set.mm. There are examples that seem to suggest that people are relying on [ getting printed literally as long as the ] comes after a space. Something like [foo] has to be written as [[foo] because otherwise it would be interpreted as a bibliography tag, but [foo bar] can't be a tag and is interpreted literally; this is the case that triggers the new warning. - * In label/url mode, non-doubled ~ is already warned by metamath.exe and there are no violators, but non-doubled [ interacts weirdly with bibliography tags, and I think rejecting these is the right thing to do (there are no violators). - * In bibliography references, there are no escapes but ~ and ` break metamath.exe, so there are no violators. - Some more fun things: * ~[ab] gets interpreted as *both* a bibliography tag and a label reference, resulting in a broken link to the statement [ and a link to the bibliography tag "ab". Currently mm-knife does the next best thing which is to interpret it as an empty label reference followed by a bibliography tag. - * ` alone in a comment starts math mode and doesn't end it, so you get a warning about "</TD></TR></TABLE></CENTER>" not having an html definition. Naturally, you can therefore add a token called </TD></TR></TABLE></CENTER> and give it htmldefs and it will pass VERIFY MARKUP, and the resulting HTML file will look just a bit off. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJStM9rQj1dYP1v6yVv_qUe9T6C_CX5gZ33fzTYrU8_CwGQ%40mail.gmail.com.
