Proposal to move projects Goedel and Pocklington to coq-community

[palmskog]

Project names: Goedel and Pocklington

Initial author(s): Russell O'Connor (Goedel), Olga Caprotti and Martijn Oostdijk (Pocklington)

Current URL: https://github.com/coq-contribs/goedel https://github.com/coq-contribs/pocklington

Kind: pure Coq libraries

License: CC-0/public domain (Goedel) LGPL-2.1-or-later (Pocklington)

Description: A constructive proof of the Gödel-Rosser incompleteness theorem in Coq, and its supporting library of primality certification. As pointed out by @Casteran, the incompleteness proof may have pedagogical uses and contains a formalization of Peano arithmetic that may be useful elsewhere.

Status: unmaintained

New maintainer: @Casteran

The last version of Coq known to work is 8.10:

• https://github.com/coq-contribs/pocklington/tree/v8.9
• https://github.com/coq-contribs/goedel/tree/v8.9

[Casteran]

I can try to start the adaptation to Coq8.12. But, since I’m not very used to modern compilation, is it possible to create a framework with a correct makefile and dune stuff. (May be one project for Pocklington and Goedel) I could work on a specific branch until it works.

…

Le 1 janv. 2021 à 14:30, Karl Palmskog ***@***.***> a écrit : Project names: Goedel and Pocklington Initial author(s): Russell O'Connor (Goedel), Olga Caprotti and Martijn Oostdijk (Pocklington) Current URL: https://github.com/coq-contribs/goedel <https://github.com/coq-contribs/goedel> https://github.com/coq-contribs/pocklington <https://github.com/coq-contribs/pocklington> Kind: pure Coq libraries License: CC-0/public domain <http://r6.ca/Goedel/goedel1.html> (Goedel) LGPL-2.1-or-later (Pocklington) Description: A constructive proof of the Gödel-Rosser incompleteness theorem in Coq, and its supporting library of primality certification. As pointed out by @Casteran <https://github.com/Casteran>, the incompleteness proof may have pedagogical uses and contains a formalization of Peano arithmetic that may be useful elsewhere. Status: unmaintained New maintainer: looking for a volunteer The last version of Coq known to work is 8.10: https://github.com/coq-contribs/pocklington/tree/v8.9 <https://github.com/coq-contribs/pocklington/tree/v8.9> https://github.com/coq-contribs/goedel/tree/v8.9 <https://github.com/coq-contribs/goedel/tree/v8.9> — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#124>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AJW6FCSPE3AA5STQY25XPQTSXXE55ANCNFSM4VQIVLSQ>.

[palmskog]

@Casteran if you create branches working with 8.12 of Goedel and Pocklington and link to them here, I can set up our usual boilerplate with Makefile/Dune/continuous integration/etc. for each repository.

[palmskog]

Thanks to Hugo's earlier maintenance work, it was actually not all that difficult to get the v8.9 branches of Pocklington and Goedel working on 8.12. I have some small patches I can apply.

@Casteran can you confirm you can be the maintainer of these projects in coq-community? (Maintainers can step down anytime.) If so, I can transfer the repositories to the coq-community organization and apply the patches.

[Casteran]

Ok, I’ll try ! I think there is a lot of things to do (bullets, comments) for making the code more readable. Will the code be available through opam ?

…

Le 1 janv. 2021 à 16:18, Karl Palmskog ***@***.***> a écrit : Thanks to Hugo's earlier maintenance work, it was actually not all that difficult to get the v8.9 branches of Pocklington and Goedel working on 8.12. I have some small patches I can apply. @Casteran <https://github.com/Casteran> can you confirm you can be the maintainer of these projects in coq-community? (Maintainers can step down anytime.) If so, I can transfer the repositories to the coq-community organization and apply the patches. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#124 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AJW6FCSG3LM6AJQDM6X7RLDSXXRT7ANCNFSM4VQIVLSQ>.

[palmskog]

We can set up opam packages and make a tag/release for 8.12 for sure. But it will take a bit of time - my first priority would be to set up continuous integration so we know that things are working properly.

[palmskog]

The repos have been moved: https://github.com/coq-community/pocklington https://github.com/coq-community/goedel

Goedel was released by its author into the public domain. However, this is a "license" which we prefer not to use in coq-community, since it doesn't work in all jurisdictions and is not an open source license. @Casteran do you mind if we switch Goedel to the (coq-community recommended) MIT license for the master branch?

[Casteran]

Personnaly, I don’t mind. Do we have to ask the author ?

…

Le 1 janv. 2021 à 17:17, Karl Palmskog ***@***.***> a écrit : The repos have been moved: https://github.com/coq-community/pocklington <https://github.com/coq-community/pocklington> https://github.com/coq-community/goedel <https://github.com/coq-community/goedel> Goedel was released by its author into the public domain. However, this is a "license" which we prefer not to use in coq-community, since it doesn't work in all jurisdictions and is not an open source license. @Casteran <https://github.com/Casteran> do you mind if we switch Goedel to the (coq-community recommended) MIT license for the master branch? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#124 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AJW6FCQQKYWJY4HDYWDFLB3SXXYSFANCNFSM4VQIVLSQ>.

[palmskog]

Public domain means we don't (legally) have to get the original author's approval to set the license. I guess we can still check as a courtesy at some later point, but since our configuration boilerplate requires a meaningful license name, I will just go ahead with MIT for now.

[Casteran]

Should I remove all the references to the LGPL License from the .v files ?

…

Le 1 janv. 2021 à 17:26, Karl Palmskog ***@***.***> a écrit : Public domain means we don't (legally) have to get the original author's approval to set the license. I guess we can still check as a courtesy at some later point, but since our configuration boilerplate requires a meaningful license name, I will just go ahead with MIT for now. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#124 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AJW6FCQKPIDZIHTOHE5ZQILSXXZTTANCNFSM4VQIVLSQ>.

[palmskog]

@Casteran from what I can see, there are no LGPL license clauses in the goedel project - only in pocklington. The change of license to MIT only applies to goedel, not to pocklington. The pocklington project legally has to keep its LGPL license (either 2.1 or 3.0), so we shouldn't change anything related to licensing there, I think.

[palmskog]

The master branches of both repositories in coq-community now work with Coq 8.12, and have continuous integration and our usual metadata and configuration files. Hence, I think we can close this issue and continue the discussion as issues in each respective repository.