VERIFY MARKUP is being run on iset.mm and set.mm and is passing.
Go to the latest entry in the Actions tab (
https://github.com/metamath/set.mm/runs/5038215989?check_suite_focus=true
), follow the link from the duplication check (takes you to
https://github.com/metamath/set.mm/runs/5032713820?check_suite_focus=true
) and open the "Run scripts/verify --top_date_skip --extra 'write
bibliography mmbiblio.html' set.mm" entry to see:
MM> !VERIFY MARKUP * / TOP_DATE_SKIP
Checking statement label conventions...
Checking latexdef, htmldef, althtmldef...
Checking statement comments...
Checking section header comments...
> Looks like it's been like this since december:
https://github.com/metamath/set.mm/commit/b6d91985163285cb27ecfcc46c31e4e4791dc2ab
.
That just affects nf.mm and the other ones other than set.mm and iset.mm.
On 2/3/22 00:16, Mario Carneiro wrote:
This actually made me curious because this should have been caught by
the existing VERIFY MARKUP check already, yet
http://us.metamath.org/mpeuni/elv.html has already made it to the
develop branch and the web site. It looks like VERIFY MARKUP has been
disabled in CI? @David what's going on here? Looks like it's been like
this since december:
https://github.com/metamath/set.mm/commit/b6d91985163285cb27ecfcc46c31e4e4791dc2ab
.
Mario
On Thu, Feb 3, 2022 at 3:07 AM Mario Carneiro <[email protected]> wrote:
On Thu, Feb 3, 2022 at 2:45 AM Mázsa Péter <[email protected]> wrote:
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)
I see this in set.mm <http://set.mm>:
${
elv.1 $e |- ( x e. _V -> ph ) $.
$( New way ( ~ elv , ~ el2v theorems and ~ el3v theorems) to
shorten some
proofs. Inference forms (with ` $e |- A e. _V $. ` ) of
the general
theorems (with ` $p |- ( A e. V -> ` ) may be superfluous.
(Contributed
by Peter Mazsa, 13-Oct-2018.) $)
elv $p |- ph $=
( cv cvv wcel vex ax-mp ) BDEFABGCH $.
$}
I didn't find this in my local copy, I guess it's a new addition.
If I had it would have shown up in my markup check because $e and
$p are not tokens.
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 <http://us2.metamat.org> yet?)
I would not recommend using stars after or within labels, at least
if you use ~ to auto-link them. What do you expect to happen? It's
an HTML link, it can't link to a whole collection of things even
if it could determine what collection you are talking about.
Alternatives include linking to all of them, linking to one or two
"representative" examples with some text to indicate that there is
more, or just using the glob notation and linking nothing.
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?
What *do* you want? You can just leave off the ticks and they will
be printed in regular text, or you can use quotes (and they will
still be printed in regular text), or you can use
<HTML><PRE></PRE></HTML> to render them in monospace font.
3. Reference to the ` $e |- A e. _V $. ` stings in set.mm
<http://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 <http://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).
Mario
--
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/CAFXXJSvrO%2BB15uKq2O6cCNJg_1x3YpkCkLynf4vrvyM5fYLRNQ%40mail.gmail.com
<https://groups.google.com/d/msgid/metamath/CAFXXJSvrO%2BB15uKq2O6cCNJg_1x3YpkCkLynf4vrvyM5fYLRNQ%40mail.gmail.com?utm_medium=email&utm_source=footer>.
--
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/e5fd7da3-3780-9c84-018a-6fafa3787441%40panix.com.
