Skip to content
.github/workflows/ci.yml

Release 3.3 #133

Sign in to view logs

Release 3.3

Release 3.3 #133

Triggered via push March 6, 2026 19:50
@vbglvbgl
pushed 8a67772
main
Status Success
Total duration 32m 1s
Artifacts –

ci.yml

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

Annotations

77 warnings
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/word.v#L1072
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/word.v#L1071
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/word.v#L1070
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/word.v#L1029
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/word.v#L615
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/word.v#L485
Notation GRing.Zmodule_isComRing.Build is deprecated
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/word.v#L26
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/word_ssrZ.v#L114
Notation GRing.ComRing_hasMulInverse.Build is deprecated
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/word_ssrZ.v#L92
Notation GRing.Zmodule_isComRing.Build is deprecated
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/word_ssrZ.v#L26
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/word.v#L1072
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/word.v#L1071
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/word.v#L1070
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/word.v#L1029
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/word.v#L615
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/word.v#L485
Notation GRing.Zmodule_isComRing.Build is deprecated
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/word.v#L26
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/word_ssrZ.v#L114
Notation GRing.ComRing_hasMulInverse.Build is deprecated
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/word_ssrZ.v#L92
Notation GRing.Zmodule_isComRing.Build is deprecated
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/word_ssrZ.v#L26
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:2.3.0-coq-8.20): src/word.v#L1072
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): src/word.v#L1071
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): src/word.v#L1070
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): src/word.v#L1029
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): src/word.v#L615
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.2.0-coq-8.20): src/word.v#L25
Notations "\pi ( _ )" defined at level 2 and "\pi"
build (mathcomp/mathcomp:2.2.0-coq-8.20): src/word.v#L25
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): src/word_ssrZ.v#L25
Notations "\pi ( _ )" defined at level 2 and "\pi"
build (mathcomp/mathcomp:2.2.0-coq-8.20): src/word_ssrZ.v#L25
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): src/word_ssrZ.v#L253
Reference can2_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): src/word_ssrZ.v#L253
Reference can2_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): src/word_ssrZ.v#L252
Reference additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): src/word_ssrZ.v#L236
Reference multiplicative is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): src/word_ssrZ.v#L232
Notation GRing.isAdditive.Build is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): src/word_ssrZ.v#L210
Reference additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): src/word_ssrZ.v#L114
Notation GRing.ComRing_hasMulInverse.Build is deprecated
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): src/word_ssrZ.v#L92
Notation GRing.Zmodule_isComRing.Build is deprecated
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): src/word_ssrZ.v#L26
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1): src/word_ssrZ.v#L25
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/word.v#L1072
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/word.v#L1071
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/word.v#L1070
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/word.v#L1029
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/word.v#L615
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/word.v#L485
Notation GRing.Zmodule_isComRing.Build is deprecated
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/word_ssrZ.v#L114
Notation GRing.ComRing_hasMulInverse.Build is deprecated
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/word_ssrZ.v#L92
Notation GRing.Zmodule_isComRing.Build is deprecated
build (mathcomp/mathcomp:2.5.0-coq-8.20): src/word_ssrZ.v#L255
Notation GRing.isAdditive.Build is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-coq-8.20): src/word_ssrZ.v#L253
Reference can2_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-coq-8.20): src/word_ssrZ.v#L253
Reference can2_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-coq-8.20): src/word_ssrZ.v#L252
Reference additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-coq-8.20): src/word_ssrZ.v#L236
Reference multiplicative is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-coq-8.20): src/word_ssrZ.v#L232
Notation GRing.isAdditive.Build is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-coq-8.20): src/word_ssrZ.v#L210
Reference additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-coq-8.20): src/word_ssrZ.v#L114
Notation GRing.ComRing_hasMulInverse.Build is deprecated
build (mathcomp/mathcomp:2.5.0-coq-8.20): src/word_ssrZ.v#L92
Notation GRing.Zmodule_isComRing.Build is deprecated
build (mathcomp/mathcomp:2.5.0-coq-8.20): src/word_ssrZ.v#L25
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): src/word_ssrZ.v#L253
Reference can2_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): src/word_ssrZ.v#L253
Reference can2_additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): src/word_ssrZ.v#L252
Reference additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): src/word_ssrZ.v#L236
Reference multiplicative is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): src/word_ssrZ.v#L232
Notation GRing.isAdditive.Build is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): src/word_ssrZ.v#L210
Reference additive is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): src/word_ssrZ.v#L114
Notation GRing.ComRing_hasMulInverse.Build is deprecated
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): src/word_ssrZ.v#L92
Notation GRing.Zmodule_isComRing.Build is deprecated
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): src/word_ssrZ.v#L26
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0): src/word_ssrZ.v#L25
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp:2.3.0-coq-8.19): src/word.v#L1072
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.19): src/word.v#L1071
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.19): src/word.v#L1070
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.19): src/word.v#L1029
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.19): src/word.v#L615
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.18): src/word.v#L1072
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.18): src/word.v#L1071
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.18): src/word.v#L1070
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.18): src/word.v#L1029
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.18): src/word.v#L615
Notation nosimpl is deprecated since mathcomp 2.3.0.