Stream: Coq devs & plugin devs

Topic: looking for assignee

Gaëtan Gilbert (Dec 14 2022 at 09:08):

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

Gaëtan Gilbert (Apr 03 2023 at 09:26):

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

Gaëtan Gilbert (May 26 2023 at 11:08):

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

Gaëtan Gilbert (May 31 2023 at 10:10):

ping

Enrico Tassi (May 31 2023 at 11:04):

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

Gaëtan Gilbert (Jun 13 2023 at 12:20):

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

Gaëtan Gilbert (Jun 21 2023 at 10:27):

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

Karl Palmskog (Jul 13 2023 at 15:44):

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

Karl Palmskog (Jul 17 2023 at 14:39):

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

Jason Gross (Jul 17 2023 at 16:16):

Merged!

Gaëtan Gilbert (Sep 21 2023 at 13:32):

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

Gaëtan Gilbert (Oct 04 2023 at 14:14):

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

Gaëtan Gilbert (Oct 04 2023 at 14:28):

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

Gaëtan Gilbert (Nov 21 2023 at 15:06):

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

Emilio Jesús Gallego Arias (Dec 08 2023 at 14:23):

• https://github.com/coq/coq/pull/18360
• https://github.com/coq/coq/pull/18359

Gaëtan Gilbert (Dec 08 2023 at 15:06):

merged one, the other needs rebase

Emilio Jesús Gallego Arias (Dec 08 2023 at 15:26):

Thanks!

Gaëtan Gilbert (Mar 12 2024 at 15:48):

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)

Gaëtan Gilbert (Mar 21 2024 at 15:52):

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

Gaëtan Gilbert (Mar 28 2024 at 13:51):

ping

Pierre Rousselin (Jun 03 2024 at 08:55):

This one removes Include Type and changes slightly the grammar:
https://github.com/coq/coq/pull/18482

Gaëtan Gilbert (Jun 03 2024 at 08:58):

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

Pierre Rousselin (Jun 03 2024 at 09:07):

Yes, I have added it as a test.

Gaëtan Gilbert (Jun 03 2024 at 09:12):

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

Pierre Roux (Jun 03 2024 at 12:45):

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

Pierre Rousselin (Jun 03 2024 at 13:51):

The Include Type command has been deprecated since 8.3.

Pierre Roux (Jun 03 2024 at 13:58):

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.

Pierre Roux (Jun 04 2024 at 11:09):

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.

Gaëtan Gilbert (Jun 04 2024 at 11:32):

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

Gaëtan Gilbert (Jun 04 2024 at 11:32):

we can remove the old syntax immediately after branch

Pierre Roux (Jun 04 2024 at 11:57):

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

Pierre Rousselin (Jun 04 2024 at 13:37):

I extracted the positive part here.

Pierre Rousselin (Jun 04 2024 at 13:38):

(Hopefully without breaking everything, though this rebase --onto felt dark-magicky to me).

Gaëtan Gilbert (Jun 04 2024 at 13:52):

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

Hugo Herbelin (Jun 05 2024 at 14:41):

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?).

Emilio Jesús Gallego Arias (Jun 07 2024 at 13:54):

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

Hugo Herbelin (Jul 04 2024 at 07:18):

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)
  • #19296 Fixes #7913: fixpoint with decreasing argument hidden behind a definition
• #19029 Experiment the addition of sealed/unsealed attributes (part of CEP #42)

Gaëtan Gilbert (Sep 11 2024 at 11:21):

https://github.com/coq/coq/pull/19513
https://github.com/coq/coq/pull/19426

Enrico Tassi (Sep 11 2024 at 12:17):

done

Andres Erbsen (Sep 18 2024 at 13:43):

stdlib PRs:
https://github.com/coq/coq/pull/19515
https://github.com/coq/coq/pull/19483

Pierre Roux (Sep 19 2024 at 09:21):

https://github.com/coq/coq/pull/19563 (trivial doc update)
https://github.com/coq/coq/pull/19519 (should be easy too, mostly removing deprecations that were turned as error in previous version)

Last updated: Oct 13 2024 at 01:02 UTC