feat: adds a simple `Http` library to `Std` #10478

algebraic-dev · 2025-09-20T18:54:03Z

This PR adds a simple Http library to Std.

leanprover-community-bot · 2025-09-21T22:08:49Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4881c3042e8d205080b19779d8dedfc672da3cd0 --onto 4379002d0582ae96d7fc6ccf5921ff4e9aa7239e. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-21 22:08:49)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase eabd7309b74f13cc12d0ab03d4826f34e3e49c0d --onto 0807f73171ca8f765c11ef37d69fd95e6613a878. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-24 00:27:54)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5ef7b45afaedd794fb39b0fbd70924b573694a00 --onto ac0b82933f6eac9914011ca2caf38d0e4e991160. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-25 13:54:11)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 486d93c5fd4ec0e1735554f9143a66327ca3f5a9 --onto 54c6efea95a0d478f2659632749035962b1f4d8d. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-07 18:22:48)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase aa86d95c0897a5aca9535dad6ffb1fd0f20cd5f1 --onto 14ff08db6f651775ead432d367b6b083878bb0f9. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-14 17:00:51)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f9adafe54d5070acbd270643f71b8455ca8c8d68 --onto 705084d9ba258dec704af428d7ce2444525f9ffb. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-31 05:29:24)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f9adafe54d5070acbd270643f71b8455ca8c8d68 --onto 1ce05b2a179eac8a902995c0caddc609c0169c49. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-01 17:03:01)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f9adafe54d5070acbd270643f71b8455ca8c8d68 --onto de073706c5446208065c7479211a3737ff99af25. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-15 02:58:43)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f9adafe54d5070acbd270643f71b8455ca8c8d68 --onto 5306a3469d20caa5f9d80384a5c1effdb14e9c67. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-23 06:25:53)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f9adafe54d5070acbd270643f71b8455ca8c8d68 --onto b0e6db322421ce368999f08870fd747e45242f86. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-27 01:48:28)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 16508196e0dfa0702868333eecf6f6dc8b58d632 --onto a4f9a793d9bdf3f3d4b69f3ebcfa7cd347df9d1a. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-30 05:08:30)
✅ Mathlib branch lean-pr-testing-10478 has successfully built against this PR. (2025-12-03 02:25:07) View Log
✅ Mathlib branch lean-pr-testing-10478 has successfully built against this PR. (2025-12-03 06:06:32) View Log
✅ Mathlib branch lean-pr-testing-10478 has successfully built against this PR. (2025-12-05 01:16:38) View Log
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 856825a4d2741f2de6d2d21454c20b1ba78b671b --onto 455fd0b4488e2adc85f825a52e2ee7d944a5740a. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-05 21:44:02)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c9b8508f6b6868be1857d207edf9ac01d764f8d2 --onto 62f2f9229356039356c0469a46d8ecd77be88e2a. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-09 00:41:29)

leanprover-bot · 2025-09-21T22:08:51Z

Reference manual CI status:

❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 4881c3042e8d205080b19779d8dedfc672da3cd0 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-09-21 22:08:50)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase eabd7309b74f13cc12d0ab03d4826f34e3e49c0d --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-09-24 00:27:56)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5ef7b45afaedd794fb39b0fbd70924b573694a00 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-09-25 13:54:14)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 486d93c5fd4ec0e1735554f9143a66327ca3f5a9 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-07 18:22:50)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase aa86d95c0897a5aca9535dad6ffb1fd0f20cd5f1 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-14 17:00:53)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase f9adafe54d5070acbd270643f71b8455ca8c8d68 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-31 05:29:25)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 16508196e0dfa0702868333eecf6f6dc8b58d632 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-30 05:08:31)
❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-30 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-12-03 01:18:19)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 856825a4d2741f2de6d2d21454c20b1ba78b671b --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-05 21:44:03)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase c9b8508f6b6868be1857d207edf9ac01d764f8d2 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-09 00:41:30)

TwoFX

Some preliminary review for the "easy" part of the PR.

src/Std/Internal/Http/Data/Body.lean

src/Std/Internal/Http/Data/Body/ByteStream.lean

src/Std/Internal/Http/Data/Headers.lean

src/Std/Internal/Http/Data/Request.lean

TwoFX · 2025-09-25T08:07:49Z

src/Std/Internal/Http/Data/Request.lean

+/--
+Builds and returns the final HTTP Request with the specified body
+-/
+def body (builder : Builder) (body : t) : Request t :=


Should this function force the user to set the Content-Type header?

I think it's something the HTTP client can infer and add when someone tries to send the request, to prevent it from being malformed.

I guess for Request it's kind of moot right now, but it does matter for Response.ok. Right now, Std.Http.Response.new |>.status .ok |>.text "hi" returns something different than Std.Http.Response.ok "hi" and I think that's just confusing.

src/Std/Internal/Http/Data/Request.lean

TwoFX · 2025-09-25T08:10:12Z

src/Std/Internal/Http/Data/Request.lean

+/--
+Creates a new HTTP POST Request with the specified URI and body
+-/
+def post (uri : RequestTarget) (body : t) : Request t :=


This function seems a bit strange to me, because it bypasses the nice helper functions with set the content type for you.

I think it's kinda nice to have a helper when you don't want to use the builder. Instead of writing Request.new |>.uri (parse! "/") |>.text "something", you can just use Request.post (parse! "/") "something"

I agree that this is nice to have, but my point is that the latter will not set the Content-Type header correctly, whereas the former does.

tests/lean/run/async_simple_http.lean

src/Std/Internal/Http/Data/URI.lean

src/Std/Internal/Http/Protocol/H1.lean

src/Std/Internal/Http/Server/Connection.lean

src/Std/Internal/Http/Server/Client.lean

tests/lean/run/async_simple_http.lean

TwoFX · 2025-09-25T15:06:52Z

I don't have a full test case for this, but when I create a response like

    return Std.Http.Response.new
      |>.status .ok
      |>.binary ByteArray.empty

then I think the Content-Length header should be set to 0, but it seems to be missing.

src/Std/Internal/Http/Util/BufferBuilder.lean

src/Std/Internal/Http/Protocol/H1.lean

TwoFX · 2025-09-26T07:42:16Z

It seems to me that there are some problems with timeouts around keep-alive.

I have this super simple server:

import Std.Internal.Http

def main : IO Unit := do
  (Std.Http.Server.serve (Std.Net.SocketAddress.v6 ⟨.ofParts 0 0 0 0 0 0 0 0, 8007⟩) (fun _ => pure <| .ok "hi")).block

Then I have this script:

#!/bin/bash

while true; do
  printf "GET / HTTP/1.1\r\nHost: localhost\r\n\r\n"
  sleep 2
done

When I run the server and do ./print.sh | nc localhost 8007, I expect the server to reply with hi every two seconds until the maximum number of requests is reached, and then I guess netcat should complain that the connection is closed. Instead, the server just seems to hang after the first request. It looks like it runs into the timeout (which is 1000 milliseconds by default), and then the Connection.handle function exists and the connection just... stays open in limbo.

This also reproduces in a browser. If I open localhost:8007, wait two seconds, and press F5, then the page will load indefinitely.

This seems to highlight several problems:

the request timeout starts too early, before the next request is even sent
the timeout is handled incorrectly
on a more basic level: it sounds problematic that we keep-alive connections only by number of requests, not by time. If a connection is used only once, it will stay open on the server for a potentially unbounded time. This last one might be acceptable because presumably a reverse proxy will timeout the connection after a while.

tests/lean/run/async_http_uri_parser.lean

algebraic-dev · 2025-09-26T20:45:25Z

It's probably a problem with the Timer API, the interaction with Selectable and the reference counting. I'm not sure how to fix this right now but I have a solution that changes a lot of stuff in the timer api :S

algebraic-dev self-assigned this Sep 20, 2025

algebraic-dev requested a review from TwoFX as a code owner September 20, 2025 18:54

algebraic-dev added the changelog-library Library label Sep 20, 2025

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Sep 21, 2025

algebraic-dev force-pushed the sofia/async-streammap branch from 29ae7af to be3f20d Compare September 22, 2025 22:09

algebraic-dev force-pushed the sofia/async-http branch from 8b58da0 to 3009358 Compare September 22, 2025 22:18

algebraic-dev changed the base branch from sofia/async-streammap to sofia/async-cancellation-token September 22, 2025 22:18

algebraic-dev force-pushed the sofia/async-cancellation-token branch from dde6cfa to 380dae6 Compare September 24, 2025 23:52

algebraic-dev force-pushed the sofia/async-http branch from 206ffa3 to ac37427 Compare September 25, 2025 03:06

TwoFX reviewed Sep 25, 2025

View reviewed changes

algebraic-dev force-pushed the sofia/async-cancellation-token branch 2 times, most recently from 8c47efc to 45e2368 Compare September 25, 2025 12:26

algebraic-dev force-pushed the sofia/async-http branch from ac37427 to 577dfde Compare September 25, 2025 12:27

TwoFX reviewed Sep 25, 2025

View reviewed changes

TwoFX reviewed Sep 26, 2025

View reviewed changes

src/Std/Internal/Http/Util/BufferBuilder.lean Outdated Show resolved Hide resolved

src/Std/Internal/Http/Protocol/H1.lean Outdated Show resolved Hide resolved

src/Std/Internal/Http/Protocol/H1.lean Outdated Show resolved Hide resolved

algebraic-dev requested a review from TwoFX September 26, 2025 06:57

TwoFX reviewed Sep 26, 2025

View reviewed changes

tests/lean/run/async_http_uri_parser.lean Show resolved Hide resolved

algebraic-dev force-pushed the sofia/async-cancellation-token branch from 60aeda4 to 4ac2b87 Compare October 7, 2025 01:41

algebraic-dev changed the base branch from sofia/async-cancellation-token to master October 7, 2025 15:03

algebraic-dev force-pushed the sofia/async-http branch from 93182a1 to 2bf41e9 Compare October 7, 2025 16:09

algebraic-dev requested review from hargoniX, kim-em, kmill, leodemoura and mhuisi as code owners October 14, 2025 04:12

algebraic-dev added 28 commits December 8, 2025 20:51

feat: limits and tests

9c10bc5

fix: copyright header

7391d81

fix: test

47d71cd

fix: import structure

e36bb26

feat: small improvements in tests and client

87fe876

feat: header changes

59c617b

fix: test

59a0171

fix: bug fixes and improvement in performance

7b7d49e

fix: tests

148f83f

fix: remove client related

edd9759

fix: details of connection: close

a389f93

fix: test

ce85f65

fix: weird behaviro when message as not sent :)

fd36c96

fix: multiple small problems

942c044

fix: string changes

9e7d485

fix: trailers parsing

beaa1e6

feat: parse chunk

ba27d70

fix: trailer

a0c9b3a

fix: parser

709fea1

fix: grammatical issues

1c590b5

fix: gramatic issues

b9d0c50

fix: ext chunk

99bc6ce

fix: context

912025d

feat: contextual fixes

dfdb3b5

feat: add more tests

6c3e392

fix: docs

aa5a6d3

fix: comments

0489523

feat: cancellation backwards

db6975c

algebraic-dev force-pushed the sofia/async-http branch from 546bc7f to db6975c Compare December 8, 2025 23:51

github-actions bot removed the changes-stage0 Contains stage0 changes, merge manually using rebase label Dec 8, 2025

feat: adds a simple Http library to Std #10478

Are you sure you want to change the base?

feat: adds a simple Http library to Std #10478

Uh oh!

Conversation

algebraic-dev commented Sep 20, 2025

Uh oh!

leanprover-community-bot commented Sep 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Sep 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

TwoFX left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

TwoFX Sep 25, 2025

Choose a reason for hiding this comment

Uh oh!

algebraic-dev Sep 26, 2025

Choose a reason for hiding this comment

Uh oh!

TwoFX Sep 26, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

TwoFX Sep 25, 2025

Choose a reason for hiding this comment

Uh oh!

algebraic-dev Sep 26, 2025 • 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!

TwoFX Sep 26, 2025 • 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!

TwoFX commented Sep 25, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

TwoFX commented Sep 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

algebraic-dev commented Sep 26, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

feat: adds a simple `Http` library to `Std` #10478

feat: adds a simple `Http` library to `Std` #10478

leanprover-community-bot commented Sep 21, 2025 •

edited

Loading

leanprover-bot commented Sep 21, 2025 •

edited

Loading

algebraic-dev Sep 26, 2025 •

edited

Loading

TwoFX Sep 26, 2025 •

edited

Loading

TwoFX commented Sep 26, 2025 •

edited

Loading