feat: add HTTP client connection by algebraic-dev · Pull Request #14547 · leanprover/lean4

algebraic-dev · 2026-07-25T12:23:06Z

This PR adds a Connection module that bridges the async runtime with the H1 state machine with with a Session structure that manages the lifecycle of a single Connection handling both outgoing requests and incoming responses.

Foundation: feat: add HTTP client foundation and configuration #14546
Connection: feat: add HTTP client connection #14547
Agent: feat: add HTTP client #14548

…ia/async-http-client-config

mathlib-lean-pr-testing · 2026-07-27T14:51:08Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6832de296014011d0f126e3fa32a8366b5299b35 --onto 0bfc3acaef4ed0576307a77fbaa0c6e1a5dca402. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-27 14:51:07)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6832de296014011d0f126e3fa32a8366b5299b35 --onto 110db9cb751afaee8b2ac344887d6c7e632f77b4. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-04 13:16:47)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6832de296014011d0f126e3fa32a8366b5299b35 --onto 945e78b86645b179655123cd2fdba83d89d28d07. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-04 20:36:46)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6832de296014011d0f126e3fa32a8366b5299b35 --onto f2bcf2e8660ab2d16cf3cb50c8e127de0439a337. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-05 16:31:14)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6832de296014011d0f126e3fa32a8366b5299b35 --onto bd97ed8e35639e17a11d1490cbc46d994e7b4513. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-07 16:43:41)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 174754bba9943a578ce980d59a0f5e7f05749182 --onto 4620e4d946957ae7c582764c79eb93cc779f77e2. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-25 21:21:21)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 174754bba9943a578ce980d59a0f5e7f05749182 --onto 138ca9f20763523c4093baa092cf371e89535098. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-31 20:23:54)

leanprover-bot · 2026-07-27T14:51:09Z

Reference manual CI status:

❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 6832de296014011d0f126e3fa32a8366b5299b35 --onto 0bfc3acaef4ed0576307a77fbaa0c6e1a5dca402. You can force reference manual CI using the force-manual-ci label. (2026-07-27 14:51:09)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 6832de296014011d0f126e3fa32a8366b5299b35 --onto 23393b959b33e3a8d15796b2397f8a04c315b9f4. You can force reference manual CI using the force-manual-ci label. (2026-08-04 13:16:48)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 6832de296014011d0f126e3fa32a8366b5299b35 --onto c4e6b62c3d955ef20da94310797072f7c4c5fa2b. You can force reference manual CI using the force-manual-ci label. (2026-08-07 16:43:44)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 174754bba9943a578ce980d59a0f5e7f05749182 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force reference manual CI using the force-manual-ci label. (2026-08-25 21:21:22)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 174754bba9943a578ce980d59a0f5e7f05749182 --onto e991a05e359a25988f49bff3ab8af986e959b866. You can force reference manual CI using the force-manual-ci label. (2026-08-31 20:23:56)

TwoFX

Just some preliminary comments, I will have to read through the logic in more detail in August.

TwoFX

Two more issues discovered by Codex, which seem legit to me:

module

import Std.Http.Test.Helpers

/-!
Regression tests for HTTP client connection lifecycle failures found while reviewing #14547,
involving response backpressure, request-body producer errors, and graceful retirement with queued
requests.
-/

open Std.Async
open Std Http Internal
open Std.Http.Client
open Std.Http.Internal.Test.ClientHelpers

namespace ClientConnectionLifecycleTests

private def mkRequest (path : String)
    (body : Body.Any := Body.Any.ofBody ({} : Body.Empty)) : Request Body.Any :=
  { (Request.new |>.method .post |>.uri! path |>.header! "Host" "example.com").body body with }

private def sendInBackground (connection : Connection) (request : Request Body.Any) :
    Async (IO.Promise (Except Error (Response Body.Stream × IO.Promise (Except Error Unit)))) := do
  let promise ← IO.Promise.new
  background do
    promise.resolve (← connection.sendTracked request)
  pure promise

private def expectResponse
    (promise : IO.Promise (Except Error (Response Body.Stream × IO.Promise (Except Error Unit)))) :
    Async (Response Body.Stream × IO.Promise (Except Error Unit)) := do
  match ← await promise.result! with
  | .ok result => pure result
  | .error e => throw (IO.userError s!"expected a response, got {e}")

private def readHead (peer : Mock.Server) : Async String := do
  let mut bytes := ByteArray.empty
  repeat
    if (String.fromUTF8! bytes).contains "\r\n\r\n" then break
    let some chunk ← peer.recv?
      | throw (IO.userError "connection closed before the request head")
    bytes := bytes ++ chunk
  pure (String.fromUTF8! bytes)

private def errorConstructor : Error → String
  | .connect _ => ".connect"
  | .timeout => ".timeout"
  | .closed _ => ".closed"
  | .protocol _ => ".protocol"
  | .bodyLimitExceeded => ".bodyLimitExceeded"
  | .invalidRequest _ => ".invalidRequest"
  | .io _ => ".io"

/-!
The read timeout bounds waits for network data, not time spent waiting for the caller to consume
body bytes that have already arrived.
-/
#eval show IO _ from runWithTimeout "buffered response body survives readTimeout" 3000 <|
    Async.block do
  let (client, peer) ← Mock.new
  let connection ← Connection.new client
    ({ readTimeout := ⟨100, by decide⟩, requestTimeout := ⟨2000, by decide⟩,
       keepAliveTimeout := ⟨2000, by decide⟩ } : Client.Config)
  try
    let result ← sendInBackground connection (mkRequest "/buffered")
    discard <| readHead peer
    peer.send (rawResp "200 OK" #[("Content-Length", "2")] "ok")
    let (response, _) ← expectResponse result

    sleep 250

    let body : String ← response.body.readAll
    unless body == "ok" do
      throw (IO.userError s!"expected buffered body \"ok\", got {body.quote}")
  finally
    connection.close

/-!
An error raised by a request-body producer is an `.io` failure. It must not be collapsed into the
retryable `.closed` constructor merely because it arrives through a selector.
-/
#eval show IO _ from runWithTimeout "request body selector preserves producer error" 3000 <|
    Async.block do
  let (client, peer) ← Mock.new
  let connection ← Connection.new client
    ({ readTimeout := ⟨2000, by decide⟩, requestTimeout := ⟨2000, by decide⟩ } : Client.Config)
  try
    let stream ← Body.mkStream
    stream.setKnownSize (some (.fixed 1))
    let result ← sendInBackground connection
      (mkRequest "/body-error" (Body.Any.ofBody stream))
    discard <| readHead peer

    -- Let the connection register the request-body selector before failing the producer.
    sleep 50
    stream.closeWithError (IO.userError "producer failed")

    match ← await result.result! with
    | .error (.io _) => pure ()
    | .error e =>
      throw (IO.userError s!"expected .io, got {errorConstructor e}")
    | .ok _ =>
      throw (IO.userError "expected the request-body failure to reject the request")
  finally
    connection.close


end ClientConnectionLifecycleTests

TwoFX · 2026-08-13T09:28:47Z

+private inductive Recv
+  | bytes (x : Option ByteArray)
+  | requestBody (x : Option Chunk)
+  | bodyInterest (x : Bool)


Optional: this is a private type, so it's fine, but reviewing this would be easier if the variable names weren't all x :)

TwoFX · 2026-08-13T09:30:14Z

+-/
+private def stopAcceptingRequests (requestChannel : Std.CloseableChannel PendingRequest) :
+    IO Unit := do
+  try requestChannel.close catch _ => pure ()


This seems like it should be a proper tryClose function on CloseableChannel instead.

TwoFX · 2026-08-13T09:37:01Z

+A request queued to the background connection loop, paired with the promises that deliver its
+outcome.
+-/
+structure PendingRequest where


I think most of the material in this file should be considered internal implementation, but it is not marked as such.

TwoFX · 2026-08-13T09:41:54Z

+      selectables := selectables.push
+        (.case responseBody.interestSelector (pure <| .bodyInterest ·))
+
+  try Selectable.one selectables catch _ => pure .close


Do we just lose all error information here? Seems quite crude.

TwoFX · 2026-08-13T09:46:24Z

+  Transport.close socket
+
+/--
+Queues a request and awaits its response, together with a completion promise that


Does it really "await" the response?

TwoFX · 2026-08-13T09:47:16Z

+-/
+def sendTracked (connection : Connection) (request : Request Body.Any)
+    (requestOverrides : RequestOverrides := {}) :
+    Async (Except Error (Response Body.Stream × IO.Promise (Except Error Unit))) := do


This is a super complicated return type which needs to be simplified or at least explained in the docstring.

TwoFX · 2026-08-13T10:01:15Z

+
+/--
+Retires the connection without disturbing the exchange running on it: no further request is
+accepted, and the background loop shuts down once it next goes idle. `isClosed` reports `true`


This should clarify that pending requests are still handled, not just the currently in flight request.

…lient-connection

algebraic-dev added 2 commits July 24, 2026 13:19

feat: add http client config and base changes to the client

63bfcc0

revert: useless changes

25411ec

algebraic-dev self-assigned this Jul 25, 2026

algebraic-dev added the changelog-library Library label Jul 25, 2026

algebraic-dev requested a review from TwoFX as a code owner July 25, 2026 12:23

Merge branch 'master' of https://github.com/leanprover/lean4 into sof…

10db4c3

…ia/async-http-client-config

github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jul 27, 2026

This was referenced Jul 27, 2026

feat: add HTTP Client #13902

Closed

feat: add HTTP client foundation and configuration #14546

Open

feat: add HTTP client #14548

Open

feat: add HTTP client Pool #14549

Merged

TwoFX reviewed Jul 30, 2026

View reviewed changes

chore: small fixes

6ecb640

algebraic-dev changed the title ~~feat: add HTTP client connection and session~~ feat: add HTTP client connection Aug 4, 2026

algebraic-dev added 5 commits August 5, 2026 11:45

fix: eof on parser and base changes

936ce30

feat: connection and session

bbe034d

refactor: rename RequestPacket and merge Session and Connection

b372dfe

fix: bugs related to 100-Contineu

8eb2197

fix: close requestchannel when machine is closing

708dfa7

algebraic-dev force-pushed the sofia/async-http-client-connection branch from f06afea to 708dfa7 Compare August 5, 2026 14:59

algebraic-dev added 6 commits August 5, 2026 14:39

fix: simplify and make determinsitic

6596822

fix: TOCTOU in connection

83bf79c

fix: forced drain

21aab9d

fix: simplify

d2bc79a

fix: pull body

473aba2

fix: bugs related to URI

73b004d

TwoFX reviewed Aug 13, 2026

View reviewed changes

feat: add handlers

15f2c93

algebraic-dev added 4 commits August 25, 2026 11:21

feat: add authentication, cookie and proxy handlers

cd37397

Merge branch 'sofia/async-http-client-config' into sofia/async-http-c…

c7ea09a

…lient-connection

Merge branch 'sofia/async-http-client-config' into sofia/async-http-c…

a0fde0d

…lient-connection

fix: adapt connection to the new config

52a98a7

algebraic-dev added 2 commits August 26, 2026 01:45

fix: readTimeout bug

7d8351e

fix: remove public form leavesconnectionreusable

b9eeaf6

Uh oh!

Conversation

algebraic-dev commented Jul 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-lean-pr-testing Bot commented Jul 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Jul 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

TwoFX left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

TwoFX left a comment

Choose a reason for hiding this comment

Uh oh!

TwoFX Aug 13, 2026

Choose a reason for hiding this comment

Uh oh!

TwoFX Aug 13, 2026

Choose a reason for hiding this comment

Uh oh!

TwoFX Aug 13, 2026

Choose a reason for hiding this comment

Uh oh!

TwoFX Aug 13, 2026

Choose a reason for hiding this comment

Uh oh!

TwoFX Aug 13, 2026

Choose a reason for hiding this comment

Uh oh!

TwoFX Aug 13, 2026

Choose a reason for hiding this comment

Uh oh!

TwoFX Aug 13, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

algebraic-dev commented Jul 25, 2026 •

edited

Loading

mathlib-lean-pr-testing Bot commented Jul 27, 2026 •

edited

Loading

leanprover-bot commented Jul 27, 2026 •

edited

Loading