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.
