Get 'make all' to work in VST 2.15, 32-bit mode #1118
Triggered via pull request
January 9, 2025 15:35
andrew-appel
Status
Cancelled
Total duration
10m 37s
Artifacts
–
Annotations
8 errors and 32 warnings
|
build (8.20, 32, vst)
The run was canceled by @andrew-appel.
|
|
build (dev, 64, vst)
The run was canceled by @andrew-appel.
|
|
build (8.20, 32, vst)
The operation was canceled.
|
|
build (dev, 64, vst)
The operation was canceled.
|
|
build (8.20, 64, vst)
The run was canceled by @andrew-appel.
|
|
build (8.19, 64, vst)
The run was canceled by @andrew-appel.
|
|
build (8.19, 64, vst)
The operation was canceled.
|
|
build (8.20, 64, vst)
The operation was canceled.
|
|
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):
msl/functors.v#L12
Automatically putting functorFacts in Prop even though it was
|
|
build (8.20, 32, vst):
msl/functors.v#L30
Automatically putting functorFacts in Prop even though it was
|
|
build (8.20, 32, vst):
msl/functors.v#L48
Automatically putting functorFacts in Prop even though it was
|
|
build (dev, 64, vst):
msl/Axioms.v#L7
"From Coq" has been replaced by "From Stdlib".
|
|
build (8.20, 32, vst):
msl/functors.v#L66
Automatically putting functorFacts in Prop even though it was
|
|
build (dev, 64, vst):
msl/Axioms.v#L23
"From Coq" has been replaced by "From Stdlib".
|
|
build (8.20, 32, vst):
msl/functors.v#L87
Automatically putting functorFacts in Prop even though it was
|
|
build (dev, 64, vst):
msl/Extensionality.v#L5
"From Coq" has been replaced by "From Stdlib".
|
|
build (8.20, 32, vst):
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|
|
build (dev, 64, vst):
msl/Extensionality.v#L139
Coq.Init.Prelude.f_equal has been replaced by
|
|
build (8.20, 32, vst):
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|
|
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 (8.20, 32, vst):
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|
|
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".
|
|
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):
msl/functors.v#L12
Automatically putting functorFacts in Prop even though it was
|
|
build (8.20, 64, vst):
msl/functors.v#L30
Automatically putting functorFacts in Prop even though it was
|
|
build (8.20, 64, vst):
msl/functors.v#L48
Automatically putting functorFacts in Prop even though it was
|
|
build (8.20, 64, vst):
msl/functors.v#L66
Automatically putting functorFacts in Prop even though it was
|
|
build (8.20, 64, vst):
msl/functors.v#L87
Automatically putting functorFacts in Prop even though it was
|
|
build (8.19, 64, vst):
compcert/lib/IEEE754_extra.v#L434
Notation IZR_neq is deprecated since 8.19.
|
|
build (8.20, 64, vst):
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|
|
build (8.19, 64, vst):
compcert/lib/IEEE754_extra.v#L434
Notation IZR_neq is deprecated since 8.19.
|
|
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.
|