Skip to content
Docker CI

Address the deprecation warnings introduced in MathComp <= 2.4 #235

Sign in to view logs

Address the deprecation warnings introduced in MathComp <= 2.4

Address the deprecation warnings introduced in MathComp <= 2.4 #235

Triggered via pull request July 21, 2026 12:25
@proux01proux01
synchronize #106
deprecation_mc2.4
Status Success
Total duration 19m 34s
Artifacts –

docker-action.yml

on: pull_request
Matrix: build
Fit to window
Zoom out
Zoom in

Annotations

78 warnings
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0)
Node.js 20 is deprecated. The following actions target Node.js 20 but are being forced to run on Node.js 24: actions/checkout@v4. For more information see: https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): theories/abel.v#L1331
Notation ivt_sign is deprecated since mathcomp-real-closed 1.1.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): theories/abel.v#L1329
Notation ivt_sign is deprecated since mathcomp-real-closed 1.1.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): theories/abel.v#L1327
Notation ivt_sign is deprecated since mathcomp-real-closed 1.1.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): theories/xmathcomp/real_closed_ext.v#L43
Notation rolle is deprecated since mathcomp-real-closed 2.1.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): theories/xmathcomp/various.v#L165
HB: no new instance is generated
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1)
Node.js 20 is deprecated. The following actions target Node.js 20 but are being forced to run on Node.js 24: actions/checkout@v4. For more information see: https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): theories/abel.v#L1331
Notation ivt_sign is deprecated since mathcomp-real-closed 1.1.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): theories/abel.v#L1329
Notation ivt_sign is deprecated since mathcomp-real-closed 1.1.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): theories/abel.v#L1327
Notation ivt_sign is deprecated since mathcomp-real-closed 1.1.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): theories/xmathcomp/real_closed_ext.v#L43
Notation rolle is deprecated since mathcomp-real-closed 2.1.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): theories/xmathcomp/various.v#L165
HB: no new instance is generated
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1)
Node.js 20 is deprecated. The following actions target Node.js 20 but are being forced to run on Node.js 24: actions/checkout@v4. For more information see: https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): theories/xmathcomp/various.v#L731
Reference multiplicative is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): theories/xmathcomp/various.v#L292
Notation Num.conj_op is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): theories/xmathcomp/various.v#L290
Notation Num.conj_op is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): theories/xmathcomp/various.v#L165
HB: no new instance is generated
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): theories/xmathcomp/various.v#L165
Notation isMulGroup.Build is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): theories/xmathcomp/char0.v#L76
Notation GRing.isAdditive.Build is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): theories/xmathcomp/char0.v#L64
Reference multiplicative is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): theories/xmathcomp/char0.v#L50
Reference additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): theories/xmathcomp/various.v#L2
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): theories/xmathcomp/char0.v#L2
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0)
Node.js 20 is deprecated. The following actions target Node.js 20 but are being forced to run on Node.js 24: actions/checkout@v4. For more information see: https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): theories/xmathcomp/various.v#L731
Reference multiplicative is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): theories/xmathcomp/various.v#L292
Notation Num.conj_op is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): theories/xmathcomp/various.v#L290
Notation Num.conj_op is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): theories/xmathcomp/various.v#L165
HB: no new instance is generated
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): theories/xmathcomp/various.v#L165
Notation isMulGroup.Build is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): theories/xmathcomp/char0.v#L76
Notation GRing.isAdditive.Build is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): theories/xmathcomp/char0.v#L64
Reference multiplicative is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): theories/xmathcomp/char0.v#L50
Reference additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): theories/xmathcomp/various.v#L2
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): theories/xmathcomp/char0.v#L2
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.0)
Node.js 20 is deprecated. The following actions target Node.js 20 but are being forced to run on Node.js 24: actions/checkout@v4. For more information see: https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/xmathcomp/char0.v#L64
Reference multiplicative is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/xmathcomp/char0.v#L50
Reference additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/xmathcomp/various.v#L3
Library File mathcomp.field.all_field is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/xmathcomp/char0.v#L2
Library File mathcomp.field.all_field is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/xmathcomp/various.v#L2
Library File mathcomp.solvable.all_solvable is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/xmathcomp/various.v#L2
Library File mathcomp.algebra.all_algebra is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/xmathcomp/char0.v#L2
Library File mathcomp.algebra.all_algebra is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/xmathcomp/various.v#L2
Library File mathcomp.finite_group.all_fingroup is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/xmathcomp/various.v#L2
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/xmathcomp/char0.v#L2
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.2)
Node.js 20 is deprecated. The following actions target Node.js 20 but are being forced to run on Node.js 24: actions/checkout@v4. For more information see: https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/
build (mathcomp/mathcomp-dev:rocq-prover-9.2): theories/xmathcomp/char0.v#L48
Use of "Notation" keyword for abbreviations is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-9.2): theories/xmathcomp/char0.v#L13
Use of "Notation" keyword for abbreviations is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-9.2): theories/xmathcomp/various.v#L3
Library File mathcomp.field.all_field is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.2): theories/xmathcomp/char0.v#L2
Library File mathcomp.field.all_field is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.2): theories/xmathcomp/various.v#L2
Library File mathcomp.solvable.all_solvable is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.2): theories/xmathcomp/various.v#L2
Library File mathcomp.algebra.all_algebra is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.2): theories/xmathcomp/char0.v#L2
Library File mathcomp.algebra.all_algebra is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.2): theories/xmathcomp/various.v#L2
Library File mathcomp.finite_group.all_fingroup is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.2): theories/xmathcomp/various.v#L2
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.2): theories/xmathcomp/char0.v#L2
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-dev)
Node.js 20 is deprecated. The following actions target Node.js 20 but are being forced to run on Node.js 24: actions/checkout@v4. For more information see: https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/xmathcomp/char0.v#L25
The 'rewrite' tactic has been renamed 'rw'.
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/xmathcomp/char0.v#L13
Use of "Notation" keyword for abbreviations is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/xmathcomp/various.v#L3
Library File mathcomp.field.all_field is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/xmathcomp/char0.v#L2
Library File mathcomp.field.all_field is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/xmathcomp/various.v#L2
Library File mathcomp.solvable.all_solvable is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/xmathcomp/various.v#L2
Library File mathcomp.algebra.all_algebra is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/xmathcomp/char0.v#L2
Library File mathcomp.algebra.all_algebra is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/xmathcomp/various.v#L2
Library File mathcomp.finite_group.all_fingroup is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/xmathcomp/various.v#L2
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/xmathcomp/char0.v#L2
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.1)
Node.js 20 is deprecated. The following actions target Node.js 20 but are being forced to run on Node.js 24: actions/checkout@v4. For more information see: https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/xmathcomp/char0.v#L64
Reference multiplicative is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/xmathcomp/char0.v#L50
Reference additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/xmathcomp/various.v#L3
Library File mathcomp.field.all_field is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/xmathcomp/char0.v#L2
Library File mathcomp.field.all_field is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/xmathcomp/various.v#L2
Library File mathcomp.solvable.all_solvable is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/xmathcomp/various.v#L2
Library File mathcomp.algebra.all_algebra is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/xmathcomp/char0.v#L2
Library File mathcomp.algebra.all_algebra is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/xmathcomp/various.v#L2
Library File mathcomp.finite_group.all_fingroup is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/xmathcomp/various.v#L2
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/xmathcomp/char0.v#L2
Library File mathcomp.ssreflect.all_ssreflect is deprecated