Hi Mario,
I have 3 questions: 1. You see ( ~ elv , ~ el2v and ~ el3v theorems) here: http://us2.metamath.org/mpeuni/elv.html In /develop, you find ( ~ elv , ~ el2v* and ~ el3v* theorems) Is it possible to refer to a set of theorems with one string? I mean, you understand that ~ el3v* means all theorems beginning with el3v (i.e. ~ el3v ~ el3v1 ~ el3v2 ~ el3v3 ~ el3v12 ~ el3v13 and ~ el3v23 ), but can you express this in a way that shows ( ~ elv , ~ el2v* and ~ el3v* theorems) here http://us2.metamath.org/mpeuni/elv.html as well? Or should I write this: ( ~ elv , and the theorems beginning with ` el2v ` or ` el3v ` ) ? (Or is it solved already just didn't show up at us2.metamat.org yet?) 2. You see Inference forms (with ) of the general theorems (with ) may be superfluous. here: http://us2.metamath.org/mpeuni/elv.html In /develop, you find Inference forms (with ` $e |- A e. _V $. ` ) of the general theorems (with ` $p |- ( A e. V -> ` ) may be superfluous. How should I express what I want? 3. Reference to the ` $e |- A e. _V $. ` stings in set.mm (cf. above) are verified by the verify markup feature. Sometimes, in the notes parts of other theorems, I want to refer to longer strings in set.mm , but verify markup doesn't allow it. Is it a way to do it? Thank you: Peter On 2/3/22, Mario Carneiro <[email protected]> wrote: > ... I suppose it's apropos that a post about bugs in text->html > autoformatting would itself have buggy formatting. Please ignore the > non-ascii list item formatting. > > On Wed, Feb 2, 2022 at 9:39 PM Mario Carneiro <[email protected]> wrote: > >> 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/CAFXXJStewJedDRcyp_GnCH2NO4zSX4A__eKMF620a%3DvdAA56kg%40mail.gmail.com. > -- 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/CAJJTU5qUjD8t-pckgoypciyi2UZVZb0aqncS9XS7mDqTUrqEXw%40mail.gmail.com.
