Publish on crates.io

[tirix]

This is not an issue per se, just an open conversation and a place to record consumers.

Our API is still changing a lot and I don't think it's a problem, however we start to have a few consumers for this library:

• metamath-web : a dynamic web page rendering engine,
• mm-web-rs : a static/dynamic web page rendering engine,
• rumm : a rudimentary experimental tactics-based metamath proof assistant,
• metamath-vspa : a Visual Studio Code extension,

I think we might consider tagging some versions in order to help those dependent keep stable compatibility. There is a discussion about version numbering here, and I think it's worth reviving it now.

What about tagging the original version with 0.3 and starting to count up from there?

[digama0]

Putting it on crates.io will help a lot. That will give it a versioning system as well. I'm on board with starting at 0.3.0.

[tirix]

I would definitely like to put it in crates.io, so that these dependent can start pulling stable crate versions instead of metamath-knife = { path = "../metamath-knife" } as is currently the case.

I was somehow waiting for it to be moved to metamath's github account but maybe it actually does not matter, and repositories can move while keeping the same crates.io name. I don't have experience with that.

[tirix]

Ok, so the guide to publishing on crates.io is here. I did not see anything specifically for changing the repository, and there seem to be shenanigans with GitHub authentication, so which user/organization publishes probably matters. @david-a-wheeler

Let's redirect this issue to "Publish on crates.io".

[digama0]

@david-a-wheeler I don't think there are any blockers to moving this project to the metamath organization. I'm not an admin on this repo so I think you will have to do it.

[david-a-wheeler]

I definitely think we should publish to crates.io. If we're going to move this to the metamath organization, I suggest moving this to the metamath org first, so that we don't need to this this later.

I do think metamath-knife should move to the metamath organization. You're now a co-owner of the metamath organization, so if I should die (I'm trying not to!) things could just keep moving.

However: before this moves to the metamath organization, I think it's important that we discuss this publicly on the Metamath mailing list. I don't think unanimous agreement is necessary, but maximum transparency seems to me to be important. I guess I'm the one who should post the proposal - seem okay to everyone else?

[digama0]

Sure, but I don't think the move itself is a big deal. Big organizations often have lots of little projects associated to them, it doesn't necessarily imply some kind of official-ness so much as it is a place to centralize and organize work on a project.

[david-a-wheeler]

Proposed email:

===

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). However, Mario, Tirix, and I have added a number of features (hopefully improvements) to it. 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) it'll be easier to just keep things going.

[tirix]

Looks good to me!

Thank you for taking the time to look into this, David!

[tirix]

I went ahead and created a draft release v0.3.1, visible here. Here is an explanation for the somewhat arbitrary choice of v0.3.1 :

• I've checked other examples and saw the v prefix everywhere. I guess it will be dropped on crates.io.
• the 0 major version means we are not production ready yet,
• the 3 minor version stems from the "3" in SMM3, meaning this is already the third iteration of the project,
• the 1 patch version means we added changes on top of SMM3 (even if not always in a backwards-compatible manner)

@digama0 @david-a-wheeler once I have your blessings I will publish it, so we can start referring to a fixed version in dependent projects.

That shall be possible with this kind of tags in Cargo.toml:

metamath-knife = { git = "https://github.com/david-a-wheeler/metamath-knife", tag = "v0.3.1" }

...this shall do the trick, until we publish on crates.io.

[david-a-wheeler]

@tirix - I have some really serious family issues I'm having to deal with, so I haven't been very responsive & probably won't be for a little while longer :-(.

Tagging makes sense to me.

[tirix]

Thank you David!

And don't worry too much about this, my thoughts are with you.

[tirix]

@david-a-wheeler I'm moving on with tags, and we're already at v0.3.3.

[jkingdon]

In case this is waiting for community feedback:

• I support moving this repository to the metamath organization.
• Publishing on crates.io sounds like a good idea. I don't know if there are any open questions about how (for example, a crate can be owned by one or more github users or teams and perhaps https://github.com/orgs/metamath/teams/team-set-mm would be a suitable owner or perhaps it should be a smaller/different list, but as long as it is at least two active people we should be OK).
• The version number of 0.3.3 (or whatever we are up to by the time this gets acted on) sounds good.

[david-a-wheeler]

I support moving this repository to the metamath organization.

Me too, actually. It's currently on my personal account for reasons I can't remember.

However, that is a different issue. So I recommend that people comment on it as its own issue. I've proposed it here:

https://github.com/david-a-wheeler/metamath-knife/issues/119

[programmerjake]

now that this repo is in the metamath org, is there anything blocking publishing it on crates.io?

[digama0]

No, it looks like all the prerequisites are satisfied. I've pushed our first version as v0.3.8 to both github and crates.io. :tada:

I had to add a readme for the library, and cobbled something together based on the main readme. Feel free to post follow ups to improve it.

[digama0]

I tried to add @david-a-wheeler as co-owner, but I got

$ cargo owner --add david-a-wheeler metamath-rs
    Updating crates.io index
error: failed to invite owners to crate `metamath-rs` on registry at https://crates.io

Caused by:
  the remote server responded with an error (status 400 Bad Request): could not find user with login `david-a-wheeler`

I think this means that David needs to use cargo login to get an API key for publishing first.