Skip to content
Docker CI

Replace paramcoq with elpi derive.param2 #158

Sign in to view logs

Replace paramcoq with elpi derive.param2

Replace paramcoq with elpi derive.param2 #158

Triggered via pull request January 24, 2025 14:02
@proux01proux01
opened #99
proux01:use_derive
Status Failure
Total duration 16m 40s
Artifacts –

docker-action.yml

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

Annotations

25 warnings
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-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-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.