Port VST 2.x to CompCert master #1086
andrew-appelAnnotations
122 warnings
|
build (dev, 64, vst)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/upload-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
build (dev, 64, vst)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/checkout@v2, actions/upload-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
build (dev, 64, vst):
msl/sepalg.v#L104
Automatically putting Flat_alg in Prop even though it was declared
|
|
build (dev, 64, vst):
msl/sepalg_generators.v#L49
Automatically putting Void in Prop even though it was declared with
|
|
build (dev, 64, vst):
msl/functors.v#L12
Automatically putting functorFacts in Prop even though it was
|
|
build (dev, 64, vst):
msl/functors.v#L30
Automatically putting functorFacts in Prop even though it was
|
|
build (dev, 64, vst):
msl/functors.v#L48
Automatically putting functorFacts in Prop even though it was
|
|
build (dev, 64, vst):
msl/functors.v#L66
Automatically putting functorFacts in Prop even though it was
|
|
build (dev, 64, vst):
msl/functors.v#L87
Automatically putting functorFacts in Prop even though it was
|
|
build (dev, 64, vst):
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|
|
build (dev, 64, vst):
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|
|
build (dev, 64, vst):
compcert/lib/Coqlib.v#L861
Notation rev_length is deprecated since 8.20.
|
|
build (8.19, 32, vst)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/upload-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
build (8.19, 32, vst)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/checkout@v2, actions/upload-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
build (8.19, 32, vst):
compcert/lib/IEEE754_extra.v#L434
Notation IZR_neq is deprecated since 8.19.
|
|
build (8.19, 32, vst):
compcert/lib/IEEE754_extra.v#L434
Notation IZR_neq is deprecated since 8.19.
|
|
build (8.19, 32, vst):
floyd/canon.v#L14
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
build (8.19, 32, vst):
floyd/canon.v#L505
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
build (8.19, 32, vst):
floyd/proofauto.v#L61
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
build (8.19, 32, vst):
concurrency/semax_conc_pred.v#L20
Notation "_ oo _" was already used.
|
|
build (8.18, 64, vst)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/upload-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
build (8.18, 64, vst)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/checkout@v2, actions/upload-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
build (8.18, 64, vst):
compcert/lib/IEEE754_extra.v#L434
Notation IZR_neq is deprecated since 8.19.
|
|
build (8.18, 64, vst):
compcert/lib/IEEE754_extra.v#L434
Notation IZR_neq is deprecated since 8.19.
|
|
build (8.18, 64, vst):
concurrency/semax_conc_pred.v#L20
Notation "_ oo _" was already used.
|
|
build (8.19, 64, vst)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/upload-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
build (8.19, 64, vst)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/checkout@v2, actions/upload-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
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.
|
|
test (dev, assumptions.txt, 64)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/download-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
test (dev, assumptions.txt, 64)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/download-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
test (8.18, assumptions.txt, 64)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/download-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
test (8.18, assumptions.txt, 64)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/download-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
test (8.19, assumptions.txt, 32)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/download-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
test (8.19, assumptions.txt, 32)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/download-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
test (8.19, assumptions.txt, 64)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/download-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
test (8.19, assumptions.txt, 64)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/download-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
test (dev, test5, 64)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/download-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
test (dev, test5, 64)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/download-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
test (dev, test5, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (dev, test5, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (dev, test5, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (dev, test5, 64)
Notations "( _ , _ , .. , _ )" defined at level 0 with arguments
|
|
test (dev, test5, 64)
Notations "_ : _" defined at level 100 with arguments constr
|
|
test (dev, test5, 64)
Notations "_ , _" defined at level 26 with arguments constr
|
|
test (dev, test5, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (dev, test5, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (dev, test5, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (dev, test5, 64)
Notations "( _ , _ , .. , _ )" defined at level 0 with arguments
|
|
test (dev, test4, 64)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/download-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
test (dev, test4, 64)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/download-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
test (dev, test4, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (dev, test4, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (dev, test4, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (dev, test4, 64)
Notations "( _ , _ , .. , _ )" defined at level 0 with arguments
|
|
test (dev, test4, 64)
Notations "_ : _" defined at level 100 with arguments constr
|
|
test (dev, test4, 64)
Notations "_ , _" defined at level 26 with arguments constr
|
|
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 (dev, test4, 64)
Notation map_length is deprecated since 8.20.
|
|
test (dev, test4, 64)
Notation map_length is deprecated since 8.20.
|
|
test (dev, test2, 64)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/download-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
test (dev, test2, 64)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/download-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
test (dev, test2, 64)
Automatically putting void1 in Prop even though it was declared with
|
|
test (dev, test2, 64)
Automatically putting PER in Prop even though it was declared with
|
|
test (dev, test2, 64)
Automatically putting Preorder in Prop even though it was declared
|
|
test (dev, test2, 64)
Automatically putting EquivalenceH in Prop even though it was
|
|
test (dev, test2, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (dev, test2, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (dev, test2, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (dev, test2, 64)
Notations "( _ , _ , .. , _ )" defined at level 0 with arguments
|
|
test (dev, test2, 64)
Notations "_ : _" defined at level 100 with arguments constr
|
|
test (dev, test2, 64)
Notations "_ , _" defined at level 26 with arguments constr
|
|
test (8.19, test5, 64)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/download-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
test (8.19, test5, 64)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/download-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
test (8.18, test5, 64)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/download-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
test (8.18, test5, 64)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/download-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
test (8.19, test2, 64)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/download-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
test (8.19, test2, 64)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/download-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
test (8.19, test2, 32)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/download-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
test (8.19, test2, 32)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/download-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
test (8.18, test2, 64)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/download-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
test (8.18, test2, 64)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/download-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
test (8.19, test4, 64)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/download-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
test (8.19, test4, 64)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/download-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
test (8.18, test4, 64)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/download-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
test (8.18, test4, 64)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/download-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
test (dev, test, 64)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/download-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
test (dev, test, 64)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/download-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
test (dev, test, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (dev, test, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (dev, test, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (dev, test, 64)
Notations "( _ , _ , .. , _ )" defined at level 0 with arguments
|
|
test (dev, test, 64)
Notations "_ : _" defined at level 100 with arguments constr
|
|
test (dev, test, 64)
Notations "_ , _" defined at level 26 with arguments constr
|
|
test (dev, test, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (dev, test, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (dev, test, 64)
Notations "_ = _ :> _" defined at level 70 with arguments constr
|
|
test (dev, test, 64)
Notations "( _ , _ , .. , _ )" defined at level 0 with arguments
|
|
test (8.18, test, 64)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/download-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
test (8.18, test, 64)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/download-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
test (8.19, test, 64)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/download-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
test (8.19, test, 64)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/download-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
test (8.19, test3, 32)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/download-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
test (8.19, test3, 32)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/download-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
test (8.19, test3, 32)
Notation N.add_mod_idemp_l is deprecated since 8.17.
|
|
test (8.19, test3, 32)
Notation N.add_mod_idemp_l is deprecated since 8.17.
|
|
test (8.19, test3, 32)
Notation N.add_mod_idemp_l is deprecated since 8.17.
|
|
test (8.19, test3, 32)
Notation N.add_mod_idemp_l is deprecated since 8.17.
|
|
test (8.19, test3, 32)
Notation N.mod_same is deprecated since 8.17.
|
|
test (8.19, test3, 32)
Notation N.mod_same is deprecated since 8.17.
|
|
test (8.19, test3, 32)
Notation N.mod_same is deprecated since 8.17.
|
|
test (8.19, test3, 32)
Notation N.mod_same is deprecated since 8.17.
|
|
test (8.19, test3, 32)
Notation N.mod_eq is deprecated since 8.17. Use Div0.mod_eq instead.
|
|
test (8.19, test3, 32)
Notation N.mod_eq is deprecated since 8.17. Use Div0.mod_eq instead.
|
|
test (8.19, test, 32)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/download-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
test (8.19, test, 32)
The following actions uses Node.js version which is deprecated and will be forced to run on node20: actions/download-artifact@v2. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/
|
|
Deprecation notice: v1, v2, and v3 of the artifact actions
The following artifacts were uploaded using a version of actions/upload-artifact that is scheduled for deprecation: "VST build artifacts 8.18 64", "VST build artifacts 8.19 32", "VST build artifacts 8.19 64", "VST build artifacts dev 64".
Please update your workflow to use v4 of the artifact actions.
Learn more: https://github.blog/changelog/2024-04-16-deprecation-notice-v3-of-the-artifact-actions/
|
Artifacts
Produced during runtime
| Name | Size | |
|---|---|---|
|
VST build artifacts 8.18 64
Expired
|
121 MB |
|
|
VST build artifacts 8.19 32
Expired
|
126 MB |
|
|
VST build artifacts 8.19 64
Expired
|
126 MB |
|
|
VST build artifacts dev 64
Expired
|
79.5 MB |
|