Skip to content
CI

Regoose 1 line change and reprove #2746

Sign in to view logs

Regoose 1 line change and reprove

Regoose 1 line change and reprove #2746

Triggered via push July 28, 2023 16:08
@upamanyusupamanyus
pushed 0169e8c
master
Status Success
Total duration 1h 17m 52s
Artifacts –
This run and associated checks have been archived and are scheduled for deletion. Learn more about checks retention

build.yml

on: push
check-goose
56s
check-goose
Matrix: build-vos
Matrix: build
Fit to window
Zoom out
Zoom in

Annotations

30 warnings
build-vos (dev): external/stdpp/stdpp/options.v#L13
Syntax "Export Set" is deprecated, use the attribute syntax
build-vos (dev): external/stdpp/stdpp/options.v#L19
Syntax "Export Set" is deprecated, use the attribute syntax
build-vos (dev): external/iris/iris/prelude/options.v#L13
Syntax "Export Set" is deprecated, use the attribute syntax
build-vos (dev): external/iris/iris/prelude/options.v#L17
Syntax "Export Set" is deprecated, use the attribute syntax
build-vos (dev): external/iris/iris/prelude/options.v#L17
Could not enable unknown warning deprecated-hint-without-locality
build-vos (dev): external/coqutil/src/coqutil/Word/Properties.v#L61
width_nonneg_context is declared opaque (Qed) but this is not fully
build-vos (dev): external/coqutil/src/coqutil/Word/Properties.v#L228
width_nonzero is declared opaque (Qed) but this is not fully
build-vos (dev): external/coqutil/src/coqutil/Word/Properties.v#L232
twice_halfm is declared opaque (Qed) but this is not fully respected
build-vos (dev): external/iris/iris/algebra/ofe.v#L1580
Hgne is declared opaque (Qed) but this is not fully respected inside
build-vos (dev): external/iris/iris/bi/monpred.v#L56
monPred_sig_equiv is declared opaque (Qed) but this is not fully
build (8.17): external/coqutil/src/coqutil/Datatypes/List.v#L1843
Notation Nat.add_mod_idemp_l is deprecated since 8.17.
build (8.17): external/coqutil/src/coqutil/Datatypes/List.v#L1843
Notation Nat.add_mod_idemp_l is deprecated since 8.17.
build (8.17): external/coqutil/src/coqutil/Datatypes/List.v#L1843
Notation Nat.add_mod_idemp_l is deprecated since 8.17.
build (8.17): external/coqutil/src/coqutil/Datatypes/List.v#L1861
Notation Nat.div_exact is deprecated since 8.17.
build (8.17): external/coqutil/src/coqutil/Datatypes/List.v#L1861
Notation Nat.div_exact is deprecated since 8.17.
build (8.17): external/coqutil/src/coqutil/Datatypes/List.v#L1862
Notation Nat.mod_mul is deprecated since 8.17.
build (8.17): external/coqutil/src/coqutil/Datatypes/List.v#L1862
Notation Nat.mod_mul is deprecated since 8.17.
build (8.17): external/coqutil/src/coqutil/Datatypes/List.v#L2033
Notation Nat.add_mod_idemp_r is deprecated since 8.17.
build (8.17): external/coqutil/src/coqutil/Datatypes/List.v#L2033
Notation Nat.add_mod_idemp_r is deprecated since 8.17.
build (8.17): external/coqutil/src/coqutil/Datatypes/List.v#L2033
Notation Nat.add_mod_idemp_r is deprecated since 8.17.
build (dev): external/stdpp/stdpp/options.v#L13
Syntax "Export Set" is deprecated, use the attribute syntax
build (dev): external/stdpp/stdpp/options.v#L19
Syntax "Export Set" is deprecated, use the attribute syntax
build (dev): external/iris/iris/prelude/options.v#L13
Syntax "Export Set" is deprecated, use the attribute syntax
build (dev): external/iris/iris/prelude/options.v#L17
Syntax "Export Set" is deprecated, use the attribute syntax
build (dev): external/iris/iris/prelude/options.v#L17
Could not enable unknown warning deprecated-hint-without-locality
build (dev): external/coqutil/src/coqutil/Word/Properties.v#L61
width_nonneg_context is declared opaque (Qed) but this is not fully
build (dev): external/coqutil/src/coqutil/Word/Properties.v#L228
width_nonzero is declared opaque (Qed) but this is not fully
build (dev): external/coqutil/src/coqutil/Word/Properties.v#L232
twice_halfm is declared opaque (Qed) but this is not fully respected
build (dev): external/coqutil/src/coqutil/Datatypes/List.v#L1843
Notation Nat.add_mod_idemp_l is deprecated since 8.17.
build (dev): external/coqutil/src/coqutil/Datatypes/List.v#L1843
Notation Nat.add_mod_idemp_l is deprecated since 8.17.