Skip to content

Fix a bunch of Coq 8.20 deprecations #1109

Fix a bunch of Coq 8.20 deprecations

Fix a bunch of Coq 8.20 deprecations #1109

Triggered via pull request January 3, 2025 13:19
Status Failure
Total duration 20m 53s
Artifacts 1

coq-action.yml

on: pull_request
Matrix: build
Matrix: test
Fit to window
Zoom out
Zoom in

Annotations

3 errors and 14 warnings
build (8.19, 64, vst): zlist/sublist.v#L340
The variable length_rev was not found in the current environment.
build (8.19, 32, vst): zlist/sublist.v#L340
The variable length_rev was not found in the current environment.
build (8.18, 64, vst): zlist/sublist.v#L340
The variable length_rev was not found in the current environment.
build (8.19, 64, vst)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
build (8.19, 32, vst)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
build (8.18, 64, vst)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
build (dev, 64, vst)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
build (dev, 64, vst): msl/Axioms.v#L7
"From Coq" has been replaced by "From Stdlib".
build (dev, 64, vst): msl/Axioms.v#L23
"From Coq" has been replaced by "From Stdlib".
build (dev, 64, vst): msl/Extensionality.v#L5
"From Coq" has been replaced by "From Stdlib".
build (dev, 64, vst): msl/Extensionality.v#L139
Coq.Init.Prelude.f_equal has been replaced by
build (dev, 64, vst): msl/base.v#L10
"From Coq" has been replaced by "From Stdlib".
build (dev, 64, vst): msl/base.v#L11
"From Coq" has been replaced by "From Stdlib".
build (dev, 64, vst): msl/base.v#L12
"From Coq" has been replaced by "From Stdlib".
build (dev, 64, vst): msl/base.v#L13
Loading Stdlib without prefix is deprecated.
build (dev, 64, vst): msl/ageable.v#L7
"From Coq" has been replaced by "From Stdlib".
build (dev, 64, vst): msl/ageable.v#L193
"From Coq" has been replaced by "From Stdlib".

Artifacts

Produced during runtime
Name Size
VST build artifacts dev 64 Expired
109 MB