Skip to content
Docker CI

Require MathComp 2.5 #53

Sign in to view logs

Require MathComp 2.5

Require MathComp 2.5 #53

Triggered via pull request July 13, 2026 14:57
@pi8027pi8027
opened #130
require-mc-2.5
Status Success
Total duration 7m 19s
Artifacts –

docker-action.yml

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

Annotations

66 warnings
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
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/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-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/monalg.v#L14
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:rocq-prover-9.0): src/monalg.v#L14
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
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/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
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
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/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/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/monalg.v#L14
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): src/monalg.v#L14
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
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/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-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