Tweak CI #1215
andrew-appelAnnotations
1 error and 23 warnings
|
build (9.1, 64, vst):
msl/Axioms.v#L7
Cannot find a physical path bound to logical path
|
|
build (9.0, 32, vst):
compcert/lib/IEEE754_extra.v#L22
"From Coq" has been replaced by "From Stdlib".
|
|
build (9.0, 32, vst):
compcert/lib/IEEE754_extra.v#L21
"From Coq" has been replaced by "From Stdlib".
|
|
build (9.0, 32, vst):
compcert/common/Errors.v#L19
"From Coq" has been replaced by "From Stdlib".
|
|
build (9.0, 32, vst):
compcert/lib/Coqlib.v#L1336
"From Coq" has been replaced by "From Stdlib".
|
|
build (9.0, 32, vst):
compcert/lib/Coqlib.v#L866
Notation rev_length is deprecated since 8.20.
|
|
build (9.0, 32, vst):
compcert/lib/Coqlib.v#L866
Notation rev_length is deprecated since 8.20.
|
|
build (9.0, 32, vst):
compcert/lib/Coqlib.v#L866
Notation rev_length is deprecated since 8.20.
|
|
build (9.0, 32, vst):
compcert/lib/Coqlib.v#L866
Notation rev_length is deprecated since 8.20.
|
|
build (9.0, 32, vst):
compcert/lib/Coqlib.v#L866
Notation rev_length is deprecated since 8.20.
|
|
build (9.0, 32, vst):
compcert/lib/Coqlib.v#L21
"From Coq" has been replaced by "From Stdlib".
|
|
build (dev, 64, vst):
msl/sepalg_functors.v#L86
Using "..." is deprecated, use "; auto." instead
|
|
build (dev, 64, vst):
msl/sepalg_functors.v#L84
Using "..." is deprecated, use "; auto." instead
|
|
build (dev, 64, vst):
msl/sepalg_functors.v#L82
Using "..." is deprecated, use "; auto." instead
|
|
build (dev, 64, vst):
msl/psepalg.v#L36
Using "..." is deprecated, use "; eauto." instead
|
|
build (dev, 64, vst):
msl/psepalg.v#L34
Using "..." is deprecated, use "; eauto." instead
|
|
build (dev, 64, vst):
msl/sepalg.v#L702
Using "..." is deprecated, use "; auto." instead
|
|
build (dev, 64, vst):
msl/eq_dec.v#L50
Using "..." is deprecated, use "; auto." instead
|
|
build (dev, 64, vst):
msl/eq_dec.v#L47
Using "..." is deprecated, use "; auto." instead
|
|
build (dev, 64, vst):
msl/eq_dec.v#L29
Using "..." is deprecated, use "; auto." instead
|
|
build (dev, 64, vst):
msl/eq_dec.v#L27
Using "..." is deprecated, use "; auto." instead
|
|
build (9.0, 64, vst):
concurrency/semax_conc_pred.v#L20
Notation "_ oo _" was already used.
|
|
build (9.0, 64, vst):
floyd/functional_base.v#L96
Coq.Init.Logic.I has been replaced by Corelib.Init.Logic.I.
|
|
build (9.0, 64, vst):
floyd/functional_base.v#L96
Coq.Init.Logic.I has been replaced by Corelib.Init.Logic.I.
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
VST build artifacts 9.0 32
Expired
|
113 MB |
sha256:b828bd251885958004c962cbaeff65ea58f905a484dd6c6f5a9d0a9cca301b72
|
|
|
VST build artifacts 9.0 64
Expired
|
151 MB |
sha256:a2b122b1edea67c630b4050b1de6564cdcd1b4a4cc03c552cc43802e79175f18
|
|
|
VST build artifacts dev 64
Expired
|
114 MB |
sha256:b97f3a3a08f31d34a6194a1d2a5cbce1b78916302517376c439a07a2fa65d3af
|
|