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 coq-library-complexity to coq-community #150

Open yforster opened 8 months ago

yforster commented 8 months ago

Project name: Coq Library of Complexity proofs

Initial author(s): Fabian Kunze, Lennard Gäher, Maxi Wuttke, Yannick Forster

Current URL: https://github.com/uds-psl/coq-library-complexity

Kind: pure Coq library, formalization of mathematical theorems

License: CeCill 2.1 (but re-licensing to something like MIT or MPL should be possible)

Description: This library contains complexity theory formalised in the Coq proof assistant, developed at Saarland University and initiated by Fabian Kunze. It is built upon the Coq Library of Undecidability Proofs.

Status: not maintained since November 2022 (last version coq.8.16)

New maintainer: looking for a volunteer

ana-borges commented 7 months ago

I took a brief look at this and it seems like the first step to bring it up to speed with Coq would be to bring it up to speed with the Undecidability Library v1.1+8.16. Seems hard though, since https://github.com/uds-psl/coq-library-undecidability/pull/176 removed many things that the Complexity Library apparently depends on and I have no intuition on whether it would be best to vendor the removed files or to stop relying on them somehow.