Skip to content
Nix CI for bundle rocq-9.0

Adapt to rocq-prover/rocq#21392. #562

Sign in to view logs

Adapt to rocq-prover/rocq#21392.

Adapt to rocq-prover/rocq#21392. #562

Triggered via pull request December 4, 2025 09:40
@ppedrotppedrot
opened #227
Status Success
Total duration 1h 29m 53s
Artifacts –

nix-action-rocq-9.0.yml

on: pull_request_target
rocq-core
1m 0s
rocq-core
stdlib-warnings
4m 5s
stdlib-warnings
coq
1m 3s
coq
stdlib
3m 58s
stdlib
rocq-elpi
1m 51s
rocq-elpi
unicoq
59s
unicoq
ExtLib
1m 34s
ExtLib
equations
1m 36s
equations
StructTact
1m 27s
StructTact
coq-hammer-tactics
1m 30s
coq-hammer-tactics
paco
1m 37s
paco
MenhirLib
2m 39s
MenhirLib
ceres
1m 25s
ceres
aac-tactics
1m 28s
aac-tactics
stalmarck
1m 35s
stalmarck
InfSeqExt
1m 20s
InfSeqExt
bignums
1m 49s
bignums
argosy
4m 56s
argosy
atbr
2m 18s
atbr
bbv
1m 32s
bbv
coinduction
1m 25s
coinduction
coqutil
2m 18s
coqutil
dpdgraph-test
1m 27s
dpdgraph-test
flocq
2m 38s
flocq
kami
4m 28s
kami
neural-net-coq-interp
2m 6s
neural-net-coq-interp
paramcoq-test
1m 32s
paramcoq-test
rocq-lean-import
1m 53s
rocq-lean-import
smtcoq
2m 0s
smtcoq
stdpp
2m 40s
stdpp
tlc
1m 48s
tlc
waterproof
2m 11s
waterproof
stdlib-refman-html
3m 59s
stdlib-refman-html
hierarchy-builder
2m 30s
hierarchy-builder
coq-elpi
2m 15s
coq-elpi
rocq-elpi-test
4m 21s
rocq-elpi-test
mtac2
1m 53s
mtac2
simple-io
1m 22s
simple-io
metarocq-utils
2m 25s
metarocq-utils
Cheerios
1m 35s
Cheerios
coq-hammer
1m 33s
coq-hammer
ITree
3m 7s
ITree
parsec
1m 30s
parsec
stalmarck-tactic
1m 32s
stalmarck-tactic
bignums-test
1m 30s
bignums-test
coqprime
2m 18s
coqprime
math-classes
2m 17s
math-classes
mathcomp-boot
3m 1s
mathcomp-boot
metarocq-common
2m 1s
metarocq-common
itree-io
3m 6s
itree-io
json
2m 43s
json
QuickChick
2m 7s
QuickChick
mathcomp-fingroup
2m 5s
mathcomp-fingroup
mathcomp-order
3m 37s
mathcomp-order
mathcomp-bigenough
1m 34s
mathcomp-bigenough
mathcomp-finmap
1m 44s
mathcomp-finmap
relation-algebra
2m 38s
relation-algebra
autosubst
1m 38s
autosubst
coquelicot
2m 9s
coquelicot
metarocq-template-rocq
3m 56s
metarocq-template-rocq
async-test
3m 28s
async-test
quickchick-test
2m 40s
quickchick-test
mathcomp-algebra
7m 51s
mathcomp-algebra
mathcomp-ssreflect
3m 58s
mathcomp-ssreflect
metarocq-translations
1m 42s
metarocq-translations
http
3m 8s
http
mathcomp-solvable
7m 38s
mathcomp-solvable
mathcomp-zify
6m 56s
mathcomp-zify
fcsl-pcm
7m 33s
fcsl-pcm
mathcomp-classical
8m 22s
mathcomp-classical
Verdi
2m 11s
Verdi
mathcomp-word
6m 31s
mathcomp-word
deriving
2m 12s
deriving
mathcomp-field
7m 29s
mathcomp-field
mathcomp-algebra-tactics
2m 55s
mathcomp-algebra-tactics
mathcomp-reals
5m 2s
mathcomp-reals
mathcomp-character
7m 5s
mathcomp-character
mathcomp-analysis
20m 42s
mathcomp-analysis
mathcomp-reals-stdlib
1m 48s
mathcomp-reals-stdlib
mathcomp
1m 54s
mathcomp
mathcomp-analysis-stdlib
17m 49s
mathcomp-analysis-stdlib
Fit to window
Zoom out
Zoom in