Skip to content

feat: add core HTTP data types#12126

Open
algebraic-dev wants to merge 39 commits intomasterfrom
sofia/async-http-data
Open

feat: add core HTTP data types#12126
algebraic-dev wants to merge 39 commits intomasterfrom
sofia/async-http-data

Conversation

@algebraic-dev
Copy link
Member

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

This PR introduces the core HTTP data types: Request, Response, Status, Version, and Method. Currently, URIs are represented as String and headers as HashMap String (Array String). These are placeholders, future PRs will replace them with strict implementations.

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 requested a review from TwoFX as a code owner January 23, 2026 20:19
@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 23, 2026
@ghost
Copy link

ghost commented Jan 23, 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-23 22:09:50)
  • ❗ 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 15:22:19)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Jan 23, 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-23 22:09:52)
  • ❗ 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:13:53)
  • ❗ 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:48:04)
  • ❗ 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 13:56:21)
  • ❗ 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:20)

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.

Looks mostly good with a couple of small improvements

algebraic-dev and others added 4 commits January 25, 2026 11:19
@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 a6ba7312cc7c8a95b258353325d34ff36b24babe --onto 4cdc199f772977113bd6c1bf87a6c02b78d5c4d3. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-10 21:13:51)
  • ❗ 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 15:48:03)
  • ❗ 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 13:56:18)
  • ❗ 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: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:18:19)
  • ❗ 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-26 00:57:55)

@ericlesaquiles
Copy link

I'm looking into using this for a project of mine (I just need simple http requesting, actually).
Is there something I could do to help with this PR (and the other related ones)?
Cheers

@algebraic-dev
Copy link
Member Author

@ericlesaquiles It’s almost at a stage where it will only need some adjustments, so I think taking a look at the code and checking if anything is missing or if anything is incorrect would be really helpful! :) If you need any guidance on the code, I can provide it.

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.

6 participants