b763ab8a5e
This PR addresses two review points on `IO.CancelToken`: * `set` now resolves the underlying promise *before* writing the `Bool` fast-path flag, so observing `isSet = true` implies any synchronously chained `onSet` callback has already run. The previous order (flag first, then resolve) was a subtle footgun: code seeing `isSet = true` could not rely on the cancellation task having fired. * The underlying promise and the task it produces are kept private. The prior `task : Task (Option Unit)` accessor is removed; consumers should use `onSet` to react to cancellation. A comment on the structure records that re-exposing the task in the future requires re-auditing the order in `set` for races between the promise and the `Bool` flag. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
42 lines
1.1 KiB
Text
42 lines
1.1 KiB
Text
/-! Tests for `IO.CancelToken.onSet`. -/
|
|
|
|
/-- `onSet` registered before `set` fires synchronously when `set` is called. -/
|
|
def testOnSetBeforeSet : IO Unit := do
|
|
let tk ← IO.CancelToken.new
|
|
let cell ← IO.mkRef false
|
|
tk.onSet (cell.set true)
|
|
if (← cell.get) then panic! "onSet fired too early"
|
|
tk.set
|
|
if !(← cell.get) then panic! "onSet did not fire"
|
|
IO.println "ok"
|
|
|
|
/-- `onSet` registered after `set` fires immediately at registration time. -/
|
|
def testOnSetAfterSet : IO Unit := do
|
|
let tk ← IO.CancelToken.new
|
|
tk.set
|
|
let cell ← IO.mkRef false
|
|
tk.onSet (cell.set true)
|
|
if !(← cell.get) then panic! "onSet did not fire on already-set token"
|
|
IO.println "ok"
|
|
|
|
/-- Multiple `onSet` callbacks all fire. -/
|
|
def testOnSetMultiple : IO Unit := do
|
|
let tk ← IO.CancelToken.new
|
|
let counter ← IO.mkRef 0
|
|
for _ in [0:5] do
|
|
tk.onSet (counter.modify (· + 1))
|
|
tk.set
|
|
let n ← counter.get
|
|
if n != 5 then panic! s!"expected 5 callbacks, got {n}"
|
|
IO.println "ok"
|
|
|
|
/--
|
|
info: ok
|
|
ok
|
|
ok
|
|
-/
|
|
#guard_msgs in
|
|
#eval do
|
|
testOnSetBeforeSet
|
|
testOnSetAfterSet
|
|
testOnSetMultiple
|