Skip to content

Cleanup legacy-loading-removed#21852

Merged
coqbot-app[bot] merged 1 commit into
rocq-prover:masterfrom
proux01:warnerror-legacy-loading
Apr 24, 2026
Merged

Cleanup legacy-loading-removed#21852
coqbot-app[bot] merged 1 commit into
rocq-prover:masterfrom
proux01:warnerror-legacy-loading

Conversation

@proux01

@proux01 proux01 commented Mar 31, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

@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 09:09
@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-legacy-loading branch from 90c6edb to 590f266 Compare March 31, 2026 10:52
@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 mentioned this pull request Mar 31, 2026
Merged
proux01 added a commit to rocq-community/atbr that referenced this pull request Mar 31, 2026
@proux01
Adapt to rocq-prover/rocq#21852
9df8793
@proux01 proux01 mentioned this pull request Mar 31, 2026
Merged
SkySkimmer added a commit to rocq-community/atbr that referenced this pull request Mar 31, 2026
@SkySkimmer
Merge pull request #46 from rocq-community/rocq21852
aedf700 
Adapt to rocq-prover/rocq#21852
@SkySkimmer SkySkimmer self-assigned this Mar 31, 2026
SkySkimmer pushed a commit to HoTT/Coq-HoTT that referenced this pull request Mar 31, 2026
@proux01
Adapt to rocq-prover/rocq#21852
a36596f
SkySkimmer added a commit to HoTT/Coq-HoTT that referenced this pull request Mar 31, 2026
@SkySkimmer
Merge pull request #2350 from proux01/rocq21852
dfcfc05 
Adapt to rocq-prover/rocq#21852
@SkySkimmer

SkySkimmer commented Mar 31, 2026

Copy link
Copy Markdown
Contributor

Overlays (to be merged before the current overlay)

current overlay -> current PR? ;)

@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/unicoq that referenced this pull request Mar 31, 2026
@proux01
Adapt to rocq-prover/rocq#21852
0f93834
@proux01 proux01 mentioned this pull request Mar 31, 2026
Merged
proux01 added a commit to rocq-community/paramcoq that referenced this pull request Mar 31, 2026
@proux01
Adapt to rocq-prover/rocq#21852
951b888
@proux01 proux01 mentioned this pull request Mar 31, 2026
Merged
proux01 added a commit to rocq-community/paramcoq that referenced this pull request Mar 31, 2026
@proux01
Merge pull request #154 from rocq-community/rocq21852
1af01c4 
Adapt to rocq-prover/rocq#21852
proux01 added a commit to rocq-community/stalmarck that referenced this pull request Mar 31, 2026
@proux01
Adapt to rocq-prover/rocq#21852
55b7b81
@proux01 proux01 mentioned this pull request Mar 31, 2026
Merged
proux01 added a commit to rocq-community/stalmarck that referenced this pull request Mar 31, 2026
@proux01
Merge pull request #33 from rocq-community/rocq21852
b4bf58e 
Adapt to rocq-prover/rocq#21852
proux01 added a commit to proux01/coq-tactician that referenced this pull request Mar 31, 2026
@proux01
Adapt to rocq-prover/rocq#21852
caf8133
@proux01 proux01 mentioned this pull request Mar 31, 2026
Merged
Janno added a commit to unicoq/unicoq that referenced this pull request Apr 1, 2026
@Janno
Merge pull request #109 from proux01/rocq21852
626dd2f 
Adapt to rocq-prover/rocq#21852
@proux01 proux01 removed the needs: overlay This is breaking external developments we track in CI. label Apr 4, 2026
LasseBlaauwbroek added a commit to coq-tactician/coq-tactician that referenced this pull request Apr 12, 2026
@LasseBlaauwbroek
Merge pull request #133 from proux01/coqdev
18d3f54 
Adapt to rocq-prover/rocq#21852
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 13, 2026
@proux01 proux01 force-pushed the warnerror-legacy-loading branch from 590f266 to e0af0b4 Compare April 13, 2026 06:08
@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 13, 2026
@proux01

proux01 commented Apr 13, 2026

Copy link
Copy Markdown
Contributor Author

All overlays merged, CI green, this can be merged

SkySkimmer
SkySkimmer requested changes Apr 20, 2026
View reviewed changes

@SkySkimmer SkySkimmer left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should just be an error (or even stop detecting it and let findlib do whatever it wants with :)

@SkySkimmer SkySkimmer added the needs: progress Work in progress: awaiting action from the author. label Apr 20, 2026
@proux01 proux01 added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: progress Work in progress: awaiting action from the author. labels Apr 20, 2026
@proux01 proux01 force-pushed the warnerror-legacy-loading branch from e0af0b4 to fe50f3a Compare April 20, 2026 13:11
@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 20, 2026
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 20, 2026
@proux01 proux01 force-pushed the warnerror-legacy-loading branch from fe50f3a to 01c34b1 Compare April 20, 2026 13:16
@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 20, 2026
@SkySkimmer SkySkimmer added the needs: changelog entry This should be documented in doc/changelog. label Apr 20, 2026
@SkySkimmer

SkySkimmer commented Apr 20, 2026

Copy link
Copy Markdown
Contributor

could use changelog too

@proux01 proux01 changed the title Turn legacy-loading-removed as error by default Cleanup legacy-loading-removed Apr 20, 2026
@proux01
Remove legacy-loading-removed
20013af 
Deprecated since 9.0
@proux01 proux01 added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: changelog entry This should be documented in doc/changelog. labels Apr 20, 2026
@proux01 proux01 force-pushed the warnerror-legacy-loading branch from 01c34b1 to 20013af Compare April 20, 2026 13:30
@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 20, 2026
@proux01

proux01 commented Apr 21, 2026

Copy link
Copy Markdown
Contributor Author

Should just be an error (or even stop detecting it and let findlib do whatever it wants with :)

Indeed, done, CI green

@SkySkimmer

SkySkimmer commented Apr 24, 2026

Copy link
Copy Markdown
Contributor

@coqbot merge now

@coqbot-app coqbot-app Bot merged commit 31aac9a into rocq-prover:master Apr 24, 2026
9 checks passed
@proux01 proux01 deleted the warnerror-legacy-loading branch April 24, 2026 12:00
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.

2 participants

@proux01 @SkySkimmer