Skip to content

feat: introduce HTTP/1.1 server#12151

Open
algebraic-dev wants to merge 131 commits intosofia/async-http-h1from
sofia/async-http-server
Open

feat: introduce HTTP/1.1 server#12151
algebraic-dev wants to merge 131 commits intosofia/async-http-h1from
sofia/async-http-server

Conversation

@algebraic-dev
Copy link
Member

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

This PR introduces the Server module, an Async HTTP/1.1 server.

This contains the same code as #10478, divided into separate pieces to facilitate easier review.

The pieces of this feature are:

@ghost
Copy link

ghost commented Jan 25, 2026

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0a0323734b2d10c3f9355659f8e44b67bd36f644 --onto 4c1e4a77b4952098ea043f9b8c2d155c20b24523. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-25 08:06:00)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Jan 25, 2026

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 0a0323734b2d10c3f9355659f8e44b67bd36f644 --onto e9a1c9ef63d8e53803c16077f03e2dacd4a890bd. You can force reference manual CI using the force-manual-ci label. (2026-01-25 08:06:02)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 0a0323734b2d10c3f9355659f8e44b67bd36f644 --onto 75d7f7eb227bc54dc6ea3d8ead090ee4180debaf. You can force reference manual CI using the force-manual-ci label. (2026-02-10 02:30:17)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase a6ba7312cc7c8a95b258353325d34ff36b24babe --onto 03dc334f73259e1bae0b8f2b80a39a82e1de3df6. You can force reference manual CI using the force-manual-ci label. (2026-02-11 23:57:02)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase a6ba7312cc7c8a95b258353325d34ff36b24babe --onto 9da8f5dce42832b8411d58446653f3640a94a6e3. You can force reference manual CI using the force-manual-ci label. (2026-02-14 10:06:17)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase a6ba7312cc7c8a95b258353325d34ff36b24babe --onto 5c7a508e21c5ebc710b0dfe65648d5beba4e34e0. You can force reference manual CI using the force-manual-ci label. (2026-02-18 14:20:58)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase a6ba7312cc7c8a95b258353325d34ff36b24babe --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-20 22:26:08)

@algebraic-dev algebraic-dev force-pushed the sofia/async-http-server branch from 740a68a to bc21289 Compare January 25, 2026 15:49
@milessabin
Copy link

One thing I think that's missing is the ability to get the remote address of clients (ie. getPeerName on accepted connections).

@mathlib-lean-pr-testing
Copy link

mathlib-lean-pr-testing bot commented Feb 10, 2026

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0a0323734b2d10c3f9355659f8e44b67bd36f644 --onto 39c26fce1da321b24eaf949d0d7d028ba589e4e1. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-10 02:30:15)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a6ba7312cc7c8a95b258353325d34ff36b24babe --onto 4cdc199f772977113bd6c1bf87a6c02b78d5c4d3. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-11 23:57:00)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a6ba7312cc7c8a95b258353325d34ff36b24babe --onto 6ca23a7b8bee57152110ce500ce795148707d4ed. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-13 14:50:38)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a6ba7312cc7c8a95b258353325d34ff36b24babe --onto 91bd6e19a7b7aca769f9720e1127c768df0cd2a7. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-18 14:20:55)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a6ba7312cc7c8a95b258353325d34ff36b24babe --onto 309f44d00757482e1c5a2b2427fdca818a24615a. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-19 21:56:25)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a6ba7312cc7c8a95b258353325d34ff36b24babe --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-21 02:21:18)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a6ba7312cc7c8a95b258353325d34ff36b24babe --onto ed0fd1e933239beaa7aaa12598f961c260062ab6. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-24 23:16:02)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a6ba7312cc7c8a95b258353325d34ff36b24babe --onto c595413fccaa47ebdc399d9b817c17425687fc26. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-25 03:13:02)

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