Skip to content
Docker CI

Update CI: Add Rocq 9.2 #49

Sign in to view logs

Update CI: Add Rocq 9.2

Update CI: Add Rocq 9.2 #49

Triggered via pull request June 19, 2026 11:03
@pi8027pi8027
opened #129
ci
Status Success
Total duration 19m 23s
Artifacts –

docker-action.yml

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

Annotations

88 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): src/monalg.v#L14
Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/monalg.v#L14
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/monalg.v#L14
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/monalg.v#L14
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ f set _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
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): src/monalg.v#L14
Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/monalg.v#L14
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/monalg.v#L14
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/monalg.v#L14
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/xfinmap.v#L5
Notations "[ f set _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/xfinmap.v#L5
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/xfinmap.v#L5
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
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): src/monalg.v#L14
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): src/monalg.v#L14
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): src/freeg.v#L583
Reference additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): src/freeg.v#L573
Reference additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): src/xfinmap.v#L5
Notations "[ f set _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): src/xfinmap.v#L5
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): src/xfinmap.v#L5
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
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): src/monalg.v#L14
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): src/freeg.v#L587
Notation GRing.isAdditive.Build is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): src/freeg.v#L583
Reference additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): src/freeg.v#L573
Reference additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ f set _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
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): src/monalg.v#L14
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp-dev:rocq-prover-9.2): src/monalg.v#L14
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:rocq-prover-9.2): src/ssrcomplements.v#L173
In term, tolerating this expression at a higher level than expected
build (mathcomp/mathcomp-dev:rocq-prover-9.2): src/freeg.v#L42
Use of "Notation" keyword for abbreviations is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-9.2): src/xfinmap.v#L5
Notations "[ f set _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp-dev:rocq-prover-9.2): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:rocq-prover-9.2): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:rocq-prover-9.2): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:rocq-prover-9.2): src/xfinmap.v#L5
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp-dev:rocq-prover-9.2): src/xfinmap.v#L5
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
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): src/monalg.v#L14
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:rocq-prover-9.1): src/monalg.v#L14
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp-dev:rocq-prover-9.1): src/monalg.v#L14
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:rocq-prover-9.1): src/freeg.v#L573
Reference additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.1): src/xfinmap.v#L5
Notations "[ f set _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp-dev:rocq-prover-9.1): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:rocq-prover-9.1): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:rocq-prover-9.1): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:rocq-prover-9.1): src/xfinmap.v#L5
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp-dev:rocq-prover-9.1): src/xfinmap.v#L5
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
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): src/ssrcomplements.v#L24
The 'rewrite' tactic has been renamed 'rw'.
build (mathcomp/mathcomp-dev:rocq-prover-dev): src/xfinmap.v#L23
The 'rewrite' tactic has been renamed 'rw'.
build (mathcomp/mathcomp-dev:rocq-prover-dev): src/xfinmap.v#L23
The 'rewrite' tactic has been renamed 'rw'.
build (mathcomp/mathcomp-dev:rocq-prover-dev): src/xfinmap.v#L22
The 'rewrite' tactic has been renamed 'rw'.
build (mathcomp/mathcomp-dev:rocq-prover-dev): src/xfinmap.v#L5
Notations "[ f set _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp-dev:rocq-prover-dev): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:rocq-prover-dev): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:rocq-prover-dev): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:rocq-prover-dev): src/xfinmap.v#L5
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp-dev:rocq-prover-dev): src/xfinmap.v#L5
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
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): src/monalg.v#L14
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:rocq-prover-9.0): src/freeg.v#L587
Notation GRing.isAdditive.Build is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.0): src/freeg.v#L583
Reference additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.0): src/freeg.v#L573
Reference additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ f set _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp-dev:rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp-dev:rocq-prover-9.0): src/xfinmap.v#L5
Notations "[ fset _ | _ : _ in _ ]" defined at level 0