It took me longer than I wanted to find the specification we wrote for
the definition checker. It is in
https://us.metamath.org/mpeuni/conventions.html towards the bottom
(search for "additional rules for definitions"). As Mario said in this
email thread it is not (at least currently) based on $j commands; it
knows about various details of set.mm.
In an effort to make it a bit easier to deal with this definition
checker specification I submitted
https://github.com/metamath/set.mm/pull/2929 which adds a section header
to the conventions page and also updates some of the text on
https://us.metamath.org/mpeuni/mmset.html to link to the conventions
page and clean up a few issues.
On 11/13/22 16:17, Mario Carneiro wrote:
No, there are more rules than just that. I'm sure I've posted about
this on the group before but the best link I can find at the moment is
https://groups.google.com/g/metamath/c/HdfvWF2WhBE/m/bqL0Q7E_BQAJ .
The "definition" $j command is rarely used; it is only there to help
parse a definitional axiom as preparation for running the actual
definition check. Most of the time, the structure of the definition is
manifest, because it is an equality of some kind (like `<->`) with the
defined symbol on the left and the body of the definition on the
right. Once these parts are identified, it is possible to check the
definition rules; in your example the "definition" ~ancom would be
rejected because the defined symbol `/\` occurs in the definition body.
On Sun, Nov 13, 2022 at 5:54 PM Zheng Fan <[email protected]>
wrote:
In the document on the $j comments, it says that "The definition
should have a top level equality declared by the
<code>equality</code> command with the definition on the right
hand side," except for df-bi. Is this condition sufficient for a
definition? For example, we have the theorem
ancom $p |- ( ( ph /\ ps ) <-> ( ps /\ ph ) ) $= ... $.
It also has a top level equality (<->) for wff, but it is not a
definition for /\.
在2022年11月13日星期日 UTC+1 02:44:32<[email protected]> 写道：
On Sat, Nov 12, 2022 at 7:10 PM Zheng Fan
<[email protected]> wrote:
I haven't paid a lot of attention to the $j comments. I
was under the impression from the official specs that
comments are mostly ignored. Anyway, is there any specs
about the meaning of the $j comments? And which part of
the program (if any) is responsible for parsing the $j
comments? And what does unambiguous 'klr 5' mean?
It's not yet up on the website (cc: David), but
https://github.com/metamath/set.mm/blob/develop/j-commands.html
has some documentation on the meaning of all the $j commands.
The purpose of the commands is to make the various
"conventions" around metamath database naming and
interpretation of axioms more formalized and
machine-checkable, so it is particularly of interest to
metamath-knife. The $j commands are ignored by metamath
verifiers, but it still has relevant information for tools
that want to do more than simply verify the database; in
particular it is relevant for parsing the statements and
identifying definitions (as distinct from axioms) and
verifying conservativity.
In metamath-knife, the case that handles parsing $t and $j
commands is:
https://github.com/david-a-wheeler/metamath-knife/blob/614c3527fe79206e12eaa633d4c7561736cbb9fd/src/parser.rs#L747-L758
which defers to CommandIter which does the low level parsing.
(Parsing $t and $j commands is a bit more difficult than the
rest of it since it has more C-like lexing rules, which allow
you to omit spaces before `;` and such.) The parsing of $t
comments is also described in the Metamath book, and $j
commands use the same parser.
.
After parsing the broad structure of the $j command, the
result is stashed in Segment.j_commands, and further
interpretation is done on the fly as required by individual
analysis passes. The most important $j command which is read
by almost every parser that makes an attempt to read $j
commands at all is "syntax"; this tells you the information
that you were asking about - that theorems start with "|-" and
"wff" is the typecode for formulas. It is parsed by the
Grammar module at:
https://github.com/david-a-wheeler/metamath-knife/blob/071292ef3a10350d0dae9e409b4921f91a08ce95/src/grammar.rs#L417-L433
The "unambiguous" command is used to signal that grammatical
parsing is possible at all. The 'klr 5' indicates more
specifically that a KLR parser table can be built, which is
one way to verify that the grammar is in fact unambiguous, but
for most purposes it suffices just to know the mere fact of
unambiguity (which is in general undecidable), and even then
most tools that attempt grammatical parsing ignore the
directive and simply fail or produce odd results on ambiguous
grammars. Metamath-knife ignores this command.
Mario
在2022年11月12日星期六 UTC+1 21:05:54<[email protected]> 写道：
On Sat, Nov 12, 2022 at 1:44 PM Zheng Fan
<[email protected]> wrote:
if I want to add some new functions, is it better
to add it to the relevant file or create a new file?
That depends on the function. Usually a function would
go in the file which defines the type on which the
function is exposed, unless it is really big in which
case you might consider separate files. Rust source
files tend to be fairly large, they are only broken up
by topic and there aren't any strict file limits.
Also, do we assume the syntax of set.mm
<http://set.mm> in the source code, e.g., wff
precedes a formula, |- precedes a theorem,
These "conventions" are encoded in $j comments, so I
would prefer to make use of that information when
possible rather than hard coding them in the tool.
and the label of a definition begins with "df-"?
This one is only used in linter-like behavior, but I
believe it is hard-coded. A lot of "verify markup"'s
behavior is hard coded to maintenance of set.mm
<http://set.mm> specifically.
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/1cbae7e9-53bf-4c83-9e23-e2bb31c965dfn%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/1cbae7e9-53bf-4c83-9e23-e2bb31c965dfn%40googlegroups.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/c2cd90b8-fb09-40fb-8e5a-4ffbb3e1d042n%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/c2cd90b8-fb09-40fb-8e5a-4ffbb3e1d042n%40googlegroups.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/CAFXXJSvQmzWbc26LzcMy0-ahtfTgHJJYFCwb9BUgEAk7rHGDWA%40mail.gmail.com
<https://groups.google.com/d/msgid/metamath/CAFXXJSvQmzWbc26LzcMy0-ahtfTgHJJYFCwb9BUgEAk7rHGDWA%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/fd6c8bca-6d88-9cbe-c2e3-cff40c8d5b19%40panix.com.
