Docker CI

Merge pull request #42 from coq-community/coq-makefile-opam #620

Sign in to view logs

Re-run triggered December 1, 2024 13:20

palmskog

master

Status Failure

Total duration 3m 41s

Artifacts –

docker-action.yml

on: push

Matrix: build

Annotations

34 warnings

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

Cast types are ignored in patterns

build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/core/structures.v#L28

The '%' scope delimiter in 'Arguments' commands is deprecated, use

build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/core/excluded.v#L264

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

build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/planar/hmap_ops.v#L221

The '%' scope delimiter in 'Arguments' commands is deprecated, use

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

Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments

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

Notations "\pi ( _ )" defined at level 2 and "\pi"

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

Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments

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

Notations "\pi ( _ )" defined at level 2 and "\pi"

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

Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments

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

Notations "\pi ( _ )" defined at level 2 and "\pi"

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

Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments

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

Notations "\pi ( _ )" defined at level 2 and "\pi"

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

Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments

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

Notations "\pi ( _ )" defined at level 2 and "\pi"

build (mathcomp/mathcomp:2.2.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.1.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.2.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.2.0-coq-8.18): theories/core/finite_quotient.v#L384

Cast types are ignored in patterns

build (mathcomp/mathcomp:2.1.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.2.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.1.0-coq-8.18): theories/core/finite_quotient.v#L384

Cast types are ignored in patterns

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

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

build (mathcomp/mathcomp:2.1.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.2.0-coq-8.18): theories/core/structures.v#L168

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

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

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

build (mathcomp/mathcomp:2.2.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.1.0-coq-8.18): theories/core/structures.v#L168

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

build (mathcomp/mathcomp:2.2.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.1.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.2.0-coq-8.18): theories/core/sgraph.v#L490

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

build (mathcomp/mathcomp:2.1.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.2.0-coq-8.18): theories/core/sgraph.v#L492

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

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

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

build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/core/sgraph.v#L492

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