Skip to content
Docker CI

Merge pull request #122 from proux01/fix-110 #370

Sign in to view logs

Merge pull request #122 from proux01/fix-110

Merge pull request #122 from proux01/fix-110 #370

Triggered via push September 15, 2025 12:49
@proux01proux01
pushed 88aab35
master
Status Failure
Total duration 19m 59s
Artifacts –

docker-action.yml

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

Annotations

50 warnings
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/common.v#L1072
Use of "Notation" keyword for abbreviations is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/common.v#L764
Use of "Notation" keyword for abbreviations is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/common.v#L761
Use of "Notation" keyword for abbreviations is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/common.v#L560
Use of "Notation" keyword for abbreviations is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/common.v#L557
Use of "Notation" keyword for abbreviations is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/common.v#L389
Use of "Notation" keyword for abbreviations is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/common.v#L387
Use of "Notation" keyword for abbreviations is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/common.v#L5
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/common.v#L4
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/common.v#L3
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:2.4.0-coq-8.20)
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20): examples/ring_examples_check.v#L4
To avoid stack overflow, large numbers in nat are interpreted as
build (mathcomp/mathcomp:2.4.0-coq-8.20): examples/ring_examples_check.v#L4
To avoid stack overflow, large numbers in nat are interpreted as
build (mathcomp/mathcomp:2.4.0-coq-8.20)
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20): examples/ring_examples_check.v#L4
To avoid stack overflow, large numbers in nat are interpreted as
build (mathcomp/mathcomp:2.4.0-coq-8.20)
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20)
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20)
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20)
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20)
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20)
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20)
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20)
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20)
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20)
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): examples/ring_examples_no_check.v#L1
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp-dev:coq-8.20): examples/ring_examples_check.v#L1
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp-dev:coq-8.20): examples/field_examples_check.v#L1
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp-dev:coq-8.20): examples/field_examples_no_check.v#L1
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp-dev:coq-8.20): theories/common.v#L5
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.0): examples/field_examples_check.v#L1
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.0): examples/field_examples_no_check.v#L1
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/lra.v#L4
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/ring.v#L3
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/lra.v#L3
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/common.v#L1335
Reference Zeq_is_eq_bool is deprecated since 9.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/common.v#L1335
Reference Zeq_is_eq_bool is deprecated since 9.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/common.v#L5
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/common.v#L4
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/common.v#L3
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0)
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0)
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0)
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): theories/lra.v#L4
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): theories/lra.v#L3
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): theories/ring.v#L3
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): theories/common.v#L1335
Reference Zeq_is_eq_bool is deprecated since 9.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): theories/common.v#L1335
Reference Zeq_is_eq_bool is deprecated since 9.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): theories/common.v#L4
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): theories/common.v#L3
"From Coq" has been replaced by "From Stdlib".