Bump F* to nightly 2026-09-25 - #327
Merged
Merged
Annotations
21 warnings and 1 notice
|
Complete job
Node.js 20 is deprecated. The following actions target Node.js 20 but are being forced to run on Node.js 24: actions/checkout@v3. For more information see: https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/
|
|
Test pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/pulse.checked/Pulse.fst.checked
instead of _cache/Pulse.fst.checked
|
|
Test pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse.Main to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/common.checked/Pulse.Main.fsti.checked
instead of _cache/Pulse.Main.fsti.checked
|
|
Test pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/pulse.checked/Pulse.fst.checked
instead of _cache/Pulse.fst.checked
|
|
Test pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse.Main to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/common.checked/Pulse.Main.fsti.checked
instead of _cache/Pulse.Main.fsti.checked
|
|
Test pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/pulse.checked/Pulse.fst.checked
instead of _cache/Pulse.fst.checked
|
|
Test pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse.Main to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/common.checked/Pulse.Main.fsti.checked
instead of _cache/Pulse.Main.fsti.checked
|
|
Test pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/pulse.checked/Pulse.fst.checked
instead of _cache/Pulse.fst.checked
|
|
Test pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/pulse.checked/Pulse.fst.checked
instead of _cache/Pulse.fst.checked
|
|
Test pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse.Main to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/common.checked/Pulse.Main.fsti.checked
instead of _cache/Pulse.Main.fsti.checked
|
|
Test pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse.Main to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/common.checked/Pulse.Main.fsti.checked
instead of _cache/Pulse.Main.fsti.checked
|
|
Build pal:
Pulse.Lib.C.Array.fst#L232
(288) * Warning 288 at Pulse.Lib.C.Array.fst(232,4-232,13):
- Pulse.Lib.Array.Core.mask_free is deprecated
- Array.mask_free is unsound; only use for model implementations
- See also Pulse.Lib.C.Array.fst(232,2-232,15)
|
|
Build pal:
Pulse.Lib.C.Array.fst#L232
(288) * Warning 288 at Pulse.Lib.C.Array.fst(232,4-232,13):
- Pulse.Lib.Array.Core.mask_free is deprecated
- Array.mask_free is unsound; only use for model implementations
- See also Pulse.Lib.C.Array.fst(232,2-232,15)
|
|
Build pal:
Pulse.Lib.C.Array.fst#L214
(288) * Warning 288 at Pulse.Lib.C.Array.fst(215,12-215,22):
- Pulse.Lib.Array.Core.mask_alloc is deprecated
- Array.mask_alloc is unsound; only use for model implementations
- See also Pulse.Lib.C.Array.fst(214,1-222,3)
|
|
Build pal:
Pulse.Lib.C.Array.fst#L214
(288) * Warning 288 at Pulse.Lib.C.Array.fst(215,12-215,22):
- Pulse.Lib.Array.Core.mask_alloc is deprecated
- Array.mask_alloc is unsound; only use for model implementations
- See also Pulse.Lib.C.Array.fst(214,1-222,3)
|
|
Build pal:
FStar.Int.Cast.fst#L170
(288) * Warning 288 at Pulse.Lib.C.Casts.fst(25,4-25,19):
- FStar.Int.Cast.uint64_to_int64 is deprecated
- with care; in C the result is implementation-defined when not representable
- See also /home/runner/.local/fstar/lib/fstar/ulib/FStar.Int.Cast.fst(170,4-170,19)
|
|
Build pal:
FStar.Int.Cast.fst#L170
(288) * Warning 288 at Pulse.Lib.C.Casts.fst(25,4-25,19):
- FStar.Int.Cast.uint64_to_int64 is deprecated
- with care; in C the result is implementation-defined when not representable
- See also /home/runner/.local/fstar/lib/fstar/ulib/FStar.Int.Cast.fst(170,4-170,19)
|
|
Build pal:
FStar.Int.Cast.fst#L155
(288) * Warning 288 at Pulse.Lib.C.Casts.fst(21,4-21,19):
- FStar.Int.Cast.uint32_to_int32 is deprecated
- with care; in C the result is implementation-defined when not representable
- See also /home/runner/.local/fstar/lib/fstar/ulib/FStar.Int.Cast.fst(155,4-155,19)
|
|
Build pal:
FStar.Int.Cast.fst#L155
(288) * Warning 288 at Pulse.Lib.C.Casts.fst(21,4-21,19):
- FStar.Int.Cast.uint32_to_int32 is deprecated
- with care; in C the result is implementation-defined when not representable
- See also /home/runner/.local/fstar/lib/fstar/ulib/FStar.Int.Cast.fst(155,4-155,19)
|
|
Build pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/pulse.checked/Pulse.fst.checked
instead of _cache/Pulse.fst.checked
|
|
Build pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse.Main to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/common.checked/Pulse.Main.fsti.checked
instead of _cache/Pulse.Main.fsti.checked
|
|
"The ubuntu-latest label will migrate to Ubuntu 26 beginning October 19, 2026. For more information, see https://github.com/actions/runner-images/issues/14748"
|
background
wait
wait-all
cancel
parallel
Loading