On Thu, Feb 3, 2022 at 5:28 AM Mázsa Péter <[email protected]> wrote:
> >> 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? > >> > > > > I don't understand the question. Math strings allow you to render > metamath > > token strings the same way as they would appear normally in proofs. They > > don't do any cross referencing. Label references can be used for cross > > referencing, and they only link to theorems, not subsections or other > > things like that, although you can use <HTML> to write arbitrary markup > if > > you really want (although I think this was a bad idea and I would like to > > decrease use of <HTML> in favor of more structured markup). > > The function of it is cross referencing by searchability. If you are > able to put searchable strings into the notes of theorems, they may be > not cross-references in html-way, but they are cross-references in a > way that you can search them in set.mm locally. > 2 examples: > >> Inference forms (with ` $e |- A e. _V $. ` ) of the general theorems > >> (with ` $p |- ( A e. V -> ` ) may be superfluous. > You search for $e |- A e. _V $. locally and you see that these el*v* > theorems refer to 395 theorems in set.mm containing $e |- A e. _V $. . > Actually, I usually use searches for $e and $p when I want to *not* get any comment hits. For example searching for " label $p" is a very reliable way to jump to the definition of "label" via text search. For the purpose of this particular comment I think it suffices to just have ` |- A e. _V ` in the description. > Or: > $( Two ways of saying that two classes are disjoint (when ` C = (/) ` : > ` ( ( A i^i B ) = (/) <-> ( B i^i A ) = (/) ) ` ). (Contributed by > Peter > Mazsa, 22-Mar-2017.) $) > ineqcom $p |- ( ( A i^i B ) = C <-> ( B i^i A ) = C ) $= > ( cin incom eqeq1i ) ABDBADCABEF $. > means that when you search for ( A i^i B ) = (/) in set.mm you will > find the more general ineqcom (rendered perfectly az > http://us.metamath.org/mpeuni/ineqcom.html ). The problem is that if > you put too much characters between ` and ` , the /rewrap feature is > not able to rewrapping it: how should I quote longer strings? And: if > you write e.g. ` u ( `' _E |` A ) x ` in the notes of a theorem, it is > not allowed by verify markup, because the second ` is interpreded as > the closing ` instead of the third one. > As mentioned, the fix is to split the math string by closing it on the first line and reopening it on the second line. The renderer will combine the strings. On Thu, Feb 3, 2022 at 10:48 AM Jim Kingdon <[email protected]> wrote: > VERIFY MARKUP is being run on iset.mm and set.mm and is passing. > On further investigation, it seems like VERIFY MARKUP has a bug that is preventing this error from being caught: the following test file $c wff $. $v ph $. wph $f wff ph $. $( ` foo ` $) a $p wff ph $= wph $. $( $t $) gives the error ?Warning: In the comment for statement "a", math symbol token "foo" does not have a LaTeX and/or an HTML definition. but replacing "foo" with "$e" yields no such error. In fact, this should probably be a separate error, since tokens can never contain $, although you will get the runaround if you try to quell this error: putting the htmldef "$e" as "..."; will silence this error but produce another error saying $e isn't a declared token, and $c $e $. is a syntax error. On Thu, Feb 3, 2022 at 12:53 PM 'Alexander van der Vekens' via Metamath < [email protected]> wrote: > And here my remarks on Mario's rules/checks: > > - * 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. > > There ARE real URLs which contain ~. In such URLs, ~~ must be used, see > mmset.raw.html "http://www.math.miami.edu/~~ec/book";. What exactly > happens if this is written as "http://www.math.miami.edu/~ec/book";? > It works, but metamath complains at you. > > - * 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. > > As far as I can remember there are strict rules for bibliographic > references (no whitespaces, etc.) , and all other cases are interpreted > literally. We should stick with this and should not enforce the usage of [[ > in these cases. > I'm inclined towards this as well. The rule is fairly simple: [<no whitespaces>] is a bib tag, anything else is not. > > - * In bibliography references, there are no escapes but ~ and ` break > metamath.exe, so there are no violators. > > I do not really understand this case. Could you give an example? > The question is what happens if you have a bib tag like [foo~bar`baz]. As I said, the rule is quite simple - no whitespace - and this permits a whole lot of escape characters, that somehow make their way through the nested regex substitutions that form metamath's markup renderer. In this case, it will complain about "baz]" not being a math token, meaning that it started math mode even though it's in a bib reference. If you close the string it even seems to work correctly: [foo`bar] ` is plaintext "[foo" followed by a math string consisting of the "bar]" token. (I guess I need to update the comment parser again...) If you use [foo``bar], then you get an error saying ?Error: The bibliographic reference "[foo``bar]" in statement "a" was not found as an <A NAME="foo``bar"></A> anchor in the file "mmset.html". which indicates that it treated the foo``bar literally (without unescaping), but if you look at the generated HTML there will be [<A HREF="mmset.html#foo`bar">foo`bar</A>], so it does remove the escapes when actually printing it (so it's not possible to make a tag like this work correctly because it will either fail the VERIFY MARKUP check or it will be a broken link). Similar things apply with the ~ escape character: using [foo~~bar] results in a search for the "foo~~bar" bib tag but the generated HTML uses "foo~bar" instead. If you use the ~ unescaped, you get some extra-strange errors: $( [foo~bar] $) a $p wff ph $= wph $. ?Error: The bibliographic reference "[foo~bar]" in statement "a" was not found as an <A NAME="foo~bar"></A> anchor in the file "mmset.html". ?Warning: There is a "~" inside of a label in the comment of statement "a". Use "~~" to escape "~" in an http reference. ?Warning: The label token "bar">foo" (referenced in comment of statement "a") is not a $a or $p statement label. The first error looks fine, what you would expect for a nonexistent bibref, and indicates that "foo~bar" is the reference. The second error is weird because there is only one ~ in the text, so the part after it, "bar]", doesn't have any ~ in it. The generated HTML is also very broken: [<A HREF="mmset.html#foo<FONT COLOR=blue >bar">foo</FONT> <SPAN CLASS=r STYLE="color:#000000">(future)</SPAN>bar</A>] Notice that the <A> tag does not end before the <FONT> tag starts - that stuff is all inside the string literal. We can see something like an attempt to reference the nonexistent "bar">foo" label in the middle of generating a bibref to "foo~bar". This is why I think they should be banned entirely - metamath.exe does nothing sensible here. > - 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. > > Really funny, but this won't be possible in the future (if the strict > space-separated tilde rule is enforced): it will have to be either "~ > [ab]", then [ab] must be a label, or "~~[ab]", then [ab] must be a > bibliography tag. > No, the space doesn't help. ~ [ab] is still a label and a bibref. The reason is that bibrefs have really high "priority" In the markup parser, as a result of their being handled in the first "regex pass" before looking for other things. (The fact that it is a bunch of passes is why you see various bits of bleeding implementation details like a search for "</TD></TR></TABLE></CENTER>" token.) > > - * ` 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. > > If this can be checked, it should not be allowed in the future. > It's certainly not allowed by the new parser, which is a proper parser. it sees an unclosed math string and warns on that; in HTML generation it auto-closes the string. No leakage. -- 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/CAFXXJStUSBv5Ek5CExDzHH-9japvpx-XwOyaQ4bocjG85sceeQ%40mail.gmail.com.
