Skip to content

fix: close idle HTTP server connections after the keep-alive timeout - #15043

Open
counter2015 wants to merge 1 commit into
leanprover:masterfrom
counter2015:fix-http-idle-timeout
Open

fix: close idle HTTP server connections after the keep-alive timeout#15043
counter2015 wants to merge 1 commit into
leanprover:masterfrom
counter2015:fix-http-idle-timeout

Conversation

@counter2015

@counter2015 counter2015 commented Sep 5, 2026

Copy link
Copy Markdown

This PR fixes Std.Http.Server stalls caused by idle connections retaining connection slots past the configured keep-alive timeout.

Schedule the idle timeout before the first request and between requests, closing the connection silently when it expires. Keep the existing timeout behavior once a request starts. Add regression tests for both idle states and for handlers that run longer than the idle timeout.

AI assistance: Codex assisted with the implementation, regression tests, and this description.

Closes #15041

This PR fixes HTTP server stalls caused by idle connections retaining connection slots past the configured keep-alive timeout.

Schedule the idle timeout before the first request and between requests, closing the connection silently when it expires. Keep the existing timeout behavior once a request starts. Add regression tests for both idle states and for handlers that run longer than the idle timeout.

AI assistance: Codex assisted with the implementation, regression tests, and this description.

Closes leanprover#15041
@counter2015

Copy link
Copy Markdown
Author

Validation on macOS ARM64:

  • Release stage1 build passed with make -j14 -C build/release, using the official 4.35.0-nightly-2026-09-05 toolchain at the base commit 9de86005af5061b5ccf438d01134ee6d3ecea6b3 as the bootstrap compiler.
  • All 23 HTTP tests passed with CTEST_PARALLEL_LEVEL=14 CTEST_OUTPUT_ON_FAILURE=1 make -j14 -C build/release test ARGS="-R 'async_http'", including the new regression file.
  • Running the same new regression file with the unmodified official nightly fails in all three cases with idle connection did not close.
  • python3 tests/lint.py and git diff --cached --check passed.

The local run covers the HTTP test group; the full Lean test suite and other platforms have not been run locally.

@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 Sep 5, 2026
@mathlib-lean-pr-testing

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-09-05 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-09-05 15:56:44)

@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Sep 5, 2026
@leanprover-bot

leanprover-bot commented Sep 5, 2026

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

@counter2015
counter2015 marked this pull request as ready for review September 5, 2026 16:09
@counter2015
counter2015 requested a review from TwoFX as a code owner September 5, 2026 16:09
@counter2015

Copy link
Copy Markdown
Author

changelog-library

@github-actions github-actions Bot added the changelog-library Library label Sep 5, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

builds-manual CI has verified that the Lean Language Reference builds against this PR 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.

Std.Http.Server: idle keep-alive timeout is not scheduled, exhausting maxConnections

2 participants