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 Apery to coq-community #137

Closed amahboubi closed 2 years ago

amahboubi commented 2 years ago

Project name: Apery

Initial author(s): Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote

Current URL: https://github.com/math-comp/apery

Kind: pure Coq library, formalization of a mathematical theorem

License: CeCiLL-C

Description: This project contains a formal proof that the real number ζ(3), also known as Apéry's constant, is irrational. It follows roughly Apéry's original sketch of a proof. However, the recurrence relations constituting the crux of the proof have been guessed by a computer algebra program (in this case in Maple/Algolib). These relations are formally checked a posteriori, so that Coq's kernel remains the sole trusted code base.

Status: Maintained, part of MathComp CI

New maintainer: @amahboubi

palmskog commented 2 years ago

Thanks @amahboubi, this project fulfills all our requirements. As a final checkpoint, however, we have the following item:

The main authors of the package must either consent [to the move to coq-community] or be completely unresponsive

For example, you could email Frédéric and Thomas and let us know what they say, or ping them in this issue if you know their GitHub names.

amahboubi commented 2 years ago

Sure, I have contacted them already. Note that Thomas has left academia now.

amahboubi commented 2 years ago

Ping @thery, who also expressed interest in following this process (of moving a repo from the mathcomp organization to the coq community one).

amahboubi commented 2 years ago

I am pleased to report that both Frédéric and Thomas have answered. They agree with moving the apery repo to coq-community.

amahboubi commented 2 years ago

Now this repo does not have a proper github release, only a 1.0.0 tag. It would deserve a new release. Should I do it before the move or after?

palmskog commented 2 years ago

@amahboubi there is no requirement for doing any tags releases to move the repo, so let's tag release after the move. Please go ahead and move the repository now to coq-community, at your convenience. You will find the option to move under "Settings" for the project on GitHub, under the "Danger Zone" heading.

amahboubi commented 2 years ago

Done.

palmskog commented 2 years ago

Thanks! Let's close this issue and continue further discussions as pull requests and issues in the repo itself - in particular, I did a pull request with the usual adjustments to boilerplate.