Skip to content

CI (Coq)

CI (Coq) #607

Triggered via schedule March 1, 2025 00:44
Status Success
Total duration 3h 30m 10s
Artifacts 13

coq.yml

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

Annotations

66 warnings
build (8.16-native)
Unused variable nlimbs catches more than one case.
build (dev-native)
"From Coq" has been replaced by "From Stdlib".
build (dev-native)
"From Coq" has been replaced by "From Stdlib".
build (dev-native)
Loading Stdlib without prefix is deprecated.
build (dev-native)
"From Coq" has been replaced by "From Stdlib".
build (dev-native)
"From Coq" has been replaced by "From Stdlib".
build (dev-native)
"From Coq" has been replaced by "From Stdlib".
build (dev-native)
"From Coq" has been replaced by "From Stdlib".
build (dev-native)
"From Coq" has been replaced by "From Stdlib".
build (dev-native)
"From Coq" has been replaced by "From Stdlib".
build (dev-native)
"From Coq" has been replaced by "From Stdlib".
build (8.10)
There is no option NativeCompute Timing.
build (8.10)
There is no option NativeCompute Timing.
build (8.10)
There is no option NativeCompute Timing.
build (8.10)
There is no option NativeCompute Timing.
build (8.10)
There is no option NativeCompute Timing.
build (8.10)
There is no option NativeCompute Timing.
build (8.10)
There is no option NativeCompute Timing.
build (8.10)
There is no option NativeCompute Timing.
build (8.10)
There is no option NativeCompute Timing.
build (8.13)
Unused variable nlimbs catches more than one case.
build (8.13)
grammar entry "ident" permitted "_" in addition to proper
build (8.13)
grammar entry "ident" permitted "_" in addition to proper
build (8.13)
grammar entry "ident" permitted "_" in addition to proper
build (8.13)
grammar entry "ident" permitted "_" in addition to proper
build (8.13)
native_compute disabled at configure time; falling back to
build (8.13)
grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead.
build (8.13)
grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead.
build (8.13)
grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead.
build (8.13)
native_compute disabled at configure time; falling back to vm_compute.
build (8.18-native)
Unused variable nlimbs might be a misspelled constructor. Use _ or
build (8.19-native)
Unused variable nlimbs might be a misspelled constructor. Use _ or
build (8.8)
There is no option NativeCompute Timing.
build (8.8)
There is no option NativeCompute Timing.
build (8.15)
Unused variable nlimbs catches more than one case.
build (8.15)
grammar entry "ident" permitted "_" in addition to proper
build (8.15)
grammar entry "ident" permitted "_" in addition to proper
build (8.15)
grammar entry "ident" permitted "_" in addition to proper
build (8.15)
grammar entry "ident" permitted "_" in addition to proper
build (8.15)
native_compute disabled at configure time; falling back to
build (8.15)
grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead.
build (8.15)
grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead.
build (8.15)
grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead.
build (8.15)
native_compute disabled at configure time; falling back to vm_compute.
build (8.17-native)
Unused variable nlimbs might be a misspelled constructor. Use _ or
build (8.14)
Unused variable nlimbs catches more than one case.
build (8.14)
grammar entry "ident" permitted "_" in addition to proper
build (8.14)
grammar entry "ident" permitted "_" in addition to proper
build (8.14)
grammar entry "ident" permitted "_" in addition to proper
build (8.14)
grammar entry "ident" permitted "_" in addition to proper
build (8.14)
native_compute disabled at configure time; falling back to
build (8.14)
grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead.
build (8.14)
grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead.
build (8.14)
grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead.
build (8.14)
native_compute disabled at configure time; falling back to vm_compute.
build (8.9)
There is no option NativeCompute Timing.
build (8.9)
There is no option NativeCompute Timing.
build (8.11)
There is no option NativeCompute Timing.
build (8.11)
There is no option NativeCompute Timing.
build (8.11)
There is no option NativeCompute Timing.
build (8.11)
There is no option NativeCompute Timing.
build (8.11)
There is no option NativeCompute Timing.
build (8.11)
There is no option NativeCompute Timing.
build (8.11)
There is no option NativeCompute Timing.
build (8.11)
There is no option NativeCompute Timing.
build (8.11)
There is no option NativeCompute Timing.

Artifacts

Produced during runtime
Name Size Digest
8.10
14.1 MB
sha256:60edb4283d48fed30278b15f87c5a4b0599c609296e99fd839f3af79393b8a14
8.11
16.6 MB
sha256:1cf5cd047451fac38e4baf359aedf8580397de438fc23fba3dd9d65e3514a8da
8.12
17.4 MB
sha256:99b4bc491d62374d20a399798ed96e55df0602fccf991348da66b6b61efdf4ab
8.13
17 MB
sha256:9169ca469f36257fa08be0704cfea0d93481c17d1e443a2abc77005973de9649
8.14
16.3 MB
sha256:f6146d78f9993f40a0b127ed9941f3ff620587f4d0083c87a861b652f8acd3ba
8.15
16.4 MB
sha256:ebfb474ac525e71027bd699134959827408c68c1f4666dabce23980597f2bfee
8.16-native
17.1 MB
sha256:31d07308096b31b8b4a8d359e229480569b51c151758eb891442dcd5f6bded99
8.17-native
16.9 MB
sha256:e91703ed3afc4e0b733b3206efa1ffc669105a8dfae45714477c1fb3db9a88f5
8.18-native
17.2 MB
sha256:9bef9adfd40b624967663be6568919920a8e25f8e73fafa484ab6b3b30c4efb9
8.19-native
17.3 MB
sha256:220bbfe7b2617fc79ebbf12a6855707aa97c836f2ea3274fef51ca1eb71b01fe
8.8
13.2 MB
sha256:01f192f5e1ecc5e2e5f06cb9c7bb55b560c833653d4e829a2dfa91813b12b12b
8.9
13.4 MB
sha256:997c24c67d99da0df57f03708c55a2cb63a9a1c92ab5e33033974dcbe4139e97
dev-native
17.1 MB
sha256:048fa1cdf69ed01a0c885d0b6f1fbb768c8259151263809ea23207e1e15e244b