Metamath verifier in Zig

256 views
Skip to first unread message

Marnix Klooster

unread,
May 5, 2021, 10:51:53 AM5/5/21
to Metamath
Hello all,

In case anyone is interested, I'm not sure but I don't think I announced this earlier: Since almost a year I've been working on and mostly-off on a Metamath verifier in Zig (https://ziglang.org).  And today I've reached the milestone of supporting the last missing feature (except for allowing '?' in a proof, which is not really important for me yet).

The code is at https://github.com/marnix/zigmmverify; any feedback is welcome.

Groetjes,
 <><
Marnix
--
Marnix Klooster
marnix....@gmail.com

Mario Carneiro

unread,
May 5, 2021, 10:59:27 AM5/5/21
to metamath
Exciting! How is the performance? I would guess that a Zig verifier could compete with the best.

--
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/CAF7V2P_C7QcKP8b_rxvEO6e5uXTMpS6gySU-iVCiqLD1gCW5qQ%40mail.gmail.com.

Marnix Klooster

unread,
May 6, 2021, 4:13:48 PM5/6/21
to Metamath
Hi Mario,

Thanks!  I didn't attempt to optimize for speed or use any parallelism, and on an older 32GB RAM laptop using a recent set.mm I'm seeing ~145,000 lines/second / 8 MB/second, with all of set.mm handled in about 5 seconds using a single core.  (That's with Zig 0.7.1 in release-fast mode.)

My main goal is actually doing stuff (parsing statements, and use that for definition checking and 'modular Metamath'), and it is not about raw performance, so smm3 / Rust is still the best there probably. :-)

That said, I do want to see how parallelism improves things.

As I said, any feedback is welcome.

Groetjes,
 <><
Marnix

Op wo 5 mei 2021 om 16:59 schreef Mario Carneiro <di....@gmail.com>:

Thierry Arnoux

unread,
Jun 7, 2021, 6:53:20 AM6/7/21
to meta...@googlegroups.com

Hello all,

My main goal is actually doing stuff (parsing statements... )
I've also been interested in this, and did a few additions to the Rust-based SMM3 / smetamath-rs / metamath-knife, including recently simple parsing of set.mm formulas. I expect it will be easy to perform e.g. unification in that format.

The code is available at https://github.com/tirix/metamath-knife/tree/grammar, it is a fork from David's metamath-knife (itself a fork of Stefan's repository).

You can launch the statement parser using:

    cargo run -- --timing --print_formula subset.mm

There are two steps, one for building the grammar from the syntactic axioms $a and $f, and another one for parsing the $e and $p statements into what I name "formula".
Finally, the option --print_formula flattens and outputs the formulas back, to give a visual confirmation that the process works.

However this parsing is not yet LALR(7) as required by the set.mm grammar. I've been working on a subset of set.mm which only includes first order logic and predicate calculus, for which LALR(1) is sufficient (set.mm 's type codes are currently also hard-coded, but this can be easily overcome by parsing the "$j syntax" comments).

My next step will of course be to improve the current parser and get LALR(7), but I thought it might already be worth sharing at this early stage.

BR,
_
Thierry

PS. I'm very new to Rust and I still consider myself in the process of learning, so if anyone is interested to review the code, I could open a PR so that the changes appear clearly.

Thierry Arnoux

unread,
Jul 4, 2021, 2:32:35 PM7/4/21
to meta...@googlegroups.com

Hi Marnix, Stefan and all,

I've been slowly progressing in adding to SMM3 / metamath-knife the capability to parse the set.mm database, and although a few steps remain, I'd like to share where I am.

Before the actual parsing can start, the program builds a grammar from the syntax axioms. This Grammar is a tree, and I've recently added a function to export this tree and to visualize it using GraphViz. I find this is probably an interesting byproduct to share, I don't think I've seen any such thing before.

The grammar building deals with several kinds of ambiguities, and I now understand how hard Mel O'Cat's fight must have been!

As for a simple example, here is the part of the grammar used to describe ~ wex (` E. x ph `) and ~ wrex (` E. x e. A ph `) :

This is to be interpreted as:

When encountering the ` E. ` token, move to state 86. Then, parse a setvar, and move to state 87. From there, either parse a wff, perform a ~ wex reduce and stop, or expect a ` e. ` token and move to state 87.

In state 87, if a setvar is parsed, first a ~ cv reduce shall be performed (this transforms the setvar into a class).

And so on until ~ wrex is completely parsed.

The full tree is very big, and in some cases very complex, however, once it is built, parsing can be done by "just" following it like a recipe.

You can browse the full graph here: http://metamath.tirix.org/grammar.svg
I've also uploaded the source DOT file here: http://metamath.tirix.org/grammar.dot.
The source code for this project is still at https://github.com/tirix/metamath-knife/tree/grammar.

BR,
_
Thierry

PS. Another snapshot for fun:

Here between states 1239 and 16, the automaton has read ` ( A =/= x ` , and does 2 "reduce" along the way (cv and wne).
Reply all
Reply to author
Forward
0 new messages