Skip to content
Docker CI

mathcomp 2.1 #8

Sign in to view logs

mathcomp 2.1

mathcomp 2.1 #8

Triggered via push October 28, 2023 00:47
@therythery
pushed 64bfde1
master
Status Failure
Total duration 2m 53s
Artifacts –

docker-action.yml

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

Annotations

1 error and 10 warnings
build (mathcomp/mathcomp:2.1.0-coq-8.18): Ssreflect15min/quesako.v#L63
Stack overflow.
build (mathcomp/mathcomp:2.1.0-coq-8.18): AnIntroductionToSmallScaleReflectionInCoq/section4.v#L74
Not a truly recursive fixpoint.
build (mathcomp/mathcomp:2.1.0-coq-8.18): AnIntroductionToSmallScaleReflectionInCoq/section4.v#L98
Not a truly recursive fixpoint.
build (mathcomp/mathcomp:2.1.0-coq-8.18): AnIntroductionToSmallScaleReflectionInCoq/section4.v#L108
Not a truly recursive fixpoint.
build (mathcomp/mathcomp:2.1.0-coq-8.18): AnIntroductionToSmallScaleReflectionInCoq/section6.v#L21
Ignoring canonical projection to cons by isFinite.enum_subdef in
build (mathcomp/mathcomp:2.1.0-coq-8.18): AnIntroductionToSmallScaleReflectionInCoq/section6.v#L82
Notation UniqFinMixin is deprecated since mathcomp 2.0.0.
build (mathcomp/mathcomp:2.1.0-coq-8.18): AnIntroductionToSmallScaleReflectionInCoq/section6.v#L375
Projection value has no head constant:
build (mathcomp/mathcomp:2.1.0-coq-8.18): AnIntroductionToSmallScaleReflectionInCoq/section6.v#L375
Ignoring canonical projection to vrefl_rect by isSub.SubK_subproof
build (mathcomp/mathcomp:2.1.0-coq-8.18): AnIntroductionToSmallScaleReflectionInCoq/section6.v#L378
Projection value has no head constant:
build (mathcomp/mathcomp:2.1.0-coq-8.18): AnIntroductionToSmallScaleReflectionInCoq/section6.v#L378
Ignoring canonical projection to vrefl_rect by isSub.SubK_subproof
build (mathcomp/mathcomp:2.1.0-coq-8.18): AnIntroductionToSmallScaleReflectionInCoq/section6.v#L389
Ignoring canonical projection to cat by tval in cat_tuple: redundant