From c5f2c192d62adec96c6d266f9e2d8083ea69d44a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 2 Sep 2025 13:55:36 +0200 Subject: [PATCH] fix: Selectable.one does not panic on empty array (#10216) This PR fixes #10193. --- src/Std/Internal/Async/Select.lean | 3 +++ tests/lean/run/async_select_timer.lean | 5 +++++ 2 files changed, 8 insertions(+) diff --git a/src/Std/Internal/Async/Select.lean b/src/Std/Internal/Async/Select.lean index b893d86825..ebbb51d48d 100644 --- a/src/Std/Internal/Async/Select.lean +++ b/src/Std/Internal/Async/Select.lean @@ -123,6 +123,9 @@ The protocol for this is as follows: the `Selectable.cont` of the winning `Selector` is executed and returned. -/ partial def Selectable.one (selectables : Array (Selectable α)) : IO (AsyncTask α) := do + if selectables.isEmpty then + throw <| .userError "Selectable.one requires at least one Selectable" + let seed := UInt64.toNat (ByteArray.toUInt64LE! (← IO.getRandomBytes 8)) let gen := mkStdGen seed let selectables := shuffleIt selectables gen diff --git a/tests/lean/run/async_select_timer.lean b/tests/lean/run/async_select_timer.lean index ecb2232825..7999798c7b 100644 --- a/tests/lean/run/async_select_timer.lean +++ b/tests/lean/run/async_select_timer.lean @@ -27,3 +27,8 @@ def test2 : IO (AsyncTask Nat) := do #eval show IO _ from do let task ← test2 IO.ofExcept task.get + +/-- error: Selectable.one requires at least one Selectable -/ +#guard_msgs in +#eval show IO _ from do + let foo ← Selectable.one (α := Unit) #[]