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 <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. On 07/05/2021 04:13, Marnix Klooster wrote:
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 <http://set.mm> I'm seeing ~145,000 lines/second / 8 MB/second, with all of set.mm <http://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 <[email protected] <mailto:[email protected]>>: Exciting! How is the performance? I would guess that a Zig verifier could compete with the best. On Wed, May 5, 2021 at 10:51 AM Marnix Klooster <[email protected] <mailto:[email protected]>> wrote: 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 <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 <https://github.com/marnix/zigmmverify>; any feedback is welcome. Groetjes, <>< Marnix -- Marnix Klooster [email protected] <mailto:[email protected]> -- 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] <mailto:[email protected]>. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAF7V2P_C7QcKP8b_rxvEO6e5uXTMpS6gySU-iVCiqLD1gCW5qQ%40mail.gmail.com <https://groups.google.com/d/msgid/metamath/CAF7V2P_C7QcKP8b_rxvEO6e5uXTMpS6gySU-iVCiqLD1gCW5qQ%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] <mailto:[email protected]>. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvqg4vHT%2B4HmaBhHSMCTdE0-EX0vRyVr6_tn%3DYFGgJmGA%40mail.gmail.com <https://groups.google.com/d/msgid/metamath/CAFXXJSvqg4vHT%2B4HmaBhHSMCTdE0-EX0vRyVr6_tn%3DYFGgJmGA%40mail.gmail.com?utm_medium=email&utm_source=footer>. -- Marnix Klooster [email protected] <mailto:[email protected]> -- 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] <mailto:[email protected]>. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAF7V2P_PM0_JE7zMQ61rFOYgX-RzUQc4RKqvLDAirE9SFwaBhg%40mail.gmail.com <https://groups.google.com/d/msgid/metamath/CAF7V2P_PM0_JE7zMQ61rFOYgX-RzUQc4RKqvLDAirE9SFwaBhg%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/73ce43d8-fcc3-9521-6669-ec01f0a03d16%40gmx.net.
