Skip to content

Make argument-scope-delimiter error by default#21849

Merged
coqbot-app[bot] merged 1 commit intorocq-prover:masterfrom
proux01:warnerror-argument-scope-delimiter
Apr 24, 2026
Merged

Make argument-scope-delimiter error by default#21849
coqbot-app[bot] merged 1 commit intorocq-prover:masterfrom
proux01:warnerror-argument-scope-delimiter

Conversation

@proux01
Copy link
Copy Markdown
Contributor

@proux01 proux01 commented Mar 31, 2026 •
edited
Loading

In order to actually handle this 8.19 deprecation in 9.4.

Overlays (to be merged before the current PR)

@proux01 proux01 added this to the 9.3+rc1 milestone Mar 31, 2026
@proux01 proux01 requested a review from a team as a code owner March 31, 2026 08:57
@proux01 proux01 added kind: cleanup Code removal, deprecation, refactorings, etc. request: full CI Use this label when you want your next push to trigger a full CI. labels Mar 31, 2026
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 31, 2026
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 31, 2026
@proux01 proux01 force-pushed the warnerror-argument-scope-delimiter branch from 080f565 to efc9633 Compare March 31, 2026 09:21
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 31, 2026
@SkySkimmer SkySkimmer self-assigned this Mar 31, 2026
@SkySkimmer SkySkimmer added the needs: overlay This is breaking external developments we track in CI. label Mar 31, 2026
proux01 added a commit to proux01/Mtac2 that referenced this pull request Apr 1, 2026
@proux01
Adapt to rocq-prover/rocq#21849
a2c82ce
@proux01 proux01 mentioned this pull request Apr 1, 2026
Merged
proux01 added a commit to proux01/fiat that referenced this pull request Apr 1, 2026
@proux01
Adapt to rocq-prover/rocq#21849
550258d
@proux01 proux01 mentioned this pull request Apr 1, 2026
Merged
proux01 added a commit to proux01/finmap that referenced this pull request Apr 1, 2026
@proux01
Adapt to rocq-prover/rocq#21849
f49fdc4
@proux01 proux01 mentioned this pull request Apr 1, 2026
Merged
Janno added a commit to Mtac2/Mtac2 that referenced this pull request Apr 1, 2026
@Janno
Merge pull request #429 from proux01/rocq21849
d3115ad 
Adapt to rocq-prover/rocq#21849
proux01 added a commit to math-comp/finmap that referenced this pull request Apr 1, 2026
@proux01
Adapt to rocq-prover/rocq#21849 (#155)
53239c7
proux01 added a commit to rocq-community/fourcolor that referenced this pull request Apr 1, 2026
@proux01
Adapt to rocq-prover/rocq#21849
7fd114d
@proux01 proux01 mentioned this pull request Apr 1, 2026
Merged
proux01 added a commit to proux01/odd-order that referenced this pull request Apr 1, 2026
@proux01
Adapt to rocq-prover/rocq#21849
05751ed
@proux01 proux01 mentioned this pull request Apr 1, 2026
Merged
proux01 added a commit to rocq-community/fourcolor that referenced this pull request Apr 1, 2026
@proux01
Merge pull request #77 from rocq-community/rocq21849
f2fcc83 
Adapt to rocq-prover/rocq#21849
proux01 added a commit to math-comp/odd-order that referenced this pull request Apr 1, 2026
@proux01
Merge pull request #80 from proux01/rocq21849
89503cd 
Adapt to rocq-prover/rocq#21849
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 1, 2026
@proux01 proux01 force-pushed the warnerror-argument-scope-delimiter branch from efc9633 to 634d39d Compare April 1, 2026 13:58
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 1, 2026
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 2, 2026
@proux01 proux01 force-pushed the warnerror-argument-scope-delimiter branch from 634d39d to dd65428 Compare April 2, 2026 06:09
@proux01 proux01 force-pushed the warnerror-argument-scope-delimiter branch from 811b610 to 9a50a82 Compare April 2, 2026 16:15
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 2, 2026
JasonGross pushed a commit to mit-plv/rewriter that referenced this pull request Apr 2, 2026
@proux01 @JasonGross
Adapt to rocq-prover/rocq#21849
f1e4430
JasonGross added a commit to mit-plv/rewriter that referenced this pull request Apr 2, 2026
@proux01 @JasonGross
Adapt to rocq-prover/rocq#21849 (#199)
963487b 
* Adapt to rocq-prover/rocq#21849

* Update Coq dependency version to 8.19

* Update README

---------

Co-authored-by: Jason Gross <jasongross9@gmail.com>
Co-authored-by: Jason Gross <jgross@mit.edu>
samuelgruetter added a commit to mit-plv/bedrock2 that referenced this pull request Apr 3, 2026
@samuelgruetter
Merge pull request #522 from proux01/rocq21849
e7fa959 
Adapt to rocq-prover/rocq#21849
@SkySkimmer SkySkimmer removed the needs: overlay This is breaking external developments we track in CI. label Apr 3, 2026
JasonGross pushed a commit to mit-plv/cross-crypto that referenced this pull request Apr 3, 2026
@proux01
Adapt to rocq-prover/rocq#21849 (#44)
bbd1b2c
JasonGross pushed a commit to JasonGross/neural-net-coq-interp that referenced this pull request Apr 3, 2026
@proux01
Adapt to rocq-prover/rocq#21849 (#95)
6f2c7db
@andres-erbsen
Copy link
Copy Markdown
Contributor

andres-erbsen commented Apr 4, 2026

IIRC the overall plan is to change the bahvior of % to something incompatible. That's fine. But why is the transition path here to error rather than to introduce the new behavior, perhaps with a flag that could make it error instead for porting?

@proux01
Copy link
Copy Markdown
Contributor Author

proux01 commented Apr 4, 2026

That's the usual deprecation process:

  1. In Rocq X.Y, when deprecating, add a warning message, so users know about it (and can typically silence the warning and note to take care of it at some point)
  2. In Rocq X.Y+k (k > 0), turn the flag as error by default, to ensure users who didn't notice do, and still have a release cycle left to act
  3. In Rocq X.Y+k+1, remove the warning and do the actual removal/change

@SkySkimmer
Copy link
Copy Markdown
Contributor

SkySkimmer commented Apr 4, 2026

It's a process we've done before but IDK about usual. And when the change is to something that may be compatible forcing an error does not seem useful.

proux01 added a commit to proux01/category-theory that referenced this pull request Apr 4, 2026
@proux01
Adapt to rocq-prover/rocq#21849
a777574
JasonGross pushed a commit to mit-plv/fiat-crypto that referenced this pull request Apr 5, 2026
@proux01
Adapt to rocq-prover/rocq#21849 (#2296)
7a7a7db
jwiegley added a commit to jwiegley/category-theory that referenced this pull request Apr 5, 2026
@jwiegley
Merge pull request #171 from proux01/rocq21849
ceafa54 
Adapt to rocq-prover/rocq#21849
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 6, 2026
@proux01 proux01 force-pushed the warnerror-argument-scope-delimiter branch from 9a50a82 to a8ec73c Compare April 6, 2026 14:50
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 6, 2026
@proux01 proux01 mentioned this pull request Apr 7, 2026
Merged
JasonGross pushed a commit to JasonGross/neural-net-coq-interp that referenced this pull request Apr 7, 2026
@proux01
Adapt to rocq-prover/rocq#21849 (#96)
98a2540
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 7, 2026
@proux01 proux01 force-pushed the warnerror-argument-scope-delimiter branch from a8ec73c to 6672ea9 Compare April 7, 2026 07:35
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 7, 2026
@proux01
Copy link
Copy Markdown
Contributor Author

proux01 commented Apr 13, 2026

@andres-erbsen, @JasonGross, @samuelgruetter please ensure the bedrock2 overlay gets propagated through all the submodules, it has been merged more than a week ago now

@proux01
Make argument-scope-delimiter error by default
a3c4ca6 
In order to actually handle this 8.19 deprecation in 9.4.
@proux01
Copy link
Copy Markdown
Contributor Author

proux01 commented Apr 17, 2026

Thanks! CI is finally green, this can be merged

@SkySkimmer
Copy link
Copy Markdown
Contributor

SkySkimmer commented Apr 20, 2026

So do we really want this error-by-default step or should we directly change to the final desired behaviour instead?

@proux01
Copy link
Copy Markdown
Contributor Author

proux01 commented Apr 20, 2026

The semantics change could be subtly breaking scripts and be painful to debug I guess, so I'd rather go through the error by default step in 9.3 before changing the semantics in 9.4.

@SkySkimmer
Copy link
Copy Markdown
Contributor

SkySkimmer commented Apr 24, 2026

still not super convinced but @coqbot merge now

This was referenced Apr 24, 2026
Merged
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@SkySkimmer SkySkimmer SkySkimmer approved these changes

Assignees

@SkySkimmer SkySkimmer

Labels

kind: cleanup Code removal, deprecation, refactorings, etc.

Projects

None yet

Milestone

9.3+rc1

Development

Successfully merging this pull request may close these issues.

3 participants

@proux01 @andres-erbsen @SkySkimmer