coq / ceps Goto Github PK

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.

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

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.

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.

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