Skip to content

feat: add HTTP Client - #13902

Closed
algebraic-dev wants to merge 27 commits into
sofia/async-http-h1-head-framingfrom
sofia/async-http-client-impl
Closed

feat: add HTTP Client#13902
algebraic-dev wants to merge 27 commits into
sofia/async-http-h1-head-framingfrom
sofia/async-http-client-impl

Conversation

@algebraic-dev

@algebraic-dev algebraic-dev commented May 30, 2026

Copy link
Copy Markdown
Member

This PR adds a HTTP Client.

@algebraic-dev algebraic-dev self-assigned this May 30, 2026
@algebraic-dev
algebraic-dev requested a review from TwoFX as a code owner May 30, 2026 13:14
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label May 30, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented May 30, 2026 •
edited
Loading

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b5f7399bf19d623b3a5171732f1b3e617cfac38f --onto c47a0c7cf035381a2bcdd4cdf2442782eb4a5214. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-30 14:01:06)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b5f7399bf19d623b3a5171732f1b3e617cfac38f --onto 9e0092d0f0ef62de06235b67023f4b6621151116. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-05 16:14:17)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ab122a187d64224faf53004c9631f664b852bb96 --onto 659e8bb858995b0a1ada239c5b3819c8f8f2772f. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-15 22:19:41)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ab122a187d64224faf53004c9631f664b852bb96 --onto 4792cd22887c8b529a351f6563b693426ff2a8f8. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-18 10:45:11)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ab122a187d64224faf53004c9631f664b852bb96 --onto ab9722836dea9e2f5ca3157f14cc1460454b3a67. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-23 13:08:06)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ab122a187d64224faf53004c9631f664b852bb96 --onto 89d728b53ccfda77971b5381649d2bbe9eae2039. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-01 23:31:19)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ab122a187d64224faf53004c9631f664b852bb96 --onto e281ba87c2c967b1662ee28bd201046956d0494a. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-02 14:29:19)

@leanprover-bot

leanprover-bot commented May 30, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase b5f7399bf19d623b3a5171732f1b3e617cfac38f --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-05-30 14:01:07)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase ab122a187d64224faf53004c9631f664b852bb96 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-15 22:19:43)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase ab122a187d64224faf53004c9631f664b852bb96 --onto 89d728b53ccfda77971b5381649d2bbe9eae2039. You can force reference manual CI using the force-manual-ci label. (2026-07-01 23:31:21)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase ab122a187d64224faf53004c9631f664b852bb96 --onto e281ba87c2c967b1662ee28bd201046956d0494a. You can force reference manual CI using the force-manual-ci label. (2026-07-02 14:29:21)

@algebraic-dev
algebraic-dev changed the base branch from master to sofia/async-http-redirect-plan May 30, 2026 14:15
@algebraic-dev
algebraic-dev force-pushed the sofia/async-http-client-impl branch 2 times, most recently from 936c34f to 2ca949f Compare May 30, 2026 14:17
@algebraic-dev
algebraic-dev force-pushed the sofia/async-http-redirect-plan branch from dbd4cc6 to ee33e6e Compare June 5, 2026 13:52
@algebraic-dev
algebraic-dev force-pushed the sofia/async-http-client-impl branch from 67c3c73 to 87ad6ff Compare June 5, 2026 13:55
@algebraic-dev
algebraic-dev force-pushed the sofia/async-http-redirect-plan branch from ee33e6e to 03468f6 Compare June 5, 2026 14:00
@algebraic-dev
algebraic-dev force-pushed the sofia/async-http-client-impl branch 2 times, most recently from 511eebf to 47160c8 Compare June 5, 2026 14:35
@algebraic-dev
algebraic-dev force-pushed the sofia/async-http-redirect-plan branch from a42f923 to f8ecc1c Compare June 5, 2026 14:37
@algebraic-dev
algebraic-dev force-pushed the sofia/async-http-client-impl branch from 47160c8 to 5c7fbea Compare June 5, 2026 14:38
@algebraic-dev
algebraic-dev force-pushed the sofia/async-http-client-impl branch from 5c7fbea to ba2a8d2 Compare June 5, 2026 15:02
@algebraic-dev
algebraic-dev changed the base branch from sofia/async-http-redirect-plan to sofia/async-http-stream-close-error June 15, 2026 21:45
@algebraic-dev
algebraic-dev changed the base branch from sofia/async-http-stream-close-error to sofia/async-http-h1-head-framing June 16, 2026 00:25
algebraic-dev and others added 16 commits June 16, 2026 00:57
@algebraic-dev @claude
fix: align client pool defaults and dedupe Host header formatting
b34266e 
This PR aligns the `maxPerHost` struct default with `Client.builder` (both 4), removes the unreachable `lastErr` accumulator in the pool retry loop, and derives the default `Host` header through `URI.Origin.hostHeader` so the `host[:port]` formatting lives in one place.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@algebraic-dev @claude
fix: restore bodyless-response auto-drain lost in stream-close merge
404137c 
Re-applies the HEAD/204/304 auto-drain and HEAD body suppression that the
stream-close-error merge silently reverted, so bodyless responses complete
instead of stalling.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@algebraic-dev
Merge branch 'sofia/async-http-h1-head-framing' into sofia/async-http…
38af776 
…-client-impl
@algebraic-dev
Merge branch 'sofia/async-http-h1-head-framing' into sofia/async-http…
7eeb9a5 
…-client-impl
@algebraic-dev
Merge branch 'sofia/async-http-h1-head-framing' into sofia/async-http…
ac7ca5c 
…-client-impl
@algebraic-dev
Merge branch 'sofia/async-http-h1-head-framing' into sofia/async-http…
701db41 
…-client-impl
@algebraic-dev
refactor: remove pool feature, it now is really small
56ea0bd
@algebraic-dev
Merge branch 'sofia/async-http-h1-head-framing' into sofia/async-http…
a1d5e28 
…-client-impl
@algebraic-dev
Merge branch 'sofia/async-http-h1-head-framing' into sofia/async-http…
9bc0d28 
…-client-impl
@algebraic-dev
fix: reset?
48d00b2
@algebraic-dev
Merge branch 'sofia/async-http-h1-head-framing' into sofia/async-http…
53b3ef7 
…-client-impl
@algebraic-dev
fix: try/catch in tryrecv
a104058
@algebraic-dev
fix: cycle
84c2262
@algebraic-dev
fix: pool
77721ce
@algebraic-dev
test: split tests
1c0faef
@algebraic-dev
fix: add fast path
d94347b
@algebraic-dev

algebraic-dev commented Jul 27, 2026

Copy link
Copy Markdown
Member Author

Closed because I split it into multiple PRs (#14546, #14547, #14548, #14549).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@TwoFX TwoFX Awaiting requested review from TwoFX TwoFX is a code owner

Assignees

@algebraic-dev algebraic-dev

Labels

changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@algebraic-dev @leanprover-bot