Skip to content

[CI] Add Rocq 9.1+rc1 #392

[CI] Add Rocq 9.1+rc1

[CI] Add Rocq 9.1+rc1 #392

Triggered via pull request July 10, 2025 08:27
@proux01proux01
synchronize #189
Status Cancelled
Total duration 7m 58s
Artifacts
This run and associated checks have been archived and are scheduled for deletion. Learn more about checks retention

nix-action-rocq-9.0.yml

on: pull_request_target
metacoq-utils
0s
metacoq-utils
metarocq-utils
0s
metarocq-utils
coqprime
0s
coqprime
math-classes
0s
math-classes
CoLoR
0s
CoLoR
bignums-test
0s
bignums-test
simple-io
0s
simple-io
riscvcoq
0s
riscvcoq
Cheerios
0s
Cheerios
coq-hammer
0s
coq-hammer
relation-algebra
0s
relation-algebra
stalmarck-tactic
0s
stalmarck-tactic
mathcomp-ssreflect
0s
mathcomp-ssreflect
mathcomp-fingroup
0s
mathcomp-fingroup
smtcoq-trakt
0s
smtcoq-trakt
metacoq-common
0s
metacoq-common
metarocq-common
0s
metarocq-common
fiat-crypto-legacy
0s
fiat-crypto-legacy
QuickChick
0s
QuickChick
bedrock2
0s
bedrock2
iris-examples
0s
iris-examples
itree-io
0s
itree-io
category-theory
0s
category-theory
deriving
0s
deriving
mathcomp-algebra
0s
mathcomp-algebra
metacoq-pcuic
0s
metacoq-pcuic
metacoq-template-coq
metacoq-template-coq
metarocq-pcuic
metarocq-pcuic
metarocq-template-rocq
0s
metarocq-template-rocq
quickchick-test
0s
quickchick-test
rupicola
0s
rupicola
async-test
0s
async-test
VerdiRaft
0s
VerdiRaft
mathcomp-solvable
0s
mathcomp-solvable
mathcomp-zify
mathcomp-zify
mathcomp-classical
0s
mathcomp-classical
mathcomp-word
mathcomp-word
fcsl-pcm
0s
fcsl-pcm
metacoq-safechecker
metacoq-safechecker
metacoq-template-pcuic
metacoq-template-pcuic
metacoq-translations
metacoq-translations
metarocq-safechecker
metarocq-safechecker
metarocq-template-pcuic
metarocq-template-pcuic
metarocq-translations
metarocq-translations
fiat-crypto
fiat-crypto
mathcomp-field
0s
mathcomp-field
mathcomp-algebra-tactics
mathcomp-algebra-tactics
mathcomp-reals
0s
mathcomp-reals
metacoq-erasure
0s
metacoq-erasure
metacoq-quotation
0s
metacoq-quotation
metacoq-safechecker-plugin
0s
metacoq-safechecker-plugin
metarocq-erasure
0s
metarocq-erasure
metarocq-safechecker-plugin
0s
metarocq-safechecker-plugin
metarocq-quotation
0s
metarocq-quotation
fiat-crypto-ocaml
0s
fiat-crypto-ocaml
mathcomp-character
0s
mathcomp-character
mathcomp-analysis
0s
mathcomp-analysis
mathcomp-reals-stdlib
mathcomp-reals-stdlib
metacoq-erasure-plugin
0s
metacoq-erasure-plugin
metarocq-erasure-plugin
0s
metarocq-erasure-plugin
mathcomp
mathcomp
mathcomp-analysis-stdlib
mathcomp-analysis-stdlib
metarocq-test
0s
metarocq-test
Fit to window
Zoom out
Zoom in

Annotations

43 errors
rocq-elpi-test
Process completed with exit code 1.
rocq-elpi
Process completed with exit code 1.
mathcomp-bigenough
Process completed with exit code 1.
mathcomp-finmap
Process completed with exit code 1.
coq-elpi
Process completed with exit code 1.
coq-performance-tests
The run was canceled by @proux01.
aac-tactics
The run was canceled by @proux01.
atbr
The run was canceled by @proux01.
sf
The run was canceled by @proux01.
coquelicot
The run was canceled by @proux01.
ExtLib
The run was canceled by @proux01.
ceres
The run was canceled by @proux01.
coq-tools
The run was canceled by @proux01.
argosy
The run was canceled by @proux01.
StructTact
The run was canceled by @proux01.
bbv
The run was canceled by @proux01.
engine-bench
The run was canceled by @proux01.
autosubst
The run was canceled by @proux01.
equations
The run was canceled by @proux01.
tlc
The run was canceled by @proux01.
MenhirLib
The run was canceled by @proux01.
coqutil
The run was canceled by @proux01.
bignums
The run was canceled by @proux01.
stdpp
The run was canceled by @proux01.
paco
The run was canceled by @proux01.
neural-net-coq-interp
The run was canceled by @proux01.
rewriter
The run was canceled by @proux01.
InfSeqExt
The run was canceled by @proux01.
stdlib-refman-html
The run was canceled by @proux01.
flocq
The run was canceled by @proux01.
waterproof
The run was canceled by @proux01.
stalmarck
The run was canceled by @proux01.
cross-crypto
The run was canceled by @proux01.
coinduction
The run was canceled by @proux01.
dpdgraph-test
The run was canceled by @proux01.
rocq-lean-import
The run was canceled by @proux01.
coq-hammer-tactics
The run was canceled by @proux01.
smtcoq
The run was canceled by @proux01.
mtac2
The run was canceled by @proux01.
kami
The run was canceled by @proux01.
itauto
The run was canceled by @proux01.
paramcoq-test
The run was canceled by @proux01.
Nix CI for bundle rocq-9.0
The run was canceled by @proux01.