CI Build UniMath

CI Build UniMath #22

Triggered via schedule July 10, 2023 02:35

Bigstep22

⁠ ff27f5c

master

Status Failure

Total duration 1h 39m 1s

Artifacts –

build-unimath.yml

on: schedule

Sanity Checks

1m 0s

Build on macOS (Coq 8.16)

3m 44s

Matrix: build-satellites

Matrix: build-Unimath-ubuntu

Annotations

6 errors and 69 warnings

Build TypeTheory (Coq latest)

Cannot find a physical path bound to logical path

Build TypeTheory (Coq latest)

Cannot find a physical path bound to logical path

Build TypeTheory (Coq dev)

Cannot find a physical path bound to logical path

Build TypeTheory (Coq dev)

Cannot find a physical path bound to logical path

Build GrpdHITs (Coq dev)

Case analysis on private inductive gquot

Build GrpdHITs (Coq dev)

Case analysis on private inductive gquot

Build SetHITs (Coq dev): UniMath/Foundations/PartA.v#L350

Declaring arbitrary terms as hints is fragile; it is recommended to

Build SetHITs (Coq dev): UniMath/Foundations/PartA.v#L376

Declaring arbitrary terms as hints is fragile; it is recommended to

Build SetHITs (Coq dev): UniMath/CategoryTheory/Core/Categories.v#L40

Overwriting previous delimiting key cat in scope cat

Build SetHITs (Coq dev): UniMath/CategoryTheory/Core/Isos.v#L21

Overwriting previous delimiting key cat in scope cat

Build SetHITs (Coq dev): UniMath/CategoryTheory/Core/Univalence.v#L19

Overwriting previous delimiting key cat in scope cat

Build SetHITs (Coq dev): UniMath/CategoryTheory/Core/TransportMorphisms.v#L7

Overwriting previous delimiting key cat in scope cat

Build SetHITs (Coq dev): UniMath/CategoryTheory/Core/Functors.v#L31

Overwriting previous delimiting key cat in scope cat

Build SetHITs (Coq dev): UniMath/CategoryTheory/Core/NaturalTransformations.v#L19

Overwriting previous delimiting key cat in scope cat

Build SetHITs (Coq dev): UniMath/CategoryTheory/Subcategory/Core.v#L23

Overwriting previous delimiting key cat in scope cat

Build SetHITs (Coq dev): UniMath/CategoryTheory/Core/Setcategories.v#L11

Overwriting previous delimiting key cat in scope cat

Build TypeTheory (Coq latest): UniMath/Foundations/PartA.v#L350

Declaring arbitrary terms as hints is fragile; it is recommended to

Build TypeTheory (Coq latest): UniMath/Foundations/PartA.v#L376

Declaring arbitrary terms as hints is fragile; it is recommended to

Build TypeTheory (Coq dev): UniMath/Foundations/PartA.v#L350

Declaring arbitrary terms as hints is fragile; it is recommended to

Build TypeTheory (Coq dev): UniMath/Foundations/PartA.v#L376

Declaring arbitrary terms as hints is fragile; it is recommended to

Build TypeTheory (Coq dev): UniMath/CategoryTheory/Core/Categories.v#L40

Overwriting previous delimiting key cat in scope cat

Build TypeTheory (Coq dev): UniMath/CategoryTheory/Core/Isos.v#L21

Overwriting previous delimiting key cat in scope cat

Build TypeTheory (Coq dev): UniMath/CategoryTheory/Core/Univalence.v#L19

Overwriting previous delimiting key cat in scope cat

Build TypeTheory (Coq dev): UniMath/CategoryTheory/Core/TransportMorphisms.v#L7

Overwriting previous delimiting key cat in scope cat

Build TypeTheory (Coq dev): UniMath/CategoryTheory/Core/Functors.v#L31

Overwriting previous delimiting key cat in scope cat

Build TypeTheory (Coq dev): UniMath/CategoryTheory/Core/NaturalTransformations.v#L19

Overwriting previous delimiting key cat in scope cat

Build TypeTheory (Coq dev): UniMath/CategoryTheory/Core/Setcategories.v#L11

Overwriting previous delimiting key cat in scope cat

Build TypeTheory (Coq dev): UniMath/CategoryTheory/Subcategory/Core.v#L23

Overwriting previous delimiting key cat in scope cat

Build SetHITs (Coq latest): UniMath/Foundations/PartA.v#L350

Declaring arbitrary terms as hints is fragile; it is recommended to

Build SetHITs (Coq latest): UniMath/Foundations/PartA.v#L376

Declaring arbitrary terms as hints is fragile; it is recommended to

Build largecatmodules (Coq dev): UniMath/Tactics/EnsureStructuredProofs.v#L11

Syntax "Export Set" is deprecated, use the attribute syntax

Build largecatmodules (Coq dev): UniMath/Foundations/PartA.v#L350

Declaring arbitrary terms as hints is fragile; it is recommended to

Build largecatmodules (Coq dev): UniMath/Foundations/PartA.v#L376

Declaring arbitrary terms as hints is fragile; it is recommended to

Build largecatmodules (Coq dev): UniMath/CategoryTheory/Core/Categories.v#L40

Overwriting previous delimiting key cat in scope cat

Build largecatmodules (Coq dev): UniMath/CategoryTheory/Core/Isos.v#L21

Overwriting previous delimiting key cat in scope cat

Build largecatmodules (Coq dev): UniMath/CategoryTheory/Core/Univalence.v#L19

Overwriting previous delimiting key cat in scope cat

Build largecatmodules (Coq dev): UniMath/CategoryTheory/Core/TransportMorphisms.v#L7

Overwriting previous delimiting key cat in scope cat

Build largecatmodules (Coq dev): UniMath/CategoryTheory/Core/Functors.v#L31

Overwriting previous delimiting key cat in scope cat

Build largecatmodules (Coq dev): UniMath/CategoryTheory/Subcategory/Core.v#L23

Overwriting previous delimiting key cat in scope cat

Build largecatmodules (Coq dev): UniMath/CategoryTheory/Core/NaturalTransformations.v#L19

Overwriting previous delimiting key cat in scope cat

Build largecatmodules (Coq latest): UniMath/Foundations/PartA.v#L350

Declaring arbitrary terms as hints is fragile; it is recommended to

Build largecatmodules (Coq latest): UniMath/Foundations/PartA.v#L376

Declaring arbitrary terms as hints is fragile; it is recommended to

Build GrpdHITs (Coq dev): UniMath/Tactics/EnsureStructuredProofs.v#L11

Syntax "Export Set" is deprecated, use the attribute syntax

Build GrpdHITs (Coq dev): UniMath/Foundations/PartA.v#L350

Declaring arbitrary terms as hints is fragile; it is recommended to

Build GrpdHITs (Coq dev): UniMath/Foundations/PartA.v#L376

Declaring arbitrary terms as hints is fragile; it is recommended to

Build GrpdHITs (Coq dev): UniMath/CategoryTheory/Core/Categories.v#L40

Overwriting previous delimiting key cat in scope cat

Build GrpdHITs (Coq dev): UniMath/CategoryTheory/Core/Isos.v#L21

Overwriting previous delimiting key cat in scope cat

Build GrpdHITs (Coq dev): UniMath/CategoryTheory/Core/Univalence.v#L19

Overwriting previous delimiting key cat in scope cat

Build GrpdHITs (Coq dev): UniMath/CategoryTheory/Core/TransportMorphisms.v#L7

Overwriting previous delimiting key cat in scope cat

Build GrpdHITs (Coq dev): UniMath/CategoryTheory/Core/Functors.v#L31

Overwriting previous delimiting key cat in scope cat

Build GrpdHITs (Coq dev)

Notation gradth is deprecated. Use isweq_iso instead.

Build GrpdHITs (Coq dev)

Notation gradth is deprecated. Use isweq_iso instead.

Build GrpdHITs (Coq latest): UniMath/Foundations/PartA.v#L350

Declaring arbitrary terms as hints is fragile; it is recommended to

Build GrpdHITs (Coq latest): UniMath/Foundations/PartA.v#L376

Declaring arbitrary terms as hints is fragile; it is recommended to

Build GrpdHITs (Coq latest)

Notation gradth is deprecated. Use isweq_iso instead.

Build GrpdHITs (Coq latest)

Notation gradth is deprecated. Use isweq_iso instead.

Build GrpdHITs (Coq latest)

Notation gradth is deprecated. Use isweq_iso instead.

Build GrpdHITs (Coq latest)

Notation gradth is deprecated. Use isweq_iso instead.

Build GrpdHITs (Coq latest)

Notation gradth is deprecated. Use isweq_iso instead.

Build GrpdHITs (Coq latest)

Notation gradth is deprecated. Use isweq_iso instead.

Build GrpdHITs (Coq latest)

Not a truly recursive fixpoint.

Build GrpdHITs (Coq latest)

Notation gradth is deprecated. Use isweq_iso instead.

Build on Linux (Coq latest): UniMath/Foundations/PartA.v#L350

Declaring arbitrary terms as hints is fragile; it is recommended to

Build on Linux (Coq latest): UniMath/Foundations/PartA.v#L376

Declaring arbitrary terms as hints is fragile; it is recommended to

Build on Linux (Coq latest): UniMath/Bicategories/DaggerCategories/BicatOfDaggerCats.v#L73

DAG_to_cat does not respect the uniform inheritance condition.

Build on Linux (Coq dev): UniMath/Tactics/EnsureStructuredProofs.v#L11

Syntax "Export Set" is deprecated, use the attribute syntax

Build on Linux (Coq dev): UniMath/Foundations/PartA.v#L350

Declaring arbitrary terms as hints is fragile; it is recommended to

Build on Linux (Coq dev): UniMath/Foundations/PartA.v#L376

Declaring arbitrary terms as hints is fragile; it is recommended to

Build on Linux (Coq dev): UniMath/CategoryTheory/Core/Categories.v#L40

Overwriting previous delimiting key cat in scope cat

Build on Linux (Coq dev): UniMath/Folds/from_precats_to_folds_and_back.v#L23

Overwriting previous delimiting key cat in scope cat

Build on Linux (Coq dev): UniMath/CategoryTheory/Core/Isos.v#L21

Overwriting previous delimiting key cat in scope cat

Build on Linux (Coq dev): UniMath/CategoryTheory/Core/TransportMorphisms.v#L7

Overwriting previous delimiting key cat in scope cat

Build on Linux (Coq dev): UniMath/Folds/folds_isomorphism.v#L32

Overwriting previous delimiting key cat in scope cat

Build on Linux (Coq dev): UniMath/CategoryTheory/Core/Univalence.v#L19

Overwriting previous delimiting key cat in scope cat

Build on Linux (Coq dev): UniMath/CategoryTheory/categories/preorder_categories.v#L6

Overwriting previous delimiting key cat in scope cat

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

CI Build UniMath #22

Summary