Skip to content
Docker CI

upd to MathComp 2.3.0 #508

Sign in to view logs

upd to MathComp 2.3.0

upd to MathComp 2.3.0 #508

Triggered via pull request December 20, 2024 07:19
@affeldt-aistaffeldt-aist
synchronize #150
upd_mc230
Status Success
Total duration 32m 54s
Artifacts –

docker-action.yml

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

Annotations

21 warnings
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.3.0-coq-8.20): theories/core/hierarchy.v#L798
Notation idempotent is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/core/hierarchy.v#L1228
Notations "{ ' _ | _ }" defined at level 0 and "{ affine _ -> _ }"
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/core/hierarchy.v#L1228
Notations "{ ' _ | _ }" defined at level 0 and "{ convex _ -> _ }"
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/core/hierarchy.v#L1228
Notations "{ ' _ | _ }" defined at level 0 and "{ concave _ -> _ }"
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/core/hierarchy.v#L1256
Notation idempotent is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/core/category.v#L161
Command "Undo." is not recommended in batch mode. In particular,
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/lib/monad_lib.v#L46
Postfix notations (i.e. starting with a nonterminal symbol and
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/lib/fail_lib.v#L87
Notations "{ ' _ | _ }" defined at level 0
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/lib/fail_lib.v#L87
Notations "{ ' _ | _ }" defined at level 0
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/lib/trace_lib.v#L117
Automatically putting class in Prop even though it was declared with
build (mathcomp/mathcomp:2.3.0-coq-8.19)
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.19): theories/core/hierarchy.v#L798
Notation idempotent is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.19): theories/core/hierarchy.v#L1256
Notation idempotent is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.19): theories/core/category.v#L161
Command "Undo." is not recommended in batch mode. In particular,
build (mathcomp/mathcomp:2.3.0-coq-8.19): theories/lib/proba_lib.v#L263
Use of “Require” inside a section is fragile. It is not recommended
build (mathcomp/mathcomp:2.3.0-coq-8.19): theories/models/proba_monad_model.v#L61
Notation idempotent is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.19): theories/applications/smallstep.v#L39
The default and global localities for this command outside sections
build (mathcomp/mathcomp:2.3.0-coq-8.19): theories/applications/example_typed_store.v#L897
Use of “Require” inside a section is fragile. It is not recommended
build (mathcomp/mathcomp:2.3.0-coq-8.19): theories/applications/example_typed_store.v#L897
Use of “Require” inside a module is fragile. It is not recommended
build (mathcomp/mathcomp:2.3.0-coq-8.19)
Notation idempotent is deprecated since mathcomp 2.3.0.