Proposal to move coq-library-complexity to coq-community

[yforster]

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]

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 uds-psl/coq-library-undecidability#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.