Update vst/lib to VST 2.15 and CompCert 3.15 (#804) #1116
andrew-appelAnnotations
30 warnings
|
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 (8.20, 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.20, 64, vst):
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|
|
build (8.20, 64, vst):
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|
|
build (8.20, 64, vst):
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|
|
build (8.20, 64, vst):
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|
|
build (8.20, 64, vst):
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|
|
build (8.20, 64, vst):
zlist/sublist.v#L340
Notation rev_length is deprecated since 8.20.
|
|
build (8.20, 64, vst):
zlist/sublist.v#L340
Notation rev_length is deprecated since 8.20.
|
|
build (8.20, 64, vst):
zlist/sublist.v#L346
Notation app_length is deprecated since 8.20.
|
|
build (8.20, 64, vst):
zlist/sublist.v#L346
Notation app_length is deprecated since 8.20.
|
|
build (8.20, 64, vst):
zlist/sublist.v#L346
Notation app_length is deprecated since 8.20.
|
|
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, 64, vst):
compcert/lib/IEEE754_extra.v#L434
Notation IZR_neq is deprecated since 8.19.
|
|
build (8.19, 64, vst):
compcert/lib/IEEE754_extra.v#L434
Notation IZR_neq is deprecated since 8.19.
|
|
build (8.19, 64, vst):
floyd/canon.v#L14
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
build (8.19, 64, vst):
floyd/canon.v#L505
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
build (8.19, 64, vst):
floyd/proofauto.v#L61
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
build (8.19, 64, vst):
concurrency/semax_conc_pred.v#L20
Notation "_ oo _" was already used.
|
|
build (8.20, 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.20, 32, vst):
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|
|
build (8.20, 32, vst):
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|
|
build (8.20, 32, vst):
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|
|
build (8.20, 32, vst):
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|
|
build (8.20, 32, vst):
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|
|
build (8.20, 32, vst):
zlist/sublist.v#L340
Notation rev_length is deprecated since 8.20.
|
|
build (8.20, 32, vst):
zlist/sublist.v#L340
Notation rev_length is deprecated since 8.20.
|
|
build (8.20, 32, vst):
zlist/sublist.v#L346
Notation app_length is deprecated since 8.20.
|
|
build (8.20, 32, vst):
zlist/sublist.v#L346
Notation app_length is deprecated since 8.20.
|
|
build (8.20, 32, vst):
zlist/sublist.v#L346
Notation app_length is deprecated since 8.20.
|
Artifacts
Produced during runtime
| Name | Size | |
|---|---|---|
|
VST build artifacts 8.19 64
Expired
|
126 MB |
|
|
VST build artifacts 8.20 32
Expired
|
117 MB |
|
|
VST build artifacts 8.20 64
Expired
|
117 MB |
|