From 0a168330900d8e4d20ab8da2fa3e244250525057 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Wed, 4 Dec 2024 14:36:53 +0100
Subject: [PATCH 1/8] feat: first throw at async sleep interface

---
 src/Std/Internal.lean       |   2 +
 src/Std/Internal/Async.lean | 169 ++++++++++++++++++++++++++++++++++++
 2 files changed, 171 insertions(+)
 create mode 100644 src/Std/Internal/Async.lean

diff --git a/src/Std/Internal.lean b/src/Std/Internal.lean
index 33c14dbce2e0..e772b478b0ed 100644
--- a/src/Std/Internal.lean
+++ b/src/Std/Internal.lean
@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 prelude
+-- TODO: after PR is merged
+--import Std.Internal.Async
 import Std.Internal.Parsec
 import Std.Internal.UV
 
diff --git a/src/Std/Internal/Async.lean b/src/Std/Internal/Async.lean
new file mode 100644
index 000000000000..a241fbc2940f
--- /dev/null
+++ b/src/Std/Internal/Async.lean
@@ -0,0 +1,169 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Std.Time
+import Std.Internal.UV
+
+
+namespace Std
+namespace Internal
+namespace IO
+namespace Async
+
+/--
+A `Task` that may resolve to a value or an `IO.Error`.
+-/
+def AsyncTask (α : Type u) : Type u := Task (Except IO.Error α)
+
+namespace AsyncTask
+
+@[inline]
+protected def pure (x : α) : AsyncTask α := Task.pure <| .ok x
+
+instance : Pure AsyncTask where
+  pure := AsyncTask.pure
+
+@[inline]
+protected def bind (x : AsyncTask α) (f : α → AsyncTask β) : AsyncTask β :=
+  Task.bind x fun r =>
+    match r with
+    | .ok a => f a
+    | .error e => Task.pure <| .error e
+
+-- TODO: variants with explicit error handling
+
+@[inline]
+def bindIO (x : AsyncTask α) (f : α → IO (AsyncTask β)) : BaseIO (AsyncTask β) :=
+  IO.bindTask x fun r =>
+    match r with
+    | .ok a => f a
+    | .error e => .error e
+
+@[inline]
+def mapIO (f : α → β) (x : AsyncTask α) : BaseIO (AsyncTask β) :=
+  IO.mapTask (t := x) fun r =>
+    match r with
+    | .ok a => pure (f a)
+    | .error e => .error e
+
+/--
+Run the `AsyncTask` in `x` and block until it finishes.
+-/
+def spawnBlocking (x : IO (AsyncTask α)) : IO α := do
+  let t ← x
+  let res := t.get
+  match res with
+  | .ok a => return a
+  | .error e => .error e
+
+@[inline]
+def spawn (x : IO α) : BaseIO (AsyncTask α) := do
+  IO.asTask x
+
+@[inline]
+def ofPromise (x : IO.Promise α) : AsyncTask α :=
+  x.result.map pure
+
+@[inline]
+def getState (x : AsyncTask α) : BaseIO IO.TaskState :=
+  IO.getTaskState x
+
+end AsyncTask
+
+/--
+`Sleep` can be used to sleep for some duration once.
+The underlying timer has millisecond resolution.
+-/
+structure Sleep where
+  private ofNative ::
+    native : Internal.UV.Timer
+
+-- TODO: provable constraints on duration after changes in Std.Time
+
+namespace Sleep
+
+/--
+Set up a `Sleep` that waits for `duration` milliseconds.
+This function only initializes but does not yet start the underlying timer.
+-/
+def mk (duration : Std.Time.Millisecond.Offset) : IO Sleep := do
+  let native ← Internal.UV.Timer.mk duration.toInt.toNat.toUInt64 false
+  return ofNative native
+
+/--
+Start the underlying timer of `s` and return an `AsyncTask` that will resolve once the previously
+configured duration has run out. Running this function twice returns the same `AsyncTask`.
+-/
+def wait (s : Sleep) : IO (AsyncTask Unit) := do
+  let promise ← s.native.next
+  return .ofPromise promise
+
+/--
+If:
+- `Sleep.wait` was previously called on `s` this makes the timer wait for `duration` counting from
+  the call of this function.
+- `Sleep.wait` was never called on `s` before this is a no-op.
+-/
+def reset (s : Sleep) : IO Unit :=
+  s.native.reset
+
+end Sleep
+
+/--
+Return an `AsyncTask` that resolves after `duration`.
+-/
+def sleep (duration : Std.Time.Millisecond.Offset) : IO (AsyncTask Unit) := do
+  let sleeper ← Sleep.mk duration
+  sleeper.wait
+
+/--
+`Interval` can be used to repeatedly wait for some duration like a clock.
+The underlying timer has millisecond resolution.
+-/
+structure Interval where
+  private ofNative ::
+    native : Internal.UV.Timer
+
+
+namespace Interval
+
+/--
+Setup up an `Interval` that waits for `duration` milliseconds.
+This function only initializes but does not yet start the underlying timer.
+-/
+def mk (duration : Std.Time.Millisecond.Offset) : IO Interval := do
+  let native ← Internal.UV.Timer.mk duration.toInt.toNat.toUInt64 true
+  return ofNative native
+
+/--
+Start the underlying timer of `s` and return an `AsyncTask` that will resolve upon the next tick
+of `i`. In particular:
+- calling this function for the first time starts the underlying timer of `i` and returns an
+  `AsyncTask` that instantly resolves as the 0th multiple of `duration` has elapsed.
+- calling this function while the tick from the last call has not yet finished returns the same
+  `AsyncTask` as the last call.
+- calling this function when the tick from the last call has finished returns a new `AsyncTask`
+  that waits for the closest next tick from the time of calling this function.
+-/
+def tick (i : Interval) : IO (AsyncTask Unit) := do
+  let promise ← i.native.next
+  return .ofPromise promise
+
+/--
+If:
+- `Interval.tick` was called on `i` before the next internal timer restarts counting from now and
+  the next tick happens in `duration`.
+- `Interval.tick` was never called on `i` before this is a no-op.
+-/
+def reset (i : Interval) : IO Unit :=
+  i.native.reset
+
+end Interval
+
+end Async
+end IO
+end Internal
+end Std

From 468341a8d834648c04b035ae507f1b11f79b1cdd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 2 Jan 2025 14:20:58 +0100
Subject: [PATCH 2/8] chore: inlining

---
 src/Std/Internal/Async.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/Std/Internal/Async.lean b/src/Std/Internal/Async.lean
index a241fbc2940f..ce05b70bb027 100644
--- a/src/Std/Internal/Async.lean
+++ b/src/Std/Internal/Async.lean
@@ -89,6 +89,7 @@ namespace Sleep
 Set up a `Sleep` that waits for `duration` milliseconds.
 This function only initializes but does not yet start the underlying timer.
 -/
+@[inline]
 def mk (duration : Std.Time.Millisecond.Offset) : IO Sleep := do
   let native ← Internal.UV.Timer.mk duration.toInt.toNat.toUInt64 false
   return ofNative native
@@ -97,6 +98,7 @@ def mk (duration : Std.Time.Millisecond.Offset) : IO Sleep := do
 Start the underlying timer of `s` and return an `AsyncTask` that will resolve once the previously
 configured duration has run out. Running this function twice returns the same `AsyncTask`.
 -/
+@[inline]
 def wait (s : Sleep) : IO (AsyncTask Unit) := do
   let promise ← s.native.next
   return .ofPromise promise
@@ -107,6 +109,7 @@ If:
   the call of this function.
 - `Sleep.wait` was never called on `s` before this is a no-op.
 -/
+@[inline]
 def reset (s : Sleep) : IO Unit :=
   s.native.reset
 
@@ -134,6 +137,7 @@ namespace Interval
 Setup up an `Interval` that waits for `duration` milliseconds.
 This function only initializes but does not yet start the underlying timer.
 -/
+@[inline]
 def mk (duration : Std.Time.Millisecond.Offset) : IO Interval := do
   let native ← Internal.UV.Timer.mk duration.toInt.toNat.toUInt64 true
   return ofNative native
@@ -148,6 +152,7 @@ of `i`. In particular:
 - calling this function when the tick from the last call has finished returns a new `AsyncTask`
   that waits for the closest next tick from the time of calling this function.
 -/
+@[inline]
 def tick (i : Interval) : IO (AsyncTask Unit) := do
   let promise ← i.native.next
   return .ofPromise promise
@@ -158,6 +163,7 @@ If:
   the next tick happens in `duration`.
 - `Interval.tick` was never called on `i` before this is a no-op.
 -/
+@[inline]
 def reset (i : Interval) : IO Unit :=
   i.native.reset
 

From 295baa580e4100ca4f5116ab425542fda2e3a5c2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Fri, 3 Jan 2025 10:08:18 +0100
Subject: [PATCH 3/8] chore: make the import

---
 src/Std/Internal.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Std/Internal.lean b/src/Std/Internal.lean
index e772b478b0ed..bc065b5dfef9 100644
--- a/src/Std/Internal.lean
+++ b/src/Std/Internal.lean
@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 prelude
--- TODO: after PR is merged
---import Std.Internal.Async
+import Std.Internal.Async
 import Std.Internal.Parsec
 import Std.Internal.UV
 

From 95bc5d11d8311d5505d97b6a44daf21600ce9644 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Fri, 3 Jan 2025 10:26:10 +0100
Subject: [PATCH 4/8] feat: bring over stop

---
 src/Std/Internal/Async.lean | 63 +++++++++++++++++++++++++------------
 1 file changed, 43 insertions(+), 20 deletions(-)

diff --git a/src/Std/Internal/Async.lean b/src/Std/Internal/Async.lean
index ce05b70bb027..f0bc6fda4cd1 100644
--- a/src/Std/Internal/Async.lean
+++ b/src/Std/Internal/Async.lean
@@ -81,13 +81,11 @@ structure Sleep where
   private ofNative ::
     native : Internal.UV.Timer
 
--- TODO: provable constraints on duration after changes in Std.Time
-
 namespace Sleep
 
 /--
 Set up a `Sleep` that waits for `duration` milliseconds.
-This function only initializes but does not yet start the underlying timer.
+This function only initializes but does not yet start the timer.
 -/
 @[inline]
 def mk (duration : Std.Time.Millisecond.Offset) : IO Sleep := do
@@ -95,8 +93,10 @@ def mk (duration : Std.Time.Millisecond.Offset) : IO Sleep := do
   return ofNative native
 
 /--
-Start the underlying timer of `s` and return an `AsyncTask` that will resolve once the previously
-configured duration has run out. Running this function twice returns the same `AsyncTask`.
+If:
+- `s` is not yet running start it and return an `AsyncTask` that will resolve once the previously
+   configured `duration` has run out.
+- `s` is already or not anymore running return the same `AsyncTask` as the first call to `wait`.
 -/
 @[inline]
 def wait (s : Sleep) : IO (AsyncTask Unit) := do
@@ -105,14 +105,25 @@ def wait (s : Sleep) : IO (AsyncTask Unit) := do
 
 /--
 If:
-- `Sleep.wait` was previously called on `s` this makes the timer wait for `duration` counting from
-  the call of this function.
-- `Sleep.wait` was never called on `s` before this is a no-op.
+- `s` is still running this will delay the resolution of `AsyncTask`s created with `wait` by
+  `duration` milliseconds.
+- `s` is not yet or not anymore running this is a no-op.
 -/
 @[inline]
 def reset (s : Sleep) : IO Unit :=
   s.native.reset
 
+/--
+If:
+- `s` is still running this stops `s` without resolving any remaing `AsyncTask` that were created
+  through `wait`. Note that if another `AsyncTask` is binding on any of these it is going hang
+  forever without further intervention.
+- `s` is not yet or not anymore running this is a no-op.
+-/
+@[inline]
+def stop (s : Sleep) : IO Unit :=
+  s.native.stop
+
 end Sleep
 
 /--
@@ -135,7 +146,7 @@ namespace Interval
 
 /--
 Setup up an `Interval` that waits for `duration` milliseconds.
-This function only initializes but does not yet start the underlying timer.
+This function only initializes but does not yet start the timer.
 -/
 @[inline]
 def mk (duration : Std.Time.Millisecond.Offset) : IO Interval := do
@@ -143,14 +154,15 @@ def mk (duration : Std.Time.Millisecond.Offset) : IO Interval := do
   return ofNative native
 
 /--
-Start the underlying timer of `s` and return an `AsyncTask` that will resolve upon the next tick
-of `i`. In particular:
-- calling this function for the first time starts the underlying timer of `i` and returns an
-  `AsyncTask` that instantly resolves as the 0th multiple of `duration` has elapsed.
-- calling this function while the tick from the last call has not yet finished returns the same
-  `AsyncTask` as the last call.
-- calling this function when the tick from the last call has finished returns a new `AsyncTask`
-  that waits for the closest next tick from the time of calling this function.
+If:
+- `i` is not yet running start it and return an `AsyncTask` that resolves right away as the 0th
+  multiple of `duration` has elapsed.
+- `i` is already running and:
+  - the tick from the last call of `i` has not yet finished return the same `AsyncTask` as the last
+    call
+  - the tick frrom the last call of `i` has finished return a new `AsyncTask` that waits for the
+    closest next tick from the time of calling this function.
+- `i` is not running aymore this is a no-op.
 -/
 @[inline]
 def tick (i : Interval) : IO (AsyncTask Unit) := do
@@ -159,14 +171,25 @@ def tick (i : Interval) : IO (AsyncTask Unit) := do
 
 /--
 If:
-- `Interval.tick` was called on `i` before the next internal timer restarts counting from now and
-  the next tick happens in `duration`.
-- `Interval.tick` was never called on `i` before this is a no-op.
+- `Interval.tick` was called on `i` before the timer restarts counting from now and the next tick
+   happens in `duration`.
+- `i` is not yet or not anymore running this is a no-op.
 -/
 @[inline]
 def reset (i : Interval) : IO Unit :=
   i.native.reset
 
+/--
+If:
+- `i` is still running this stops `i` without resolving any remaing `AsyncTask` that were created
+  through `tick`. Note that if another `AsyncTask` is binding on any of these it is going hang
+  forever without further intervention.
+- `i` is not yet or not anymore running this is a no-op.
+-/
+@[inline]
+def stop (i : Interval) : IO Unit :=
+  i.native.stop
+
 end Interval
 
 end Async

From 0b0ce345016adbf9b1cf96cbbed0c12971c70e3a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sun, 5 Jan 2025 18:01:59 +0100
Subject: [PATCH 5/8] chore: split it up

---
 src/Std/Internal/Async.lean       | 194 +-----------------------------
 src/Std/Internal/Async/Basic.lean | 108 +++++++++++++++++
 src/Std/Internal/Async/Timer.lean | 139 +++++++++++++++++++++
 3 files changed, 249 insertions(+), 192 deletions(-)
 create mode 100644 src/Std/Internal/Async/Basic.lean
 create mode 100644 src/Std/Internal/Async/Timer.lean

diff --git a/src/Std/Internal/Async.lean b/src/Std/Internal/Async.lean
index f0bc6fda4cd1..8d8e7db3e919 100644
--- a/src/Std/Internal/Async.lean
+++ b/src/Std/Internal/Async.lean
@@ -4,195 +4,5 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 prelude
-import Std.Time
-import Std.Internal.UV
-
-
-namespace Std
-namespace Internal
-namespace IO
-namespace Async
-
-/--
-A `Task` that may resolve to a value or an `IO.Error`.
--/
-def AsyncTask (α : Type u) : Type u := Task (Except IO.Error α)
-
-namespace AsyncTask
-
-@[inline]
-protected def pure (x : α) : AsyncTask α := Task.pure <| .ok x
-
-instance : Pure AsyncTask where
-  pure := AsyncTask.pure
-
-@[inline]
-protected def bind (x : AsyncTask α) (f : α → AsyncTask β) : AsyncTask β :=
-  Task.bind x fun r =>
-    match r with
-    | .ok a => f a
-    | .error e => Task.pure <| .error e
-
--- TODO: variants with explicit error handling
-
-@[inline]
-def bindIO (x : AsyncTask α) (f : α → IO (AsyncTask β)) : BaseIO (AsyncTask β) :=
-  IO.bindTask x fun r =>
-    match r with
-    | .ok a => f a
-    | .error e => .error e
-
-@[inline]
-def mapIO (f : α → β) (x : AsyncTask α) : BaseIO (AsyncTask β) :=
-  IO.mapTask (t := x) fun r =>
-    match r with
-    | .ok a => pure (f a)
-    | .error e => .error e
-
-/--
-Run the `AsyncTask` in `x` and block until it finishes.
--/
-def spawnBlocking (x : IO (AsyncTask α)) : IO α := do
-  let t ← x
-  let res := t.get
-  match res with
-  | .ok a => return a
-  | .error e => .error e
-
-@[inline]
-def spawn (x : IO α) : BaseIO (AsyncTask α) := do
-  IO.asTask x
-
-@[inline]
-def ofPromise (x : IO.Promise α) : AsyncTask α :=
-  x.result.map pure
-
-@[inline]
-def getState (x : AsyncTask α) : BaseIO IO.TaskState :=
-  IO.getTaskState x
-
-end AsyncTask
-
-/--
-`Sleep` can be used to sleep for some duration once.
-The underlying timer has millisecond resolution.
--/
-structure Sleep where
-  private ofNative ::
-    native : Internal.UV.Timer
-
-namespace Sleep
-
-/--
-Set up a `Sleep` that waits for `duration` milliseconds.
-This function only initializes but does not yet start the timer.
--/
-@[inline]
-def mk (duration : Std.Time.Millisecond.Offset) : IO Sleep := do
-  let native ← Internal.UV.Timer.mk duration.toInt.toNat.toUInt64 false
-  return ofNative native
-
-/--
-If:
-- `s` is not yet running start it and return an `AsyncTask` that will resolve once the previously
-   configured `duration` has run out.
-- `s` is already or not anymore running return the same `AsyncTask` as the first call to `wait`.
--/
-@[inline]
-def wait (s : Sleep) : IO (AsyncTask Unit) := do
-  let promise ← s.native.next
-  return .ofPromise promise
-
-/--
-If:
-- `s` is still running this will delay the resolution of `AsyncTask`s created with `wait` by
-  `duration` milliseconds.
-- `s` is not yet or not anymore running this is a no-op.
--/
-@[inline]
-def reset (s : Sleep) : IO Unit :=
-  s.native.reset
-
-/--
-If:
-- `s` is still running this stops `s` without resolving any remaing `AsyncTask` that were created
-  through `wait`. Note that if another `AsyncTask` is binding on any of these it is going hang
-  forever without further intervention.
-- `s` is not yet or not anymore running this is a no-op.
--/
-@[inline]
-def stop (s : Sleep) : IO Unit :=
-  s.native.stop
-
-end Sleep
-
-/--
-Return an `AsyncTask` that resolves after `duration`.
--/
-def sleep (duration : Std.Time.Millisecond.Offset) : IO (AsyncTask Unit) := do
-  let sleeper ← Sleep.mk duration
-  sleeper.wait
-
-/--
-`Interval` can be used to repeatedly wait for some duration like a clock.
-The underlying timer has millisecond resolution.
--/
-structure Interval where
-  private ofNative ::
-    native : Internal.UV.Timer
-
-
-namespace Interval
-
-/--
-Setup up an `Interval` that waits for `duration` milliseconds.
-This function only initializes but does not yet start the timer.
--/
-@[inline]
-def mk (duration : Std.Time.Millisecond.Offset) : IO Interval := do
-  let native ← Internal.UV.Timer.mk duration.toInt.toNat.toUInt64 true
-  return ofNative native
-
-/--
-If:
-- `i` is not yet running start it and return an `AsyncTask` that resolves right away as the 0th
-  multiple of `duration` has elapsed.
-- `i` is already running and:
-  - the tick from the last call of `i` has not yet finished return the same `AsyncTask` as the last
-    call
-  - the tick frrom the last call of `i` has finished return a new `AsyncTask` that waits for the
-    closest next tick from the time of calling this function.
-- `i` is not running aymore this is a no-op.
--/
-@[inline]
-def tick (i : Interval) : IO (AsyncTask Unit) := do
-  let promise ← i.native.next
-  return .ofPromise promise
-
-/--
-If:
-- `Interval.tick` was called on `i` before the timer restarts counting from now and the next tick
-   happens in `duration`.
-- `i` is not yet or not anymore running this is a no-op.
--/
-@[inline]
-def reset (i : Interval) : IO Unit :=
-  i.native.reset
-
-/--
-If:
-- `i` is still running this stops `i` without resolving any remaing `AsyncTask` that were created
-  through `tick`. Note that if another `AsyncTask` is binding on any of these it is going hang
-  forever without further intervention.
-- `i` is not yet or not anymore running this is a no-op.
--/
-@[inline]
-def stop (i : Interval) : IO Unit :=
-  i.native.stop
-
-end Interval
-
-end Async
-end IO
-end Internal
-end Std
+import Std.Internal.Async.Basic
+import Std.Internal.Async.Timer
diff --git a/src/Std/Internal/Async/Basic.lean b/src/Std/Internal/Async/Basic.lean
new file mode 100644
index 000000000000..1b2774334969
--- /dev/null
+++ b/src/Std/Internal/Async/Basic.lean
@@ -0,0 +1,108 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Init.Core
+import Init.System.IO
+import Init.System.Promise
+
+namespace Std
+namespace Internal
+namespace IO
+namespace Async
+
+/--
+A `Task` that may resolve to a value or an `IO.Error`.
+-/
+def AsyncTask (α : Type u) : Type u := Task (Except IO.Error α)
+
+namespace AsyncTask
+
+/--
+Construct an `AsyncTask` that is already resolved with value `x`.
+-/
+@[inline]
+protected def pure (x : α) : AsyncTask α := Task.pure <| .ok x
+
+instance : Pure AsyncTask where
+  pure := AsyncTask.pure
+
+/--
+Create a new `AsyncTask` that will run after `x` has finished.
+If `x`:
+- errors, return an `AsyncTask` that reolves to the error.
+- succeeds, run `f` on the result of `x` and return the `AsyncTask` produced by `f`.
+-/
+@[inline]
+protected def bind (x : AsyncTask α) (f : α → AsyncTask β) : AsyncTask β :=
+  Task.bind x fun r =>
+    match r with
+    | .ok a => f a
+    | .error e => Task.pure <| .error e
+
+/--
+Create a new `AsyncTask` that will run after `x` has finished.
+If `x`:
+- errors, return an `AsyncTask` that reolves to the error.
+- succeeds, return an `AsyncTask` that resolves to `f x`.
+-/
+@[inline]
+def map (f : α → β) (x : AsyncTask α) : AsyncTask β :=
+  Task.map (x := x) fun r =>
+    match r with
+    | .ok a => .ok (f a)
+    | .error e => .error e
+
+/--
+Similar to `bind`, however `f` has access to the `IO` monad. If `f` throws an error, the returned
+`AsyncTask` resolves to that error.
+-/
+@[inline]
+def bindIO (x : AsyncTask α) (f : α → IO (AsyncTask β)) : BaseIO (AsyncTask β) :=
+  IO.bindTask x fun r =>
+    match r with
+    | .ok a => f a
+    | .error e => .error e
+
+/--
+Similar to `bind`, however `f` has access to the `IO` monad. If `f` throws an error, the returned
+`AsyncTask` resolves to that error.
+-/
+@[inline]
+def mapIO (f : α → IO β) (x : AsyncTask α) : BaseIO (AsyncTask β) :=
+  IO.mapTask (t := x) fun r =>
+    match r with
+    | .ok a => f a
+    | .error e => .error e
+
+/--
+Block until the `AsyncTask` in `x` finishes.
+-/
+def block (x : AsyncTask α) : IO α := do
+  let res := x.get
+  match res with
+  | .ok a => return a
+  | .error e => .error e
+
+/--
+Create an `AsyncTask` that resolves to the value of `x`.
+-/
+@[inline]
+def ofPromise (x : IO.Promise α) : AsyncTask α :=
+  x.result.map pure
+
+/--
+Obtain the `IO.TaskState` of `x`.
+-/
+@[inline]
+def getState (x : AsyncTask α) : BaseIO IO.TaskState :=
+  IO.getTaskState x
+
+end AsyncTask
+
+end Async
+end IO
+end Internal
+end Std
diff --git a/src/Std/Internal/Async/Timer.lean b/src/Std/Internal/Async/Timer.lean
new file mode 100644
index 000000000000..fdaba3c0ec5b
--- /dev/null
+++ b/src/Std/Internal/Async/Timer.lean
@@ -0,0 +1,139 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Std.Time
+import Std.Internal.UV
+import Std.Internal.Async.Basic
+
+
+namespace Std
+namespace Internal
+namespace IO
+namespace Async
+
+/--
+`Sleep` can be used to sleep for some duration once.
+The underlying timer has millisecond resolution.
+-/
+structure Sleep where
+  private ofNative ::
+    native : Internal.UV.Timer
+
+namespace Sleep
+
+/--
+Set up a `Sleep` that waits for `duration` milliseconds.
+This function only initializes but does not yet start the timer.
+-/
+@[inline]
+def mk (duration : Std.Time.Millisecond.Offset) : IO Sleep := do
+  let native ← Internal.UV.Timer.mk duration.toInt.toNat.toUInt64 false
+  return ofNative native
+
+/--
+If:
+- `s` is not yet running start it and return an `AsyncTask` that will resolve once the previously
+   configured `duration` has run out.
+- `s` is already or not anymore running return the same `AsyncTask` as the first call to `wait`.
+-/
+@[inline]
+def wait (s : Sleep) : IO (AsyncTask Unit) := do
+  let promise ← s.native.next
+  return .ofPromise promise
+
+/--
+If:
+- `s` is still running this will delay the resolution of `AsyncTask`s created with `wait` by
+  `duration` milliseconds.
+- `s` is not yet or not anymore running this is a no-op.
+-/
+@[inline]
+def reset (s : Sleep) : IO Unit :=
+  s.native.reset
+
+/--
+If:
+- `s` is still running this stops `s` without resolving any remaing `AsyncTask` that were created
+  through `wait`. Note that if another `AsyncTask` is binding on any of these it is going hang
+  forever without further intervention.
+- `s` is not yet or not anymore running this is a no-op.
+-/
+@[inline]
+def stop (s : Sleep) : IO Unit :=
+  s.native.stop
+
+end Sleep
+
+/--
+Return an `AsyncTask` that resolves after `duration`.
+-/
+def sleep (duration : Std.Time.Millisecond.Offset) : IO (AsyncTask Unit) := do
+  let sleeper ← Sleep.mk duration
+  sleeper.wait
+
+/--
+`Interval` can be used to repeatedly wait for some duration like a clock.
+The underlying timer has millisecond resolution.
+-/
+structure Interval where
+  private ofNative ::
+    native : Internal.UV.Timer
+
+
+namespace Interval
+
+/--
+Setup up an `Interval` that waits for `duration` milliseconds.
+This function only initializes but does not yet start the timer.
+-/
+@[inline]
+def mk (duration : Std.Time.Millisecond.Offset) : IO Interval := do
+  let native ← Internal.UV.Timer.mk duration.toInt.toNat.toUInt64 true
+  return ofNative native
+
+/--
+If:
+- `i` is not yet running start it and return an `AsyncTask` that resolves right away as the 0th
+  multiple of `duration` has elapsed.
+- `i` is already running and:
+  - the tick from the last call of `i` has not yet finished return the same `AsyncTask` as the last
+    call
+  - the tick frrom the last call of `i` has finished return a new `AsyncTask` that waits for the
+    closest next tick from the time of calling this function.
+- `i` is not running aymore this is a no-op.
+-/
+@[inline]
+def tick (i : Interval) : IO (AsyncTask Unit) := do
+  let promise ← i.native.next
+  return .ofPromise promise
+
+/--
+If:
+- `Interval.tick` was called on `i` before the timer restarts counting from now and the next tick
+   happens in `duration`.
+- `i` is not yet or not anymore running this is a no-op.
+-/
+@[inline]
+def reset (i : Interval) : IO Unit :=
+  i.native.reset
+
+/--
+If:
+- `i` is still running this stops `i` without resolving any remaing `AsyncTask` that were created
+  through `tick`. Note that if another `AsyncTask` is binding on any of these it is going hang
+  forever without further intervention.
+- `i` is not yet or not anymore running this is a no-op.
+-/
+@[inline]
+def stop (i : Interval) : IO Unit :=
+  i.native.stop
+
+end Interval
+
+end Async
+end IO
+end Internal
+end Std

From 2ce2a60df3998229112b9c276837fea95466d83e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sun, 5 Jan 2025 19:26:19 +0100
Subject: [PATCH 6/8] test: the surface level API

---
 tests/lean/run/async_surface_sleep.lean | 99 +++++++++++++++++++++++++
 1 file changed, 99 insertions(+)
 create mode 100644 tests/lean/run/async_surface_sleep.lean

diff --git a/tests/lean/run/async_surface_sleep.lean b/tests/lean/run/async_surface_sleep.lean
new file mode 100644
index 000000000000..b548fd058f2c
--- /dev/null
+++ b/tests/lean/run/async_surface_sleep.lean
@@ -0,0 +1,99 @@
+import Std.Internal.Async.Timer
+
+/-
+these tests are just some preliminary ones as `async_sleep.lean` already contains extensive tests
+for the entire timer state machine and `Async.Timer` is merely a light wrapper around it.
+-/
+
+open Std.Internal.IO.Async
+
+def BASE_DURATION : Std.Time.Millisecond.Offset := 10
+
+namespace SleepTest
+
+def oneSleep : IO Unit := do
+  let task ← go
+  assert! (← task.block) == 37
+where
+  go : IO (AsyncTask Nat) := do
+    let sleep ← Sleep.mk BASE_DURATION
+    (← sleep.wait).mapIO fun _ =>
+      return 37
+
+def doubleSleep : IO Unit := do
+  let task ← go
+  assert! (← task.block) == 37
+where
+  go : IO (AsyncTask Nat) := do
+    let sleep ← Sleep.mk BASE_DURATION
+    (← sleep.wait).bindIO fun _ => do
+    (← sleep.wait).mapIO fun _ =>
+      return 37
+
+def resetSleep : IO Unit := do
+  let task ← go
+  assert! (← task.block) == 37
+where
+  go : IO (AsyncTask Nat) := do
+    let sleep ← Sleep.mk BASE_DURATION
+    let waiter ← sleep.wait
+    sleep.reset
+    waiter.mapIO fun _ =>
+      return 37
+
+def simpleSleep : IO Unit := do
+  let task ← go
+  assert! (← task.block) == 37
+where
+  go : IO (AsyncTask Nat) := do
+    (← sleep BASE_DURATION).mapIO fun _ =>
+      return 37
+
+#eval oneSleep
+#eval doubleSleep
+#eval resetSleep
+#eval simpleSleep
+
+end SleepTest
+
+namespace IntervalTest
+
+def oneSleep : IO Unit := do
+  let task ← go
+  assert! (← task.block) == 37
+where
+  go : IO (AsyncTask Nat) := do
+    let interval ← Interval.mk BASE_DURATION
+    (← interval.tick).mapIO fun _ => do
+      interval.stop
+      return 37
+
+def doubleSleep : IO Unit := do
+  let task ← go
+  assert! (← task.block) == 37
+where
+  go : IO (AsyncTask Nat) := do
+    let interval ← Interval.mk BASE_DURATION
+    (← interval.tick).bindIO fun _ => do
+    (← interval.tick).mapIO fun _ => do
+      interval.stop
+      return 37
+
+def resetSleep : IO Unit := do
+  let task ← go
+  assert! (← task.block) == 37
+where
+  go : IO (AsyncTask Nat) := do
+    let interval ← Interval.mk BASE_DURATION
+    (← interval.tick).bindIO fun _ => do
+      let waiter ← interval.tick
+      interval.reset
+      waiter.mapIO fun _ => do
+        interval.stop
+        return 37
+
+#eval oneSleep
+#eval doubleSleep
+#eval resetSleep
+
+end IntervalTest

From a5b05eb6d57102cee17c983b2a85564b108f3c6d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sun, 5 Jan 2025 23:32:09 +0100
Subject: [PATCH 7/8] chore: intermediate

---
 src/Std/Internal/Async/Basic.lean | 9 ++++++++-
 src/Std/Internal/Async/Timer.lean | 4 ++--
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/src/Std/Internal/Async/Basic.lean b/src/Std/Internal/Async/Basic.lean
index 1b2774334969..387bdc8f22b0 100644
--- a/src/Std/Internal/Async/Basic.lean
+++ b/src/Std/Internal/Async/Basic.lean
@@ -90,7 +90,14 @@ def block (x : AsyncTask α) : IO α := do
 Create an `AsyncTask` that resolves to the value of `x`.
 -/
 @[inline]
-def ofPromise (x : IO.Promise α) : AsyncTask α :=
+def ofPromise (x : IO.Promise (Except IO.Error α)) : AsyncTask α :=
+  x.result
+
+/--
+Create an `AsyncTask` that resolves to the value of `x`.
+-/
+@[inline]
+def ofPurePromise (x : IO.Promise α) : AsyncTask α :=
   x.result.map pure
 
 /--
diff --git a/src/Std/Internal/Async/Timer.lean b/src/Std/Internal/Async/Timer.lean
index fdaba3c0ec5b..e3fd6a77d66c 100644
--- a/src/Std/Internal/Async/Timer.lean
+++ b/src/Std/Internal/Async/Timer.lean
@@ -42,7 +42,7 @@ If:
 @[inline]
 def wait (s : Sleep) : IO (AsyncTask Unit) := do
   let promise ← s.native.next
-  return .ofPromise promise
+  return .ofPurePromise promise
 
 /--
 If:
@@ -108,7 +108,7 @@ If:
 @[inline]
 def tick (i : Interval) : IO (AsyncTask Unit) := do
   let promise ← i.native.next
-  return .ofPromise promise
+  return .ofPurePromise promise
 
 /--
 If:

From 52d5c1ee892766203e18e5675323ff5824e21037 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 7 Jan 2025 10:12:33 +0100
Subject: [PATCH 8/8] feat: add duration side condition for repeating timer

---
 src/Std/Internal/Async/Timer.lean       | 2 +-
 tests/lean/run/async_surface_sleep.lean | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Std/Internal/Async/Timer.lean b/src/Std/Internal/Async/Timer.lean
index e3fd6a77d66c..72cf604fb775 100644
--- a/src/Std/Internal/Async/Timer.lean
+++ b/src/Std/Internal/Async/Timer.lean
@@ -90,7 +90,7 @@ Setup up an `Interval` that waits for `duration` milliseconds.
 This function only initializes but does not yet start the timer.
 -/
 @[inline]
-def mk (duration : Std.Time.Millisecond.Offset) : IO Interval := do
+def mk (duration : Std.Time.Millisecond.Offset) (_ : 0 < duration := by decide) : IO Interval := do
   let native ← Internal.UV.Timer.mk duration.toInt.toNat.toUInt64 true
   return ofNative native
 
diff --git a/tests/lean/run/async_surface_sleep.lean b/tests/lean/run/async_surface_sleep.lean
index b548fd058f2c..23f6cf30b27e 100644
--- a/tests/lean/run/async_surface_sleep.lean
+++ b/tests/lean/run/async_surface_sleep.lean
@@ -63,7 +63,7 @@ def oneSleep : IO Unit := do
   assert! (← task.block) == 37
 where
   go : IO (AsyncTask Nat) := do
-    let interval ← Interval.mk BASE_DURATION
+    let interval ← Interval.mk BASE_DURATION sorry
     (← interval.tick).mapIO fun _ => do
       interval.stop
       return 37
@@ -73,7 +73,7 @@ def doubleSleep : IO Unit := do
   assert! (← task.block) == 37
 where
   go : IO (AsyncTask Nat) := do
-    let interval ← Interval.mk BASE_DURATION
+    let interval ← Interval.mk BASE_DURATION sorry
     (← interval.tick).bindIO fun _ => do
     (← interval.tick).mapIO fun _ => do
       interval.stop
@@ -84,7 +84,7 @@ def resetSleep : IO Unit := do
   assert! (← task.block) == 37
 where
   go : IO (AsyncTask Nat) := do
-    let interval ← Interval.mk BASE_DURATION
+    let interval ← Interval.mk BASE_DURATION sorry
     (← interval.tick).bindIO fun _ => do
       let waiter ← interval.tick
       interval.reset