Skip to content

feat: add type class for replayable body types - #13900

Merged
algebraic-dev merged 18 commits into
masterfrom
sofia/async-http-replayable-body
Jul 21, 2026
Merged

feat: add type class for replayable body types#13900
algebraic-dev merged 18 commits into
masterfrom
sofia/async-http-replayable-body

Conversation

@algebraic-dev

Copy link
Copy Markdown
Member

This PR adds a Replayable type class that is useful for checking if some Body can be replayed in a redirect request.

@algebraic-dev algebraic-dev self-assigned this May 30, 2026
@algebraic-dev
algebraic-dev requested a review from TwoFX as a code owner May 30, 2026 13:09
@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 May 30, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented May 30, 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 b5f7399bf19d623b3a5171732f1b3e617cfac38f --onto c47a0c7cf035381a2bcdd4cdf2442782eb4a5214. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-30 13:58:43)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b5f7399bf19d623b3a5171732f1b3e617cfac38f --onto 9e0092d0f0ef62de06235b67023f4b6621151116. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-05 14:39:28)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b5f7399bf19d623b3a5171732f1b3e617cfac38f --onto d2f48db30713019241520218d0965227bbb64eed. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-11 15:14:57)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ab122a187d64224faf53004c9631f664b852bb96 --onto 659e8bb858995b0a1ada239c5b3819c8f8f2772f. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-15 17:11:23)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ab122a187d64224faf53004c9631f664b852bb96 --onto 4792cd22887c8b529a351f6563b693426ff2a8f8. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-18 13:04:06)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ab122a187d64224faf53004c9631f664b852bb96 --onto ab9722836dea9e2f5ca3157f14cc1460454b3a67. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-23 12:56:48)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d5790c1f088236fe67b52500ff87bce2c848b0bb --onto 3259610687883ec1ea48c481aba2469f2f83facf. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-21 19:08:44)

@leanprover-bot

leanprover-bot commented May 30, 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 b5f7399bf19d623b3a5171732f1b3e617cfac38f --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-05-30 13:58:45)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase ab122a187d64224faf53004c9631f664b852bb96 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-15 17:11:24)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase d5790c1f088236fe67b52500ff87bce2c848b0bb --onto 49ff95727f98d43984726b26742d17a1ceea9dd5. You can force reference manual CI using the force-manual-ci label. (2026-07-21 19:08:45)

Comment thread src/Std/Http/Data/Body/Replayable.lean Outdated
Comment thread src/Std/Http/Data/Body/Replayable.lean Outdated
@algebraic-dev
algebraic-dev requested a review from TwoFX June 7, 2026 14:57
@algebraic-dev algebraic-dev added the grove The standard library changes in this PR should be analyzed using Grove. label Jun 12, 2026
@TwoFX TwoFX removed the grove The standard library changes in this PR should be analyzed using Grove. label Jun 19, 2026
Comment thread src/Std/Http/Data/Body/Any.lean Outdated

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

Looks good, just one minor nitpick about documentation.

Comment thread src/Std/Http/Data/Body/Any.lean
@algebraic-dev
algebraic-dev added this pull request to the merge queue Jul 21, 2026
Merged via the queue into master with commit 943e616 Jul 21, 2026
17 checks passed
robsimmons pushed a commit that referenced this pull request Jul 29, 2026
This PR adds a `Replayable` type class that is useful for checking if
some `Body` can be replayed in a redirect request.

---------

Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
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.

3 participants