Skip to content
Docker CI

Add the latest Docker images to the CI. #66

Sign in to view logs

Add the latest Docker images to the CI.

Add the latest Docker images to the CI. #66

Triggered via pull request September 29, 2025 13:23
@SkySkimmerSkySkimmer
reopened #157
ppedrot:fix-rocq-docker-image
Status Success
Total duration 1h 11m 5s
Artifacts 1

docker-action.yml

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

Annotations

121 warnings
build (coqorg/coq:8.11): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.11): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.11): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.11): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.11): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.11): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.11): theories/Structures/IXMonad.v#L14
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.11): theories/Structures/Monad.v#L58
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.11): theories/Programming/With.v#L59
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.11): theories/Data/Eq/UIP_trans.v#L56
Implicit arguments declaration relies on type. Discarding
build (coqorg/coq:8.12-ocaml-4.10-flambda): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.12-ocaml-4.10-flambda): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.12-ocaml-4.10-flambda): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.12-ocaml-4.10-flambda): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.12-ocaml-4.10-flambda): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.12-ocaml-4.10-flambda): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.12-ocaml-4.10-flambda): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.12-ocaml-4.10-flambda): theories/Structures/IXMonad.v#L14
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.12-ocaml-4.10-flambda): theories/Structures/Monad.v#L58
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.12-ocaml-4.10-flambda): theories/Programming/With.v#L59
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.13): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.13): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.13): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.13): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.13): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.13): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.13): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.13): theories/Structures/IXMonad.v#L14
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.13): theories/Structures/Monad.v#L58
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.13): theories/Programming/With.v#L59
Declaring a scope implicitly is deprecated; use in advance an
build (rocq/rocq-prover:dev): theories/Data/ListNth.v#L1
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:dev): theories/Data/PreFun.v#L2
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:dev): theories/Data/PreFun.v#L1
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:dev): theories/Core/EquivDec.v#L7
Loading Stdlib without prefix is deprecated.
build (rocq/rocq-prover:dev): theories/Core/EquivDec.v#L7
Loading Stdlib without prefix is deprecated.
build (rocq/rocq-prover:dev): theories/Core/Decision.v#L1
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:dev): theories/Core/EquivDec.v#L1
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:dev): theories/Core/RelDec.v#L3
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:dev): theories/Core/RelDec.v#L2
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:dev): theories/Core/RelDec.v#L1
"From Coq" has been replaced by "From Stdlib".
build (coqorg/coq:8.18): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.18): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.18): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.18): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.18): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.18): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.18): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.18): theories/Structures/IXMonad.v#L14
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.18): theories/Structures/Monad.v#L58
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.18): theories/Programming/With.v#L59
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.17): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.17): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.17): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.17): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.17): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.17): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.17): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.17): theories/Structures/IXMonad.v#L14
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.17): theories/Structures/Monad.v#L58
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.17): theories/Programming/With.v#L59
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.16)
No files were found with the provided path: html. No artifacts will be uploaded.
build (coqorg/coq:8.16): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.16): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.16): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.16): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.16): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.16): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.16): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.16): theories/Structures/IXMonad.v#L14
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.16): theories/Structures/Monad.v#L58
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.16): theories/Programming/With.v#L59
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.15): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.15): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.15): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.15): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.15): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.15): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.15): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.15): theories/Structures/IXMonad.v#L14
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.15): theories/Structures/Monad.v#L58
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.15): theories/Programming/With.v#L59
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.14): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.14): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.14): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.14): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.14): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.14): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.14): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.14): theories/Structures/IXMonad.v#L14
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.14): theories/Structures/Monad.v#L58
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.14): theories/Programming/With.v#L59
Declaring a scope implicitly is deprecated; use in advance an
build (rocq/rocq-prover:9.0): theories/Data/ListNth.v#L1
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/Data/PreFun.v#L2
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/Data/PreFun.v#L1
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/Core/EquivDec.v#L7
Loading Stdlib without prefix is deprecated.
build (rocq/rocq-prover:9.0): theories/Core/EquivDec.v#L7
Loading Stdlib without prefix is deprecated.
build (rocq/rocq-prover:9.0): theories/Core/Decision.v#L1
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/Core/EquivDec.v#L1
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/Core/RelDec.v#L3
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/Core/RelDec.v#L2
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/Core/RelDec.v#L1
"From Coq" has been replaced by "From Stdlib".
build (coqorg/coq:8.19): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.19): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.19): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.19): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.19): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.19): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.19): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.19): theories/Structures/IXMonad.v#L14
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.19): theories/Structures/Monad.v#L58
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.19): theories/Programming/With.v#L59
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.20): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.20): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.20): theories/Data/String.v#L34
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.20): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.20): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.20): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.20): theories/Data/String.v#L33
Notation bool_cmp is deprecated since 8.12.
build (coqorg/coq:8.20): theories/Structures/IXMonad.v#L14
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.20): theories/Structures/Monad.v#L58
Declaring a scope implicitly is deprecated; use in advance an
build (coqorg/coq:8.20): theories/Programming/With.v#L59
Declaring a scope implicitly is deprecated; use in advance an

Artifacts

Produced during runtime
Name Size Digest
coqdoc
397 KB
sha256:7adc3a8e9d26babd60867c2a8ebcccdea45be6705a617da44d2352d848e077aa