Skip to content
Docker CI

meta update for coq-community, test up to MathComp 1.17 and Coq 8.17 #26

Sign in to view logs

meta update for coq-community, test up to MathComp 1.17 and Coq 8.17

meta update for coq-community, test up to MathComp 1.17 and Coq 8.17 #26

Triggered via pull request June 19, 2023 12:53
@palmskogpalmskog
synchronize #25
mc-1-community-update
Status Success
Total duration 3m 26s
Artifacts –

docker-action.yml

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

Annotations

37 warnings
build (mathcomp/mathcomp:1.13.0-coq-8.13): theories/acyclic.v#L55
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp:1.13.0-coq-8.15): theories/acyclic.v#L55
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp:1.12.0-coq-8.12): theories/acyclic.v#L55
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/extra.v#L264
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/extra.v#L272
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/extra.v#L274
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/kosaraju.v#L23
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/kosaraju.v#L31
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/kosaraju.v#L33
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/kosaraju.v#L178
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/kosaraju.v#L187
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/kosaraju.v#L484
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.17.0-coq-8.17): theories/acyclic.v#L55
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp:1.14.0-coq-8.14): theories/acyclic.v#L55
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp:1.13.0-coq-8.12): theories/acyclic.v#L55
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp:1.14.0-coq-8.15): theories/acyclic.v#L55
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp:1.12.0-coq-8.14): theories/acyclic.v#L55
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp:1.15.0-coq-8.15): theories/extra.v#L264
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.15.0-coq-8.15): theories/extra.v#L272
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.15.0-coq-8.15): theories/extra.v#L274
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.15.0-coq-8.15): theories/kosaraju.v#L23
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.15.0-coq-8.15): theories/kosaraju.v#L31
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.15.0-coq-8.15): theories/kosaraju.v#L33
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.15.0-coq-8.15): theories/kosaraju.v#L178
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.15.0-coq-8.15): theories/kosaraju.v#L187
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.15.0-coq-8.15): theories/kosaraju.v#L484
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.15.0-coq-8.15): theories/acyclic.v#L55
Adding and removing hints in the core database implicitly is
build (mathcomp/mathcomp:1.16.0-coq-8.16): theories/extra.v#L264
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.16.0-coq-8.16): theories/extra.v#L272
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.16.0-coq-8.16): theories/extra.v#L274
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.16.0-coq-8.16): theories/kosaraju.v#L23
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.16.0-coq-8.16): theories/kosaraju.v#L31
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.16.0-coq-8.16): theories/kosaraju.v#L33
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.16.0-coq-8.16): theories/kosaraju.v#L178
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.16.0-coq-8.16): theories/kosaraju.v#L187
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.16.0-coq-8.16): theories/kosaraju.v#L484
Notation rel_of_simpl_rel is deprecated since mathcomp 1.15.
build (mathcomp/mathcomp:1.16.0-coq-8.16): theories/acyclic.v#L55
Adding and removing hints in the core database implicitly is