Skip to content

feat: add HTTP client - #14548

Open
algebraic-dev wants to merge 21 commits into
sofia/async-http-client-connectionfrom
sofia/async-http-client-agent
Open

feat: add HTTP client#14548
algebraic-dev wants to merge 21 commits into
sofia/async-http-client-connectionfrom
sofia/async-http-client-agent

Conversation

@algebraic-dev

@algebraic-dev algebraic-dev commented Jul 25, 2026

Copy link
Copy Markdown
Member

This PR adds an Client structure that provides a transport agnostic layer on top of a Connection that handles redirects.

@algebraic-dev algebraic-dev self-assigned this Jul 25, 2026
@algebraic-dev
algebraic-dev requested a review from TwoFX as a code owner July 25, 2026 12:27
@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 Jul 27, 2026
@mathlib-lean-pr-testing

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

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 6832de296014011d0f126e3fa32a8366b5299b35 --onto 0bfc3acaef4ed0576307a77fbaa0c6e1a5dca402. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-27 16:01:17)
  • ❗ 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 23:11:36)
  • ❗ 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:54:53)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6832de296014011d0f126e3fa32a8366b5299b35 --onto c4e6b62c3d955ef20da94310797072f7c4c5fa2b. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-06 15:47:34)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6832de296014011d0f126e3fa32a8366b5299b35 --onto 87e7204456bfca901bdc724c996030e13c2f80c6. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-08 13:37:26)

@leanprover-bot

leanprover-bot commented Jul 27, 2026

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 6832de296014011d0f126e3fa32a8366b5299b35 --onto 0bfc3acaef4ed0576307a77fbaa0c6e1a5dca402. You can force reference manual CI using the force-manual-ci label. (2026-07-27 16:01:19)
  • ❗ 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 23:11:37)
  • ❗ 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-06 15:47:35)

@algebraic-dev
algebraic-dev force-pushed the sofia/async-http-client-connection branch from f06afea to 708dfa7 Compare August 5, 2026 14:59
@algebraic-dev
algebraic-dev force-pushed the sofia/async-http-client-agent branch from 643e6b4 to f3674a7 Compare August 5, 2026 15:01
@algebraic-dev algebraic-dev changed the title feat: add HTTP client Agent feat: add HTTP client Aug 8, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

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

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants