Skip to content
Docker CI

[WIP] Moving to stdpp #12

Sign in to view logs

[WIP] Moving to stdpp

[WIP] Moving to stdpp #12

Triggered via pull request November 19, 2025 14:14
@LysxiaLysxia
synchronize #267
stdpp
Status Failure
Total duration 3m 49s
Artifacts –

docker-action.yml

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

Annotations

22 errors and 10 warnings
build (coqorg/coq:8.18): theories/Props/HasPost.v#L248
(in proof eutt_eq_itree): Attempt to save an incomplete proof
build (coqorg/coq:8.18): theories/Events/Exception.v#L29
The reference Functor.fmap was not found in the current environment.
build (coqorg/coq:8.18): theories/Events/Writer.v#L13
Cannot find a physical path bound to logical path
build (coqorg/coq:8.18): theories/Events/MapDefault.v#L7
Cannot find a physical path bound to logical path
build (coqorg/coq:8.18): theories/Events/Map.v#L10
Cannot find a physical path bound to logical path
build (coqorg/coq:8.19): theories/Props/HasPost.v#L248
(in proof eutt_eq_itree): Attempt to save an incomplete proof
build (coqorg/coq:8.19): theories/Events/Exception.v#L29
The reference Functor.fmap was not found in the current environment.
build (coqorg/coq:8.19): theories/Events/Writer.v#L13
Cannot find a physical path bound to logical path
build (coqorg/coq:8.19): theories/Events/MapDefault.v#L7
Cannot find a physical path bound to logical path
build (coqorg/coq:8.19): theories/Events/Map.v#L10
Cannot find a physical path bound to logical path
build (rocq/rocq-prover:9.0): theories/Props/HasPost.v#L248
(in proof eutt_eq_itree): Attempt to save an incomplete proof
build (rocq/rocq-prover:9.0): theories/Interp/InterpFacts.v#L389
Found no subterm matching "interp ?i (x ← ?i0; ?i1 x)"
build (rocq/rocq-prover:9.0): theories/Events/Exception.v#L29
The reference Functor.fmap was not found in the current environment.
build (rocq/rocq-prover:9.0): theories/Events/Writer.v#L14
Cannot find a physical path bound to logical path
build (rocq/rocq-prover:9.0): theories/Events/MapDefault.v#L8
Cannot find a physical path bound to logical path
build (rocq/rocq-prover:9.0): theories/Events/Map.v#L10
Cannot find a physical path bound to logical path
build (coqorg/coq:8.20): theories/Props/HasPost.v#L248
(in proof eutt_eq_itree): Attempt to save an incomplete proof
build (coqorg/coq:8.20): theories/Interp/InterpFacts.v#L389
Found no subterm matching "interp ?i (x ← ?i0; ?i1 x)"
build (coqorg/coq:8.20): theories/Events/Exception.v#L29
The reference Functor.fmap was not found in the current environment.
build (coqorg/coq:8.20): theories/Events/Writer.v#L14
Cannot find a physical path bound to logical path
build (coqorg/coq:8.20): theories/Events/MapDefault.v#L8
Cannot find a physical path bound to logical path
build (coqorg/coq:8.20): theories/Events/Map.v#L10
Cannot find a physical path bound to logical path
build (rocq/rocq-prover:9.0): theories/Basics/CategoryRelations.v#L1
"From Coq" has been replaced by "From Stdlib".
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/CategoryKleisli.v#L18
"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/CategoryTheory.v#L7
"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/Basics/CategoryFunctor.v#L3
"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: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".