Skip to content

test: cover stream known-size initialization race - #14552

Open
kernelpanic888 wants to merge 2 commits into
leanprover:masterfrom
kernelpanic888:codex/stream-known-size-race-14527
Open

test: cover stream known-size initialization race#14552
kernelpanic888 wants to merge 2 commits into
leanprover:masterfrom
kernelpanic888:codex/stream-known-size-race-14527

Conversation

@kernelpanic888

@kernelpanic888 kernelpanic888 commented Jul 25, 2026

Copy link
Copy Markdown

PR #14541 (commit 44d40a3d8c) has already fixed the race by initializing .chunked inside Body.stream before the producer starts. This PR now keeps only the missing regression coverage for that implementation.

The tests verify two boundaries:

  • a Body.stream producer observes .chunked immediately;
  • a producer-provided .fixed 42 size survives completion of Response.Builder.stream and is not overwritten.

The branch is merged with current master; it no longer adds or changes the Body.stream API.

This PR initializes stream size metadata before scheduling the producer, preventing a builder default from racing with and overwriting producer-provided fixed lengths.

Closes leanprover#14527
@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 Jul 25, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Jul 25, 2026

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-07-25 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-07-25 18:29:29)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d53dcb222f8122be00cfc00947e0154b9bb337c6 --onto 0bfc3acaef4ed0576307a77fbaa0c6e1a5dca402. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-30 21:05:02)

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

leanprover-bot commented Jul 25, 2026

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ✅ Reference manual branch lean-pr-testing-14552 has successfully built against this PR. (2026-07-25 18:34:35) View Log
  • 🟡 Reference manual branch lean-pr-testing-14552 build against this PR didn't complete normally. (2026-07-25 18:35:53) View Log
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase d53dcb222f8122be00cfc00947e0154b9bb337c6 --onto a39eab69e1eee9ad38f4efe507907b1026a77808. You can force reference manual CI using the force-manual-ci label. (2026-07-30 21:05:04)

@kernelpanic888 kernelpanic888 changed the title fix: initialize stream known size before producer test: cover stream known-size initialization race Jul 30, 2026
@kernelpanic888

Copy link
Copy Markdown
Author

Resolved the conflict with current master by adopting the already-merged #14541 implementation. The PR is now intentionally test-only; the unique regression coverage remains, while the duplicate API change is gone. Keeping it in draft until the refreshed CI completes.

@kernelpanic888

Copy link
Copy Markdown
Author

changelog-no

@github-actions github-actions Bot added the changelog-no Do not include this PR in the release changelog label Aug 10, 2026
@kernelpanic888
kernelpanic888 marked this pull request as ready for review August 11, 2026 00:00
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-no Do not include this PR in the release changelog 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