Skip to content
Docker CI

make coq-htt package depend on coq-htt-core #56

Sign in to view logs

make coq-htt package depend on coq-htt-core

make coq-htt package depend on coq-htt-core #56

Re-run triggered October 7, 2024 16:37
@aleksnanevskialeksnanevski
#29
proofengineering:core-package-dep
Status Success
Total duration 12m 37s
Artifacts –

docker-action.yml

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

Annotations

17 warnings
build (mathcomp/mathcomp:2.2.0-coq-8.20): examples/array.v#L15
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): examples/quicksort.v#L15
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): examples/bubblesort.v#L15
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): examples/congmath.v#L16
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): examples/hashtab.v#L16
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): examples/union_find.v#L14
Notations "[ seq _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): examples/congprog.v#L16
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:latest-coq-dev): htt/domain.v#L15
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:latest-coq-dev): examples/exploit.v#L14
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:latest-coq-dev): examples/array.v#L14
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:latest-coq-dev): examples/array.v#L15
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:latest-coq-dev): examples/gcd.v#L14
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:latest-coq-dev): examples/kvmaps.v#L19
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:latest-coq-dev): examples/dlist.v#L14
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:latest-coq-dev): examples/quicksort.v#L15
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:latest-coq-dev): examples/bubblesort.v#L14
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:latest-coq-dev): examples/bubblesort.v#L15
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments