Why is it called "knife" ? Is it because it's intended to be a "swiss knife" for metamath databases ? If this is meant to become the main metamath tool, maybe terms like metamath-parser or metamath-verifier (or mm-parser or mm-verifier), even if they capture only a part of the functionalities, would be more descriptive and less aggressive. Or mm-suite, which has several modules: mm-parser, mm-verifier, mm-proof-assistant, mm-web...
If no one else objects to "knife", I'll go with the flow. Benoît On Monday, January 24, 2022 at 3:51:40 PM UTC+1 David A. Wheeler wrote: > All: > > I propose moving the GitHub project david-a-wheeler/metamath-knife < > https://github.com/david-a-wheeler/metamath-knife>, from its current > location under my name, into the "Metamath" organization as yet another > repository (just as metamath-exe, metamath-book, and set.mm are). > > Metamath-knife is a set of basic functions in Rust for metamath and is a > friendly fork of smetamath-rs (aka SMM3) by Stephan O'Rear (sorear). Mario, > Tirix, and I have added a number of features (hopefully improvements) to as > metamath-knife. A number of other packages now depend on it, including: > * metamath-web : a dynamic web page rendering engine, > * mm-web-rs : a static web page rendering engine, > * rumm : a rudimentary experimental tactics-based metamath proof assistant > > There's no need for all metamath-related tools to move into the metamath > organization, and I don't think moving it means that "this is the one true > blessed piece of software". However, Norm's death has reminded me again > that we're all mortal. I'd like to move this software into an organization > so that when I die (as we all will, though I have no plans to do it soon) > it'll be easier to just keep things going. At this point Tirix & Mario have > made most of the recent changes, so it would make sense to move it > somewhere else. > > Please let us know if that seems reasonable or is a problem. > > --- 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/4faa0dc5-3e6d-41a0-b26e-e7198d2955b5n%40googlegroups.com.
