Skip to content
CI Build UniMath

CI Build UniMath #14

Sign in to view logs

CI Build UniMath

CI Build UniMath #14

Re-run triggered January 29, 2024 16:10
@amato-gianlucaamato-gianluca
⁠ b1c3759
universal-algebra
Status Failure
Total duration 1h 16m 40s
Artifacts –

build-unimath.yml

on: schedule
Sanity Checks
32s
Sanity Checks
Build on macOS (Coq 8.16)
1h 40m
Build on macOS (Coq 8.16)
Matrix: build-satellites
Matrix: build-Unimath-ubuntu
Fit to window
Zoom out
Zoom in

Annotations

1 error and 102 warnings
Sanity Checks
Process completed with exit code 2.
Build on macOS (Coq 8.16)
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3, actions/cache/restore@v3, actions/cache/save@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
Build on Linux (Coq latest)
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3, actions/cache/restore@v3, actions/cache/save@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
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/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/Core/Categories.v#L40
Overwriting previous delimiting key cat in scope cat
Build on Linux (Coq latest): UniMath/Folds/from_precats_to_folds_and_back.v#L23
Overwriting previous delimiting key cat in scope cat
Build on Linux (Coq latest): UniMath/CategoryTheory/Core/Isos.v#L21
Overwriting previous delimiting key cat in scope cat
Build on Linux (Coq latest): UniMath/CategoryTheory/Core/TransportMorphisms.v#L7
Overwriting previous delimiting key cat in scope cat
Build on Linux (Coq latest): UniMath/CategoryTheory/Core/Univalence.v#L19
Overwriting previous delimiting key cat in scope cat
Build on Linux (Coq latest): UniMath/Folds/folds_isomorphism.v#L32
Overwriting previous delimiting key cat in scope cat
Build on Linux (Coq latest): UniMath/CategoryTheory/categories/preorder_categories.v#L6
Overwriting previous delimiting key cat in scope cat
Build TypeTheory (Coq dev)
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3, actions/cache/restore@v3, actions/cache/save@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
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/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
Sanity Checks
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
Build GrpdHITs (Coq latest)
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3, actions/cache/restore@v3, actions/cache/save@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
Build GrpdHITs (Coq latest): UniMath/Tactics/EnsureStructuredProofs.v#L11
Syntax "Export Set" is deprecated, use the attribute syntax
Build largecatmodules (Coq latest)
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3, actions/cache/restore@v3, actions/cache/save@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
Build GrpdHITs (Coq latest): UniMath/Foundations/PartA.v#L350
Declaring arbitrary terms as hints is fragile; it is recommended to
Build largecatmodules (Coq latest): UniMath/Tactics/EnsureStructuredProofs.v#L11
Syntax "Export Set" is deprecated, use the attribute syntax
Build GrpdHITs (Coq latest): UniMath/Foundations/PartA.v#L376
Declaring arbitrary terms as hints is fragile; it is recommended to
Build largecatmodules (Coq latest): UniMath/Foundations/PartA.v#L350
Declaring arbitrary terms as hints is fragile; it is recommended to
Build GrpdHITs (Coq latest): UniMath/CategoryTheory/Core/Categories.v#L40
Overwriting previous delimiting key cat in scope cat
Build largecatmodules (Coq latest): UniMath/Foundations/PartA.v#L376
Declaring arbitrary terms as hints is fragile; it is recommended to
Build GrpdHITs (Coq latest): UniMath/CategoryTheory/Core/Isos.v#L21
Overwriting previous delimiting key cat in scope cat
Build largecatmodules (Coq latest): UniMath/CategoryTheory/Core/Categories.v#L40
Overwriting previous delimiting key cat in scope cat
Build GrpdHITs (Coq latest): UniMath/CategoryTheory/Core/Univalence.v#L19
Overwriting previous delimiting key cat in scope cat
Build largecatmodules (Coq latest): UniMath/CategoryTheory/Core/Isos.v#L21
Overwriting previous delimiting key cat in scope cat
Build largecatmodules (Coq latest): UniMath/CategoryTheory/Core/Univalence.v#L19
Overwriting previous delimiting key cat in scope cat
Build GrpdHITs (Coq latest): UniMath/CategoryTheory/Core/TransportMorphisms.v#L7
Overwriting previous delimiting key cat in scope cat
Build largecatmodules (Coq latest): UniMath/CategoryTheory/Core/TransportMorphisms.v#L7
Overwriting previous delimiting key cat in scope cat
Build GrpdHITs (Coq latest): UniMath/CategoryTheory/Core/Functors.v#L31
Overwriting previous delimiting key cat in scope cat
Build largecatmodules (Coq latest): UniMath/CategoryTheory/Core/Functors.v#L31
Overwriting previous delimiting key cat in scope cat
Build GrpdHITs (Coq latest): UniMath/CategoryTheory/Core/NaturalTransformations.v#L19
Overwriting previous delimiting key cat in scope cat
Build largecatmodules (Coq latest): UniMath/CategoryTheory/Subcategory/Core.v#L23
Overwriting previous delimiting key cat in scope cat
Build GrpdHITs (Coq latest): UniMath/CategoryTheory/Core/Setcategories.v#L11
Overwriting previous delimiting key cat in scope cat
Build largecatmodules (Coq latest): UniMath/CategoryTheory/Core/Setcategories.v#L11
Overwriting previous delimiting key cat in scope cat
Build SetHITs (Coq latest)
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3, actions/cache/restore@v3, actions/cache/save@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
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 dev)
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3, actions/cache/restore@v3, actions/cache/save@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
Build SetHITs (Coq latest): UniMath/CategoryTheory/Core/Categories.v#L40
Overwriting previous delimiting key cat in scope cat
Build SetHITs (Coq dev): UniMath/Foundations/Preamble.v#L68
The '%' scope delimiter in 'Arguments' commands is deprecated, use
Build SetHITs (Coq latest): UniMath/CategoryTheory/Core/Isos.v#L21
Overwriting previous delimiting key cat in scope cat
Build SetHITs (Coq dev): UniMath/Foundations/PartA.v#L350
Declaring arbitrary terms as hints is fragile; it is recommended to
Build SetHITs (Coq latest): UniMath/CategoryTheory/Core/Univalence.v#L19
Overwriting previous delimiting key cat in scope cat
Build SetHITs (Coq dev): UniMath/Foundations/PartA.v#L376
Declaring arbitrary terms as hints is fragile; it is recommended to
Build SetHITs (Coq latest): UniMath/CategoryTheory/Core/TransportMorphisms.v#L7
Overwriting previous delimiting key cat in scope cat
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 latest): UniMath/CategoryTheory/Core/Functors.v#L31
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 latest): UniMath/CategoryTheory/Core/NaturalTransformations.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 latest): UniMath/CategoryTheory/Subcategory/Core.v#L23
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 latest): UniMath/CategoryTheory/Core/Setcategories.v#L11
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 largecatmodules (Coq dev)
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3, actions/cache/restore@v3, actions/cache/save@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
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/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 TypeTheory (Coq latest)
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3, actions/cache/restore@v3, actions/cache/save@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
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/Core/Categories.v#L40
Overwriting previous delimiting key cat in scope cat
Build TypeTheory (Coq latest): UniMath/CategoryTheory/Core/Isos.v#L21
Overwriting previous delimiting key cat in scope cat
Build TypeTheory (Coq latest): UniMath/CategoryTheory/Core/Univalence.v#L19
Overwriting previous delimiting key cat in scope cat
Build TypeTheory (Coq latest): UniMath/CategoryTheory/Core/TransportMorphisms.v#L7
Overwriting previous delimiting key cat in scope cat
Build TypeTheory (Coq latest): UniMath/CategoryTheory/Core/Functors.v#L31
Overwriting previous delimiting key cat in scope cat
Build TypeTheory (Coq latest): UniMath/CategoryTheory/Core/NaturalTransformations.v#L19
Overwriting previous delimiting key cat in scope cat
Build TypeTheory (Coq latest): UniMath/CategoryTheory/Core/Setcategories.v#L11
Overwriting previous delimiting key cat in scope cat
Build TypeTheory (Coq latest): UniMath/CategoryTheory/Subcategory/Core.v#L23
Overwriting previous delimiting key cat in scope cat
Build on Linux (Coq dev)
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3, actions/cache/restore@v3, actions/cache/save@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
Build on Linux (Coq dev)
Cache save failed.
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/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