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 projects Goedel and Pocklington to coq-community #124

Closed palmskog closed 3 years ago

palmskog commented 3 years ago

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:

Casteran commented 3 years ago

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 notifications@github.com 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 https://github.com/coq-community/manifesto/issues/124, or unsubscribe https://github.com/notifications/unsubscribe-auth/AJW6FCSPE3AA5STQY25XPQTSXXE55ANCNFSM4VQIVLSQ.

palmskog commented 3 years ago

@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 commented 3 years ago

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 commented 3 years ago

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 notifications@github.com 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 https://github.com/coq-community/manifesto/issues/124#issuecomment-753328546, or unsubscribe https://github.com/notifications/unsubscribe-auth/AJW6FCSG3LM6AJQDM6X7RLDSXXRT7ANCNFSM4VQIVLSQ.

palmskog commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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

Le 1 janv. 2021 à 17:17, Karl Palmskog notifications@github.com 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 https://github.com/coq-community/manifesto/issues/124#issuecomment-753334696, or unsubscribe https://github.com/notifications/unsubscribe-auth/AJW6FCQQKYWJY4HDYWDFLB3SXXYSFANCNFSM4VQIVLSQ.

palmskog commented 3 years ago

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 commented 3 years ago

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

Le 1 janv. 2021 à 17:26, Karl Palmskog notifications@github.com 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 https://github.com/coq-community/manifesto/issues/124#issuecomment-753337481, or unsubscribe https://github.com/notifications/unsubscribe-auth/AJW6FCQKPIDZIHTOHE5ZQILSXXZTTANCNFSM4VQIVLSQ.

palmskog commented 3 years ago

@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 commented 3 years ago

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.