Skip to content
Docker CI

updates for infotheo 0.9 (#151) #547

Sign in to view logs

updates for infotheo 0.9 (#151)

updates for infotheo 0.9 (#151) #547

Triggered via push February 25, 2025 03:39
@affeldt-aistaffeldt-aist
pushed ef25be7
master
Status Success
Total duration 28m 9s
Artifacts –

docker-action.yml

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

Annotations

20 warnings
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/core/hierarchy.v#L797
Notation idempotent is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/core/hierarchy.v#L1227
Notations "{ ' _ | _ }" defined at level 0 and "{ affine _ -> _ }"
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/core/hierarchy.v#L1227
Notations "{ ' _ | _ }" defined at level 0 and "{ convex _ -> _ }"
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/core/hierarchy.v#L1227
Notations "{ ' _ | _ }" defined at level 0 and "{ concave _ -> _ }"
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/core/hierarchy.v#L1255
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/core/category.v#L966
HB: no new instance is generated
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/lib/trace_lib.v#L116
Automatically putting class in Prop even though it was declared with
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.19): theories/core/hierarchy.v#L797
Notation idempotent is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.19): theories/core/hierarchy.v#L1255
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/core/category.v#L966
HB: no new instance is generated
build (mathcomp/mathcomp:2.3.0-coq-8.19): theories/lib/fail_lib.v#L488
Notation idempotent is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.19): theories/lib/fail_lib.v#L649
Notation idempotent is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.19): theories/models/monad_model.v#L837
HB: no new instance is generated
build (mathcomp/mathcomp:2.3.0-coq-8.19): theories/models/monad_model.v#L943
Notation idempotent is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.19): theories/models/monad_model.v#L1662
Notation idempotent is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.19): theories/models/monad_model.v#L1772
Notation idempotent is deprecated since mathcomp 2.3.0.