> On 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. >
Cool! I briefly looked though it here: https://github.com/tirix/metamath-knife/commits/grammar <https://github.com/tirix/metamath-knife/commits/grammar> > 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 think that’s one of the bigger arguments for Rust. Modern systems have multiple CPUs, but it’s often hard to safely use them. Rust’s compiler-enforced ownership model simplifies much while retaining both safety & speed. > 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 :-) I think that makes sense. At least send me a pull request. > > 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>` ? Well, I’m biased. Pick me, pick me :-). Though certainly feel free to propose it to Stefan’s smetamath as well. It’s quite easy for different repos to bring in commits from other places. And just to make sure credit is given: I’ve made minor tweaks to his work, but Stefan O’Rear *absolutely* did the heavy lifting with smetamath. > 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? I think that makes sense. If it’s okay, I’d like to move metamath-knife into the metamath repo. I see Norm agreed to that; is there a lot of opposition? I’ve had less time to work on metamath-knife than expected recently due to work & my father having a lot of health problems. But I still think a library in Rust for Metamath has a lot of promise. --- David A. Wheeler -- 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/F46D492B-3DC2-47CA-AB70-1B704DBED86D%40dwheeler.com.
