Exciting news! Where did you get the grammar parsing algorithm from? Is it based on LRParser, a backtracking parser algorithm, or something tailored for set.mm?
Regarding the questions, my own opinions are: (1) Lots of bits of a metamath proof assistant can be separated into crates and put on crates.io for reuse. Especially if you have a second application, this is definitely a good idea, although it often requires reworking the code to make the library more modular and less entangled with the application. (2) I believe David has shown some interest in keeping up maintenance on the project, so I'm inclined toward the metamath-knife repo if it can be opened up to other contributors. And indeed, re: (3), putting it on the metamath organization would be a way to avoid having to pick sides and help establish it as a community project. Mario On Sun, Aug 15, 2021 at 9:23 AM Thierry Arnoux <[email protected]> wrote: > Hi Stefan, David and all, > > Eight months after this discussion was launched I have made what I think > is an important breakthrough: the "grammar" addition to SMM3 / > metamath-knife can now parse all statements of set.mm, including the > complex ones where look ahead is required, into tree-like "formula" > structures. Code is as always available on my fork > <https://github.com/tirix/metamath-knife/tree/grammar> for those > interested. > > On my MacBookPro 2015, parsing the full database takes around 3s on one > single thread, and 1s when multi-threaded. This is roughly the same cost as > the "scopeck" step. Building the grammar for the parsing, based on the > syntactical axioms, only takes around 13ms. I was surprised how easy it was > to introduce multi-threading. > > I believe this is the first step to make `metamath-knife` a library for a > new community proof assistant. I want to continue to evolve the resulting > "Formula" structure so that it supports basic functionalities such as > substitution and unification. However I don't want to go too far beyond > that, I think further functionality shall be placed in the "application" > part. > > Stefan, David, I would like to soon move on pulling this code into an > official rust crate. You own the repositories for `smetamath`, respectively > `metamath-knife`. > How could we proceed? > > Specifically: > > - I believe the 'statement parsing' functionality shall be part of a > basic Metamath library. Do we have an agreement here? This would mean I > could go ahead an issue a PR :-) > - Which repository shall be used and evolve? Stefan's `smetamath > <https://github.com/sorear/smetamath-rs>`, or David's `metamath-knife > <https://github.com/david-a-wheeler/metamath-knife>` ? > - Since there was broad agreement to build a community project on > Rust, could we move the repository into GitHub's Metamath organization > <https://github.com/metamath>? Norm, would you agree? > > BR, > _ > Thierry > > PS. smetamath's TODO <https://crates.io/crates/smetamath#todo> lists both > *grammatical > parser* (the topic of this mail), and also *outline inference*: I've also > added outline inference in the branch 'outline > <https://github.com/tirix/metamath-knife/blob/outline/src/outline.rs>'. > > -- > 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/76f1763b-c048-06ed-92fd-5e8ca45e30e6%40gmx.net > <https://groups.google.com/d/msgid/metamath/76f1763b-c048-06ed-92fd-5e8ca45e30e6%40gmx.net?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/CAFXXJSsrTpp7jk459er-geX_wNbgp6hsSUAJ8Sw10xRLu5Ta6A%40mail.gmail.com.
