VST on Iris #1131
mansky1Annotations
212 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 (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/boolean_alg.v#L25
Loading Stdlib without prefix is deprecated.
|
|
build (dev, 64, vst):
msl/tree_shares.v#L12
Loading Stdlib without prefix is deprecated.
|
|
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):
msl/sepalg.v#L104
Automatically putting Flat_alg in Prop even though it was declared
|
|
build (8.20, 64, vst):
msl/sepalg_generators.v#L49
Automatically putting Void in Prop even though it was declared with
|
|
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, 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):
msl/sepalg.v#L104
Automatically putting Flat_alg in Prop even though it was declared
|
|
build (8.20, 32, vst):
msl/sepalg_generators.v#L49
Automatically putting Void in Prop even though it was declared with
|
|
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.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):
ora/theories/algebra/ora.v#L104
Projection value has no head constant:
|
|
build (8.19, 64, vst):
ora/theories/algebra/ora.v#L150
Notation "_ ⋅? _" was already used in scope stdpp_scope.
|
|
build (8.19, 64, vst):
ora/theories/algebra/ora.v#L863
Hiding binding of key RF to rFunctor_scope
|
|
build (8.19, 64, vst):
ora/theories/algebra/ora.v#L900
Hiding binding of key URF to urFunctor_scope
|
|
build (8.19, 64, vst):
ora/theories/algebra/ora.v#L1067
Ignoring canonical projection to discrete_orderN by ora_orderN in
|
|
build (8.19, 64, vst):
ora/theories/algebra/ora.v#L1075
Ignoring canonical projection to discrete_orderN by uora_orderN in
|
|
build (8.19, 64, vst):
ora/theories/algebra/ora.v#L1092
Ignoring canonical projection to discrete_orderN by ora_orderN in
|
|
build (8.19, 64, vst):
ora/theories/algebra/ora.v#L1092
Ignoring canonical projection to discrete_orderN by uora_orderN in
|
|
test (8.20, assumptions.txt, 32)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
test (8.19, assumptions.txt, 64)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
test (8.20, assumptions.txt, 64)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
test (dev, assumptions.txt, 64)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
test (dev, test2, 64)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
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, test2, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
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, test2, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
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, test2, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test2, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test5, 64)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
test (dev, test5, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test5, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test5, 64)
Custom entry dfrac has been overridden.
|
|
test (dev, test5, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test5, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test5, 64)
Custom entry dfrac has been overridden.
|
|
test (dev, test5, 64)
Custom entry dfrac has been overridden.
|
|
test (dev, test5, 64)
Custom entry dfrac has been overridden.
|
|
test (dev, test5, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test5, 64)
Custom entry dfrac has been overridden.
|
|
test (8.20, test2, 64)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
test (8.20, test2, 64)
Automatically putting void1 in Prop even though it was declared with
|
|
test (8.20, test2, 64)
Automatically putting PER in Prop even though it was declared with
|
|
test (8.20, test2, 64)
Automatically putting Preorder in Prop even though it was declared
|
|
test (8.20, test2, 64)
Automatically putting EquivalenceH in Prop even though it was
|
|
test (8.20, test2, 64)
Custom entry dfrac has been overridden.
|
|
test (8.20, test2, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (8.20, test2, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (8.20, test2, 64)
Notations "if _ then _ else _" defined at level 200
|
|
test (8.20, test2, 64)
Notations "if _ then _ else _" defined at level 200
|
|
test (8.20, test2, 64)
Notations "_ _ : _" defined at level 1 with arguments constr
|
|
test (8.19, test2, 64)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
test (8.19, test2, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test2, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test2, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test2, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test2, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test2, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test2, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test2, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test2, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test2, 64)
Custom entry dfrac has been overridden.
|
|
test (8.20, test2, 32)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
test (8.20, test2, 32)
Automatically putting void1 in Prop even though it was declared with
|
|
test (8.20, test2, 32)
Automatically putting PER in Prop even though it was declared with
|
|
test (8.20, test2, 32)
Automatically putting Preorder in Prop even though it was declared
|
|
test (8.20, test2, 32)
Automatically putting EquivalenceH in Prop even though it was
|
|
test (8.20, test2, 32)
Custom entry dfrac has been overridden.
|
|
test (8.20, test2, 32)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (8.20, test2, 32)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (8.20, test2, 32)
Notations "if _ then _ else _" defined at level 200
|
|
test (8.20, test2, 32)
Notations "if _ then _ else _" defined at level 200
|
|
test (8.20, test2, 32)
Notations "_ _ : _" defined at level 1 with arguments constr
|
|
test (8.19, test5, 64)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
test (8.19, test5, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test5, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test5, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test5, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test5, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test5, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test5, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test5, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test5, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test5, 64)
Custom entry dfrac has been overridden.
|
|
test (8.20, test5, 64)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
test (8.20, test5, 64)
Custom entry dfrac has been overridden.
|
|
test (8.20, test5, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (8.20, test5, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (8.20, test5, 64)
Notations "if _ then _ else _" defined at level 200
|
|
test (8.20, test5, 64)
Notations "if _ then _ else _" defined at level 200
|
|
test (8.20, test5, 64)
Notations "_ _ : _" defined at level 1 with arguments constr
|
|
test (8.20, test5, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (8.20, test5, 64)
Notations "( _ , _ , .. , _ )" defined at level 0 with arguments
|
|
test (8.20, test5, 64)
Notations "_ : _" defined at level 100 with arguments constr
|
|
test (8.20, test5, 64)
Notations "_ , _" defined at level 26 with arguments constr
|
|
test (dev, test4, 64)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
test (dev, test4, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test4, 64)
Custom entry dfrac has been overridden.
|
|
test (dev, test4, 64)
Custom entry dfrac has been overridden.
|
|
test (dev, test4, 64)
Custom entry dfrac has been overridden.
|
|
test (dev, test4, 64)
Custom entry dfrac has been overridden.
|
|
test (dev, test4, 64)
Custom entry dfrac has been overridden.
|
|
test (dev, test4, 64)
Custom entry dfrac has been overridden.
|
|
test (dev, test4, 64)
Custom entry dfrac has been overridden.
|
|
test (dev, test4, 64)
Notation map_length is deprecated since 8.20.
|
|
test (dev, test4, 64)
Notation map_length is deprecated since 8.20.
|
|
test (8.20, test4, 64)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
test (8.20, test4, 64)
Custom entry dfrac has been overridden.
|
|
test (8.20, test4, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (8.20, test4, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (8.20, test4, 64)
Notations "if _ then _ else _" defined at level 200
|
|
test (8.20, test4, 64)
Notations "if _ then _ else _" defined at level 200
|
|
test (8.20, test4, 64)
Notations "_ _ : _" defined at level 1 with arguments constr
|
|
test (8.20, test4, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (8.20, test4, 64)
Notations "( _ , _ , .. , _ )" defined at level 0 with arguments
|
|
test (8.20, test4, 64)
Notations "_ : _" defined at level 100 with arguments constr
|
|
test (8.20, test4, 64)
Notations "_ , _" defined at level 26 with arguments constr
|
|
test (8.19, test4, 64)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
test (8.19, test4, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test4, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test4, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test4, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test4, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test4, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test4, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test4, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test4, 64)
Custom entry dfrac has been overridden.
|
|
test (dev, test, 64)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
test (dev, test, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test, 64)
Custom entry dfrac has been overridden.
|
|
test (dev, test, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test, 64)
Custom entry dfrac has been overridden.
|
|
test (dev, test, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test, 64)
Custom entry dfrac has been overridden.
|
|
test (dev, test, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test, 64)
Custom entry dfrac has been overridden.
|
|
test (dev, test, 64)
"From Coq" has been replaced by "From Stdlib".
|
|
test (dev, test, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test, 64)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
test (8.19, test, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test, 64)
Custom entry dfrac has been overridden.
|
|
test (8.19, test, 64)
Custom entry dfrac has been overridden.
|
|
test (8.20, test, 64)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
test (8.20, test, 64)
Custom entry dfrac has been overridden.
|
|
test (8.20, test, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (8.20, test, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (8.20, test, 64)
Notations "if _ then _ else _" defined at level 200
|
|
test (8.20, test, 64)
Notations "if _ then _ else _" defined at level 200
|
|
test (8.20, test, 64)
Notations "_ _ : _" defined at level 1 with arguments constr
|
|
test (8.20, test, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (8.20, test, 64)
Notations "( _ , _ , .. , _ )" defined at level 0 with arguments
|
|
test (8.20, test, 64)
Notations "_ : _" defined at level 100 with arguments constr
|
|
test (8.20, test, 64)
Notations "_ , _" defined at level 26 with arguments constr
|
|
test (8.20, test3, 32)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
test (8.20, test3, 32)
Notation skipn_length is deprecated since 8.20.
|
|
test (8.20, test3, 32)
Notation skipn_length is deprecated since 8.20.
|
|
test (8.20, test3, 32)
Notation skipn_length is deprecated since 8.20.
|
|
test (8.20, test3, 32)
Notation firstn_length is deprecated since 8.20.
|
|
test (8.20, test3, 32)
Notation firstn_length is deprecated since 8.20.
|
|
test (8.20, test3, 32)
Notation firstn_length is deprecated since 8.20.
|
|
test (8.20, test3, 32)
Notation firstn_length is deprecated since 8.20.
|
|
test (8.20, test3, 32)
Notation firstn_length is deprecated since 8.20.
|
|
test (8.20, test3, 32)
Notation firstn_length is deprecated since 8.20.
|
|
test (8.20, test3, 32)
Custom entry dfrac has been overridden.
|
|
test (8.20, test, 32)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
test (8.20, test, 32)
Custom entry dfrac has been overridden.
|
|
test (8.20, test, 32)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (8.20, test, 32)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (8.20, test, 32)
Notations "if _ then _ else _" defined at level 200
|
|
test (8.20, test, 32)
Notations "if _ then _ else _" defined at level 200
|
|
test (8.20, test, 32)
Notations "_ _ : _" defined at level 1 with arguments constr
|
|
test (8.20, test, 32)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (8.20, test, 32)
Notations "( _ , _ , .. , _ )" defined at level 0 with arguments
|
|
test (8.20, test, 32)
Notations "_ : _" defined at level 100 with arguments constr
|
|
test (8.20, test, 32)
Notations "_ , _" defined at level 26 with arguments constr
|
Artifacts
Produced during runtime
| Name | Size | |
|---|---|---|
|
VST build artifacts 8.19 64
Expired
|
133 MB |
|
|
VST build artifacts 8.20 32
Expired
|
121 MB |
|
|
VST build artifacts 8.20 64
Expired
|
121 MB |
|
|
VST build artifacts dev 64
Expired
|
114 MB |
|