Add the libraries for undecidability and first-order logic to the Platform

[palmskog]

Coq Library of Undecidability Proofs is a collection of definitions and results related to computability, not least the halting problem. For example, it allows Coq users to prove that some property is undecidable. The library was recently relicensed under the reusability-friendly MPL-2.0 license.

Coq Library for First-Order Logic is a library containing syntax, semantics and proof systems of first-order logic, building on the undecidability library. This library was recently relicensed under the permissive MIT license, a license known for making extensive reuse possible.

Since these two libraries formalize important basic computer science concepts that are not available in the Coq standard library and are not provided by other Platform packages (other than as isolated small fragments), I propose that these two libraries are included in the Platform. For example, if the community is aware of this FOL formalization, other FOL formalizations can be proved equivalent.

Maintainers of these two libraries I have interacted with include @yforster @dominik-kirst @DmxLarchey @mrhaandi

[yforster]

Thanks for bringing this up Karl, I'm in favour of including both!

I just prepared for an opam release compatible with 8.18 for coq-library-undecidability, @dominik-kirst and @JoJoDeveloping will soon do the same for coq-library-fol.

In the line of basic computer science concepts there is also https://github.com/uds-psl/coq-library-complexity with the Cook-Levin theorem and a time equivalence proof for Turing machines and lambda-calculus, but it's (probably) forever stuck on 8.16 due to a lack of maintainers.

[yforster]

I've filed coq-community/manifesto#150 for coq-library-complexity to look for a new maintainer, maybe we get lucky :)

[yforster]

There is a release for coq-library-fol now. Is there anything else we need to do for both libraries to be included in the platform? CC @dominik-kirst

[palmskog]

From my perspective, everything technically required is there, hopefully we can hear from the editorial board on a decision soon akin to here, cc @ybertot

I also hope we can get #344 resolved, since coq-library-undecidability depends on it.