Proposal: Move metamath-knife into the "metamath" organization

[David A. Wheeler]

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

[Benoit]

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

[Jim Kingdon]

Moving it to the metamath organization sounds good to me. Since it was always intended to be a community project, I've often thought that's the logical place for it, and all the more so if it already has multiple contributors as it seems that it does. I don't know if I have a grand theory for what other things should/could be there too (although I suppose I'd lean towards letting in most projects that want in) but metamath-knife seems like an easy call.

As for the name, I don't see anything wrong with the name. Very generic names like metamath-parser can be confusing and this tool (yes, I assume the name is a tool metaphor at least that is what it evokes for me) has been called metamath-knife ever since it existed in its current form.

P.S. if people lose interest in metamath (temporarily or otherwise), get busy at work, have other interests, etc they aren't required to die in order to leave the project. Just as a public service announcement.

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4faa0dc5-3e6d-41a0-b26e-e7198d2955b5n%40googlegroups.com.

[David A. Wheeler]

> On Jan 24, 2022, at 10:29 AM, Benoit <benoit...@gmail.com> wrote:
>
> Why is it called "knife" ? Is it because it's intended to be a "swiss knife" for metamath databases ?

Yes, it's intended to be a "Swiss Army Knife" - a collection of useful basic tools. It's also a pun on "fork", and I didn't want to call it "metamath" by itself as that's too ambiguous (which one do you mean?). I'm not married to the name, but the point of names is to clearly distinguish things from other things, so it needs to distinguish it from other things.

--- David A. Wheeler