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 the Tarjan and Kosaraju project to Coq-community #146

Closed palmskog closed 1 year ago

palmskog commented 1 year ago

Project name: Tarjan and Kosaraju

Initial author(s): Cyril Cohen, Jean-Jacques Lévy, and Laurent Théry

Current URL: https://github.com/math-comp/tarjan

Kind: pure Coq library

License: CeCILL-B

Description: Formalizations and correctness proofs, using Coq and the Mathematical Components library, of algorithms originally due to Kosaraju and Tarjan for finding strongly connected components in finite graphs. It also contains a verified implementation of topological sorting with extended guarantees for acyclic graphs.

Status: Currently maintained as part of the math-comp GitHub organization, in particular by @CohenCyril, @proux01, and @thery. Moving this project to Coq-community while keeping any willing maintainer(s) can allow for more streamlined and collaborative maintenance and regular (opam) releases.

New maintainer: Member(s) of the Mathematical Components team who are also Coq-community members. If viewed as good idea by current maintainers, @palmskog can co-maintain formally or informally.

proux01 commented 1 year ago

(note that I don't consider myself as a maintainer of Tarjan)

CohenCyril commented 1 year ago

I approve

palmskog commented 1 year ago

OK, in this case I propose @CohenCyril and myself as the formal (named) maintainers in Coq-community, and @proux01 is welcome to help out anytime. My own goal would just be to put out releases compatible with stable Coq/MathComp and minor changes to facilitate easier maintenance.

If this sounds reasonable, we could transfer the repo the Coq-community GitHub organizations as soon as @thery gives his approval.

proux01 commented 1 year ago

Done: https://github.com/coq-community/tarjan