Buiding on metamath-knife

[Zheng Fan]

These days I am looking at the code of metamth-knife, hoping to do some more data processing based on the existing functions. But as a newbie in rust, I found the code a little bit hard to grasp, mainly because the database is stored in a fancy data structure (to improve performance, as far as I can see), and it is not immediate clear how to process it further. Is there somewhere I can find a detailed description of the data structure being used? Thanks in advance.

[David A. Wheeler]

> On Nov 11, 2022, at 2:38 PM, Zheng Fan <fanzhe...@outlook.com> wrote:
>
> These days I am looking at the code of metamth-knife, hoping to do some more data processing based on the existing functions. But as a newbie in rust, I found the code a little bit hard to grasp, mainly because the database is stored in a fancy data structure (to improve performance, as far as I can see), and it is not immediate clear how to process it further. Is there somewhere I can find a detailed description of the data structure being used? Thanks in advance.

Sadly, no.

Pull requests to fix that would be welcome. I think it might be best to put them in the code itself
(to increase the likelihood that the code would be updated when the data structures are modified).

--- David A. Wheeler

[Mario Carneiro]

What kind of data processing are you interested in? Ideally this should be doable using the public API of the crate so that you don't have to worry about the fancy data structure stuff.

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2CF94F5C-2D99-4793-956B-E54C487D8C81%40dwheeler.com.

[Zheng Fan]

Now I sort of understand the structure of the crate, but I have some more questions: if I want to add some new functions, is it better to add it to the relevant file or create a new file? Also, do we assume the syntax of set.mm in the source code, e.g., wff precedes a formula, |- precedes a theorem, and the label of a definition begins with "df-"?

[Mario Carneiro]

On Sat, Nov 12, 2022 at 1:44 PM Zheng Fan <fanzhe...@outlook.com> 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

[Zheng Fan]

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?

[Mario Carneiro]

On Sat, Nov 12, 2022 at 7:10 PM Zheng Fan <fanzhe...@outlook.com> 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<di....@gmail.com> 写道：

On Sat, Nov 12, 2022 at 1:44 PM Zheng Fan <fanzhe...@outlook.com> 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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/1cbae7e9-53bf-4c83-9e23-e2bb31c965dfn%40googlegroups.com.

[Zheng Fan]

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 /\.

[Mario Carneiro]

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/c2cd90b8-fb09-40fb-8e5a-4ffbb3e1d042n%40googlegroups.com.

[Zheng Fan]

Are you referring to metamath-knife? I can't find relevant code dealing with definitions in the source.

[Mario Carneiro]

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

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/a43f4e76-aacf-4394-a251-b2303811016an%40googlegroups.com.

[Jim Kingdon]

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvQmzWbc26LzcMy0-ahtfTgHJJYFCwb9BUgEAk7rHGDWA%40mail.gmail.com.