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

Consolidation of generally useful Coq code into Coq Platform projects #143

Open palmskog opened 1 year ago

palmskog commented 1 year ago

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.

Zimmi48 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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

SnarkBoojum commented 1 year ago

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 commented 1 year ago

@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 commented 1 year ago

@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 commented 1 year ago

@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 commented 1 year ago

@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