MetaCoq CI

Drastically speed up ByteCompareSpec #527

Triggered via push September 30, 2023 06:21

JasonGross

pushed 75214dc

coq-8.16+bytecomparespec-better

Status Success

Total duration 1h 12m 27s

Artifacts –

build.yml

on: push

checktodos

Matrix: build

Annotations

29 warnings

build (8.16, 4.14-flambda, quick)

Notation "_ { _ := _ }" was already used.

build (8.16, 4.14-flambda, quick)

Notation "_ ,,, _" was already used.

build (8.16, 4.14-flambda, quick)

Notation "_ * _" was already used in scope type_scope.

build (8.16, 4.14-flambda, quick)

Notation "_ <-> _" was already used in scope type_scope.

build (8.16, 4.14-flambda, quick)

Notation "_ + _" was already used in scope type_scope.

build (8.16, 4.14-flambda, quick)

Notation "_ * _" was already used in scope type_scope.

build (8.16, 4.14-flambda, quick)

Notation "_ <-> _" was already used in scope type_scope.

build (8.16, 4.14-flambda, quick)

Notation "_ + _" was already used in scope type_scope.

build (8.16, 4.14-flambda, quick)

Trying to mask the absolute name "normalization_in"!

build (8.16, 4.14-flambda, local)

Notation "_ { _ := _ }" was already used.

build (8.16, 4.14-flambda, local)

Notation "_ ,,, _" was already used.

build (8.16, 4.14-flambda, local)

Notation "_ * _" was already used in scope type_scope.

build (8.16, 4.14-flambda, local)

Notation "_ <-> _" was already used in scope type_scope.

build (8.16, 4.14-flambda, local)

Notation "_ + _" was already used in scope type_scope.

build (8.16, 4.14-flambda, local)

Notation "_ * _" was already used in scope type_scope.

build (8.16, 4.14-flambda, local)

Notation "_ <-> _" was already used in scope type_scope.

build (8.16, 4.14-flambda, local)

Notation "_ + _" was already used in scope type_scope.

build (8.16, 4.14-flambda, local)