Docker CI

Require Rocq 9.0 and update Docker CI #137

Sign in to view logs

Triggered via pull request July 29, 2026 12:23

pi8027

opened #72

require-rocq-9.0

Status Failure

Total duration 17m 46s

Artifacts –

docker-action.yml

on: pull_request

Matrix: build

Annotations

25 warnings

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.6.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.6.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.6.0-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: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.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): examples/test_algebra.v#L1

"From Coq" has been replaced by "From Stdlib".

build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): examples/test_ssreflect.v#L1

"From Coq" has been replaced by "From Stdlib".

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): examples/test_algebra.v#L1

"From Coq" has been replaced by "From Stdlib".

build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): examples/test_ssreflect.v#L1

"From Coq" has been replaced by "From Stdlib".

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/zify_ssreflect.v#L246

The 'rewrite' tactic has been renamed 'rw'.

build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/zify_ssreflect.v#L245

The 'rewrite' tactic has been renamed 'rw'.

build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/zify_ssreflect.v#L235

The 'rewrite' tactic has been renamed 'rw'.

build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/zify_ssreflect.v#L226

The 'rewrite' tactic has been renamed 'rw'.

build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/zify_ssreflect.v#L226

The 'rewrite' tactic has been renamed 'rw'.

build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/zify_ssreflect.v#L222

The 'rewrite' tactic has been renamed 'rw'.

build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/zify_ssreflect.v#L217

The 'rewrite' tactic has been renamed 'rw'.

build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/zify_ssreflect.v#L182

The 'rewrite' tactic has been renamed 'rw'.

build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/zify_ssreflect.v#L177

The 'rewrite' tactic has been renamed 'rw'.

build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/zify_ssreflect.v#L164

The 'rewrite' tactic has been renamed 'rw'.

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.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.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/