Skip to content

CI (Coq)

CI (Coq) #586

Triggered via schedule July 1, 2024 00:38
Status Success
Total duration 3h 43m 9s
Artifacts 13

coq.yml

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

Annotations

63 warnings
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.16-native)
Unused variable nlimbs catches more than one case.
build (8.9)
There is no option NativeCompute Timing.
build (8.9)
There is no option NativeCompute Timing.
build (8.8)
There is no option NativeCompute Timing.
build (8.8)
There is no option NativeCompute Timing.
build (8.17-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 (dev-native)
Unused variable: id.
build (dev-native)
Unused variable: id.
build (dev-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.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.18-native)
Unused variable nlimbs might be a misspelled constructor. Use _ or
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.
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.
deploy
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: JamesIves/github-pages-deploy-action@releases/v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
deploy
The following actions uses node12 which is deprecated and will be forced to run on node16: JamesIves/github-pages-deploy-action@releases/v3. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
deploy-history
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: JamesIves/github-pages-deploy-action@releases/v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
deploy-history
The following actions uses node12 which is deprecated and will be forced to run on node16: JamesIves/github-pages-deploy-action@releases/v3. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/

Artifacts

Produced during runtime
Name Size
8.10 Expired
13.8 MB
8.11 Expired
16.5 MB
8.12 Expired
17.1 MB
8.13 Expired
16.2 MB
8.14 Expired
16.4 MB
8.15 Expired
16.5 MB
8.16-native Expired
17.6 MB
8.17-native Expired
17 MB
8.18-native Expired
17.4 MB
8.19-native Expired
17.2 MB
8.8 Expired
12.9 MB
8.9 Expired
13.3 MB
dev-native Expired
17 MB