Skip to content
Docker CI

fix Nix CI #548

# to view logs

fix Nix CI

fix Nix CI #548

Triggered via pull request February 25, 2025 03:44
@affeldt-aistaffeldt-aist
opened #152
fix_CI
Status Success
Total duration 29m 54s
Artifacts –

docker-action.yml

on: pull_request
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/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.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.