Consolidation of generally useful Coq code into Coq Platform projects

[palmskog]

Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of a program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.

This issue is an attempt at driving consolidation of Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.

• Transfer of Bertrand's postulate to CoqPrime bertrand#18
• Merging fiat-crypto utilities into coqutil? mit-plv/coqutil#55
• Transfer general Instances.v lemma to Stdlib aac-tactics#123
• Std lib ommisions corn#58
• Possible consolidation with mathcomp-finmap arthuraa/extructures#22
• Please remove the copy of ssrZ (or rename it) jasmin-lang/coqword#15
• Integration to mathcomp thery/grobner#1
• Consolidation after inclusion of matrix canonical forms coqeal#55
• Additional MMaps implementations using efficient trees coq-mmaps#8
• Refinement of MathComp matrices and matrix operations coqeal#72
• Propagate finmap results to upstream graph-theory#29
• Propagating general results upstream thery/mathcomp-extra#2
• Upstream integration of ALEA changes math-comp/Coq-Combi#2

[Zimmi48]

Related to this project, it would be really useful to produce a mapping of the content of the packages in the Coq ecosystem (similar to how the Lean community does it for mathlib) so that we have an overview of the available results and how the package boundaries are a good match or not with the results these packages contain.

[andres-erbsen]

Additional candidates for consolidation are the utility libraries of Fiat Cryptography and Bedrock2. There is an issue about consolidating them with each other here. Both projects are on Coq CI and actively maintained. Fiat Cryptography already uses Coqprime so consolidation between them would have immediate benefits.

[spitters]

Corn: https://github.com/coq-community/corn/tree/master/stdlib_omissions
Extructures and finmap: coq/platform#61 (comment)
Coq word:
https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/unsigned.20integer.20library.20using.20Cyclic.3F

[SnarkBoojum]

Some projects have additions for stdlib ; stdpp is a whole project of it, corn has a stdlib_omissions directory... that's just from the top of my head.

[spitters]

@andres-erbsen What is the status of https://github.com/mit-plv/coqutil/ ? It does not seem to come with opam files.
Would it be worth including it in platform? Or should it be refactored? It looks like part of it could be included into coq-prime, or at least should have a common home.

[palmskog]

@spitters coq-coqutil.0.0.2 was the in latest Coq Platform extended level.

However, I don't think it was included by itself, but rather as a dependency for Fiat Crypto (which had some really valuable release engineering to be included in the Platform).

[andres-erbsen]

@spitters I am not sure which parts of coqutil would be a good fit for coqprime, but I am looking to contribute substantially overlapping functionality to the standard library. The two PRs linked right above your message are of this nature. Is there a specific part of coqutil that you would be interested in?

As for opam, coqutil and related repositories do not include opam files because their maintainers do not use opam. @JasonGross did make some opam files at the request of Coq Bench & Coq Platform developers, but I am not sure of the status of these files.

[spitters]

@andres-erbsen I think it's a great start to move such lemmas to the stdlib. Since you mention using modulo arithmetic for machine integers, it might be worth having a peek at the other machine integer projects mentioned here:
https://github.com/coq/coq/pull/17043/files#diff-b656e8beafc96bdf5e12ce145cf875e6b72f2d48810d53642deadc0a373bc889