Skip to content
Docker CI

update for 2.5 #10

Sign in to view logs

update for 2.5

update for 2.5 #10

Triggered via pull request July 1, 2026 13:22
@therythery
opened #2
v2_2
Status Success
Total duration 3m 40s
Artifacts –

docker-action.yml

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

Annotations

11 warnings
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): AnIntroductionToSmallScaleReflectionInCoq/section6.v#L375
Ignoring canonical projection to vrefl_rect by isSub.SubK_subproof
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): AnIntroductionToSmallScaleReflectionInCoq/section6.v#L375
Projection value has no head constant:
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): AnIntroductionToSmallScaleReflectionInCoq/section7.v#L18
Reference muln_rec is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): AnIntroductionToSmallScaleReflectionInCoq/section6.v#L21
HB: no new instance is generated
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): AnIntroductionToSmallScaleReflectionInCoq/section6.v#L21
Ignoring canonical projection to cons by isFinite.enum_subdef in
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): AnIntroductionToSmallScaleReflectionInCoq/section4.v#L108
Not a truly recursive fixpoint.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): AnIntroductionToSmallScaleReflectionInCoq/section4.v#L98
Not a truly recursive fixpoint.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): AnIntroductionToSmallScaleReflectionInCoq/section4.v#L74
Not a truly recursive fixpoint.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): AnSsreflectTutorial/tutorial_Gonthier_LeRoux.v#L242
Reference subn_rec is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): AnSsreflectTutorial/tutorial_Gonthier_LeRoux.v#L2
Loading Stdlib without prefix is deprecated.