Skip to content

feat: add HTTP client connection - #14547

Open
algebraic-dev wants to merge 10 commits into
sofia/async-http-client-configfrom
sofia/async-http-client-connection
Open

feat: add HTTP client connection#14547
algebraic-dev wants to merge 10 commits into
sofia/async-http-client-configfrom
sofia/async-http-client-connection

Conversation

@algebraic-dev

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

Copy link
Copy Markdown
Member

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.

@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:23
@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 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)

@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 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)

@TwoFX TwoFX left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Comment thread src/Std/Http/Test/Helpers.lean
Comment thread src/Std/Http/Client/Connection.lean Outdated
Comment thread src/Std/Http/Client/Connection.lean Outdated
Comment thread src/Std/Http/Client/Connection.lean Outdated
Comment thread src/Std/Http/Client/Session.lean Outdated
Comment thread src/Std/Http/Client/Connection.lean Outdated
@algebraic-dev algebraic-dev changed the title feat: add HTTP client connection and session feat: add HTTP client connection Aug 4, 2026
@algebraic-dev
algebraic-dev force-pushed the sofia/async-http-client-connection branch from f06afea to 708dfa7 Compare August 5, 2026 14:59
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.

4 participants