Skip to content
Docker CI

Use coinduction instead of paco #13

Sign in to view logs

Use coinduction instead of paco

Use coinduction instead of paco #13

Triggered via pull request January 22, 2026 17:45
@LysxiaLysxia
opened #282
coinduction
Status Failure
Total duration 3m 3s
Artifacts –

docker-action.yml

on: pull_request
Matrix: build
Fit to window
Zoom out
Zoom in

Annotations

9 errors and 20 warnings
build (coqorg/coq:8.17): theories/Eq/Eqit.v#L33
Cannot find a physical path bound to logical path
build (coqorg/coq:8.19): theories/Eq/Eqit.v#L33
Cannot find a physical path bound to logical path
build (coqorg/coq:8.20): theories/Eq/Eqit.v#L33
Cannot find a physical path bound to logical path
build (coqorg/coq:8.14): theories/Eq/Eqit.v#L33
Cannot find a physical path bound to logical path matching suffix
build (rocq/rocq-prover:9.0): theories/Eq/Eqit.v#L33
Cannot find a physical path bound to logical path
build (coqorg/coq:8.18): theories/Eq/Eqit.v#L33
Cannot find a physical path bound to logical path
build (coqorg/coq:8.16): theories/Eq/Eqit.v#L33
Cannot find a physical path bound to logical path
build (coqorg/coq:8.15): theories/Eq/Eqit.v#L33
Cannot find a physical path bound to logical path
build (rocq/rocq-prover:dev): theories/Eq/Eqit.v#L33
Cannot find a physical path bound to logical path
build (rocq/rocq-prover:9.0): theories/Basics/HeterogeneousRelations.v#L1
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/Basics/CategoryTheory.v#L7
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/Eq/Shallow.v#L14
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/Basics/Monad.v#L4
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/Basics/CategoryFunctor.v#L3
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/Indexed/Relation.v#L4
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/Axioms.v#L14
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/Axioms.v#L6
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/Basics/Basics.v#L9
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/Basics/Basics.v#L6
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:dev): theories/Basics/CategoryOps.v#L251
Use of "Notation" keyword for abbreviations is deprecated, use
build (rocq/rocq-prover:dev): theories/Basics/CategoryOps.v#L250
Use of "Notation" keyword for abbreviations is deprecated, use
build (rocq/rocq-prover:dev): theories/Basics/CategoryOps.v#L249
Use of "Notation" keyword for abbreviations is deprecated, use
build (rocq/rocq-prover:dev): theories/Basics/CategoryOps.v#L79
Use of "Notation" keyword for abbreviations is deprecated, use
build (rocq/rocq-prover:dev): theories/Basics/CategoryOps.v#L62
Use of "Notation" keyword for abbreviations is deprecated, use
build (rocq/rocq-prover:dev): theories/Axioms.v#L14
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:dev): theories/Axioms.v#L6
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:dev): theories/Basics/Basics.v#L46
Use of "Notation" keyword for abbreviations is deprecated, use
build (rocq/rocq-prover:dev): theories/Basics/Basics.v#L9
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:dev): theories/Basics/Basics.v#L6
"From Coq" has been replaced by "From Stdlib".