Skip to content

Hopefully fix permission errors on native compute profiles #595

Hopefully fix permission errors on native compute profiles

Hopefully fix permission errors on native compute profiles #595

Triggered via push September 20, 2024 21:32
Status Failure
Total duration 1h 58m 18s
Artifacts 13

coq.yml

on: push
Matrix: build
check-all
0s
check-all
deploy
0s
deploy
deploy-history
0s
deploy-history
Fit to window
Zoom out
Zoom in

Annotations

1 error and 66 warnings
check-all
Process completed with exit code 1.
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.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.17-native)
Unused variable nlimbs might be a misspelled constructor. Use _ or
build (8.16-native)
Unused variable nlimbs catches more than one case.
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 (dev-native)
Coq.ZArith.ZArith has been replaced by Stdlib.ZArith.ZArith.
build (dev-native)
Coq.micromega.Lia has been replaced by Stdlib.micromega.Lia.
build (dev-native)
Coq.Classes.Morphisms has been replaced by Stdlib.Classes.Morphisms.
build (dev-native)
Coq.Setoids.Setoid has been replaced by Stdlib.Setoids.Setoid.
build (dev-native)
Coq.Lists.List has been replaced by Stdlib.Lists.List.
build (dev-native)
Coq.Classes.Morphisms has been replaced by Stdlib.Classes.Morphisms.
build (dev-native)
Coq.Setoids.Setoid has been replaced by Stdlib.Setoids.Setoid.
build (dev-native)
Coq.Classes.Morphisms has been replaced by Stdlib.Classes.Morphisms.
build (dev-native)
Coq.Strings.String has been replaced by Stdlib.Strings.String.
build (dev-native)
Coq.Structures.Orders has been replaced by Stdlib.Structures.Orders.
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.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
generated-files-8.10
7.66 MB
generated-files-8.11
1.82 MB
generated-files-8.12
2.03 MB
generated-files-8.13
1.16 MB
generated-files-8.14
1.16 MB
generated-files-8.15
1.16 MB
generated-files-8.16-native
3.78 MB
generated-files-8.17-native
5.66 MB
generated-files-8.18-native
5.64 MB
generated-files-8.19-native
2.31 MB
generated-files-8.8
4.28 MB
generated-files-8.9
4.58 MB
generated-files-dev-native
6.82 MB