Skip to content

Commit 8b10d38

Browse files
committed
fix: remove async from notify and test
1 parent 2f6adf3 commit 8b10d38

File tree

2 files changed

+112
-4
lines changed

2 files changed

+112
-4
lines changed

src/Std/Sync/Notify.lean

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -106,13 +106,13 @@ def notifyOne (x : Notify) : BaseIO Bool := do
106106
Wait to be notified. Returns a task that completes when notify is called.
107107
Note: if notify was called before wait, this will wait for the next notify call.
108108
-/
109-
def wait (x : Notify) : Async Unit :=
109+
def wait (x : Notify) : IO (AsyncTask Unit) :=
110110
x.state.atomically do
111111
let promise ← IO.Promise.new
112112
modify fun st => { st with consumers := st.consumers.enqueue (.normal promise) }
113-
match ← await promise.result? with
114-
| some res => pure res
115-
| none => throw (IO.userError "notify dropped")
113+
IO.bindTask promise.result? fun
114+
| some res => pure <| Task.pure (.ok res)
115+
| none => throw (IO.userError "notify dropped")
116116

117117
/--
118118
Creates a selector that waits for notifications

tests/lean/run/sync_notify.lean

Lines changed: 108 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,108 @@
1+
import Std.Internal.Async
2+
import Std.Sync
3+
4+
open Std.Internal.IO Async
5+
6+
-- Test basic wait and notifyOne functionality
7+
def testBasicWaitNotifyOne : Async Unit := do
8+
let notify ← Std.Notify.new
9+
let waitTask ← notify.wait
10+
11+
assert! (← waitTask.getState) = .waiting
12+
discard <| notify.notifyOne
13+
await waitTask
14+
assert! (← waitTask.getState) = .finished
15+
16+
#eval testBasicWaitNotifyOne.block
17+
18+
-- Test multiple waiters with notifyOne (only one should be notified)
19+
def testMultipleWaitersNotifyOne : Async Unit := do
20+
let notify ← Std.Notify.new
21+
let task1 ← notify.wait
22+
let task2 ← notify.wait
23+
let task3 ← notify.wait
24+
25+
assert! (← task1.getState) = .waiting
26+
assert! (← task2.getState) = .waiting
27+
assert! (← task3.getState) = .waiting
28+
29+
discard <| notify.notifyOne
30+
31+
IO.sleep 100
32+
33+
let states ← [task1, task2, task3].mapM (fun t => t.getState)
34+
let finishedCount := states.filter (· == .finished) |>.length
35+
let waitingCount := states.filter (· == .waiting) |>.length
36+
37+
assert! finishedCount == 1
38+
assert! waitingCount == 2
39+
40+
discard <| notify.notifyOne
41+
42+
#eval testMultipleWaitersNotifyOne.block
43+
44+
-- Test multiple waiters with notify (all should be notified)
45+
def testMultipleWaitersNotifyAll : Async Unit := do
46+
let notify ← Std.Notify.new
47+
let task1 ← notify.wait
48+
let task2 ← notify.wait
49+
let task3 ← notify.wait
50+
51+
assert! (← task1.getState) = .waiting
52+
assert! (← task2.getState) = .waiting
53+
assert! (← task3.getState) = .waiting
54+
55+
discard <| notify.notify
56+
57+
await task1
58+
await task2
59+
await task3
60+
61+
assert! (← task1.getState) = .finished
62+
assert! (← task2.getState) = .finished
63+
assert! (← task3.getState) = .finished
64+
65+
#eval testMultipleWaitersNotifyAll.block
66+
67+
-- Test sequential notification
68+
def testSequentialNotification : Async Unit := do
69+
let notify ← Std.Notify.new
70+
let task1 ← notify.wait
71+
let task2 ← notify.wait
72+
let task3 ← notify.wait
73+
74+
discard <| notify.notifyOne
75+
await task1
76+
assert! (← task1.getState) = .finished
77+
assert! (← task2.getState) = .waiting
78+
assert! (← task3.getState) = .waiting
79+
80+
discard <| notify.notifyOne
81+
await task2
82+
assert! (← task2.getState) = .finished
83+
assert! (← task3.getState) = .waiting
84+
85+
discard <| notify.notifyOne
86+
await task3
87+
assert! (← task3.getState) = .finished
88+
89+
#eval testSequentialNotification.block
90+
91+
def testReuseAfterCompletion : Async Unit := do
92+
let notify ← Std.Notify.new
93+
94+
let task1 ← notify.wait
95+
discard <| notify.notifyOne
96+
await task1
97+
assert! (← task1.getState) = .finished
98+
99+
let task2 ← notify.wait
100+
let task3 ← notify.wait
101+
discard <| notify.notify
102+
await task2
103+
await task3
104+
105+
assert! (← task2.getState) = .finished
106+
assert! (← task3.getState) = .finished
107+
108+
#eval testReuseAfterCompletion.block

0 commit comments

Comments
 (0)