feat: add `RedirectPlan` for validating and following redirects by algebraic-dev · Pull Request #13901 · leanprover/lean4

algebraic-dev · 2026-05-30T13:11:51Z

This PR adds a RedirectPlan type that uses the RFC9110 logic to validate redirect responses and automatically redirect.

mathlib-lean-pr-testing · 2026-05-30T14:01:45Z

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 14:01:45)
❗ 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 16:34:51)
❗ 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:17:45)
❗ 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:41:11)
❗ 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:55:46)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ab122a187d64224faf53004c9631f664b852bb96 --onto 0758b1d2e33c65ccea578abb0c668aab1f811608. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-25 14:28:40)
❗ 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 21:20:50)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 943e616509e287b7055c0571e11dba6cbb8c9b3b --onto 3259610687883ec1ea48c481aba2469f2f83facf. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-22 00:47:09)

leanprover-bot · 2026-05-30T14:01:47Z

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 14:01:46)
❗ 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:17:46)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase ab122a187d64224faf53004c9631f664b852bb96 --onto 2e72131c7f007ab9d2538b676106c5141b24ba22. You can force reference manual CI using the force-manual-ci label. (2026-06-25 14:28:42)
❗ 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 21:20:52)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 943e616509e287b7055c0571e11dba6cbb8c9b3b --onto 49ff95727f98d43984726b26742d17a1ceea9dd5. You can force reference manual CI using the force-manual-ci label. (2026-07-22 00:47:10)

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

ecyrbe · 2026-06-14T11:21:10Z

+  let scrubbed := RedirectPlan.scrubHeaders request.headers isCrossOrigin methodChanged
+  let newHeaders :=
+    if isCrossOrigin then
+      RedirectPlan.rewriteHostHeader scrubbed newOrigin
+    else scrubbed


This is really great. It's usually one of the big security issues when issuing redirections.
This is so important for security that i wonder if some proof of adherance to spec could be added just for this ?

…ia/async-http-redirect-plan

…-redirect-plan

…ia/async-http-replayable-body

…-redirect-plan

…ia/async-http-redirect-plan

This PR adds a `RedirectPlan` type that uses the RFC9110 logic to validate redirect responses and automatically redirect. --------- Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

algebraic-dev added 3 commits May 26, 2026 17:40

feat: add type class to in the Http library

503a3cf

test: add test

789cde4

fix: stream closeError

cb5ee2a

algebraic-dev self-assigned this May 30, 2026

algebraic-dev requested a review from TwoFX as a code owner May 30, 2026 13:11

algebraic-dev added the changelog-library Library label May 30, 2026

algebraic-dev changed the base branch from master to sofia/async-http-replayable-body May 30, 2026 13:12

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

TwoFX reviewed Jun 5, 2026

View reviewed changes

Comment thread src/Std/Http/Protocol/H1/Redirect.lean Outdated

fix: removed reset and simplified docs

e1ce85d

algebraic-dev force-pushed the sofia/async-http-redirect-plan branch from dbd4cc6 to ee33e6e Compare June 5, 2026 13:52

feat: remove replay from full keep only replayInPlace

5c6d0c1

algebraic-dev force-pushed the sofia/async-http-redirect-plan branch from ee33e6e to 03468f6 Compare June 5, 2026 14:00

algebraic-dev added 8 commits June 5, 2026 11:02

test: remove replay tests

39c1217

feat: RedirectPlan structure inside H1

73ea40b

fix: redirect and uri

95bb5e6

fix: h1 supression

401a56b

fix: CORS

7a99814

revert: test

31950e8

revert: empty file

da4ee0a

fix: indexmultimap erasekeys

f8ecc1c

algebraic-dev force-pushed the sofia/async-http-redirect-plan branch from a42f923 to f8ecc1c Compare June 5, 2026 14:37

algebraic-dev and others added 3 commits June 5, 2026 12:02

fix: remove orphaned module

3918490

doc: drop external-system reference from Replayable docstring

42c47ee

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

refactor: move to another branch Stream changesz

00aa334

ecyrbe reviewed Jun 14, 2026

View reviewed changes

algebraic-dev added 2 commits June 15, 2026 11:07

Merge branch 'master' of https://github.com/leanprover/lean4 into sof…

1ade557

…ia/async-http-redirect-plan

fix: bug with host header twice

e2a6072

algebraic-dev removed the changes-stage0 Contains stage0 changes, merge manually using rebase label Jun 15, 2026

algebraic-dev added 16 commits June 15, 2026 16:09

fix: head preservation

0869b1f

revert: content type changes

a2ddd8b

feat: empty is replayable

6d94b76

Merge branch 'sofia/async-http-replayable-body' into sofia/async-http…

c4bd971

…-redirect-plan

fix: small comment issues

ea6f33a

refactor: drop body-framing changes

c6b2db4

chore: remove comments that mention redirect to keep the PR small

8b46ee5

fix: wrong isClosed behavior

95e3bea

Merge branch 'sofia/async-http-replayable-body' into sofia/async-http…

9e02ba7

…-redirect-plan

fix: query parameters and conneciton headers

1fdc617

fix: remove isReplayable and resetInPlace

5082745

Merge branch 'sofia/async-http-replayable-body' into sofia/async-http…

2769907

…-redirect-plan

fix: make reset? public

56b55c0

Merge branch 'sofia/async-http-replayable-body' into sofia/async-http…

d27ecf6

…-redirect-plan

fix: reset? tests

7948216

Merge branch 'sofia/async-http-replayable-body' into sofia/async-http…

4688994

…-redirect-plan

TwoFX reviewed Jun 25, 2026

View reviewed changes

Comment thread src/Std/Http/Internal/IndexMultiMap.lean Outdated

Comment thread src/Std/Http/Protocol/H1/Redirect.lean Outdated

Comment thread src/Std/Http/Protocol/H1/Redirect.lean Outdated

TwoFX reviewed Jun 25, 2026

View reviewed changes

Comment thread src/Std/Http/Protocol/H1/Redirect.lean Outdated

Comment thread src/Std/Http/Protocol/H1/Redirect.lean Outdated

Comment thread src/Std/Http/Protocol/H1/Redirect.lean Outdated

fix: query redirect

cdf9f6f

TwoFX approved these changes Jun 30, 2026

View reviewed changes

algebraic-dev added 3 commits July 21, 2026 15:23

Merge branch 'master' of https://github.com/leanprover/lean4 into sof…

e14443c

…ia/async-http-replayable-body

feat: add comment

c1a6513

Merge branch 'sofia/async-http-replayable-body' into sofia/async-http…

a605e84

…-redirect-plan

algebraic-dev changed the base branch from sofia/async-http-replayable-body to master July 22, 2026 00:20

Merge branch 'master' of https://github.com/leanprover/lean4 into sof…

0a65159

…ia/async-http-redirect-plan

algebraic-dev added this pull request to the merge queue Jul 23, 2026

Merged via the queue into master with commit 202c791 Jul 23, 2026
17 checks passed

Navigation Menu

Uh oh!

feat: add `RedirectPlan` for validating and following redirects - #13901

feat: add `RedirectPlan` for validating and following redirects#13901
algebraic-dev merged 41 commits into
masterfrom
sofia/async-http-redirect-plan

algebraic-dev commented May 30, 2026

Uh oh!

mathlib-lean-pr-testing Bot commented May 30, 2026 •

edited

Loading

Uh oh!

leanprover-bot commented May 30, 2026 •

edited

Loading

Uh oh!

Uh oh!

ecyrbe Jun 14, 2026 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Uh oh!

Conversation

algebraic-dev commented May 30, 2026

Uh oh!

mathlib-lean-pr-testing Bot commented May 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented May 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

ecyrbe Jun 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

mathlib-lean-pr-testing Bot commented May 30, 2026 •

edited

Loading

leanprover-bot commented May 30, 2026 •

edited

Loading

ecyrbe Jun 14, 2026 •

edited

Loading