Skip to content
Docker CI

For monae #541

Sign in to view logs

For monae

For monae #541

Triggered via pull request February 7, 2025 19:57
@t6st6s
synchronize #137
for_monae
Status Success
Total duration 25m 1s
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): lib/realType_ext.v#L23
Postfix notations (i.e. starting with a nonterminal symbol and
build (mathcomp/mathcomp:2.3.0-coq-8.20): lib/realType_ext.v#L27
Postfix notations (i.e. starting with a nonterminal symbol and
build (mathcomp/mathcomp:2.3.0-coq-8.20): lib/realType_ext.v#L28
Postfix notations (i.e. starting with a nonterminal symbol and
build (mathcomp/mathcomp:2.3.0-coq-8.20): lib/ssralg_ext.v#L38
Postfix notations (i.e. starting with a nonterminal symbol and
build (mathcomp/mathcomp:2.3.0-coq-8.20): lib/derive_ext.v#L5
Notations "[ fun _ => _ ]" defined at level 0 with arguments name
build (mathcomp/mathcomp:2.3.0-coq-8.20): lib/derive_ext.v#L7
Notations "{ ' _ | _ }" defined at level 0
build (mathcomp/mathcomp:2.3.0-coq-8.20): lib/derive_ext.v#L122
Argument a was previously inferred to be in scope ring_scope but is
build (mathcomp/mathcomp:2.3.0-coq-8.20): probability/fdist.v#L78
Notations "_ <| _" defined at level 70 with arguments constr
build (mathcomp/mathcomp:2.3.0-coq-8.20): probability/fdist.v#L936
Postfix notations (i.e. starting with a nonterminal symbol and
build (mathcomp/mathcomp:2.3.0-coq-8.20): probability/fdist.v#L937
Postfix notations (i.e. starting with a nonterminal symbol and
build (mathcomp/mathcomp:2.3.0-coq-8.19): lib/derive_ext.v#L122
Argument a was previously inferred to be in scope ring_scope but is
build (mathcomp/mathcomp:2.3.0-coq-8.19): probability/convex.v#L2675
HB: no new instance is generated
build (mathcomp/mathcomp:2.3.0-coq-8.19): probability/convex.v#L3175
Use of “Require” inside a section is fragile. It is not recommended
build (mathcomp/mathcomp:2.3.0-coq-8.19): probability/fsdist.v#L974
Use of “Require” inside a section is fragile. It is not recommended
build (mathcomp/mathcomp:2.3.0-coq-8.19): probability/fsdist.v#L1137
HB: no new instance is generated
build (mathcomp/mathcomp:2.3.0-coq-8.19): probability/necset.v#L735
Variables F, i and n do not occur in the right-hand side. The
build (mathcomp/mathcomp:2.3.0-coq-8.19): probability/necset.v#L893
HB: no new instance is generated
build (mathcomp/mathcomp:2.3.0-coq-8.19): probability/necset.v#L899
HB: no new instance is generated
build (mathcomp/mathcomp:2.3.0-coq-8.19): robust/weightedmean.v#L1025
Cannot define induction principle(s) for
build (mathcomp/mathcomp:2.3.0-coq-8.19): information_theory/shannon_fano.v#L78
Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0.