feat: inject unreachable! after break-less repeat to unblock dead-code warnings

When a `repeat` body has no `break`, the loop does not terminate
normally and the `ForIn.forIn` result type is fixed to `PUnit`. Using
such a `repeat` in a do block that expects a non-`Unit` result type
used to require a trailing `return`/`unreachable!` from the user. To
make matters worse, that trailing element was flagged as dead by the
`ControlInfo`-based warning, yet removing it broke the do block's
type, so the warning was not actionable and had to be suppressed.

This PR teaches `elabDoRepeat` to append its own `unreachable!` after
the `for _ in Loop.mk do ...` expansion when the body cannot `break`.
The `unreachable!` gives the continuation a polymorphic value, so the
enclosing do block's result type is inferred from context and the
user no longer needs to write any trailing filler. The
`ControlInfo` for break-less `repeat` now reports `noFallthrough`
(and `numRegularExits := 0`) honestly, so dead-code warnings fire on
any user-written element after the loop — and because the loop
supplies its own `unreachable!`, those warnings are actionable: the
user can simply delete the flagged element.

Co-authored-by: Rob23oba <robin.arnez@web.de>

src/Lean/Elab/BuiltinDo/Repeat.lean

@@ -19,13 +19,19 @@ open Lean.Parser.Term
 /--
 Builtin do-element elaborator for `repeat` (syntax kind `Lean.Parser.Term.doRepeat`).
 
-Expands to `for _ in Loop.mk do ...`. A follow-up change will extend this
-elaborator to choose between `Loop.mk` and a well-founded `Repeat.mk` based on a
-configuration option.
+Expands to `for _ in Loop.mk do ...`. When the body cannot `break`, the loop's own expression
+type is fixed to `PUnit`, yet the surrounding do block may require a different result type;
+we append an `unreachable!` so the continuation has a polymorphic value of any type. The
+`unreachable!` is never actually executed (the loop never terminates normally), and any
+dead-code warning that fires on the surrounding continuation is actionable — the user can
+remove the following code without breaking the do block's type.
 -/
 @[builtin_doElem_elab Lean.Parser.Term.doRepeat] def elabDoRepeat : DoElab := fun stx dec => do
   let `(doElem| repeat%$tk $seq) := stx | throwUnsupportedSyntax
-  let expanded ← `(doElem| for%$tk _ in Loop.mk do $seq)
+  let mut expanded ← `(doElem| for%$tk _ in Loop.mk do $seq)
+  let info ← inferControlInfoSeq seq
+  if !info.breaks then
+    expanded ← `(doElem| do $expanded:doElem; unreachable!)
   Term.withMacroExpansion stx expanded <|
     withRef expanded <| elabDoElem ⟨expanded⟩ dec
 

src/Lean/Elab/Do/InferControlInfo.lean

@@ -165,8 +165,7 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
   | `(doElem| unless $_ do $elseSeq) =>
     ControlInfo.alternative {} <$> ofSeq elseSeq
   -- For/Repeat
-  | `(doElem| for $[$[$_ :]? $_ in $_],* do $bodySeq)
-  | `(doRepeat| repeat $bodySeq) =>
+  | `(doElem| for $[$[$_ :]? $_ in $_],* do $bodySeq) =>
     let info ← ofSeq bodySeq
     return { info with  -- keep only reassigns and earlyReturn
       numRegularExits := 1,
@@ -174,6 +173,17 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
       breaks := false,
       noFallthrough := false,
     }
+  | `(doRepeat| repeat $bodySeq) =>
+    -- A break-less `repeat` never falls through; the elaborator injects an `unreachable!` so the
+    -- surrounding continuation still has a polymorphic value to hand back, and any dead-code
+    -- warning on subsequent elements is actionable.
+    let info ← ofSeq bodySeq
+    return { info with  -- keep only reassigns and earlyReturn
+      numRegularExits := if info.breaks then 1 else 0,
+      continues := false,
+      breaks := false,
+      noFallthrough := !info.breaks,
+    }
   -- Try
   | `(doElem| try $trySeq:doSeq $[$catches]* $[finally $finSeq?]?) =>
     let mut info ← ofSeq trySeq

src/Lean/Elab/Idbg.lean

@@ -8,7 +8,7 @@ module
 prelude
 public import Lean.Elab.Do.Basic
 meta import Lean.Parser.Do
-import Std.Async.TCP
+import Std.Internal.Async.TCP
 
 /-!
 # Interactive Debug Expression Evaluator (`idbg`)
@@ -22,7 +22,7 @@ and client (compiled program side) compute a deterministic port from the source
 -/
 
 open Lean Lean.Elab Lean.Elab.Term Lean.Meta
-open Std.Net Std.Async
+open Std.Net Std.Internal.IO.Async
 
 namespace Lean.Idbg
 

src/Std/Async.lean

@@ -1,19 +0,0 @@
-/-
-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
--/
-module
-
-prelude
-public import Std.Async.Basic
-public import Std.Async.ContextAsync
-public import Std.Async.Timer
-public import Std.Async.TCP
-public import Std.Async.UDP
-public import Std.Async.DNS
-public import Std.Async.Select
-public import Std.Async.Process
-public import Std.Async.System
-public import Std.Async.Signal
-public import Std.Async.IO

src/Std/Http/Data.lean

@@ -1,24 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sofia Rodrigues
--/
-module
-
-prelude
-public import Std.Http.Data.Method
-public import Std.Http.Data.Version
-public import Std.Http.Data.Request
-public import Std.Http.Data.Response
-public import Std.Http.Data.Status
-public import Std.Http.Data.Chunk
-public import Std.Http.Data.Headers
-public import Std.Http.Data.URI
-public import Std.Http.Data.Body
-
-/-!
-# HTTP Data Types
-
-This module re-exports all HTTP data types including request/response structures,
-methods, status codes, chunks, and extension metadata.
--/

src/Std/Http/Internal.lean

@@ -1,22 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sofia Rodrigues
--/
-module
-
-prelude
-public import Std.Http.Internal.Char
-public import Std.Http.Internal.ChunkedBuffer
-public import Std.Http.Internal.LowerCase
-public import Std.Http.Internal.IndexMultiMap
-public import Std.Http.Internal.Encode
-public import Std.Http.Internal.String
-public import Std.Http.Internal.Char
-
-/-!
-# HTTP Internal Utilities
-
-This module re-exports internal utilities used by the HTTP library including
-data structures, encoding functions, and buffer management.
--/

src/Std/Internal.lean

@@ -6,8 +6,8 @@ Authors: Henrik Böving
 module
 
 prelude
-public import Std.Async
-public import Std.Http
+public import Std.Internal.Async
+public import Std.Internal.Http
 public import Std.Internal.Parsec
 public import Std.Internal.UV
 

src/Std/Internal/Async.lean

@@ -0,0 +1,19 @@
+/-
+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
+-/
+module
+
+prelude
+public import Std.Internal.Async.Basic
+public import Std.Internal.Async.ContextAsync
+public import Std.Internal.Async.Timer
+public import Std.Internal.Async.TCP
+public import Std.Internal.Async.UDP
+public import Std.Internal.Async.DNS
+public import Std.Internal.Async.Select
+public import Std.Internal.Async.Process
+public import Std.Internal.Async.System
+public import Std.Internal.Async.Signal
+public import Std.Internal.Async.IO

src/Std/Internal/Async/Basic.lean

@@ -12,6 +12,8 @@ public import Init.While
 public section
 
 namespace Std
+namespace Internal
+namespace IO
 namespace Async
 
 /-!
@@ -995,4 +997,6 @@ def background [Monad m] [MonadAsync t m] (action : m α) (prio := Task.Priority
   discard (async (t := t) (prio := prio) action)
 
 end Async
+end IO
+end Internal
 end Std

src/Std/Internal/Async/ContextAsync.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Std.Internal.UV
-public import Std.Async.Timer
+public import Std.Internal.Async.Timer
 public import Std.Sync.CancellationContext
 
 public section
@@ -18,6 +18,8 @@ cooperative cancellation support that must be explicitly checked for and cancell
 -/
 
 namespace Std
+namespace Internal
+namespace IO
 namespace Async
 
 /--
@@ -264,4 +266,6 @@ def Selector.cancelled : ContextAsync (Selector Unit) := do
   ContextAsync.doneSelector
 
 end Async
+end IO
+end Internal
 end Std

src/Std/Internal/Async/DNS.lean

@@ -8,14 +8,14 @@ module
 prelude
 public import Std.Time
 public import Std.Internal.UV
-public import Std.Async.Basic
+public import Std.Internal.Async.Basic
 public import Init.Data.Function
 
 public section
 
-open Std.Internal
-
 namespace Std
+namespace Internal
+namespace IO
 namespace Async
 namespace DNS
 
@@ -59,4 +59,6 @@ def getNameInfo (host : @& SocketAddress) : Async NameInfo :=
 
 end DNS
 end Async
+end IO
+end Internal
 end Std

src/Std/Internal/Async/IO.lean

@@ -6,15 +6,16 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Async.Select
+public import Std.Internal.Async.Select
 
 public section
 
 namespace Std
+namespace Internal
 namespace Async
 namespace IO
 
-open Std.Async
+open Std.Internal.IO.Async
 
 /-!
 This module provides buffered asynchronous I/O operations for efficient reading and writing.
@@ -49,4 +50,5 @@ class AsyncStream (α : Type) (β : outParam Type) where
 
 end IO
 end Async
+end Internal
 end Std

src/Std/Internal/Async/Process.lean

@@ -15,9 +15,9 @@ public section
 
 open Std Time
 open System
-open Std.Internal
 
 namespace Std
+namespace Internal
 namespace IO
 namespace Process
 
@@ -239,4 +239,5 @@ def availableMemory : IO UInt64 :=
 
 end Process
 end IO
+end Internal
 end Std

src/Std/Internal/Async/Select.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.Random
-public import Std.Async.Basic
+public import Std.Internal.Async.Basic
 import Init.Data.ByteArray.Extra
 import Init.Data.Array.Lemmas
 import Init.Omega
@@ -21,6 +21,8 @@ The main entrypoint for users is `Selectable.one` and the various functions to p
 -/
 
 namespace Std
+namespace Internal
+namespace IO
 namespace Async
 
 /--
@@ -256,4 +258,6 @@ def Selectable.combine (selectables : Array (Selectable α)) : IO (Selector α)
   }
 
 end Async
+end IO
+end Internal
 end Std

src/Std/Internal/Async/Signal.lean

@@ -8,11 +8,13 @@ module
 prelude
 public import Std.Time
 public import Std.Internal.UV.Signal
-public import Std.Async.Select
+public import Std.Internal.Async.Select
 
 public section
 
 namespace Std
+namespace Internal
+namespace IO
 namespace Async
 
 /--

src/Std/Internal/Async/System.lean

@@ -19,9 +19,10 @@ manipulation.
 
 open Std Time
 open System
-open Std.Internal
 
 namespace Std
+namespace Internal
+namespace IO
 namespace Async
 namespace System
 
@@ -315,4 +316,6 @@ def getGroup (groupId : GroupId) : IO (Option GroupInfo) := do
 
 end System
 end Async
+end IO
+end Internal
 end Std

src/Std/Internal/Async/TCP.lean

@@ -8,11 +8,13 @@ module
 prelude
 public import Std.Time
 public import Std.Internal.UV.TCP
-public import Std.Async.Select
+public import Std.Internal.Async.Select
 
 public section
 
 namespace Std
+namespace Internal
+namespace IO
 namespace Async
 namespace TCP
 open Std.Net
@@ -256,4 +258,6 @@ end Client
 end Socket
 end TCP
 end Async
+end IO
+end Internal
 end Std

src/Std/Internal/Async/Timer.lean

@@ -8,12 +8,14 @@ module
 prelude
 public import Std.Time
 public import Std.Internal.UV.Timer
-public import Std.Async.Select
+public import Std.Internal.Async.Select
 
 public section
 
 
 namespace Std
+namespace Internal
+namespace IO
 namespace Async
 
 /--
@@ -166,4 +168,6 @@ def stop (i : Interval) : IO Unit :=
 end Interval
 
 end Async
+end IO
+end Internal
 end Std

src/Std/Internal/Async/UDP.lean

@@ -8,11 +8,13 @@ module
 prelude
 public import Std.Time
 public import Std.Internal.UV.UDP
-public import Std.Async.Select
+public import Std.Internal.Async.Select
 
 public section
 
 namespace Std
+namespace Internal
+namespace IO
 namespace Async
 namespace UDP
 
@@ -190,4 +192,6 @@ end Socket
 
 end UDP
 end Async
+end IO
+end Internal
 end Std

src/Std/Internal/Http.lean

@@ -6,8 +6,8 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Http.Server
-public import Std.Http.Test.Helpers
+public import Std.Internal.Http.Server
+public import Std.Internal.Http.Test.Helpers
 
 public section
 
@@ -40,9 +40,9 @@ The main entry point is `Server.serve`, which starts an HTTP/1.1 server. Impleme
 `Expect: 100-continue` headers:
 
 ```lean
-import Std.Http
+import Std.Internal.Http
 
-open Std Async
+open Std Internal IO Async
 open Std Http Server
 
 structure MyHandler

src/Std/Internal/Http/Data.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Http.Data.Method
+public import Std.Internal.Http.Data.Version
+public import Std.Internal.Http.Data.Request
+public import Std.Internal.Http.Data.Response
+public import Std.Internal.Http.Data.Status
+public import Std.Internal.Http.Data.Chunk
+public import Std.Internal.Http.Data.Headers
+public import Std.Internal.Http.Data.URI
+public import Std.Internal.Http.Data.Body
+
+/-!
+# HTTP Data Types
+
+This module re-exports all HTTP data types including request/response structures,
+methods, status codes, chunks, and extension metadata.
+-/

src/Std/Internal/Http/Data/Body.lean

@@ -6,12 +6,12 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Http.Data.Body.Basic
-public import Std.Http.Data.Body.Length
-public import Std.Http.Data.Body.Any
-public import Std.Http.Data.Body.Stream
-public import Std.Http.Data.Body.Empty
-public import Std.Http.Data.Body.Full
+public import Std.Internal.Http.Data.Body.Basic
+public import Std.Internal.Http.Data.Body.Length
+public import Std.Internal.Http.Data.Body.Any
+public import Std.Internal.Http.Data.Body.Stream
+public import Std.Internal.Http.Data.Body.Empty
+public import Std.Internal.Http.Data.Body.Full
 
 public section
 

src/Std/Internal/Http/Data/Body/Any.lean

@@ -6,7 +6,7 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Http.Data.Body.Basic
+public import Std.Internal.Http.Data.Body.Basic
 
 public section
 
@@ -18,7 +18,7 @@ type that also implements `Http.Body`. Used as the default handler response body
 -/
 
 namespace Std.Http.Body
-open Std Async
+open Std Internal IO Async
 
 set_option linter.all true
 

src/Std/Internal/Http/Data/Body/Basic.lean

@@ -6,11 +6,11 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Async
-public import Std.Async.ContextAsync
-public import Std.Http.Data.Chunk
-public import Std.Http.Data.Headers
-public import Std.Http.Data.Body.Length
+public import Std.Internal.Async
+public import Std.Internal.Async.ContextAsync
+public import Std.Internal.Http.Data.Chunk
+public import Std.Internal.Http.Data.Headers
+public import Std.Internal.Http.Data.Body.Length
 
 public section
 
@@ -22,7 +22,7 @@ This module defines the `Body` typeclass for HTTP body streams, and shared conve
 -/
 
 namespace Std.Http
-open Std Async
+open Std Internal IO Async
 
 set_option linter.all true
 

src/Std/Internal/Http/Data/Body/Empty.lean

@@ -6,9 +6,9 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Http.Data.Request
-public import Std.Http.Data.Response
-public import Std.Http.Data.Body.Any
+public import Std.Internal.Http.Data.Request
+public import Std.Internal.Http.Data.Response
+public import Std.Internal.Http.Data.Body.Any
 
 public section
 
@@ -19,7 +19,7 @@ Represents an always-empty, already-closed body handle.
 -/
 
 namespace Std.Http.Body
-open Std Async
+open Std Internal IO Async
 
 set_option linter.all true
 
@@ -102,7 +102,7 @@ instance : Coe (Async (Response Empty)) (ContextAsync (Response Any)) where
 end Body
 
 namespace Request.Builder
-open Async
+open Internal.IO.Async
 
 /--
 Builds a request with no body.
@@ -113,7 +113,7 @@ def empty (builder : Builder) : Async (Request Body.Empty) :=
 end Request.Builder
 
 namespace Response.Builder
-open Async
+open Internal.IO.Async
 
 /--
 Builds a response with no body.

src/Std/Internal/Http/Data/Body/Full.lean

@@ -7,9 +7,9 @@ module
 
 prelude
 public import Std.Sync
-public import Std.Http.Data.Request
-public import Std.Http.Data.Response
-public import Std.Http.Data.Body.Any
+public import Std.Internal.Http.Data.Request
+public import Std.Internal.Http.Data.Response
+public import Std.Internal.Http.Data.Body.Any
 public import Init.Data.ByteArray
 
 public section
@@ -25,7 +25,7 @@ Closing the body discards any unconsumed data.
 -/
 
 namespace Std.Http.Body
-open Std Async
+open Std Internal IO Async
 
 set_option linter.all true
 
@@ -159,7 +159,7 @@ end Body
 
 namespace Request.Builder
 
-open Async
+open Internal.IO.Async
 
 /--
 Builds a request body from raw bytes without setting any headers.
@@ -200,7 +200,7 @@ def html (builder : Builder) (content : String) : Async (Request Body.Full) :=
 end Request.Builder
 
 namespace Response.Builder
-open Async
+open Internal.IO.Async
 
 /--
 Builds a response body from raw bytes without setting any headers.

src/Std/Internal/Http/Data/Body/Stream.lean

@@ -7,12 +7,12 @@ module
 
 prelude
 public import Std.Sync
-public import Std.Async
-public import Std.Http.Data.Request
-public import Std.Http.Data.Response
-public import Std.Http.Data.Chunk
-public import Std.Http.Data.Body.Basic
-public import Std.Http.Data.Body.Any
+public import Std.Internal.Async
+public import Std.Internal.Http.Data.Request
+public import Std.Internal.Http.Data.Response
+public import Std.Internal.Http.Data.Chunk
+public import Std.Internal.Http.Data.Body.Basic
+public import Std.Internal.Http.Data.Body.Any
 public import Init.Data.ByteArray
 
 public section
@@ -31,13 +31,13 @@ namespace Std.Http
 
 namespace Body
 
-open Std Async
+open Std Internal IO Async
 
 set_option linter.all true
 
 namespace Channel
 
-open Async in
+open Internal.IO.Async in
 private inductive Consumer where
   | normal (promise : IO.Promise (Option Chunk))
   | select (finished : Waiter (Option Chunk))
@@ -62,7 +62,7 @@ private structure Producer where
   -/
   done : IO.Promise Bool
 
-open Async in
+open Internal.IO.Async in
 private def resolveInterestWaiter (waiter : Waiter Bool) (x : Bool) : BaseIO Bool := do
   let lose := return false
   let win promise := do
@@ -84,7 +84,7 @@ private structure State where
   /--
   A waiter for `Stream.interestSelector`.
   -/
-  interestWaiter : Option (Async.Waiter Bool)
+  interestWaiter : Option (Internal.IO.Async.Waiter Bool)
 
   /--
   Whether the channel is closed.
@@ -299,7 +299,7 @@ def setKnownSize (stream : Stream) (size : Option Body.Length) : Async Unit :=
   stream.state.atomically do
     modify fun st => { st with knownSize := size }
 
-open Async in
+open Internal.IO.Async in
 
 /--
 Creates a selector that resolves when a producer is waiting (or the channel closes).
@@ -521,7 +521,7 @@ def hasInterest (stream : Stream) : Async Bool :=
     Channel.pruneFinishedWaiters
     Channel.hasInterest'
 
-open Async in
+open Internal.IO.Async in
 /--
 Creates a selector that resolves when consumer interest is present.
 Returns `true` when a consumer is waiting, `false` when the channel closes first.
@@ -634,7 +634,7 @@ end Body
 
 namespace Request.Builder
 
-open Async
+open Internal.IO.Async
 
 /--
 Builds a request with a streaming body generator.
@@ -649,7 +649,7 @@ def stream
 end Request.Builder
 
 namespace Response.Builder
-open Async
+open Internal.IO.Async
 
 /--
 Builds a response with a streaming body generator.

src/Std/Internal/Http/Data/Chunk.lean

@@ -6,9 +6,9 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Http.Internal
-public import Std.Http.Data.Headers
-public meta import Std.Http.Internal.String
+public import Std.Internal.Http.Internal
+public import Std.Internal.Http.Data.Headers
+public meta import Std.Internal.Http.Internal.String
 
 public section
 

src/Std/Internal/Http/Data/Headers.lean

@@ -6,9 +6,9 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Http.Data.Headers.Basic
-public import Std.Http.Data.Headers.Name
-public import Std.Http.Data.Headers.Value
+public import Std.Internal.Http.Data.Headers.Basic
+public import Std.Internal.Http.Data.Headers.Name
+public import Std.Internal.Http.Data.Headers.Value
 
 public section
 

src/Std/Internal/Http/Data/Headers/Basic.lean

@@ -6,9 +6,9 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Http.Data.URI
-public import Std.Http.Data.Headers.Name
-public import Std.Http.Data.Headers.Value
+public import Std.Internal.Http.Data.URI
+public import Std.Internal.Http.Data.Headers.Name
+public import Std.Internal.Http.Data.Headers.Value
 public import Std.Internal.Parsec.Basic
 import Init.Data.String.Search
 

src/Std/Internal/Http/Data/Headers/Name.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.ToString
-public import Std.Http.Internal
+public import Std.Internal.Http.Internal
 import Init.Data.String.Search
 import Init.Data.String.Iter
 

src/Std/Internal/Http/Data/Headers/Value.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.ToString
-public import Std.Http.Internal
+public import Std.Internal.Http.Internal
 
 public section
 

src/Std/Internal/Http/Data/Method.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.ToString
-public import Std.Http.Internal
+public import Std.Internal.Http.Internal
 
 public section
 

src/Std/Internal/Http/Data/Request.lean

@@ -6,11 +6,11 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Http.Data.Extensions
-public import Std.Http.Data.Method
-public import Std.Http.Data.Version
-public import Std.Http.Data.Headers
-public import Std.Http.Data.URI
+public import Std.Internal.Http.Data.Extensions
+public import Std.Internal.Http.Data.Method
+public import Std.Internal.Http.Data.Version
+public import Std.Internal.Http.Data.Headers
+public import Std.Internal.Http.Data.URI
 
 public section
 

src/Std/Internal/Http/Data/Response.lean

@@ -6,10 +6,10 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Http.Data.Extensions
-public import Std.Http.Data.Status
-public import Std.Http.Data.Version
-public import Std.Http.Data.Headers
+public import Std.Internal.Http.Data.Extensions
+public import Std.Internal.Http.Data.Status
+public import Std.Internal.Http.Data.Version
+public import Std.Internal.Http.Data.Headers
 
 public section
 

src/Std/Internal/Http/Data/Status.lean

@@ -6,7 +6,7 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Http.Internal
+public import Std.Internal.Http.Internal
 
 public section
 

src/Std/Internal/Http/Data/URI.lean

@@ -6,8 +6,8 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Http.Data.URI.Basic
-public import Std.Http.Data.URI.Parser
+public import Std.Internal.Http.Data.URI.Basic
+public import Std.Internal.Http.Data.URI.Parser
 
 public section
 

src/Std/Internal/Http/Data/URI/Basic.lean

@@ -8,8 +8,8 @@ module
 prelude
 import Init.Data.ToString
 public import Std.Net
-public import Std.Http.Internal
-public import Std.Http.Data.URI.Encoding
+public import Std.Internal.Http.Internal
+public import Std.Internal.Http.Data.URI.Encoding
 public import Init.Data.String.Search
 
 public section

src/Std/Internal/Http/Data/URI/Encoding.lean

@@ -13,7 +13,7 @@ import Init.Data.UInt.Lemmas
 import Init.Data.UInt.Bitwise
 import Init.Data.Array.Lemmas
 public import Init.Data.String.Basic
-public import Std.Http.Internal.Char
+public import Std.Internal.Http.Internal.Char
 
 public section
 

src/Std/Internal/Http/Data/URI/Parser.lean

@@ -10,8 +10,8 @@ import Init.While
 public import Init.Data.String.Basic
 public import Std.Internal.Parsec
 public import Std.Internal.Parsec.ByteArray
-public import Std.Http.Data.URI.Basic
-public import Std.Http.Data.URI.Config
+public import Std.Internal.Http.Data.URI.Basic
+public import Std.Internal.Http.Data.URI.Config
 import Init.Data.String.Search
 
 public section

src/Std/Internal/Http/Internal.lean

@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Http.Internal.Char
+public import Std.Internal.Http.Internal.ChunkedBuffer
+public import Std.Internal.Http.Internal.LowerCase
+public import Std.Internal.Http.Internal.IndexMultiMap
+public import Std.Internal.Http.Internal.Encode
+public import Std.Internal.Http.Internal.String
+public import Std.Internal.Http.Internal.Char
+
+/-!
+# HTTP Internal Utilities
+
+This module re-exports internal utilities used by the HTTP library including
+data structures, encoding functions, and buffer management.
+-/

src/Std/Internal/Http/Internal/Encode.lean

@@ -6,8 +6,8 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Http.Internal.ChunkedBuffer
-public import Std.Http.Data.Version
+public import Std.Internal.Http.Internal.ChunkedBuffer
+public import Std.Internal.Http.Data.Version
 
 public section
 

src/Std/Internal/Http/Internal/String.lean

@@ -8,7 +8,7 @@ module
 prelude
 import Init.Grind
 public import Init.Data.String.TakeDrop
-public import Std.Http.Internal.Char
+public import Std.Internal.Http.Internal.Char
 
 public section
 

src/Std/Internal/Http/Protocol/H1.lean

@@ -8,14 +8,14 @@ module
 prelude
 public import Std.Time
 public import Init.Data.Array
-public import Std.Http.Data
-public import Std.Http.Internal
-public import Std.Http.Protocol.H1.Parser
-public import Std.Http.Protocol.H1.Config
-public import Std.Http.Protocol.H1.Message
-public import Std.Http.Protocol.H1.Reader
-public import Std.Http.Protocol.H1.Writer
-public import Std.Http.Protocol.H1.Event
+public import Std.Internal.Http.Data
+public import Std.Internal.Http.Internal
+public import Std.Internal.Http.Protocol.H1.Parser
+public import Std.Internal.Http.Protocol.H1.Config
+public import Std.Internal.Http.Protocol.H1.Message
+public import Std.Internal.Http.Protocol.H1.Reader
+public import Std.Internal.Http.Protocol.H1.Writer
+public import Std.Internal.Http.Protocol.H1.Event
 
 public section
 

src/Std/Internal/Http/Protocol/H1/Config.lean

@@ -6,8 +6,8 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Http.Data
-public import Std.Http.Internal
+public import Std.Internal.Http.Data
+public import Std.Internal.Http.Internal
 
 public section
 

src/Std/Internal/Http/Protocol/H1/Error.lean

@@ -7,11 +7,11 @@ module
 
 prelude
 public import Std.Time
-public import Std.Http.Data
-public import Std.Http.Internal
-public import Std.Http.Protocol.H1.Parser
-public import Std.Http.Protocol.H1.Config
-public import Std.Http.Protocol.H1.Message
+public import Std.Internal.Http.Data
+public import Std.Internal.Http.Internal
+public import Std.Internal.Http.Protocol.H1.Parser
+public import Std.Internal.Http.Protocol.H1.Config
+public import Std.Internal.Http.Protocol.H1.Message
 
 public section
 

src/Std/Internal/Http/Protocol/H1/Event.lean

@@ -7,12 +7,12 @@ module
 
 prelude
 public import Std.Time
-public import Std.Http.Data
-public import Std.Http.Internal
-public import Std.Http.Protocol.H1.Parser
-public import Std.Http.Protocol.H1.Config
-public import Std.Http.Protocol.H1.Message
-public import Std.Http.Protocol.H1.Error
+public import Std.Internal.Http.Data
+public import Std.Internal.Http.Internal
+public import Std.Internal.Http.Protocol.H1.Parser
+public import Std.Internal.Http.Protocol.H1.Config
+public import Std.Internal.Http.Protocol.H1.Message
+public import Std.Internal.Http.Protocol.H1.Error
 
 public section
 

src/Std/Internal/Http/Protocol/H1/Message.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 import Init.Data.Array
-public import Std.Http.Data
+public import Std.Internal.Http.Data
 
 public section
 

src/Std/Internal/Http/Protocol/H1/Parser.lean

@@ -7,9 +7,9 @@ module
 
 prelude
 public import Std.Internal.Parsec
-public import Std.Http.Data
+public import Std.Internal.Http.Data
 public import Std.Internal.Parsec.ByteArray
-public import Std.Http.Protocol.H1.Config
+public import Std.Internal.Http.Protocol.H1.Config
 
 /-!
 This module defines parsers for HTTP/1.1 request and response lines, headers, and body framing. The

src/Std/Internal/Http/Protocol/H1/Reader.lean

@@ -7,12 +7,12 @@ module
 
 prelude
 public import Std.Time
-public import Std.Http.Data
-public import Std.Http.Internal
-public import Std.Http.Protocol.H1.Parser
-public import Std.Http.Protocol.H1.Config
-public import Std.Http.Protocol.H1.Message
-public import Std.Http.Protocol.H1.Error
+public import Std.Internal.Http.Data
+public import Std.Internal.Http.Internal
+public import Std.Internal.Http.Protocol.H1.Parser
+public import Std.Internal.Http.Protocol.H1.Config
+public import Std.Internal.Http.Protocol.H1.Message
+public import Std.Internal.Http.Protocol.H1.Error
 
 public section
 

src/Std/Internal/Http/Protocol/H1/Writer.lean

@@ -7,12 +7,12 @@ module
 
 prelude
 public import Std.Time
-public import Std.Http.Data
-public import Std.Http.Internal
-public import Std.Http.Protocol.H1.Parser
-public import Std.Http.Protocol.H1.Config
-public import Std.Http.Protocol.H1.Message
-public import Std.Http.Protocol.H1.Error
+public import Std.Internal.Http.Data
+public import Std.Internal.Http.Internal
+public import Std.Internal.Http.Protocol.H1.Parser
+public import Std.Internal.Http.Protocol.H1.Config
+public import Std.Internal.Http.Protocol.H1.Message
+public import Std.Internal.Http.Protocol.H1.Error
 
 public section
 

src/Std/Internal/Http/Server.lean

@@ -6,13 +6,13 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Async
-public import Std.Async.TCP
+public import Std.Internal.Async
+public import Std.Internal.Async.TCP
 public import Std.Sync.CancellationToken
 public import Std.Sync.Semaphore
-public import Std.Http.Server.Config
-public import Std.Http.Server.Handler
-public import Std.Http.Server.Connection
+public import Std.Internal.Http.Server.Config
+public import Std.Internal.Http.Server.Handler
+public import Std.Internal.Http.Server.Connection
 
 public section
 
@@ -30,7 +30,7 @@ promise once all connections have closed.
 -/
 
 namespace Std.Http
-open Std.Async TCP
+open Std.Internal.IO.Async TCP
 
 set_option linter.all true
 

src/Std/Internal/Http/Server/Config.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Std.Time
-public import Std.Http.Protocol.H1
+public import Std.Internal.Http.Protocol.H1
 
 public section
 

src/Std/Internal/Http/Server/Connection.lean

@@ -6,12 +6,12 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Async.TCP
-public import Std.Async.ContextAsync
-public import Std.Http.Transport
-public import Std.Http.Protocol.H1
-public import Std.Http.Server.Config
-public import Std.Http.Server.Handler
+public import Std.Internal.Async.TCP
+public import Std.Internal.Async.ContextAsync
+public import Std.Internal.Http.Transport
+public import Std.Internal.Http.Protocol.H1
+public import Std.Internal.Http.Server.Config
+public import Std.Internal.Http.Server.Handler
 
 public section
 
@@ -19,7 +19,7 @@ namespace Std
 namespace Http
 namespace Server
 
-open Std Async TCP Protocol
+open Std Internal IO Async TCP Protocol
 open Time
 
 /-!
@@ -73,7 +73,7 @@ private inductive Recv (β : Type)
   | bytes (x : Option ByteArray)
   | responseBody (x : Option Chunk)
   | bodyInterest (x : Bool)
-  | response (x : (Except IO.Error (Response β)))
+  | response (x : (Except Error (Response β)))
   | timeout
   | shutdown
   | close
@@ -85,7 +85,7 @@ Each `Option` field is `none` when that source is not currently active.
 private structure PollSources (α β : Type) where
   socket : Option α
   expect : Option Nat
-  response : Option (Std.Channel (Except IO.Error (Response β)))
+  response : Option (Std.Channel (Except Error (Response β)))
   responseBody : Option β
   requestBody : Option Body.Stream
   timeout : Millisecond.Offset
@@ -214,7 +214,7 @@ private structure ConnectionState (β : Type) where
   keepAliveTimeout : Option Millisecond.Offset
   currentTimeout : Millisecond.Offset
   headerTimeout : Option Timestamp
-  response : Std.Channel (Except IO.Error (Response β))
+  response : Std.Channel (Except Error (Response β))
   respStream : Option β
   requiresData : Bool
   expectData : Option Nat

src/Std/Internal/Http/Server/Handler.lean

@@ -6,15 +6,15 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Async
-public import Std.Http.Data
-public import Std.Async.ContextAsync
+public import Std.Internal.Async
+public import Std.Internal.Http.Data
+public import Std.Internal.Async.ContextAsync
 
 public section
 
 namespace Std.Http.Server
 
-open Std.Async
+open Std.Internal.IO.Async
 
 set_option linter.all true
 

src/Std/Internal/Http/Test/Helpers.lean

@@ -6,14 +6,14 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Http.Server
-public import Std.Async
-public import Std.Async.Timer
+public import Std.Internal.Http.Server
+public import Std.Internal.Async
+public import Std.Internal.Async.Timer
 import Init.Data.String.Legacy
 
 public section
 
-open Std.Async
+open Std.Internal.IO Async
 open Std Http
 
 namespace Std.Http.Internal.Test

src/Std/Internal/Http/Transport.lean

@@ -6,7 +6,7 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Http.Protocol.H1
+public import Std.Internal.Http.Protocol.H1
 
 public section
 
@@ -18,7 +18,7 @@ that can be used with an HTTP connection.
 -/
 
 namespace Std.Http
-open Std Async TCP
+open Std Internal IO Async TCP
 
 set_option linter.all true
 
@@ -56,7 +56,7 @@ instance : Transport Socket.Client where
 
 namespace Internal
 
-open Async in
+open Internal.IO.Async in
 
 /--
 Shared state for a bidirectional mock connection.

src/Std/Sync/Broadcast.lean

@@ -10,14 +10,14 @@ public import Std.Data
 public import Init.Data.Queue
 public import Init.Data.Vector
 public import Std.Sync.Mutex
-public import Std.Async.IO
+public import Std.Internal.Async.IO
 
 public section
 
 namespace Std
 
-open Std.Async.IO
-open Std.Async
+open Std.Internal.Async.IO
+open Std.Internal.IO.Async
 
 /-!
 The `Std.Sync.Broadcast` module implements a broadcasting primitive for sending values
@@ -60,7 +60,7 @@ instance instMonadLiftBroadcastIO : MonadLift (EIO Broadcast.Error) IO where
 
 private structure Broadcast.Consumer (α : Type) where
   promise : IO.Promise Bool
-  waiter : Option (Async.Waiter (Option α))
+  waiter : Option (Internal.IO.Async.Waiter (Option α))
 
 private def Broadcast.Consumer.resolve (c : Broadcast.Consumer α) (b : Bool) : BaseIO Unit :=
   c.promise.resolve b
@@ -403,7 +403,7 @@ private def recvReady'
     let slotVal ← slot.get
     return slotVal.pos = next
 
-open Async in
+open Internal.IO.Async in
 private partial def recvSelector (ch : Bounded.Receiver α) : Selector (Option α) where
   tryFn := do
     ch.state.atomically do
@@ -537,7 +537,7 @@ the next available message. This will block until a message is available.
 def recv [Inhabited α] (ch : Broadcast.Receiver α) : BaseIO (Task (Option α)) := do
   Std.Bounded.Receiver.recv ch.inner
 
-open Async in
+open Internal.IO.Async in
 
 /--
 Creates a `Selector` that resolves once the broadcast channel `ch` has data available and provides that data.
@@ -567,7 +567,7 @@ instance [Inhabited α] : AsyncStream (Broadcast.Receiver α) (Option α) where
   stop channel := channel.unsubscribe
 
 instance [Inhabited α] : AsyncRead (Broadcast.Receiver α) (Option α) where
-  read receiver := Async.ofIOTask receiver.recv
+  read receiver := Internal.IO.Async.Async.ofIOTask receiver.recv
 
 instance [Inhabited α] : AsyncWrite (Broadcast α) α where
   write receiver x := do

src/Std/Sync/CancellationContext.lean

@@ -17,7 +17,7 @@ automatically cancels all child contexts.
 -/
 
 namespace Std
-open Std.Async
+open Std.Internal.IO.Async
 
 structure CancellationContext.State where
   /--

src/Std/Sync/CancellationToken.lean

@@ -9,7 +9,7 @@ prelude
 public import Std.Data
 public import Init.Data.Queue
 public import Std.Sync.Mutex
-public import Std.Async.Select
+public import Std.Internal.Async.Select
 public import Init.Data.ToString.Macro
 
 public section
@@ -22,7 +22,7 @@ that a cancellation has occurred.
 -/
 
 namespace Std
-open Std.Async
+open Std.Internal.IO.Async
 
 /--
 Reasons for cancellation.

src/Std/Sync/Channel.lean

@@ -8,15 +8,15 @@ module
 prelude
 public import Init.Data.Queue
 public import Std.Sync.Mutex
-public import Std.Async.IO
+public import Std.Internal.Async.IO
 import Init.Data.Vector.Basic
 import Init.Data.Option.BasicAux
 import Init.Omega
 
 public section
 
-open Std.Async.IO
-open Std.Async
+open Std.Internal.Async.IO
+open Std.Internal.IO.Async
 
 /-!
 This module contains the implementation of `Std.Channel`. `Std.Channel` is a multi-producer
@@ -53,7 +53,7 @@ instance : ToString Error where
 instance : MonadLift (EIO Error) IO where
   monadLift x := EIO.toIO (.userError <| toString ·) x
 
-open Async in
+open Internal.IO.Async in
 private inductive Consumer (α : Type) where
   | normal (promise : IO.Promise (Option α))
   | select (finished : Waiter (Option α))
@@ -174,7 +174,7 @@ private def recvReady' [Monad m] [MonadLiftT (ST IO.RealWorld) m] :
   let st ← get
   return !st.values.isEmpty || st.closed
 
-open Async in
+open Internal.IO.Async in
 private def recvSelector (ch : Unbounded α) : Selector (Option α) where
   tryFn := do
     ch.state.atomically do
@@ -324,7 +324,7 @@ private def recvReady' [Monad m] [MonadLiftT (ST IO.RealWorld) m] :
   let st ← get
   return !st.producers.isEmpty || st.closed
 
-open Async in
+open Internal.IO.Async in
 private def recvSelector (ch : Zero α) : Selector (Option α) where
   tryFn := do
     ch.state.atomically do
@@ -358,7 +358,7 @@ private def recvSelector (ch : Zero α) : Selector (Option α) where
 
 end Zero
 
-open Async in
+open Internal.IO.Async in
 private structure Bounded.Consumer (α : Type) where
   promise : IO.Promise Bool
   waiter : Option (Waiter (Option α))
@@ -560,7 +560,7 @@ private def recvReady' [Monad m] [MonadLiftT (ST IO.RealWorld) m] :
   let st ← get
   return st.bufCount != 0 || st.closed
 
-open Async in
+open Internal.IO.Async in
 private partial def recvSelector (ch : Bounded α) : Selector (Option α) where
   tryFn := do
     ch.state.atomically do
@@ -734,7 +734,7 @@ def recv (ch : CloseableChannel α) : BaseIO (Task (Option α)) :=
   | .zero ch => CloseableChannel.Zero.recv ch
   | .bounded ch => CloseableChannel.Bounded.recv ch
 
-open Async in
+open Internal.IO.Async in
 /--
 Creates a `Selector` that resolves once `ch` has data available and provides that data.
 In particular if `ch` is closed while waiting on this `Selector` and no data is available already
@@ -761,7 +761,7 @@ instance [Inhabited α] : AsyncStream (CloseableChannel α) (Option α) where
   next channel := channel.recvSelector
 
 instance [Inhabited α] : AsyncRead (CloseableChannel α) (Option α) where
-  read receiver := Async.ofIOTask receiver.recv
+  read receiver := Internal.IO.Async.Async.ofIOTask receiver.recv
 
 instance [Inhabited α] : AsyncWrite (CloseableChannel α) α where
   write receiver x := do
@@ -879,7 +879,7 @@ def recv [Inhabited α] (ch : Channel α) : BaseIO (Task α) := do
       | some val => return .pure val
       | none => unreachable!
 
-open Async in
+open Internal.IO.Async in
 /--
 Creates a `Selector` that resolves once `ch` has data available and provides that data.
 -/
@@ -911,7 +911,7 @@ instance [Inhabited α] : AsyncStream (Channel α) α where
   next channel := channel.recvSelector
 
 instance [Inhabited α] : AsyncRead (Channel α) α where
-  read receiver := Async.ofIOTask receiver.recv
+  read receiver := Internal.IO.Async.Async.ofIOTask receiver.recv
 
 instance [Inhabited α] : AsyncWrite (Channel α) α where
   write receiver x := do

src/Std/Sync/Notify.lean

@@ -8,7 +8,7 @@ module
 prelude
 public import Init.Data.Queue
 public import Std.Sync.Mutex
-public import Std.Async.Select
+public import Std.Internal.Async.Select
 
 public section
 
@@ -24,7 +24,7 @@ will be woken up per notification.
 -/
 
 namespace Std
-open Std.Async
+open Std.Internal.IO.Async
 
 inductive Notify.Consumer (α : Type) where
   | normal (promise : IO.Promise α)

src/Std/Sync/StreamMap.lean

@@ -8,12 +8,12 @@ module
 prelude
 public import Std.Data
 public import Init.Data.Queue
-public import Std.Async.IO
+public import Std.Internal.Async.IO
 
 public section
 
-open Std.Async.IO
-open Std.Async
+open Std.Internal.Async.IO
+open Std.Internal.IO.Async
 
 /-!
 This module provides `StreamMap`, a container that maps keys to async streams.

tests/elab/async.lean

@@ -1,9 +1,9 @@
-import Std.Async
+import Std.Internal.Async
 import Std.Internal.UV
 import Std.Net.Addr
 
-open Std.Async.UDP
-open Std.Async
+open Std.Internal.IO.Async.UDP
+open Std.Internal.IO.Async
 open Std.Net
 
 def t : IO (Async Nat) := do

tests/elab/async_base_functions.lean

@@ -1,9 +1,9 @@
-import Std.Async
+import Std.Internal.Async
 import Std.Sync.Mutex
 
 open Std
 
-open Std.Async
+open Std.Internal.IO.Async
 
 def wait (ms : UInt32) (ref : Std.Mutex Nat) (val : Nat) : Async Unit := do
   ref.atomically (·.modify (· * val))

tests/elab/async_cancellation.lean

@@ -1,7 +1,7 @@
-import Std.Async
+import Std.Internal.Async
 import Std.Sync
 
-open Std Async
+open Std.Internal.IO Async
 
 def cancellableSelector [Monad m] [MonadLift IO m] [MonadAsync AsyncTask m] (fn : Std.CancellationToken → m α) : m (Selector (Except IO.Error α)) := do
   let signal ← Std.CancellationToken.new

tests/elab/async_cancellation_reasons.lean

@@ -1,7 +1,7 @@
-import Std.Async
+import Std.Internal.Async
 import Std.Sync
 
-open Std Async
+open Std.Internal.IO Async
 
 -- Test basic cancellation with default reason
 def testBasicCancellationWithReason : Async Unit := do

tests/elab/async_dns.lean

@@ -1,8 +1,8 @@
-import Std.Async
+import Std.Internal.Async
 import Std.Internal.UV
 import Std.Net.Addr
 
-open Std.Async
+open Std.Internal.IO Async
 open Std.Net
 
 open Std.Net

tests/elab/async_http_body.lean

@@ -1,6 +1,6 @@
-import Std.Http.Data.Body
+import Std.Internal.Http.Data.Body
 
-open Std.Async
+open Std.Internal.IO Async
 open Std.Http
 open Std.Http.Body
 

tests/elab/async_http_body_framing.lean

@@ -1,6 +1,6 @@
-import Std.Http.Test.Helpers
+import Std.Internal.Http.Test.Helpers
 
-open Std.Async
+open Std.Internal.IO Async
 open Std Http Internal Test
 
 -- RFC 9112 §6: Transfer-Encoding and Content-Length framing

tests/elab/async_http_dispatch.lean

@@ -1,6 +1,6 @@
-import Std.Http.Test.Helpers
+import Std.Internal.Http.Test.Helpers
 
-open Std.Async
+open Std.Internal.IO Async
 open Std Http Internal Test
 
 -- Basic method dispatch and streaming responses

tests/elab/async_http_encode.lean

@@ -1,6 +1,6 @@
-import Std.Http.Data.Chunk
-import Std.Http.Data.Request
-import Std.Http.Data.Response
+import Std.Internal.Http.Data.Chunk
+import Std.Internal.Http.Data.Request
+import Std.Internal.Http.Data.Response
 
 open Std.Http
 open Std.Http.Internal

tests/elab/async_http_expect.lean

@@ -1,6 +1,6 @@
-import Std.Http.Test.Helpers
+import Std.Internal.Http.Test.Helpers
 
-open Std.Async
+open Std.Internal.IO Async
 open Std Http Internal Test
 
 -- Handlers for Expect: 100-continue testing

tests/elab/async_http_fuzz.lean

@@ -1,8 +1,8 @@
-import Std.Http
-import Std.Async
-import Std.Async.Timer
+import Std.Internal.Http
+import Std.Internal.Async
+import Std.Internal.Async.Timer
 
-open Std.Async
+open Std.Internal.IO Async
 open Std Http Internal Test
 
 

tests/elab/async_http_fuzz_limits.lean

@@ -1,7 +1,7 @@
-import Std.Http
-import Std.Async
+import Std.Internal.Http
+import Std.Internal.Async
 
-open Std.Async
+open Std.Internal.IO Async
 open Std Http Internal Test
 
 /-!

tests/elab/async_http_fuzz_random.lean

@@ -1,7 +1,7 @@
-import Std.Http
-import Std.Async
+import Std.Internal.Http
+import Std.Internal.Async
 
-open Std.Async
+open Std.Internal.IO Async
 open Std Http Internal Test
 
 /-!

tests/elab/async_http_h1_incremental.lean

@@ -1,4 +1,4 @@
-import Std.Http
+import Std.Internal.Http
 
 open Std Http
 open Std.Http.Protocol.H1

tests/elab/async_http_h1_parser_fuzz.lean

@@ -1,5 +1,5 @@
-import Std.Http
-import Std.Http.Protocol.H1.Parser
+import Std.Internal.Http
+import Std.Internal.Http.Protocol.H1.Parser
 
 open Std Internal Parsec ByteArray
 open Std.Http.Protocol.H1

tests/elab/async_http_h1_rfc_compliance.lean

@@ -1,4 +1,4 @@
-import Std.Http
+import Std.Internal.Http
 
 open Std Http
 open Std.Http.Internal.Test

tests/elab/async_http_hang_regressions.lean

@@ -1,8 +1,8 @@
-import Std.Http
-import Std.Async
-import Std.Async.Timer
+import Std.Internal.Http
+import Std.Internal.Async
+import Std.Internal.Async.Timer
 
-open Std.Async
+open Std.Internal.IO Async
 open Std Http Internal Test
 
 def runWithTimeout {α : Type} (name : String) (timeoutMs : Nat := 2000) (action : IO α) : IO α := do

tests/elab/async_http_headers.lean

@@ -1,5 +1,5 @@
-import Std.Http.Data.Headers
-import Std.Http.Protocol.H1
+import Std.Internal.Http.Data.Headers
+import Std.Internal.Http.Protocol.H1
 
 open Std.Http
 open Std.Http.Header

tests/elab/async_http_keepalive.lean

@@ -1,6 +1,6 @@
-import Std.Http.Test.Helpers
+import Std.Internal.Http.Test.Helpers
 
-open Std.Async
+open Std.Internal.IO Async
 open Std Http Internal Test
 
 -- Helper: run pipelined raw request string, closing the client after send.

tests/elab/async_http_request_headers.lean

@@ -1,6 +1,6 @@
-import Std.Http.Test.Helpers
+import Std.Internal.Http.Test.Helpers
 
-open Std.Async
+open Std.Internal.IO Async
 open Std Http Internal Test
 
 -- Shared fixtures

tests/elab/async_http_request_line.lean

@@ -1,6 +1,6 @@
-import Std.Http.Test.Helpers
+import Std.Internal.Http.Test.Helpers
 
-open Std.Async
+open Std.Internal.IO Async
 open Std Http Internal Test
 
 -- Shared fixtures

tests/elab/async_http_response_framing.lean

@@ -1,6 +1,6 @@
-import Std.Http.Test.Helpers
+import Std.Internal.Http.Test.Helpers
 
-open Std.Async
+open Std.Internal.IO Async
 open Std Http Internal Test
 
 -- Shared fixtures

tests/elab/async_http_string_quoting.lean

@@ -1,5 +1,5 @@
-import Std.Http.Internal.String
-import Std.Http.Internal.Char
+import Std.Internal.Http.Internal.String
+import Std.Internal.Http.Internal.Char
 
 open Std.Http.Internal
 

tests/elab/async_http_trailers.lean

@@ -1,7 +1,7 @@
-import Std.Http
-import Std.Async
+import Std.Internal.Http
+import Std.Internal.Async
 
-open Std.Async
+open Std.Internal.IO Async
 open Std Http Internal Test
 open Std.Http.Internal
 

tests/elab/async_http_uri.lean

@@ -3,8 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sofia Rodrigues
 -/
-import Std.Http.Data.URI
-import Std.Http.Data.URI.Encoding
+import Std.Internal.Http.Data.URI
+import Std.Internal.Http.Data.URI.Encoding
 
 open Std.Http
 open Std.Http.URI

tests/elab/async_select_channel.lean

@@ -1,6 +1,6 @@
 import Std.Sync.Channel
 
-open Std Async
+open Std Internal IO Async
 
 namespace A
 

tests/elab/async_select_gate.lean

@@ -1,7 +1,7 @@
-import Std.Async.Select
+import Std.Internal.Async.Select
 import Std.Sync.Channel
 
-open Std Async
+open Std Internal IO Async
 
 /-!
 Tests for the `gate` in `Selectable.one`.

tests/elab/async_select_socket.lean

@@ -1,10 +1,10 @@
-import Std.Async.Timer
-import Std.Async.TCP
-import Std.Async.UDP
+import Std.Internal.Async.Timer
+import Std.Internal.Async.TCP
+import Std.Internal.Async.UDP
 
 #exit -- TODO: remove `#exit` after nondet issue is resolved.
 
-open Std Async
+open Std Internal IO Async
 
 namespace TCP
 

tests/elab/async_select_timer.lean

@@ -1,6 +1,6 @@
-import Std.Async.Timer
+import Std.Internal.Async.Timer
 
-open Std Async
+open Std Internal IO Async
 
 def test1 : Async Nat := do
   let s1 ← Sleep.mk 1000