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 comp-dec-modal to coq-community #115

Closed chdoc closed 3 years ago

chdoc commented 3 years ago

Project name: Completeness and Decidability of Modal-Logic Calculi

Initial author(s): Christian Doczkal (me)

Current URL: https://github.com/chdoc/comp-dec-modal, https://github.com/chdoc/comp-dec-pdl

Kind: pure Coq library / formalization of mathematical theorems

License: CeCILL-B

Description: Constructive machine-checked proofs of soundness and completeness of calculi for for various modal logics (i.e, K,K*, CTL, (C)PDL).

Status: maintained

New maintainer: Christian Doczkal (@chdoc) / looking for co-maintainer.

Remark: Currently these results are spread out over the two aforementioned repositories and their shared submodule. To simplify long-term maintenance, I would gather everything in a single repository and convert the current recursive make build infrastructure to a single centralized Makefile.

chdoc commented 3 years ago

Would comp-dec-modal be okay as a repo-name / identifier?

palmskog commented 3 years ago

@chdoc comp-dec-modal sounds good to me. You may want to think carefully about which repository out of the two to transfer to coq-community (probably: the one whose URL is used most in publications).

I can help this project out in the short term with some basic metadata/automation adjustments. To advertise for a co-maintainer, the best way may be to open a help-wanted issue in the repo.

chdoc commented 3 years ago

@chdoc comp-dec-modal sounds good to me.

Okay.

You may want to think carefully about which repository out of the two to transfer to coq-community (probably: the one whose URL is used most in publications).

Good point. However, the "main" repository was only created well after my thesis, so only the URL of the PDL repository has been used in a single publication. My inclination would be to "archive" both original repositories and add a link to the (shared) coq-community project.

chdoc commented 3 years ago

@palmskog I cleaned up my old development. My idea would be to create a new repository in coq-community and push this branch and this branch only. Afterwards, I would add archival notes to the other repositories.

palmskog commented 3 years ago

@chdoc that sounds good to me, it seems to cover all bases so that no history is lost or inaccessible. You should already privileges to create a new repository, so please go ahead when ready.

chdoc commented 3 years ago

I pushed the aforementioned branch. There are still some things to do (like an opam package or a gh-pages branch for the doc), but this I will do at a later point. Anyway, possible issues can be handled in the repository issue tracker.