Skip to content
Docker CI

Remove Stdlib dependency #215

Sign in to view logs

Remove Stdlib dependency

Remove Stdlib dependency #215

Triggered via pull request February 24, 2025 08:22
@proux01proux01
synchronize #97
proux01:no-stdlib
Status Success
Total duration 30m 38s
Artifacts –

docker-action.yml

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

Annotations

44 warnings
build (mathcomp/mathcomp-dev:coq-8.19): theories/xmathcomp/various.v#L164
HB: no new instance is generated
build (mathcomp/mathcomp-dev:coq-8.19): theories/xmathcomp/various.v#L252
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.19): theories/xmathcomp/various.v#L259
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.19): theories/xmathcomp/various.v#L301
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.19): theories/xmathcomp/various.v#L318
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.19): theories/xmathcomp/various.v#L322
Notation size_opp is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.19): theories/xmathcomp/various.v#L322
Notation size_opp is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.19): theories/xmathcomp/various.v#L322
Notation size_opp is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.19): theories/xmathcomp/various.v#L325
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.19): theories/xmathcomp/various.v#L329
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/xmathcomp/real_closed_ext.v#L42
Notation rolle is deprecated since mathcomp-real-closed 2.1.0.
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/abel.v#L906
p_neq0 is declared opaque (Qed) but this is not fully respected
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/abel.v#L911
ratr_p' is declared opaque (Qed) but this is not fully respected
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/abel.v#L921
rp'_uniq is declared opaque (Qed) but this is not fully respected
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/abel.v#L930
rp_perm is declared opaque (Qed) but this is not fully respected
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/abel.v#L931
rp_uniq is declared opaque (Qed) but this is not fully respected
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/abel.v#L936
ratr_p is declared opaque (Qed) but this is not fully respected
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/abel.v#L950
K_eq is declared opaque (Qed) but this is not fully respected inside
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/abel.v#L953
K_split_p is declared opaque (Qed) but this is not fully respected
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/abel.v#L959
p_sep is declared opaque (Qed) but this is not fully respected
build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/xmathcomp/real_closed_ext.v#L42
Notation rolle is deprecated since mathcomp-real-closed 2.1.0.
build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/abel.v#L1326
Notation ivt_sign is deprecated since mathcomp-real-closed 1.1.0.
build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/abel.v#L1328
Notation ivt_sign is deprecated since mathcomp-real-closed 1.1.0.
build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/abel.v#L1330
Notation ivt_sign is deprecated since mathcomp-real-closed 1.1.0.
build (mathcomp/mathcomp:2.2.0-coq-8.20): theories/xmathcomp/various.v#L2
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): theories/xmathcomp/char0.v#L2
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): theories/xmathcomp/various.v#L2
Notations "\pi ( _ )" defined at level 2 and "\pi"
build (mathcomp/mathcomp:2.2.0-coq-8.20): theories/xmathcomp/char0.v#L2
Notations "\pi ( _ )" defined at level 2 and "\pi"
build (mathcomp/mathcomp:2.2.0-coq-8.20): theories/xmathcomp/cyclotomic_ext.v#L1
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): theories/xmathcomp/cyclotomic_ext.v#L1
Notations "\pi ( _ )" defined at level 2 and "\pi"
build (mathcomp/mathcomp:2.2.0-coq-8.20): theories/xmathcomp/map_gal.v#L2
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): theories/xmathcomp/map_gal.v#L2
Notations "\pi ( _ )" defined at level 2 and "\pi"
build (mathcomp/mathcomp:2.2.0-coq-8.20): theories/xmathcomp/algR.v#L2
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): theories/xmathcomp/algR.v#L2
Notations "\pi ( _ )" defined at level 2 and "\pi"
build (mathcomp/mathcomp-dev:coq-8.20): theories/xmathcomp/various.v#L164
HB: no new instance is generated
build (mathcomp/mathcomp-dev:coq-8.20): theories/xmathcomp/various.v#L252
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/xmathcomp/various.v#L259
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/xmathcomp/various.v#L301
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/xmathcomp/various.v#L318
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/xmathcomp/various.v#L322
Notation size_opp is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/xmathcomp/various.v#L322
Notation size_opp is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/xmathcomp/various.v#L322
Notation size_opp is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/xmathcomp/various.v#L325
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/xmathcomp/various.v#L329
Notation ringType is deprecated since mathcomp 2.4.0.