HTP Body.Stream can override user setKnownSize from fixed to chunked

[ecyrbe]

Prerequisites

• [ X] Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• [ X] Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• [ X] Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

In main branch the stream builder set the stream to chunk encoding by default, but it can lead to a Override the user setKnownSize set to fixed length.

Context

The newly merged code sets the Stream to Chunk encoding, but sometimes you know the side of what you want to stream and don't want chunk encoding.

Now the stream builder does this :

def stream
    (builder : Builder)
    (gen : Body.Stream → Async Unit) :
    Async (Request Body.Stream) := do
  let s ← Body.stream gen
  s.setKnownSize (some .chunked)
  return Request.Builder.body builder s

and the gen is run in background with :

def stream (gen : Stream → Async Unit) : Async Stream := do
  let s ← mkStream
  background <| do
    try
      gen s
    finally
      s.close
  return s

Now if the user want to set the known size in gen to evoid chunk encoding, like this :

def myGen  (knownLen : Nat) (stream : Body.Stream) : Async Unit := do
    stream.setKnownSize (some (.fixed knownLen))
    ...
    stream.send { data := ... }
    ...

It would be possible that the setKnownSize with fixed len could be overwritten since the gen could technically be scheduled before the setKnownSize with chunked encoding. Making it tricky to debug.

A solution would be to call setKnownSize to chunked encoding only if it's currently set to none or better that mkStream sets the known size to chunked at creation (or with an optional size value).
Another approach would be to have the builder .stream that let the user set the size of the stream as an optional parameter that defaults to Chunk.

Steps to Reproduce

This is hard to reproduce, since it depends on system scheduler, scheduling one thread before the other.

Expected behavior: [Clear and concise description of what you expect to happen]

The chunked encoding is set before the gen code has any chance to be run. For possible solutions, see my proposals in context section.

Actual behavior: [Clear and concise description of what actually happens]

The chunked encoding can be set after the gen code is run overriding user fixed setKnownSize.

Additional informations

See zulip for first time this was reported.

Versions

Current main version, (nighly of 24/07/2026)

Impact

LeanIO for serving file rely on fixed size streaming. This bug could make file serving experience surpising.
Sometimes downloading file has clear progress bar, while other times it has unknown progress bar.

[ecyrbe]

fixed by #14541