Skip to content

Drop support for Coq 8.20#1853

Merged
affeldt-aist merged 1 commit intomath-comp:masterfrom
proux01:drop820
Mar 3, 2026
Merged

Drop support for Coq 8.20#1853
affeldt-aist merged 1 commit intomath-comp:masterfrom
proux01:drop820

Conversation

@proux01
Copy link
Collaborator

@proux01 proux01 commented Feb 20, 2026

Maybe something we want to do after the next release (this will also enable improving the deprecations by using use=).

Cc @affeldt-aist

@affeldt-aist
Copy link
Member

What about merging it now for the release of 1.16.0?
I am asking because

  • there was a Coq 8.20 related CI problem in another PR Tail expectation formula for L1 random variable #1865 (comment) , I don't get the error and I am not able to reproduce it by recreating an opam environment with Coq 8.20 and MathComp 2.4.0
  • Rocq 9.0 and Rocq.9.1 seem to be both supported, so we abide by the "at least two versions supported" rule

@proux01
Copy link
Collaborator Author

proux01 commented Mar 2, 2026

My reasoning was that if the current master supports 8.20 you may as well do a last release supporting it before dropping it. But if you want to fit #1865 in the release, then it may indded make sense to merge the current PR first. No strong opinion here, in any case the current PR is mergeable so do as you prefer.

@affeldt-aist
Copy link
Member

Thanks for the information. Then unless somebody figures out a solution I think we'll merge before the release.

@affeldt-aist
Copy link
Member

I wonder why the CI triggers "Nix CI for bundle 8.20-2.4.0". Is that intended?
(Or did I mess up the rebase?)

@proux01
Copy link
Collaborator Author

proux01 commented Mar 3, 2026

The importnat part is "pull_request_target" (i.e., master), there is no "pull_request" equivalent. It's a way to make explicit the CI config has changed and its indeed expected to be red.

@affeldt-aist affeldt-aist merged commit 530de63 into math-comp:master Mar 3, 2026
59 of 60 checks passed
@proux01 proux01 deleted the drop820 branch March 3, 2026 12:33
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants