Proposal to move reglang to coq-community

[palmskog]

Project name: Regular Language Representations in the Constructive Type Theory of Coq (reglang)

Initial author(s): Christian Doczkal, Gert Smolka, and Jan-Oliver Kaiser

Current URL: https://github.com/chdoc/coq-reglang

Kind: pure Coq library

License: CeCILL-B

Description: Definitions and properties of regular languages (including, e.g., regexps), using the MathComp library and the SSReflect proof language. Artifact for a research paper.

Status: maintained by @chdoc

New maintainers: @chdoc and @palmskog

Based on a previous discussion with @chdoc, this is a memento that reglang can be transferred to coq-community when convenient. I volunteer to take care of initial CI, adding metadata, and so on. I suggest the repo should be renamed to simply reglang in line with conventions in coq-community.

[chdoc]

I support the move of [coq-]reglang to coq-community. What do I need to do in order to make this switch happen? My main concern is that I would like the link in the published journal paper to remain intact.

According to this post redirects should follow both renamings and ownership transfers. So should I just rename "my" repository to reglang and then transfer ownership to coq-community?

If I understand correctly, transferred projects maintain their licence. In particular, me and @Janno keep the intellectual property of the things we wrote and any contributor maintains the intellectual property of his/her contribution. Correct? In any case, @Janno should be among the initial authors of the package.

Also mentioning @gert-smolka, in case he wants to add something.

[palmskog]

@chdoc I don't think it technically matters if you do the renaming before or after the transfer. It should work fine to do it in the order you said, i.e., first rename repo and then transfer the repo.

There is no implicit or explicit change in copyright status just because you move the repo to the coq-community organization - everything is owned by the same people as before. Moreover, there is no change in license unless the owners want there to be. The main implication is that organization members can help out with ongoing project maintenance. A maintainer can still restrict commits to master if he wants.

Our standard templates for README.md allows for putting research paper links front and center, see for example the README for AAC Tactics. However, we don't force projects to use this template - but personally I find it useful.

We also encourage adding metadata that allows preserving initial authorship information outside of Git repo commit history.

[palmskog]

Just a quick example of how forwarding works, in this case for the bits project:

• original repository was at https://github.com/artart78/coq-bits
• it was moved to https://github.com/coq-community/coq-bits
• then renamed to https://github.com/coq-community/bits

As can be checked easily, forwarding works for all previous URLs.

[chdoc]

I prepared a meta.yml and generated a new README.md from that. I don't know how to set up the repository such that the default Travis CI template and the automatic deployment of the coqdoc documents work. See #6.

I guess the next step is to actually transfer the repository, before setting up the rest? Just out of curiosity: could I, in principle, transfer ownership back to myself if I wanted?

[palmskog]

@chdoc technically, a transfer of the repository back to your own account has to be done by an owner of the coq-community organization (due to how GitHub organization permissions work). Currently, the owners are, myself, @Zimmi48, and @anton-trunov, and the manifesto specifies that there should always be exactly three owners.

The manifesto and guidelines currently do not specify a process for transferring back ownership of a previously-transferred repository - please contribute to #2 if you want this to be more fleshed out. Personally, I would be fine with a transfer back if all (substantial) contributors to a repo gave their permission.

Setting up CI is indeed best done after the transfer.

[Zimmi48]

@palmskog We usually make maintainers admin of the projects under their supervision. According to this doc it seems that this is enough permission to be able to transfer the repository:

If you have owner permissions in an organization or admin permissions to one of its repositories, you can transfer a repository owned by your organization to your user account or to another organization.

[Zimmi48]

But yes, the policy of transferring back should be discussed at some point.

[chdoc]

My point was indeed only half about what is technically possible. The other half was about what's "right" or "acceptable" according to the rules of the organization.

[Zimmi48]

Until we do get a clear policy, let's say that if you transfer your repository to coq-community the project stays under your full control until you voluntarily step down as a maintainer or become completely unresponsive for an extended period.

[chdoc]

I just transferred the project, please add me as maintainer/administrator.

[palmskog]

@chdoc you now have the admin role for the repo. The final step of the transfer in my mind would be to rename the repo to reglang, maybe you can do this? It would also verify that you have admin privileges.

[chdoc]

Done! I guess the rest can be discussed in #6