HTTP backends: reactor matches nginx (10x libuv), CI throughput tracker

[junjihashimoto]

Summary

• New HTTP backends — LeanTea.Net.FastServer (POSIX FFI, SO_REUSEPORT, thread-per-conn) and LeanTea.Net.ReactorServer (kqueue/epoll non-blocking event loop). Unified via LeanTea.Net.Backend + LEANTEA_HTTP_BACKEND env-var picker.
• Reactor matches / slightly beats nginx at 128 keep-alive conns on M-series: 72 149 RPS vs nginx 69 428. libuv baseline was 6 218 RPS; that's ~10× on RPS and ~5-10× on p99 tail latency.
• CI throughput tracker — .github/workflows/bench.yml runs on every push to main, boots lean-tea + nginx side-by-side on the same runner, records both absolute RPS and the parity ratio through benchmark-action/github-action-benchmark, persists to bench-data/http-bench.json.
• Typed LeanTea.Web.Route — Yesod-style inductive routes so Route.link refuses raw String hrefs; dead links become compile errors.

The measured story

server	health RPS	vs nginx	p99 (ms)
libuv Server	6 218	9 %	17
FFI FastServer (SO_REUSEPORT)	64 297	90 %	2.1
Reactor (kqueue/epoll)	72 149	104 %	2.1
nginx (same box, same conf)	69 428	—	2.0

Full breakdown (three routes × three concurrency levels + saturation runs) in docs/BENCHMARKS.md.

Why the libuv version was slow

Every recv/send hopped through: Lean IO → AsyncTask alloc → .block submit → libuv epoll → completion callback → Lean scheduler wake → fiber resume. Profiled at 100–500 µs per hop; each request paid 3–5 hops. Matches the measured T=1 ceiling of 1 933 RPS ≈ 500 µs/req.

The FFI variants skip that entire path — recv() and send() are direct syscalls. The reactor additionally keeps every idle connection at ~100 bytes of C state (no OS thread per fd) so it scales to 10 k+ idle connections without the LEAN_NUM_THREADS >= concurrency sharp edge the FastServer has.

Which backend to use

LeanTea.Net.Backend.fromEnv picks one from LEANTEA_HTTP_BACKEND:

var	pick	best for
unset / reactor	reactor	default — HTTP APIs
fast / fast:16	FastServer N workers	short-req APIs, no idle floods
libuv	Server.serveConcurrent	LLM proxy, WS, SSE, chat

Apps typically write:

def main : IO Unit := do
  let backend ← LeanTea.Net.Backend.fromEnv (default := .reactor)
  LeanTea.Net.Backend.serve backend 8080 "0.0.0.0" myHandler

Also in this PR

• Fixed a Response.toBytes bug — used to append a hardcoded connection: close even when the annotator added connection: keep-alive, so responses carried both. ab was lenient; strict clients would have dropped. The serializer is now a single growing string + one toUTF8.
• bench_server picks up the backend from Backend.fromEnv; the --fast N / --reactor CLI flags stay for explicit perf runs and win over the env var.
• LeanTea.Web.Route (typed inductive route + Route.link compile-time dead-link check). Standalone commit at the bottom of the branch — not on the critical perf path but was blocked in the same session.

Test plan

• lake build clean on macOS (176 targets)
• Smoke test all three backends via env var:
  • LEANTEA_HTTP_BACKEND=reactor ./bench_server → curl /health /json /echo all 200 OK
  • LEANTEA_HTTP_BACKEND=libuv → same
  • LEANTEA_HTTP_BACKEND=fast:4 → same
  • Unknown value → warns to stderr, falls back to default
• wrk -t8 -c128 -d10s http://.../health on all three backends produces the numbers in the table above
• Reactor doesn't crash under wrk -t16 -c2000 -d10s (63 k RPS, matches nginx at same load)
• CI bench.yml — first run will land after merge; watch it produce a populated bench-data/http-bench.json and not infinite-loop
• Downstream repos (chuhan, meta) still build after merge (they require this via git; no user-facing API removed but they gain the new imports)