Skip to content
Docker CI

CI #124

Sign in to view logs

CI

CI #124

Triggered via pull request December 9, 2025 15:01
@pi8027pi8027
synchronize #66
ci
Status Failure
Total duration 30m 23s
Artifacts –

docker-action.yml

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

Annotations

73 warnings
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.0): theories/ssrZ.v#L139
Notation GRing.ComRing_hasMulInverse.Build is deprecated
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): theories/ssrZ.v#L123
Notation GRing.Zmodule_isComRing.Build is deprecated
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): theories/ssrZ.v#L48
Notation GRing.Nmodule_isComSemiRing.Build is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/ssrZ.v#L79
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/ssrZ.v#L72
Reference multiplicative is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/ssrZ.v#L65
Reference multiplicative is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/ssrZ.v#L62
Notation GRing.isSemiAdditive.Build is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/ssrZ.v#L58
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/ssrZ.v#L55
Notation GRing.isSemiAdditive.Build is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/ssrZ.v#L51
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/ssrZ.v#L48
Notation GRing.Nmodule_isComSemiRing.Build is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/zify_ssreflect.v#L484
Reference Znumtheory.Zdivide_Zabs_l is deprecated since 9.1.
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/zify_ssreflect.v#L484
Reference Znumtheory.Zdivide_Zabs_l is deprecated since 9.1.
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:2.4.0-rocq-prover-9.1): theories/ssrZ.v#L139
Notation GRing.ComRing_hasMulInverse.Build is deprecated
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): theories/ssrZ.v#L123
Notation GRing.Zmodule_isComRing.Build is deprecated
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): theories/ssrZ.v#L48
Notation GRing.Nmodule_isComSemiRing.Build is deprecated
build (mathcomp/mathcomp:2.4.0-coq-8.20): theories/ssrZ.v#L139
Notation GRing.ComRing_hasMulInverse.Build is deprecated
build (mathcomp/mathcomp:2.4.0-coq-8.20): theories/ssrZ.v#L123
Notation GRing.Zmodule_isComRing.Build is deprecated
build (mathcomp/mathcomp:2.4.0-coq-8.20): theories/ssrZ.v#L48
Notation GRing.Nmodule_isComSemiRing.Build is deprecated
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): theories/ssrZ.v#L86
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): theories/ssrZ.v#L83
Notation GRing.isSemiAdditive.Build is deprecated
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): theories/ssrZ.v#L79
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): theories/ssrZ.v#L72
Reference multiplicative is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): theories/ssrZ.v#L65
Reference multiplicative is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): theories/ssrZ.v#L62
Notation GRing.isSemiAdditive.Build is deprecated
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): theories/ssrZ.v#L58
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): theories/ssrZ.v#L55
Notation GRing.isSemiAdditive.Build is deprecated
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): theories/ssrZ.v#L51
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): theories/ssrZ.v#L48
Notation GRing.Nmodule_isComSemiRing.Build is deprecated
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): theories/ssrZ.v#L86
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): theories/ssrZ.v#L83
Notation GRing.isSemiAdditive.Build is deprecated
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): theories/ssrZ.v#L79
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): theories/ssrZ.v#L72
Reference multiplicative is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): theories/ssrZ.v#L65
Reference multiplicative is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): theories/ssrZ.v#L62
Notation GRing.isSemiAdditive.Build is deprecated
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): theories/ssrZ.v#L58
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): theories/ssrZ.v#L55
Notation GRing.isSemiAdditive.Build is deprecated
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): theories/ssrZ.v#L51
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): theories/ssrZ.v#L48
Notation GRing.Nmodule_isComSemiRing.Build is deprecated
build (mathcomp/mathcomp:2.5.0-coq-8.20): theories/ssrZ.v#L86
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-coq-8.20): theories/ssrZ.v#L83
Notation GRing.isSemiAdditive.Build is deprecated
build (mathcomp/mathcomp:2.5.0-coq-8.20): theories/ssrZ.v#L79
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-coq-8.20): theories/ssrZ.v#L72
Reference multiplicative is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-coq-8.20): theories/ssrZ.v#L65
Reference multiplicative is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-coq-8.20): theories/ssrZ.v#L62
Notation GRing.isSemiAdditive.Build is deprecated
build (mathcomp/mathcomp:2.5.0-coq-8.20): theories/ssrZ.v#L58
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-coq-8.20): theories/ssrZ.v#L55
Notation GRing.isSemiAdditive.Build is deprecated
build (mathcomp/mathcomp:2.5.0-coq-8.20): theories/ssrZ.v#L51
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-coq-8.20): theories/ssrZ.v#L48
Notation GRing.Nmodule_isComSemiRing.Build is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/ssrZ.v#L86
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/ssrZ.v#L83
Notation GRing.isSemiAdditive.Build is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/ssrZ.v#L79
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/ssrZ.v#L72
Reference multiplicative is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/ssrZ.v#L65
Reference multiplicative is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/ssrZ.v#L62
Notation GRing.isSemiAdditive.Build is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/ssrZ.v#L58
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/ssrZ.v#L55
Notation GRing.isSemiAdditive.Build is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/ssrZ.v#L51
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/ssrZ.v#L48
Notation GRing.Nmodule_isComSemiRing.Build is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/ssrZ.v#L86
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/ssrZ.v#L83
Notation GRing.isSemiAdditive.Build is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/ssrZ.v#L79
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/ssrZ.v#L72
Reference multiplicative is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/ssrZ.v#L65
Reference multiplicative is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/ssrZ.v#L62
Notation GRing.isSemiAdditive.Build is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/ssrZ.v#L58
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/ssrZ.v#L55
Notation GRing.isSemiAdditive.Build is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/ssrZ.v#L51
Reference semi_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/ssrZ.v#L48
Notation GRing.Nmodule_isComSemiRing.Build is deprecated