Skip to content
Docker CI

Delay monad interface and model #513

Sign in to view logs

Delay monad interface and model

Delay monad interface and model #513

Re-run triggered December 29, 2024 08:56
@affeldt-aistaffeldt-aist
#147
Ryuji-Kawakami:delaypull
Status Failure
Total duration 33m 40s
Artifacts –

docker-action.yml

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

Annotations

22 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#L799
Notation idempotent is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/core/hierarchy.v#L1331
Notations "{ ' _ | _ }" defined at level 0 and "{ affine _ -> _ }"
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/core/hierarchy.v#L1331
Notations "{ ' _ | _ }" defined at level 0 and "{ convex _ -> _ }"
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/core/hierarchy.v#L1331
Notations "{ ' _ | _ }" defined at level 0 and "{ concave _ -> _ }"
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/core/hierarchy.v#L1359
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/models/delay_monad_model.v#L304
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/models/delay_monad_model.v#L343
Adding and removing hints in the core database implicitly is
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#L799
Notation idempotent is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.19): theories/core/hierarchy.v#L1359
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/models/delay_monad_model.v#L304
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp:2.3.0-coq-8.19): theories/models/delay_monad_model.v#L343
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp:2.3.0-coq-8.19): theories/models/delayexcept_model.v#L34
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp:2.3.0-coq-8.19): theories/models/delayexcept_model.v#L35
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp:2.3.0-coq-8.19): theories/models/delaystate_model.v#L60
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp:2.3.0-coq-8.19): theories/models/delaystate_model.v#L243
Use of “Require” inside a section is fragile. It is not recommended
build (mathcomp/mathcomp:2.3.0-coq-8.19): theories/models/delaystate_model.v#L243
Use of “Require” inside a module is fragile. It is not recommended