> 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? ?
That's fine by me. Norm On Sunday, August 15, 2021 at 9:23:56 AM UTC-4 Thierry Arnoux 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/865f3632-58f4-4d2d-b963-c109d61df611n%40googlegroups.com.
