Skip to content

Commit

Permalink
fix: flaky test (#889)
Browse files Browse the repository at this point in the history
  • Loading branch information
digama0 authored Aug 16, 2024
1 parent 5e5e54c commit 91cf60c
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions test/MLList.lean
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ def g (n : Nat) : MLList Lean.Meta.MetaM Nat := do
/-!
### Test `MLList.ofTaskList`.
We generate three tasks which sleep for `100`, `10`, and `1` milliseconds respectively,
We generate three tasks which sleep for `100`, `50`, and `1` milliseconds respectively,
and then verify that `MLList.ofTaskList` return their results in the order they complete.
-/

Expand All @@ -29,9 +29,9 @@ def sleep (n : UInt32) : BaseIO (Task UInt32) :=
| .error _ => 0

def sleeps : MLList BaseIO UInt32 := .squash fun _ => do
let r ← [100,10,1].map sleep |>.traverse id
let r ← [100,50,1].map sleep |>.traverse id
return .ofTaskList r

/-- info: [1, 10, 100] -/
/-- info: [1, 50, 100] -/
#guard_msgs in
#eval sleeps.force

0 comments on commit 91cf60c

Please sign in to comment.