Skip to content
CI Build UniMath

uses Context consistenly (#1841) #17

Sign in to view logs

uses Context consistenly (#1841)

uses Context consistenly (#1841) #17

Triggered via push February 11, 2024 12:06
@amato-gianlucaamato-gianluca
pushed 0b85475
master
Status Failure
Total duration 1h 26m 43s
Artifacts –

build-unimath.yml

on: push
Sanity Checks
49s
Sanity Checks
Build on macOS (latest Coq on Homebrew)
1h 26m
Build on macOS (latest Coq on Homebrew)
Matrix: build-satellites
Matrix: build-Unimath-ubuntu
Fit to window
Zoom out
Zoom in

Annotations

46 warnings
Build SetHITs (Coq latest): UniMath/Foundations/Preamble.v#L68
The '%' scope delimiter in 'Arguments' commands is deprecated, use
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 SetHITs (Coq latest): UniMath/CategoryTheory/DisplayedCats/NaturalTransformations.v#L784
disp_nat_z_iso_to_trans does not respect the uniform inheritance
Build SetHITs (Coq dev): UniMath/Foundations/Preamble.v#L68
The '%' scope delimiter in 'Arguments' commands is deprecated, use
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/DisplayedCats/NaturalTransformations.v#L784
disp_nat_z_iso_to_trans does not respect the uniform inheritance
Build TypeTheory (Coq latest): UniMath/Foundations/Preamble.v#L68
The '%' scope delimiter in 'Arguments' commands is deprecated, use
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 latest): UniMath/CategoryTheory/DisplayedCats/NaturalTransformations.v#L784
disp_nat_z_iso_to_trans does not respect the uniform inheritance
Build TypeTheory (Coq dev): UniMath/Foundations/Preamble.v#L68
The '%' scope delimiter in 'Arguments' commands is deprecated, use
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/DisplayedCats/NaturalTransformations.v#L784
disp_nat_z_iso_to_trans does not respect the uniform inheritance
Build largecatmodules (Coq dev): UniMath/Tactics/EnsureStructuredProofs.v#L11
Syntax "Export Set" is deprecated, use the attribute syntax
Build largecatmodules (Coq dev): UniMath/Foundations/Preamble.v#L68
The '%' scope delimiter in 'Arguments' commands is deprecated, use
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/DisplayedCats/NaturalTransformations.v#L784
disp_nat_z_iso_to_trans does not respect the uniform inheritance
Build largecatmodules (Coq latest): UniMath/Tactics/EnsureStructuredProofs.v#L11
Syntax "Export Set" is deprecated, use the attribute syntax
Build largecatmodules (Coq latest): UniMath/Foundations/Preamble.v#L68
The '%' scope delimiter in 'Arguments' commands is deprecated, use
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 largecatmodules (Coq latest): UniMath/CategoryTheory/DisplayedCats/NaturalTransformations.v#L784
disp_nat_z_iso_to_trans does not respect the uniform inheritance
Build GrpdHITs (Coq latest): UniMath/Tactics/EnsureStructuredProofs.v#L11
Syntax "Export Set" is deprecated, use the attribute syntax
Build GrpdHITs (Coq latest): UniMath/Foundations/Preamble.v#L68
The '%' scope delimiter in 'Arguments' commands is deprecated, use
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)
Not a truly recursive fixpoint.
Build GrpdHITs (Coq latest): UniMath/CategoryTheory/DisplayedCats/NaturalTransformations.v#L784
disp_nat_z_iso_to_trans does not respect the uniform inheritance
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/Preamble.v#L68
The '%' scope delimiter in 'Arguments' commands is deprecated, use
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/DisplayedCats/NaturalTransformations.v#L784
disp_nat_z_iso_to_trans does not respect the uniform inheritance
Build on Linux (Coq dev): UniMath/OrderTheory/DCPOs/Elements/Maximal.v#L238
element_of_strongly_maximal does not respect the uniform inheritance
Build on Linux (Coq dev): UniMath/Bicategories/DaggerCategories/BicatOfDaggerCats.v#L73
DAG_to_cat does not respect the uniform inheritance condition.
Build on Linux (Coq latest): UniMath/Tactics/EnsureStructuredProofs.v#L11
Syntax "Export Set" is deprecated, use the attribute syntax
Build on Linux (Coq latest): UniMath/Foundations/Preamble.v#L68
The '%' scope delimiter in 'Arguments' commands is deprecated, use
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/CategoryTheory/DisplayedCats/NaturalTransformations.v#L784
disp_nat_z_iso_to_trans does not respect the uniform inheritance
Build on Linux (Coq latest): UniMath/OrderTheory/DCPOs/Elements/Maximal.v#L238
element_of_strongly_maximal does not respect the uniform inheritance
Build on Linux (Coq latest): UniMath/Bicategories/DaggerCategories/BicatOfDaggerCats.v#L73
DAG_to_cat does not respect the uniform inheritance condition.