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 Gaia to coq-community #117

Closed palmskog closed 3 years ago

palmskog commented 3 years ago

Project name: Gaia (Geometry, Algebra, Informatics and Applications)

Initial author(s): José Grimm, with help from Alban Quadrat and using a set theory axiomatization originally by Carlos Simpson

Current URL: https://github.com/palmskog/gaia http://www-sop.inria.fr/marelle/gaia/

Kind: pure Coq library and formalization of a mathematical theorems

License: MIT

Status: unmaintained since José Grimm passed away in 2019

Description: Gaia was a project by José Grimm to implement the "Elements of Mathematics" books by N. Bourbaki. It is based on the Mathematical Components (MathComp) library and contains formalizations of many concepts and results from set and number theory (150k+ lines of Coq code).

New maintainer: Laurent Théry (@thery)

Thanks to @ybertot, the final version of Gaia released by José in 2018 has been released under the MIT license. I (@palmskog) have ported this release to Coq 8.10 and later (depending on MathComp 1.11 and later).

I propose that the Coq community continues the maintenance of this project and at least maintains compatibility with latest Coq and MathComp. @thery has generously offered to be the initial coq-community maintainer. I will also help out but can't commit to being co-maintainer for the time being.

palmskog commented 3 years ago

I've transferred the repository and adjusted metadata: https://github.com/coq-community/gaia

At this point, we can continue the discussion in issues in the repository and elsewhere.