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.
On 1/24/22 7:29 AM, Benoit wrote:
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
<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 <http://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]
<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/4faa0dc5-3e6d-41a0-b26e-e7198d2955b5n%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/4faa0dc5-3e6d-41a0-b26e-e7198d2955b5n%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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/802fc522-713a-01bd-4044-2f0ccd5484e3%40panix.com.
