Skip to content
CI

Solve both technicalities by using ghost_map_auth #2766

Sign in to view logs

Solve both technicalities by using ghost_map_auth

Solve both technicalities by using ghost_map_auth #2766

Triggered via push August 9, 2023 19:29
@upamanyusupamanyus
pushed 748cc58
master
Status Success
Total duration 1h 45m 46s
Artifacts –

build.yml

on: push
check-goose
1m 2s
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#L1584
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 (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.
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.