Skip to content

CI Build UniMath

CI Build UniMath #336

Triggered via schedule September 29, 2025 02:24
Status Success
Total duration 54m 47s
Artifacts 1

build-unimath.yml

on: schedule
Matrix: build-Unimath-ubuntu
Sanity Checks
54s
Sanity Checks
Matrix: build-satellites
Assemble the site
28s
Assemble the site
Fit to window
Zoom out
Zoom in

Annotations

60 warnings
Build Schools (Coq dev): UniMath/Foundations/PartB.v#L870
Use of "Notation" keyword for abbreviations is deprecated, use
Build Schools (Coq dev): UniMath/Foundations/PartA.v#L1770
Use of "Notation" keyword for abbreviations is deprecated, use
Build Schools (Coq dev): UniMath/Foundations/Preamble.v#L144
Use of "Notation" keyword for abbreviations is deprecated, use
Build Schools (Coq dev): UniMath/Foundations/Preamble.v#L50
Use of "Notation" keyword for abbreviations is deprecated, use
Build Schools (Coq dev): UniMath/Foundations/Preamble.v#L49
Use of "Notation" keyword for abbreviations is deprecated, use
Build Schools (Coq dev): UniMath/Foundations/Init.v#L94
Postfix notations (i.e. starting with a nonterminal symbol and
Build Schools (Coq dev): UniMath/Foundations/Init.v#L65
Closed notations (i.e. starting and ending with a terminal symbol)
Build Schools (Coq dev): UniMath/Foundations/Init.v#L61
Postfix notations (i.e. starting with a nonterminal symbol and
Build Schools (Coq dev): UniMath/Foundations/Init.v#L6
"From Coq" has been replaced by "From Stdlib".
Build Schools (Coq dev): UniMath/Foundations/Init.v#L3
"From Coq" has been replaced by "From Stdlib".
Build SetHITs (Coq dev): UniMath/Foundations/PartB.v#L870
Use of "Notation" keyword for abbreviations is deprecated, use
Build SetHITs (Coq dev): UniMath/Foundations/PartA.v#L1770
Use of "Notation" keyword for abbreviations is deprecated, use
Build SetHITs (Coq dev): UniMath/Foundations/Preamble.v#L144
Use of "Notation" keyword for abbreviations is deprecated, use
Build SetHITs (Coq dev): UniMath/Foundations/Preamble.v#L50
Use of "Notation" keyword for abbreviations is deprecated, use
Build SetHITs (Coq dev): UniMath/Foundations/Preamble.v#L49
Use of "Notation" keyword for abbreviations is deprecated, use
Build SetHITs (Coq dev): UniMath/Foundations/Init.v#L94
Postfix notations (i.e. starting with a nonterminal symbol and
Build SetHITs (Coq dev): UniMath/Foundations/Init.v#L65
Closed notations (i.e. starting and ending with a terminal symbol)
Build SetHITs (Coq dev): UniMath/Foundations/Init.v#L61
Postfix notations (i.e. starting with a nonterminal symbol and
Build SetHITs (Coq dev): UniMath/Foundations/Init.v#L6
"From Coq" has been replaced by "From Stdlib".
Build SetHITs (Coq dev): UniMath/Foundations/Init.v#L3
"From Coq" has been replaced by "From Stdlib".
Build largecatmodules (Coq dev): UniMath/Foundations/PartB.v#L870
Use of "Notation" keyword for abbreviations is deprecated, use
Build largecatmodules (Coq dev): UniMath/Foundations/PartA.v#L1770
Use of "Notation" keyword for abbreviations is deprecated, use
Build largecatmodules (Coq dev): UniMath/Foundations/Preamble.v#L144
Use of "Notation" keyword for abbreviations is deprecated, use
Build largecatmodules (Coq dev): UniMath/Foundations/Preamble.v#L50
Use of "Notation" keyword for abbreviations is deprecated, use
Build largecatmodules (Coq dev): UniMath/Foundations/Preamble.v#L49
Use of "Notation" keyword for abbreviations is deprecated, use
Build largecatmodules (Coq dev): UniMath/Foundations/Init.v#L94
Postfix notations (i.e. starting with a nonterminal symbol and
Build largecatmodules (Coq dev): UniMath/Foundations/Init.v#L65
Closed notations (i.e. starting and ending with a terminal symbol)
Build largecatmodules (Coq dev): UniMath/Foundations/Init.v#L61
Postfix notations (i.e. starting with a nonterminal symbol and
Build largecatmodules (Coq dev): UniMath/Foundations/Init.v#L6
"From Coq" has been replaced by "From Stdlib".
Build largecatmodules (Coq dev): UniMath/Foundations/Init.v#L3
"From Coq" has been replaced by "From Stdlib".
Build TypeTheory (Coq dev): UniMath/Foundations/PartB.v#L870
Use of "Notation" keyword for abbreviations is deprecated, use
Build TypeTheory (Coq dev): UniMath/Foundations/PartA.v#L1770
Use of "Notation" keyword for abbreviations is deprecated, use
Build TypeTheory (Coq dev): UniMath/Foundations/Preamble.v#L144
Use of "Notation" keyword for abbreviations is deprecated, use
Build TypeTheory (Coq dev): UniMath/Foundations/Preamble.v#L50
Use of "Notation" keyword for abbreviations is deprecated, use
Build TypeTheory (Coq dev): UniMath/Foundations/Preamble.v#L49
Use of "Notation" keyword for abbreviations is deprecated, use
Build TypeTheory (Coq dev): UniMath/Foundations/Init.v#L94
Postfix notations (i.e. starting with a nonterminal symbol and
Build TypeTheory (Coq dev): UniMath/Foundations/Init.v#L65
Closed notations (i.e. starting and ending with a terminal symbol)
Build TypeTheory (Coq dev): UniMath/Foundations/Init.v#L61
Postfix notations (i.e. starting with a nonterminal symbol and
Build TypeTheory (Coq dev): UniMath/Foundations/Init.v#L6
"From Coq" has been replaced by "From Stdlib".
Build TypeTheory (Coq dev): UniMath/Foundations/Init.v#L3
"From Coq" has been replaced by "From Stdlib".
Build GrpdHITs (Coq dev): UniMath/Foundations/PartB.v#L870
Use of "Notation" keyword for abbreviations is deprecated, use
Build GrpdHITs (Coq dev): UniMath/Foundations/PartA.v#L1770
Use of "Notation" keyword for abbreviations is deprecated, use
Build GrpdHITs (Coq dev): UniMath/Foundations/Preamble.v#L144
Use of "Notation" keyword for abbreviations is deprecated, use
Build GrpdHITs (Coq dev): UniMath/Foundations/Preamble.v#L50
Use of "Notation" keyword for abbreviations is deprecated, use
Build GrpdHITs (Coq dev): UniMath/Foundations/Preamble.v#L49
Use of "Notation" keyword for abbreviations is deprecated, use
Build GrpdHITs (Coq dev): UniMath/Foundations/Init.v#L94
Postfix notations (i.e. starting with a nonterminal symbol and
Build GrpdHITs (Coq dev): UniMath/Foundations/Init.v#L65
Closed notations (i.e. starting and ending with a terminal symbol)
Build GrpdHITs (Coq dev): UniMath/Foundations/Init.v#L61
Postfix notations (i.e. starting with a nonterminal symbol and
Build GrpdHITs (Coq dev): UniMath/Foundations/Init.v#L6
"From Coq" has been replaced by "From Stdlib".
Build GrpdHITs (Coq dev): UniMath/Foundations/Init.v#L3
"From Coq" has been replaced by "From Stdlib".
Build on Linux (Coq dev): UniMath/Foundations/PartB.v#L870
Use of "Notation" keyword for abbreviations is deprecated, use
Build on Linux (Coq dev): UniMath/Foundations/PartA.v#L1770
Use of "Notation" keyword for abbreviations is deprecated, use
Build on Linux (Coq dev): UniMath/Foundations/Preamble.v#L144
Use of "Notation" keyword for abbreviations is deprecated, use
Build on Linux (Coq dev): UniMath/Foundations/Preamble.v#L50
Use of "Notation" keyword for abbreviations is deprecated, use
Build on Linux (Coq dev): UniMath/Foundations/Preamble.v#L49
Use of "Notation" keyword for abbreviations is deprecated, use
Build on Linux (Coq dev): UniMath/Foundations/Init.v#L94
Postfix notations (i.e. starting with a nonterminal symbol and
Build on Linux (Coq dev): UniMath/Foundations/Init.v#L65
Closed notations (i.e. starting and ending with a terminal symbol)
Build on Linux (Coq dev): UniMath/Foundations/Init.v#L61
Postfix notations (i.e. starting with a nonterminal symbol and
Build on Linux (Coq dev): UniMath/Foundations/Init.v#L6
"From Coq" has been replaced by "From Stdlib".
Build on Linux (Coq dev): UniMath/Foundations/Init.v#L3
"From Coq" has been replaced by "From Stdlib".

Artifacts

Produced during runtime
Name Size Digest
rocqdoc Expired
16.8 MB
sha256:f14afa10d7b22bbf847ce950da03a5d3cbdb3733f9facfba3a3d4c9a536ddb67