Docker CI

Docker CI #560

Sign in to view logs

Triggered via schedule December 8, 2023 05:29

palmskog

master

Status Success

Total duration 19m 36s

Artifacts –

docker-action.yml

on: schedule

Matrix: build

Annotations

24 warnings

build (mathcomp/mathcomp:2.0.0-coq-8.18): theories/core/setoid_bigop.v#L47

A coercion will be introduced instead of an instance in future

build (mathcomp/mathcomp:2.0.0-coq-8.18): theories/core/arc.v#L263

Notation sub is deprecated since mathcomp 2.0.0. Use Sub instead.

build (mathcomp/mathcomp:2.0.0-coq-8.18): theories/core/arc.v#L263

Notation sub is deprecated since mathcomp 2.0.0. Use Sub instead.

build (mathcomp/mathcomp:2.0.0-coq-8.18): theories/core/finite_quotient.v#L384

Cast types are ignored in patterns

build (mathcomp/mathcomp:2.0.0-coq-8.18): theories/core/structures.v#L166

rel_sym is declared opaque (Qed) but this is not fully respected

build (mathcomp/mathcomp:2.0.0-coq-8.18): theories/core/structures.v#L167

rel01 is declared opaque (Qed) but this is not fully respected

build (mathcomp/mathcomp:2.0.0-coq-8.18): theories/core/structures.v#L168

rel11 is declared opaque (Qed) but this is not fully respected

build (mathcomp/mathcomp:2.0.0-coq-8.18): theories/core/ptt.v#L147

tm_eqv_eqv is declared opaque (Qed) but this is not fully respected

build (mathcomp/mathcomp:2.0.0-coq-8.18): theories/core/sgraph.v#L488

dis_pq is declared opaque (Qed) but this is not fully respected

build (mathcomp/mathcomp:2.0.0-coq-8.18): theories/core/sgraph.v#L490

irr_p is declared opaque (Qed) but this is not fully respected

build (mathcomp/mathcomp-dev:coq-dev): theories/core/bounded.v#L1

Overwriting previous delimiting key nat in scope nat_scope

build (mathcomp/mathcomp-dev:coq-dev): theories/core/partition.v#L1

Overwriting previous delimiting key nat in scope nat_scope

build (mathcomp/mathcomp-dev:coq-dev): theories/core/setoid_bigop.v#L3

Overwriting previous delimiting key nat in scope nat_scope

build (mathcomp/mathcomp-dev:coq-dev): theories/core/setoid_bigop.v#L47

A coercion will be introduced instead of an instance in future

build (mathcomp/mathcomp-dev:coq-dev): theories/core/preliminaries.v#L2

Overwriting previous delimiting key nat in scope nat_scope

build (mathcomp/mathcomp-dev:coq-dev): theories/core/bij.v#L3

Overwriting previous delimiting key nat in scope nat_scope

build (mathcomp/mathcomp-dev:coq-dev): theories/core/set_tac.v#L1

Overwriting previous delimiting key nat in scope nat_scope

build (mathcomp/mathcomp-dev:coq-dev): theories/core/arc.v#L2

Overwriting previous delimiting key nat in scope nat_scope

build (mathcomp/mathcomp-dev:coq-dev): theories/core/finite_quotient.v#L3

Overwriting previous delimiting key nat in scope nat_scope

build (mathcomp/mathcomp-dev:coq-dev): theories/core/finite_quotient.v#L384

Cast types are ignored in patterns

build (mathcomp/mathcomp:2.0.0-coq-8.17): theories/core/setoid_bigop.v#L47

A coercion will be introduced instead of an instance in future

build (mathcomp/mathcomp:2.0.0-coq-8.17): theories/core/finite_quotient.v#L384

Casts are ignored in patterns

build (mathcomp/mathcomp:2.0.0-coq-8.17): theories/core/excluded.v#L264

Unused variable p might be a misspelled constructor. Use _ or _p to

build (mathcomp/mathcomp:2.0.0-coq-8.16): theories/core/finite_quotient.v#L384

Casts are ignored in patterns