Tweak CI #1219
andrew-appelAnnotations
113 warnings
|
build (9.1, 64, vst):
compcert/lib/IEEE754_extra.v#L22
"From Coq" has been replaced by "From Stdlib".
|
|
build (9.1, 64, vst):
compcert/lib/IEEE754_extra.v#L21
"From Coq" has been replaced by "From Stdlib".
|
|
build (9.1, 64, vst):
compcert/common/Errors.v#L19
"From Coq" has been replaced by "From Stdlib".
|
|
build (9.1, 64, vst):
compcert/lib/Coqlib.v#L1336
"From Coq" has been replaced by "From Stdlib".
|
|
build (9.1, 64, vst):
compcert/lib/Coqlib.v#L866
Notation rev_length is deprecated since 8.20.
|
|
build (9.1, 64, vst):
compcert/lib/Coqlib.v#L866
Notation rev_length is deprecated since 8.20.
|
|
build (9.1, 64, vst):
compcert/lib/Coqlib.v#L866
Notation rev_length is deprecated since 8.20.
|
|
build (9.1, 64, vst):
compcert/lib/Coqlib.v#L866
Notation rev_length is deprecated since 8.20.
|
|
build (9.1, 64, vst):
compcert/lib/Coqlib.v#L866
Notation rev_length is deprecated since 8.20.
|
|
build (9.1, 64, 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, 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 (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.
|
|
test (9.0, test2, 32)
"From Coq" has been replaced by "From Stdlib".
|
|
test (9.0, test2, 32)
"From Coq" has been replaced by "From Stdlib".
|
|
test (9.0, test2, 32)
"From Coq" has been replaced by "From Stdlib".
|
|
test (9.0, test2, 32)
"From Coq" has been replaced by "From Stdlib".
|
|
test (9.0, test2, 32)
"From Coq" has been replaced by "From Stdlib".
|
|
test (9.0, test2, 32)
"From Coq" has been replaced by "From Stdlib".
|
|
test (9.0, test2, 32)
"From Coq" has been replaced by "From Stdlib".
|
|
test (9.0, test2, 32)
"From Coq" has been replaced by "From Stdlib".
|
|
test (9.0, test2, 32)
"From Coq" has been replaced by "From Stdlib".
|
|
test (9.0, test2, 32)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test5, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test5, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test5, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test5, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test5, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test5, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test5, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test5, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test5, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test5, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test2, 64)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 64)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 64)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 64)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 64)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 64)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 64)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 64)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test2, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test2, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test4, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test4, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test4, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test4, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test4, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test4, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test4, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test4, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test4, 64)
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
test (dev, test4, 64)
Hint Db norm already exists and is discriminated.
|
|
test (9.0, test2, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (9.0, test2, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (9.0, test2, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (9.0, test2, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (9.0, test2, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (9.0, test2, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (9.0, test2, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (9.0, test2, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (9.0, test2, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (9.0, test2, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test, 64)
Implicitly declaring Rewrite hint databases is deprecated. Please
|
|
test (dev, test, 64)
Hint Db norm already exists and is discriminated.
|
|
test (dev, test, 64)
Hint Db norm already exists and is discriminated.
|
|
test (9.0, test3, 32)
Loading Stdlib without prefix is deprecated.
|
|
test (9.0, test3, 32)
Loading Stdlib without prefix is deprecated.
|
|
test (9.0, test3, 32)
Loading Stdlib without prefix is deprecated.
|
|
test (9.0, test3, 32)
Loading Stdlib without prefix is deprecated.
|
|
test (9.0, test3, 32)
Loading Stdlib without prefix is deprecated.
|
|
test (9.0, test3, 32)
Loading Stdlib without prefix is deprecated.
|
|
test (9.0, test3, 32)
"From Coq" has been replaced by "From Stdlib".
|
|
test (9.0, test3, 32)
"From Coq" has been replaced by "From Stdlib".
|
|
test (9.0, test3, 32)
Loading Stdlib without prefix is deprecated.
|
|
test (9.0, test3, 32)
Loading Stdlib without prefix is deprecated.
|
|
test (9.0, test, 32)
Reference Zeq_bool_eq is deprecated since 9.0. Use Z.eqb_eq instead.
|
|
test (9.0, test, 32)
Reference Zeq_bool_eq is deprecated since 9.0. Use Z.eqb_eq instead.
|
|
test (9.0, test, 32)
Reference Zeq_bool_eq is deprecated since 9.0. Use Z.eqb_eq instead.
|
|
test (9.0, test, 32)
Reference Zeq_is_eq_bool is deprecated since 9.0.
|
|
test (9.0, test, 32)
Reference Zeq_is_eq_bool is deprecated since 9.0.
|
|
test (9.0, test, 32)
Loading Stdlib without prefix is deprecated.
|
|
test (9.0, test, 32)
Loading Stdlib without prefix is deprecated.
|
|
test (9.0, test, 32)
Loading Stdlib without prefix is deprecated.
|
|
test (9.0, test, 32)
Loading Stdlib without prefix is deprecated.
|
|
test (9.0, test, 32)
Loading Stdlib without prefix is deprecated.
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
VST build artifacts 9.0 32
Expired
|
113 MB |
sha256:63eb5e2d03770bb127d77e6a57679413c97f976a1860d8f9ab48d4c0928f008e
|
|
|
VST build artifacts 9.0 64
Expired
|
151 MB |
sha256:3ccb5e9b99f56dbd17fe0842ff1a0c220499b75fad3b5255d72d7fbec35a7712
|
|
|
VST build artifacts 9.1 64
Expired
|
110 MB |
sha256:6bf7c56328a7282679a6bb71572a5f7b032695ad4d08ebcf5d29554a3922d32b
|
|
|
VST build artifacts dev 64
Expired
|
114 MB |
sha256:4af9cd756b84326f0c701ae763a7cc1f5928240409f3fb688a5b3d8293e3d82f
|
|