https://github.com/coq/coq/pull/16817

https://github.com/coq/coq/pull/16970

https://github.com/coq/coq/pull/17282

https://github.com/coq/coq/pull/17605

https://github.com/coq/coq/pull/17616

https://github.com/coq/coq/pull/17587

https://github.com/coq/coq/pull/17585

ping

Sorry I'm super busy with CoqWS 2023, but next week I'll try to help more.

https://github.com/coq/coq/pull/17587

https://github.com/coq/coq/pull/17587 is not a complicated or controversial PR, anyone can assign

would be really grateful for a full CI run here: https://github.com/coq/coq/pull/17851

looking for assignee for a new small CI addition: https://github.com/coq/coq/pull/17851 - builds fine, should only add 20-30s to total CI time

Merged!

https://github.com/coq/coq/pull/13071 (ltac2)

https://github.com/coq/coq/pull/17503

also https://github.com/coq/coq/pull/18110 is trivial

easy:

- https://github.com/coq/coq/pull/18310
- https://github.com/coq/coq/pull/18271
- https://github.com/coq/coq/pull/18264
- https://github.com/coq/coq/pull/18249

a bit complicated (test suite)

https://github.com/coq/coq/pull/18213

merged one, the other needs rebase

Thanks!

https://github.com/coq/coq/pull/18549 (easy)

https://github.com/coq/coq/pull/18299

https://github.com/coq/coq/pull/18536 (easy)

https://github.com/coq/coq/pull/18641

https://github.com/coq/coq/pull/18700

https://github.com/coq/coq/pull/18706

https://github.com/coq/coq/pull/18728 (easy)

https://github.com/coq/coq/pull/18747 (easy)

https://github.com/coq/coq/pull/18299 anyone?

ping

This one removes `Include Type`

and changes slightly the grammar:

https://github.com/coq/coq/pull/18482

did the problem which blocked https://github.com/coq/coq/pull/11876 get solved?

Yes, I have added it as a test.

shouldn't we have a version where the alternative works before removing Include Type even if it was deprecated earlier?

The compatibility policy is "should be always possible to compile on at least two successive versions". Is it the case?

The `Include Type`

command has been deprecated since 8.3.

Sure the question is: is there something that was feasible in 8.19, will be in 8.20 if we merge but no common code that would work in both 8.19 and 8.20? In which case we need to introduce the new thing in 8.20 and wait a bit to remove the old deprecated one.

So what's the answer? IIUC, In any case we need to merge something (preferably before June 16th so that it goes in 8.20), the question is whether the old syntax should be kept for a few more versions (despite being deprecated since 8.3) to satisfy the "always exist a code compiling with two successive versions" requirement.

merge https://github.com/coq/coq/pull/18482/commits/ac419407edf86fcbb6f6cea05ebec15bbd234ad3 I guess

we can remove the old syntax immediately after branch

Sounds good, @Pierre Rousselin can you please split the PR in two (one to be merged before the branch and one just after)

I extracted the positive part here.

(Hopefully without breaking everything, though this `rebase --onto`

felt dark-magicky to me).

for small numbers of commits using cherry pick may feel less magical than rebase

A list of PRs a priori ready on my side and looking for an assignee, with 8.20 in mind:

Design PRs:

- #18878 addresses an open question about the implicit
`measure`

argument of`Program Fixpoint`

: should it be considered implicit even with`@`

or not. I don't know the opinion of users and the intent of the developer of Program Fixpoint, but a choice should be made (in the direction of #18878 or not) and documented (cc @Matthieu Sozeau ) (if validated, will need overlays). - #18960 makes systematic the static check of correctness of the
`@{univs}`

clause in interactive declaration (previously, it was done only for`Theorem`

). There is an underlying design choice about whether monomorphic universes in obligations are supposed to be taken in charge by the`@{univs}`

annotation of the main definition.

Fixes, features:

- #18929 is a clear fix of
`Program`

's pattern-matching compilation. I guess it should go in (@Matthieu Sozeau, you're the canonical assignee, if ever you find some time). - #19054 is a "fix" of pretyping evaluation in the presence of conversion problems (@Gaëtan Gilbert, would you continue to look at it?).

Otherwise, here are also two ready cleanup PRs (not so critical for 8.20, but helpful to reduce the chain of PR dependencies):

- #19108 is a simple intermediate technical PR to avoid a too long list of commits in the merge of the different execution paths of
`Fixpoint`

(@Pierre-Marie Pédrot, would you like to assign?). - #19105 first step in merging
`Fixpoint`

execution paths (@Pierre-Marie Pédrot, would you continue looking at it?).

An easy one here https://github.com/coq/coq/pull/19135

If ever useful, here is the current flow of dependencies of my PRs on `declare.ml`

(CEPS #42 and #89)

- #19260 Move code for interactive definitions close to the one for non interactive definitions
- #19301 Unifying the syntax of Definition, Theorem, Fixpoint and CoFixpoint (CEP #42)

- #19091 Use multiple statements to implement interactive fixpoints
- #19092 Better integration of Derive in declare.ml + fix of #18951
- #19295 Extend Derive with an arbitrary long sequence of dependencies

- #19031 A common execution path for universe restriction + universe declaration check
- #19320 Factorization of close_proof and close_future_proof in declare.ml
- #19322 Factorizing universe treatment for Definition, Theorem and Fixpoint (part of CEP #89)

- #19320 Factorization of close_proof and close_future_proof in declare.ml
- #19296 Fixes #7913: fixpoint with decreasing argument hidden behind a definition

- #19092 Better integration of Derive in declare.ml + fix of #18951
- #19029 Experiment the addition of sealed/unsealed attributes (part of CEP #42)

Last updated: Aug 03 2024 at 00:02 UTC