search

coq-community / manifesto

Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.
Other
68 stars 6 forks source link

Proposal to move project MMaps to coq-community #142

Closed palmskog closed 1 year ago

palmskog commented 1 year ago

Project name: MMaps: Modular Finite Maps overs Ordered Types

Initial author(s): @letouzey

Current URL: https://github.com/letouzey/coq-mmaps

Kind: pure Coq library

License: LGPL-2.1-only (based on LICENSE file and file headers, can we clarify?)

Description: Several implementations of finite maps over arbitrary ordered types using Coq functors. This is an udpdated version of Coq Stdlib's FMaps. It is meant to complement the MSet library.

Status: no changes since 2020

New maintainers: @palmskog and @letouzey

This is a very useful library for which it would be useful to have an opam package, and that should reasonably be included in the Coq Platform (and eventually maybe Coq's stdlib).

I would like to volunteer to be interim maintainer to get the project on track towards the Coq Platform. @letouzey are you fine with this and with transferring the project to the coq-community GitHub organization?

letouzey commented 1 year ago

Hi @palmskog. That sounds reasonable to me, thanks for proposing your help. Indeed, I've not been active on coq-mmaps since quite some time. I might work on it again in some future, but I've no clear idea of when that might be. Feel free to do with it what you see fit.

Concerning License, indeed LGPL 2.1 for now. But that can be discussed if necessary.

Note: I've just noticed at the moment the Issue https://github.com/letouzey/coq-mmaps/issues/1 by @xavierleroy. Sorry @xavierleroy for missing the github notification, don't know what happened. I'll take the patch and further check for compilation by recent versions of coq.

Best Pierre Letouzey

palmskog commented 1 year ago

@letouzey I've invited you to be a member of the coq-community organization on GitHub. Once you accept, you will be able to transfer the repository here. You will find the option to move under "Settings" for the coq-mmaps project on GitHub, under the "Danger Zone" heading.

Regarding licensing, my initial concern was simply about whether the project was under the license LGPL-2.1-only (Coq's license) or LGPL-2.1-or-later (compatible with Coq's license, but not the same, due to the possibility of using LGPL-3.0). These are considered different according the SPDX categorization.

My interest here is mainly in keeping the project building with recent Coq and doing tested releases, so that people can start to use, e.g., red-black finite maps in their Coq projects (via the Coq Platform). So my maintenance work will be conservative, and you would still be a maintainer and can work on it when you want.

letouzey commented 1 year ago

The transfer is on the way. Btw, do you already have experience with opam packaging of Coq libraries ? I always planned to turn someday coq-mmaps into an opam package but never took the time to investigate how to make that happen...

palmskog commented 1 year ago

Yes, I co-maintain the Coq opam archive and do my best to help out the Coq Platform, which is based on opam. So I will do some quick packaging-oriented pull requests (and add continuous integration).

Since the move of the repository was successful, let's close this issue and continue the discussion as Coq-mmap issues