No, the definition checker is in mmj2, and has not yet been reimplemented in metamath-knife. https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/definitionCheck.js
On Mon, Nov 14, 2022 at 6:25 AM Zheng Fan <[email protected]> wrote: > Are you referring to metamath-knife? I can't find relevant code dealing > with definitions in the source. > > 在2022年11月14日星期一 UTC+1 01:17:39<[email protected]> 写道： > >> 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 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 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/a43f4e76-aacf-4394-a251-b2303811016an%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/a43f4e76-aacf-4394-a251-b2303811016an%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/CAFXXJSsW1XjC5hwzEQv%2BBsP%2BY5No25q_rYUrAp%2B9hRrcF%2BLbqw%40mail.gmail.com.
