CI #3145
tchajedAnnotations
14 warnings
|
check-goose
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/setup-go@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
|
|
build-vos (dev):
external/iris/iris/prelude/options.v#L17
Could not enable unknown warning deprecated-hint-without-locality
|
|
build (8.18):
external/iris/iris/prelude/options.v#L17
Could not enable unknown warning deprecated-hint-without-locality
|
|
build (8.18):
external/coqutil/src/coqutil/Word/Properties.v#L61
width_nonneg_context is declared opaque (Qed) but this is not fully
|
|
build (8.18):
external/coqutil/src/coqutil/Word/Properties.v#L228
width_nonzero is declared opaque (Qed) but this is not fully
|
|
build (8.18):
external/coqutil/src/coqutil/Word/Properties.v#L232
twice_halfm is declared opaque (Qed) but this is not fully respected
|
|
build (8.18):
src/goose_lang/lib/waitgroup/waitgroup.v#L40
This inductive will be minimized to Set even though Universe
|
|
build (8.18):
src/goose_lang/lib/waitgroup/waitgroup.v#L51
This inductive will be minimized to Set even though Universe
|
|
build (8.18):
src/goose_lang/spec_assert.v#L42
This inductive will be minimized to Set even though Universe
|
|
build (8.18):
src/goose_lang/lib/barrier/barrier.v#L12
This inductive will be minimized to Set even though Universe
|
|
build (8.18):
src/goose_lang/ffi/async_disk.v#L45
This inductive will be minimized to Set even though Universe
|
|
build (8.18):
src/goose_lang/ffi/async_disk_proph.v#L53
This inductive will be minimized to Set even though Universe
|
|
build (dev):
external/iris/iris/prelude/options.v#L17
Could not enable unknown warning deprecated-hint-without-locality
|
|
build (8.19):
external/iris/iris/prelude/options.v#L17
Could not enable unknown warning deprecated-hint-without-locality
|