Skip to content
Docker CI

Merge pull request #84 from math-comp/simple-norm #267

Sign in to view logs

Merge pull request #84 from math-comp/simple-norm

Merge pull request #84 from math-comp/simple-norm #267

Triggered via push July 12, 2023 07:44
@pi8027pi8027
pushed 119e9c7
master
Status Success
Total duration 6m 26s
Artifacts –

docker-action.yml

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

Annotations

50 warnings
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/common.v#L303
Notation ler_add2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/common.v#L303
Notation ler_add2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/common.v#L303
Notation ler_add2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/common.v#L343
Notation ler_pdivr_mulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/common.v#L343
Notation ler_pdivr_mulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/common.v#L343
Notation ler_pdivr_mulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/common.v#L344
Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/common.v#L344
Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/common.v#L344
Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/lra.v#L100
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.16.0-coq-8.17): examples/ring_examples_check.v#L4
To avoid stack overflow, large numbers in nat are interpreted as
build (mathcomp/mathcomp:1.16.0-coq-8.17): examples/ring_examples_check.v#L4
To avoid stack overflow, large numbers in nat are interpreted as
build (mathcomp/mathcomp:1.16.0-coq-8.17): examples/ring_examples_check.v#L4
To avoid stack overflow, large numbers in nat are interpreted as
build (mathcomp/mathcomp:1.16.0-coq-8.17): examples/ring_examples_no_check.v#L6
To avoid stack overflow, large numbers in nat are interpreted as
build (mathcomp/mathcomp:1.16.0-coq-8.17): examples/ring_examples_no_check.v#L6
To avoid stack overflow, large numbers in nat are interpreted as
build (mathcomp/mathcomp:1.16.0-coq-8.17): examples/ring_examples_no_check.v#L6
To avoid stack overflow, large numbers in nat are interpreted as
build (mathcomp/mathcomp:1.16.0-coq-8.17): examples/zmodule.v#L487
Ignoring canonical projection to Logic.eq_refl by zifyRingE in
build (mathcomp/mathcomp:1.16.0-coq-8.17): examples/zmodule.v#L507
Ignoring canonical projection to zify_mulrz_subproof by zifyRingE in
build (mathcomp/mathcomp:1.16.0-coq-8.17): examples/zmodule.v#L523
Ignoring canonical projection to Logic.eq_refl by zifyRingE in
build (mathcomp/mathcomp:1.16.0-coq-8.17): examples/zmodule.v#L523
Ignoring canonical projection to zify_mulrz_subproof by zifyRingE in
build (mathcomp/mathcomp:1.17.0-coq-8.16): theories/common.v#L303
Notation ler_add2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.16): theories/common.v#L303
Notation ler_add2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.16): theories/common.v#L303
Notation ler_add2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.16): theories/common.v#L343
Notation ler_pdivr_mulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.16): theories/common.v#L343
Notation ler_pdivr_mulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.16): theories/common.v#L343
Notation ler_pdivr_mulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.16): theories/common.v#L344
Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.16): theories/common.v#L344
Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.16): theories/common.v#L344
Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.16): theories/lra.v#L100
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.16.0-coq-8.16): examples/ring_examples_check.v#L4
To avoid stack overflow, large numbers in nat are interpreted as
build (mathcomp/mathcomp:1.16.0-coq-8.16): examples/ring_examples_check.v#L4
To avoid stack overflow, large numbers in nat are interpreted as
build (mathcomp/mathcomp:1.16.0-coq-8.16): examples/ring_examples_check.v#L4
To avoid stack overflow, large numbers in nat are interpreted as
build (mathcomp/mathcomp:1.16.0-coq-8.16): examples/ring_examples_no_check.v#L6
To avoid stack overflow, large numbers in nat are interpreted as
build (mathcomp/mathcomp:1.16.0-coq-8.16): examples/ring_examples_no_check.v#L6
To avoid stack overflow, large numbers in nat are interpreted as
build (mathcomp/mathcomp:1.16.0-coq-8.16): examples/ring_examples_no_check.v#L6
To avoid stack overflow, large numbers in nat are interpreted as
build (mathcomp/mathcomp:1.16.0-coq-8.16): examples/zmodule.v#L487
Ignoring canonical projection to Logic.eq_refl by zifyRingE in
build (mathcomp/mathcomp:1.16.0-coq-8.16): examples/zmodule.v#L507
Ignoring canonical projection to zify_mulrz_subproof by zifyRingE in
build (mathcomp/mathcomp:1.16.0-coq-8.16): examples/zmodule.v#L523
Ignoring canonical projection to Logic.eq_refl by zifyRingE in
build (mathcomp/mathcomp:1.16.0-coq-8.16): examples/zmodule.v#L523
Ignoring canonical projection to zify_mulrz_subproof by zifyRingE in
build (mathcomp/mathcomp:1.15.0-coq-8.16): examples/ring_examples_check.v#L4
To avoid stack overflow, large numbers in nat are interpreted as
build (mathcomp/mathcomp:1.15.0-coq-8.16): examples/ring_examples_check.v#L4
To avoid stack overflow, large numbers in nat are interpreted as
build (mathcomp/mathcomp:1.15.0-coq-8.16): examples/ring_examples_check.v#L4
To avoid stack overflow, large numbers in nat are interpreted as
build (mathcomp/mathcomp:1.15.0-coq-8.16): examples/ring_examples_no_check.v#L6
To avoid stack overflow, large numbers in nat are interpreted as
build (mathcomp/mathcomp:1.15.0-coq-8.16): examples/ring_examples_no_check.v#L6
To avoid stack overflow, large numbers in nat are interpreted as
build (mathcomp/mathcomp:1.15.0-coq-8.16): examples/ring_examples_no_check.v#L6
To avoid stack overflow, large numbers in nat are interpreted as
build (mathcomp/mathcomp:1.15.0-coq-8.16): examples/zmodule.v#L487
Ignoring canonical projection to Logic.eq_refl by zifyRingE in
build (mathcomp/mathcomp:1.15.0-coq-8.16): examples/zmodule.v#L507
Ignoring canonical projection to zify_mulrz_subproof by zifyRingE in
build (mathcomp/mathcomp:1.15.0-coq-8.16): examples/zmodule.v#L523
Ignoring canonical projection to Logic.eq_refl by zifyRingE in
build (mathcomp/mathcomp:1.15.0-coq-8.16): examples/zmodule.v#L523
Ignoring canonical projection to zify_mulrz_subproof by zifyRingE in