Port to Coq 8.9

[vbgl]

Fixes #6.

[vbgl]

Hugo, what do you think of these changes?

Do you think Containers should be moved to the coq-community?

ping @herbelin

[Zimmi48]

@vbgl We are definitely interested to have this moved in coq-community and it even seems that @siddharthist would be interested to be the maintainer, but we have first to resolve #4. No project can get into coq-community without a clear open source license set by its authors. It seems that all attempts to enter in contact with Stéphane Lescuyer have failed but maybe someone could ask Evelyne Contejean if she knows where to write.

[herbelin]

Thanks for the port. I was going to answer a yes to a move to coq-community but @Zimmi48 was quicker. To contact Stéphane L., a possibility is also via Vincent S.

[vbgl]

Thank you two for these instructive replies and for merging.

[Zimmi48]

Thanks for the hint @herbelin! You are talking about @vsiles, right?

[herbelin]

Yes.

[vsiles]

I'll transfer the question to Stéphane.

[StekiKun]

Hey everyone, Stéphane here, thanks @vsiles for warning me :)

I have nothing against moving this to coq-community, but what are the fundamental differences with coq-contribs? This work of mine started before the GitHub era, and was moved here by the helpful Coq people after I had already left academia (along with other plugins from my PhD), so I was never active on GitHub... but it turns out I actually maintained most of my plugins as best I could for my own use all these years.
For now, I just opened #8 to fix Generate OrderedType which had seemingly been broken for a while. I will add an open source license file shortly.

• SL

[Zimmi48]

Hi @StekiKun,

I think that the README in https://github.com/coq-community/manifesto, and in particular the first question of the FAQ "What is the difference with coq-contribs?" should mostly answer this. To make it short, coq-contribs more or less represent the packages that were donated by their authors but have since then been maintained by the Coq development team itself. coq-community is an effort for a user-run organization for the long-term maintenance of Coq packages, i.e. the maintenance effort shifts from the development team to the user community (with a principal maintainer for each package). In the case you are still maintaining your contrib, then two options can be considered: you could move it back to your own repository (this is what happened with Relation Algebra and Paco) or you could move it to coq-community while still being officially the principal maintainer. This second option ensures that the transition is simpler if you decide you don't want to be the principal maintainer anymore, but it can also be a way of simplifying contributions from other members of the community.

[StekiKun]

Thank you @Zimmi48 for all the information. Indeed it makes a lot of sense for containers to be moved to coq-community, even if I can be the main maintainer for the time being.