Docker CI

Merge pull request #100 from proux01/opam-update #166

Sign in to view logs

Triggered via push January 26, 2025 10:39

proux01

master

Status Failure

Total duration 13m 1s

Artifacts –

docker-action.yml

on: push

Matrix: build

Annotations

25 warnings

build (mathcomp/mathcomp-dev:coq-8.20)

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

build (mathcomp/mathcomp:2.3.0-coq-8.20)

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

build (mathcomp/mathcomp:2.2.0-coq-8.20)

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

build (mathcomp/mathcomp-dev:coq-dev)

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

build (mathcomp/mathcomp-dev:coq-dev): theory/atomic_operations.v#L15

Notation comRingType is deprecated since mathcomp 2.4.0.

build (mathcomp/mathcomp-dev:coq-dev): theory/ssrcomplements.v#L83

Notation comRingType is deprecated since mathcomp 2.4.0.

build (mathcomp/mathcomp-dev:coq-dev): theory/ssrcomplements.v#L146

Notation ringType is deprecated since mathcomp 2.4.0.

build (mathcomp/mathcomp-dev:coq-dev): theory/ssrcomplements.v#L270

Notation ringType is deprecated since mathcomp 2.4.0.

build (mathcomp/mathcomp-dev:coq-dev): theory/ssrcomplements.v#L306

Notation ringType is deprecated since mathcomp 2.4.0.

build (mathcomp/mathcomp-dev:coq-dev): theory/ssrcomplements.v#L337

Notation ringType is deprecated since mathcomp 2.4.0.

build (mathcomp/mathcomp-dev:coq-dev): theory/ssrcomplements.v#L360

Notation comRingType is deprecated since mathcomp 2.4.0.

build (mathcomp/mathcomp-dev:coq-dev): theory/minor.v#L85

Notation ringType is deprecated since mathcomp 2.4.0.

build (mathcomp/mathcomp-dev:coq-dev): theory/minor.v#L152

Notation ringType is deprecated since mathcomp 2.4.0.

build (mathcomp/mathcomp-dev:coq-dev): theory/minor.v#L166

Notation ringType is deprecated since mathcomp 2.4.0.

build (mathcomp/mathcomp:2.3.0-coq-dev)

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

build (mathcomp/mathcomp:2.3.0-coq-dev): theory/ssralg_ring_tac.v#L1

Loading Stdlib without prefix is deprecated.

build (mathcomp/mathcomp:2.3.0-coq-dev): theory/ssralg_ring_tac.v#L1

Loading Stdlib without prefix is deprecated.

build (mathcomp/mathcomp:2.3.0-coq-dev): refinements/param.v#L22

Loading Stdlib without prefix is deprecated.

build (mathcomp/mathcomp:2.3.0-coq-dev): refinements/param.v#L73

Reference subn_rec is deprecated since mathcomp 2.3.0.

build (mathcomp/mathcomp:2.3.0-coq-dev): refinements/param.v#L76

Reference addn_rec is deprecated since mathcomp 2.3.0.

build (mathcomp/mathcomp:2.3.0-coq-dev): refinements/param.v#L77

Global name addn_R is taken, using addn_R1 instead

build (mathcomp/mathcomp:2.3.0-coq-dev): refinements/param.v#L77

Global name param_addn_R is taken, using param_addn_R1 instead

build (mathcomp/mathcomp:2.3.0-coq-dev): refinements/param.v#L106

Reference muln_rec is deprecated since mathcomp 2.3.0.

build (mathcomp/mathcomp:2.3.0-coq-dev): refinements/param.v#L108

Reference expn_rec is deprecated since mathcomp 2.3.0.

build (mathcomp/mathcomp:2.3.0-coq-dev): refinements/param.v#L110

Reference fact_rec is deprecated since mathcomp 2.3.0.