Skip to content
Docker CI

change boilerplate for 8.19 and beyond #42

Sign in to view logs

change boilerplate for 8.19 and beyond

change boilerplate for 8.19 and beyond #42

Triggered via pull request January 2, 2024 13:14
@palmskogpalmskog
opened #32
fix-8.19
Status Failure
Total duration 2m 28s
Artifacts –

docker-action.yml

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

Annotations

2 errors and 44 warnings
build (coqorg/coq:8.19): ch15_general_recursion/SRC/div_it_companion2.v#L24
The variable le_plus_minus was not found in the current environment.
build (coqorg/coq:dev): ch15_general_recursion/SRC/div_it_companion2.v#L24
The variable le_plus_minus was not found in the current environment.
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: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: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): ch15_general_recursion/SRC/div_it_companion2.v#L24
Notation le_plus_minus is deprecated since 8.16.
build (coqorg/coq:8.17): ch15_general_recursion/SRC/div_it_companion2.v#L24
Notation le_plus_minus is deprecated since 8.16.
build (coqorg/coq:8.17): ch15_general_recursion/SRC/div_it_companion2.v#L24
Notation le_plus_minus is deprecated since 8.16.
build (coqorg/coq:8.17): ch15_general_recursion/SRC/div_it_companion2.v#L24
Notation le_plus_minus is deprecated since 8.16.
build (coqorg/coq:8.17): ch15_general_recursion/SRC/cubic.v#L62
Notation le_plus_minus_r is deprecated since 8.16.
build (coqorg/coq:8.17): ch15_general_recursion/SRC/cubic.v#L62
Notation le_plus_minus_r is deprecated since 8.16.
build (coqorg/coq:8.17): ch15_general_recursion/SRC/cubic.v#L62
Notation le_plus_minus_r is deprecated since 8.16.
build (coqorg/coq:8.17): ch15_general_recursion/SRC/cubic.v#L62
Notation le_plus_minus_r is deprecated since 8.16.
build (coqorg/coq:8.17): ch15_general_recursion/SRC/cubic.v#L67
Notation le_plus_minus_r is deprecated since 8.16.
build (coqorg/coq:8.16): ch15_general_recursion/SRC/div_it_companion2.v#L24
Notation le_plus_minus is deprecated since 8.16.
build (coqorg/coq:8.16): ch15_general_recursion/SRC/div_it_companion2.v#L24
Notation le_plus_minus is deprecated since 8.16.
build (coqorg/coq:8.16): ch15_general_recursion/SRC/div_it_companion2.v#L24
Notation le_plus_minus is deprecated since 8.16.
build (coqorg/coq:8.16): ch15_general_recursion/SRC/div_it_companion2.v#L24
Notation le_plus_minus is deprecated since 8.16.
build (coqorg/coq:8.16): ch15_general_recursion/SRC/cubic.v#L62
Notation le_plus_minus_r is deprecated since 8.16.
build (coqorg/coq:8.16): ch15_general_recursion/SRC/cubic.v#L62
Notation le_plus_minus_r is deprecated since 8.16.
build (coqorg/coq:8.16): ch15_general_recursion/SRC/cubic.v#L62
Notation le_plus_minus_r is deprecated since 8.16.
build (coqorg/coq:8.16): ch15_general_recursion/SRC/cubic.v#L62
Notation le_plus_minus_r is deprecated since 8.16.
build (coqorg/coq:8.16): ch15_general_recursion/SRC/cubic.v#L67
Notation le_plus_minus_r is deprecated since 8.16.
build (coqorg/coq:8.16): ch15_general_recursion/SRC/cubic.v#L67
Notation le_plus_minus_r is deprecated since 8.16.
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): ch15_general_recursion/SRC/div_it_companion2.v#L24
Notation le_plus_minus is deprecated since 8.16.
build (coqorg/coq:8.18): ch15_general_recursion/SRC/div_it_companion2.v#L24
Notation le_plus_minus is deprecated since 8.16.
build (coqorg/coq:8.18): ch15_general_recursion/SRC/div_it_companion2.v#L24
Notation le_plus_minus is deprecated since 8.16.
build (coqorg/coq:8.18): ch15_general_recursion/SRC/div_it_companion2.v#L24
Notation le_plus_minus is deprecated since 8.16.
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