Skip to content
Docker CI

change boilerplate for 8.19 and beyond (#32) #45

Sign in to view logs

change boilerplate for 8.19 and beyond (#32)

change boilerplate for 8.19 and beyond (#32) #45

Triggered via push January 3, 2024 06:32
@CasteranCasteran
pushed c41affd
master
Status Success
Total duration 2m 34s
Artifacts –

docker-action.yml

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

Annotations

31 warnings
build (coqorg/coq:8.19): ch10_extraction_and_imperative_programs/SRC/chap10.v#L12
Setting extraction output directory by default to
build (coqorg/coq:8.19): tutorial_type_classes/SRC/EMonoid.v#L7
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.19): tutorial_type_classes/SRC/Monoid_op_classes.v#L319
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.19): tutorial_type_classes/SRC/Monoid_op_classes.v#L442
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.19): tutorial_type_classes/SRC/Monoid_op_classes.v#L443
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.19): tutorial_type_classes/SRC/Monoid_op_classes.v#L464
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.19): tutorial_type_classes/SRC/Monoid_op_classes.v#L468
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.19): ch15_general_recursion/SRC/forloops.v#L536
Setting extraction output directory by default to
build (coqorg/coq:8.19): ch1_overview/SRC/chap1.v#L157
Setting extraction output directory by default to
build (coqorg/coq:8.17): tutorial_type_classes/SRC/EMonoid.v#L7
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.17): tutorial_type_classes/SRC/Monoid_op_classes.v#L319
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.17): tutorial_type_classes/SRC/Monoid_op_classes.v#L442
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.17): tutorial_type_classes/SRC/Monoid_op_classes.v#L443
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.17): tutorial_type_classes/SRC/Monoid_op_classes.v#L464
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.17): tutorial_type_classes/SRC/Monoid_op_classes.v#L468
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.18): tutorial_type_classes/SRC/EMonoid.v#L7
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.18): tutorial_type_classes/SRC/Monoid_op_classes.v#L319
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.18): tutorial_type_classes/SRC/Monoid_op_classes.v#L442
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.18): tutorial_type_classes/SRC/Monoid_op_classes.v#L443
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.18): tutorial_type_classes/SRC/Monoid_op_classes.v#L464
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.18): tutorial_type_classes/SRC/Monoid_op_classes.v#L468
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.18): ch8_inductive_predicates/SRC/magaud.v#L34
nu_constant is declared opaque (Qed) but this is not fully respected
build (coqorg/coq:dev): ch10_extraction_and_imperative_programs/SRC/chap10.v#L12
Setting extraction output directory by default to
build (coqorg/coq:dev): tutorial_type_classes/SRC/EMonoid.v#L7
A coercion will be introduced instead of an instance in future
build (coqorg/coq:dev): tutorial_type_classes/SRC/Monoid_op_classes.v#L319
A coercion will be introduced instead of an instance in future
build (coqorg/coq:dev): tutorial_type_classes/SRC/Monoid_op_classes.v#L442
A coercion will be introduced instead of an instance in future
build (coqorg/coq:dev): tutorial_type_classes/SRC/Monoid_op_classes.v#L443
A coercion will be introduced instead of an instance in future
build (coqorg/coq:dev): tutorial_type_classes/SRC/Monoid_op_classes.v#L464
A coercion will be introduced instead of an instance in future
build (coqorg/coq:dev): tutorial_type_classes/SRC/Monoid_op_classes.v#L468
A coercion will be introduced instead of an instance in future
build (coqorg/coq:dev): ch15_general_recursion/SRC/forloops.v#L536
Setting extraction output directory by default to
build (coqorg/coq:dev): ch1_overview/SRC/chap1.v#L157
Setting extraction output directory by default to