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/CAFXXJSt1uSXzQN7FXotvHnT-orBBm69_XJkhKEiTau-D9d%2BxYQ%40mail.gmail.com.
