Proposal to move Area Method to rocq-community

[palmskog]

Project name: Area Method

Initial author(s): Julien Narboux

Current URL: https://github.com/rocq-archive/area-method

Kind: pure Coq/Rocq library

License: Unknown, not specified in repo

Description: Formalization of a decision procedure for constructive theorems in Euclidean plane geometry. The procedure implemented is the area method by Chou, Gao and Zhang.

Status: Unmaintained

New maintainer: @jnarboux

[palmskog]

@jnarboux we have a requirement in Rocq-community that projects must have an explicit license that is approved as an open source license by OSI or considered a free software license by FSF.

Would you be willing to explicitly license this project under such a license? See our recommendations here on what licenses we prefer: https://github.com/rocq-community/manifesto?tab=readme-ov-file#best-practices

[jnarboux]

I added Cecill C licence.

[palmskog]

@jnarboux this is indeed a permitted license, but just to double check that you are aware that it is incompatible with the GPL license: https://www.gnu.org/licenses/license-list.en.html#CeCILL-C

What this means in practice is that if/when projects licensed under GPL reuse the project, it's likely illegal to distribute the resulting .vo files, see an example.

[Zimmi48]

In the CeCILL family, only CeCILL 2.1, which is a GPL-like, GPL-compatible, license is OSI-approved and recommended for use in new projects. It is quite unfortunate that the authors of CeCILL 2.1 did not also create an updated version for CeCILL-B and CeCILL-C or properly retire these licenses.