coq / ceps

Coq Enhancement Proposals

Coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

Installation

Please see https://coq.inria.fr/download. Information on how to build and install from sources can be found in INSTALL.md.

Documentation

The sources of the documentation can be found in directory doc. See doc/README.md to learn more about the documentation, in particular how to build it. The documentation of the last released version is available on the Coq web site at coq.inria.fr/documentation. See also Cocorico (the Coq wiki), and the Coq FAQ, for additional user-contributed documentation.

The documentation of the master branch is continuously deployed. See:

• Reference Manual (master)
• Documentation of the standard library (master)
• Documentation of the ML API (master)

Changes

The Recent changes chapter of the reference manual explains the differences and the incompatibilities of each new version of Coq. If you upgrade Coq, please read it carefully as it contains important advice on how to approach some problems you may encounter.

Questions and discussion

We have a number of channels to reach the user community and the development team:

• Our Zulip chat, for casual and high traffic discussions.
• Our Discourse forum, for more structured and easily browsable discussions and Q&A.
• Our historical mailing list, the Coq-Club.

See also coq.inria.fr/community, which lists several other active platforms.

Bug reports

Please report any bug / feature request in our issue tracker.

To be effective, bug reports should mention the OCaml version used to compile and run Coq, the Coq version (coqtop -v), the configuration used, and include a complete source example leading to the bug.

Contributing to Coq

Guidelines for contributing to Coq in various ways are listed in the contributor's guide.

Information about release plans is at https://github.com/coq/coq/wiki/Release-Plan

Supporting Coq

Help the Coq community grow and prosper by becoming a sponsor! The Coq Consortium can establish sponsorship contracts or receive donations. If you want to take an active role in shaping Coq's future, you can also become a Consortium member. If you are interested, please get in touch!

ceps's Issues

Discuss the Coq Platform naming scheme having the multiple package pick concept in mind

The Coq Platform naming scheme suggested in (https://github.com/coq/ceps/blob/master/text/052-platform-release-cycle.md#platform) was concluded on before Coq Platform supported several picks in one release. This development requires to discuss the naming again.

Currently a specific delivery of Coq - say via a Windows installer - has 3 version components:

• the version of the Coq Platform release, e.g. 2022.09.0
• the version of Coq - e.g. 8.16. I leave away the minor version of Coq here
• the version of the package pick for the version of Coq, e.g. 2022.09+beta1 (currently named 2922.09~beta1)

It is common that there are two package picks for one version of Coq - the one with which this version of Coq was originally released, and one which is as close as possible to the initial package pick of the next release of Coq. The idea behind this is to make it possible to first update the package pick and then the version of Coq for own developments. In my experience it depends on the project and the changes in Coq what is easier.

It is also so that all older versions of Coq (since Coq Platform exists), including the above two package picks - are re-released with each release of Coq Platform. What changes here are OS compatibility fixes and possibly Coq fixes. E.g. one could with Coq Platform 2022.09 build an MacOS installer for Coq 8.14, which is compatible with MacOS 10.13 - the original installer required 10.15 or so. Or there was a change in the C standard library in Ubuntu in 20.04 which made older OCaml incompatible with it. But from a Coq usage point of view, say in the view of reproduction of research artifacts, such a rerelease should behave identical to the original release - it just has somehow extended operating system support. Also pure bug fix releases of Coq are typically have the same combination of Coq+package pick version, since they should be 100% compatible - only the Coq Platform release changes (say from 2022.09.0 to 2022.09.1 ot maybe something completely different if the fix is done much later than the original release as e.g. in the case of the OCaml C library issue.

The main question is, if the current naming like

Coq-Platform-release-2022.09.0-version~8.16~2022.09~beta1-Windows-x86_64.exe

for an installer is appropriate, or if we can come up with a better naming scheme.

French name change

Is there a consensus as to what "The Rocq Prover" translates to in French ?
"Le prouveur Rocq", "Rocq", "The Rocq prover", still Coq ?

Best,
MRandl

Co-Evolution of Evars

Let me start the discussion...

I like a lot your idea, as emphasized in Examples 1 and 2. It looks to me very natural and it is not without reminding me some theoretical issues raised by the introduction of fun patterns, as well as similar co-evolution of "match" typing that we can find in Jaber, Lewertowski, Pédrot, Sozeau and Tabareau's recent paper on call-by-name forcing in type theory.

This does not seem unrelated either to the invertibility of negative rules as emphasized in calculi with focusing, namely that "destruct" (even in the case of more-than-2-constructors inductive types) is a rule of rearrangement of the context (see e.g. the use of disjunctive patterns destructing the context in Zeilberger or Munch-Maccagnoni's works, to cite names I know).

On the opposite side, I'm less convinced by Example 3 but I will think more at it [this paragraph has been edited afterwards].

On the implementation side, there are several directions possible. Personally, I'm used with ML programming so I would lean to suggest to add a line for co-evolution of evars somewhere in Tactics.apply_induction_in_context or so, but maybe this can be tried with less efforts in Ltac or MetaCoq.

API for reduction-insenstive constr traversal

I'm reviewing coq/coq#12218, and seeing a lot of code that I believe will be wrong in the presence of casts, let-ins, and reducible matches (if true then ... else ...) in surprising places (like at top-level in the types of constructors). Coq also has a number of performance issues in the presence of nested let ... in ...s, e.g., around computation of implicit arguments.

This suggests to me that Coq should have a term-traversal API which is insensitive to some sorts of reduction, much like EConstr is insensitive to evar-normalization. Ideally it would not incur overhead (it should add let-binders to the context rather than substituting them, it should, perhaps, perform beta-reduction by binding the argument in a let binder and going under the binder), and be much more light-weight than EConstr. For example, it might just be a kind function which updates the local environment and returns both the context and the kind of term modulo whatever you ask it to be modulo.

Said another way, this would be an API for traversing fully reduced terms (or perhaps βιζ-normal terms) without having to perform expensive substitutions in parts of the terms that you don't care about.

I haven't turned this into an actual CEP because I don't have a good enough sense of this, but I'd be interested in comments and/or starting a discussion here.

cc @ppedrot @andres-erbsen

Proposed name Rocq might clash with Roc

In the Coq roadmap, the new name is Rocq, which might get confusing as another language exists with a name that's pronounced the same and is almost identical, Roc.