Skip to content

feat: introduce Headers data type for HTTP#12127

Open
algebraic-dev wants to merge 60 commits intosofia/async-http-datafrom
sofia/async-http-headers
Open

feat: introduce Headers data type for HTTP#12127
algebraic-dev wants to merge 60 commits intosofia/async-http-datafrom
sofia/async-http-headers

Conversation

@algebraic-dev
Copy link
Member

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

This PR introduces the Headers data type, that provides a good and convenient abstraction for parsing, querying, and encoding HTTP/1.1 headers.

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

The pieces of this feature are:

@algebraic-dev algebraic-dev self-assigned this Jan 23, 2026
@algebraic-dev algebraic-dev changed the title feat: add HTTP Headers data type. feat: add HTTP Headers data type Jan 23, 2026
@algebraic-dev algebraic-dev changed the title feat: add HTTP Headers data type feat: introduce Headers data type for HTTP Jan 23, 2026
@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 Jan 24, 2026
@ghost
Copy link

ghost commented Jan 24, 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 57003e5c7962bd5db93fb51d4536969c3631c1db. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-24 02:11:59)
  • ❗ 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 00:38:33)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Jan 24, 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-24 02:12:00)
  • ❗ 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-10 21:16:15)
  • ❗ 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-13 15:53:29)
  • ❗ 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:17:56)
  • ❗ 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-24 23:18:33)

Copy link
Contributor

@Rob23oba Rob23oba left a comment

Choose a reason for hiding this comment

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

I'm a bit confused by the isEmpty decidable instance but otherwise some small improvements and comments

@algebraic-dev algebraic-dev force-pushed the sofia/async-http-headers branch from 9b737c6 to 6e26b90 Compare January 25, 2026 15:33
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