From eff717e1bf619d823972f8b95c871a5c32a8cccf Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Fri, 24 Jul 2026 13:53:33 -0300 Subject: [PATCH 1/5] feat: connection and session --- FS.md | 666 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 666 insertions(+) create mode 100644 FS.md diff --git a/FS.md b/FS.md new file mode 100644 index 000000000000..c7759c79466f --- /dev/null +++ b/FS.md @@ -0,0 +1,666 @@ +# Summary + +This proposal redesigns Lean's FS and Path API using LibUV, replacing a lot of types, making them more complete and removing the `FILE*` dependency in the C++ side. It also adds directory traversals, metadata inspection, some useful functions like copying without reading the entire file into memory and a way to integrate with `Std.Async` in a clean way. This design changes `FS.Handle` and `FS.Stream` to a layer approach with more low-level changes that requires the user to do synchronization and buffering on the Lean side. + +Since these things will depend on Std abstractions, it lives under `Std.FS` and `Std.Async.FS`. Path-related changes are tracked separately in issue #13922. + +# Migration + +A lot of functions are just going to be moved to other namespaces like `IO.FS.readFile` that goes to `Std.FS.readFile`. The `Handle` type will just be split into multiple low level ones like `File`, `Dir`, `Handle` (a smaller version with `uv_pipe_t` and `uv_tty_t`). + +| Old | New | Notes | +| ----------------------------------------------- | --------------------------------------------- | ------------------------------------------------------ | +| `IO.FS.Handle` | `Std.FS.File` | for regular files opened by path | +| `IO.FS.Handle` | `Std.FS.Dir` | for regular directories opened by path | +| `IO.FS.Handle` | `Std.FS.Handle` | for stdin/stdout/stderr and IPC pipes | +| `IO.FS.Stream` | `Std.FS.Stream` | Keep the abstraction for LSP capture of the Stdout | +| `IO.getStdin` / `getStdout` / `getStderr` | `Handle.stdin` / `.stdout` / `.stderr` | now `Stdin`/`Stdout`/`Stderr`, which have no `close` | +| `IO.FS.Handle.putStr` / `IO.FS.Handle.putStrLn` | `Std.FS.File.putStr` / `Std.FS.File.putStrLn` | same semantics | +| `IO.FS.Handle.isEof` | — | no direct equivalent; `File.readAt` returns empty at EOF | +| `IO.FS.readFile` | `Std.FS.readFile` | same semantics | +| `IO.FS.writeFile` | `Std.FS.writeFile` | same semantics | +| `IO.FS.readBinFile` | `Std.FS.readBinFile` | same semantics | +| `IO.FS.writeBinFile` | `Std.FS.writeBinFile` | same semantics | +| `IO.FS.lines` | `Std.FS.lines` | same semantics | +| `IO.FS.hardLink` | `Std.FS.hardLink` | same semantics | + +## Async Integration + +`uv_fs_*` operations can be used asynchronously and synchronously (by specifying a NULL loop and callback), so with a `Std/Async/FS` we can just add operations in the namespace like `.readAsync` that will return a `Promise` instead of blocking. `Std.Async.FS` gives every `Std.FS`/`Std.FS.File` operation an `*Async` counterpart, including path-keyed convenience helpers (`readFileAsync`, `writeFileAsync`, `appendFileAsync`, …), directory operations (`readDirAsync`, `removeDirAllAsync`, `copyDirAsync`, `walkAsync`, `globAsync`), symlinks, metadata/permissions, and temporary files/directories. The full list is in [Async Variants](#async-variants); everything lives in the same `Std.FS` / `Std.FS.File` namespaces as its synchronous counterpart, so the two are used side by side without extra `open`s. + +The async variants return `Async α` (over `Std.Async`'s `Promise`), not `IO α`. `Handle`, `Pipe`, and `TTY` get async read/write too — for those the asynchronous form is the *primitive* one, since `uv_read_start`/`uv_write` are natively asynchronous and the synchronous variants are what require extra machinery to emulate. `Dir` and the buffered wrappers have no async counterparts: directory iteration is exposed asynchronously only through the eager path-keyed `readDirAsync`/`walkAsync`. + +File locking is the exception: acquiring a contended lock with `flock` (POSIX) or `LockFileEx` (Windows) is a blocking syscall with no libuv equivalent and SHOULDN'T run on the event loop thread, so `File.lockAsync` schedules a dedicated work thread using `uv_queue_work` and resumes a `Promise` once it completes. `File.tryLockAsync` and `File.unlockAsync` are the exception to the exception: a non-blocking `trylock` and releasing a lock never block for an unbounded time, so they run inline rather than needing a work thread. As `flock` is advisory it does not interfere with any of the operations of libuv and thus, is safe to use with another flocks. + +`walkAsync`/`globAsync` collect eagerly into an `Array` rather than returning a lazy `IterM`, since `Async` has no lazy-iterator integration yet (unlike the synchronous `FS.walk`, which returns `IterM (α := WalkIterator) IO DirEntry`). + +## Concurrency Model + +All raw IO types (`File`, `Handle`, `Pipe`, `Dir`) are not thread-safe by default. Concurrency and parallelism safety is achieved through explicit wrappers like `Mutex α` and `RecursiveMutex α`. + +# Core Abstractions + +## Paths and Filesystem Entries + +Path types and path manipulation are specified in issue #13922. This proposal only covers the filesystem abstractions that operate on paths. + +- `Dir`: An open directory handle. +- `DirEntry`: A single filesystem entry produced during directory iteration. +- `Metadata`: Filesystem metadata for files, directories, or special entries. +- `FileType`: Enumeration of entry kinds: `file`, `dir`, `symlink`, `blockDevice`, `charDevice`, `fifo`, `socket`, `unknown`. +- `File`: A thin wrapper around `uv_file`. Not thread-safe by default, concurrent access must be explicitly synchronized using `Mutex`. +- `BufferedReader α`: Buffered wrapper around any readable type. +- `BufferedWriter α`: Buffered writer over any writable type. +- `LineWriter α`: A writer wrapper that flushes automatically on newline characters (`\n`). Used by `Stdout`. +- `FilesystemStats`: Filesystem-level statistics (total/free space, inode counts) for the filesystem containing a path. + +## Handles and Streams + +- `Handle`: A system stream endpoint whose kind (`tty`, `pipe`, or a redirected `file`) is discovered at runtime via `uv_guess_handle`. Exposes only the operations valid for every kind. +- `Pipe`: A `Handle` known by construction to be a `uv_pipe_t`. +- `TTY`: A `Handle` known by construction to be a `uv_tty_t`, adding the terminal-only operations. +- `Stdin` / `Stdout` / `Stderr`: Cached singletons over descriptors 0/1/2, with buffering and *without* a `Close` instance. +- `Stream`: A record of closures that abstracts over any readable/writable endpoint, so stdout can be substituted at runtime. + +## Type Classes + +- `Read`: Typeclass for types that support sequential, cursor-advancing reads; provides `read : α → (n : USize) → ByteArray → IO ByteArray`, which appends up to `n` bytes after `buf`'s existing content. A result with no bytes appended signals end-of-file. Implemented by `File`, `Handle`, `Pipe`, and `TTY`. +- `Write`: Typeclass for types that support writing bytes; provides `write : α → ByteArray → IO Unit`. Implemented by `File`, `Handle`, `Pipe`, `TTY`, `BufferedWriter α`, and `LineWriter α`. +- `Close`: Typeclass for types that hold a resource that must be released; provides `close : α → IO Unit`. Implemented by `File`, `Dir`, `Handle`, `Pipe`, `TTY`, and the buffered wrappers (`BufferedReader`, `BufferedWriter`, `LineWriter`, which flush before delegating to the inner sink's `close`). Lets generic code release whatever `Read`/`Write` source or sink it was handed without depending on its concrete type. `Stdin`/`Stdout`/`Stderr` deliberately have **no** instance, so no generic cleanup path can close descriptors 0/1/2 — see [Standard Streams](#standard-streams). + +# Detailed Explanation + +## Iterators + +Some operations return `IterM` (defined in `Std/Data/Iterators`) rather than eagerly collected `Array`s. + +| Iterator State Type | Element | Used by | +| ------------------- | ---------- | ----------- | +| `DirIterator` | `DirEntry` | `Dir.iter` | +| `WalkIterator` | `DirEntry` | `FS.walk` | + +## FileType + +```lean +inductive FileType where + | file -- regular file + | dir -- directory + | symlink -- symbolic link + | blockDevice -- block device (e.g. disk) + | charDevice -- character device (e.g. /dev/null) + | fifo -- named pipe (FIFO) + | socket -- Unix domain socket + | unknown -- type not reported by the OS (e.g. some network filesystems) +``` + +| Function | Type | Description | +| ----------------------- | ------------------------ | ------------------------------------------------------------------------------------------------------------- | +| `FileType.ofDirentType` | `UInt8 → FileType` | Interpret a raw `uv_dirent_t` type code. | +| `FileType.ofStatMode` | `UInt64 → FileType` | Interpret the `S_IFMT` bits of a raw POSIX `st_mode`, as returned by `stat`/`lstat`/`fstat`. | + +## OpenMode + +`OpenMode` is a struct specifying how a file is opened. The default value opens an existing file +read-only. + +**Fields** + +| Field | Type | Default | Description | +| ---------------------------- | -------------- | ------- | ---------------------------------------------------------- | +| `OpenMode.read` | `Bool` | `true` | Allow reads | +| `OpenMode.write` | `Bool` | `false` | Allow writes | +| `OpenMode.append` | `Bool` | `false` | All writes go to end-of-file; incompatible with `truncate` | +| `OpenMode.truncate` | `Bool` | `false` | Truncate to zero on open; requires `write` | +| `OpenMode.create` | `Bool` | `false` | Create the file if it does not exist (`O_CREAT`) | +| `OpenMode.createNew` | `Bool` | `false` | Create the file, failing if it already exists (`O_CREAT \| O_EXCL`); guarantees exclusive creation | +| `OpenMode.custom` | `Option USize` | `none` | Pass raw OS-level flags directly; merged with the flags derived from the other fields. Use when no predefined field covers the required behavior. | + +**Presets** + +| Name | Value | Description | +| ----------------------- | ------------------------------------------------ | -------------------------------------------------- | +| `OpenMode.readOnly` | `{ read }` | Open an existing file for reading only. | +| `OpenMode.readWrite` | `{ read, write }` | Open an existing file for reading and writing without truncation. | +| `OpenMode.writeCreate` | `{ write, create }` | Create or open a file for writing. | +| `OpenMode.appendCreate` | `{ write, append, create }` | Open a file for appending, creating it if necessary. | + +`OpenMode.rawFlags : OpenMode → UInt32` computes the `uv_fs_open` flag bitmask, merging in `custom`. +It is public so `Std.Async.FS` can share it rather than re-deriving the bits. + +## Permissions + +`AccessRight` and `FileRight` keep the same shape as `IO.AccessRight`/`IO.FileRight` in the current API, moved to `Std.FS`. + +```lean +structure AccessRight where + /-- The file can be read. -/ + read : Bool := false + /-- The file can be written to. -/ + write : Bool := false + /-- The file can be executed. -/ + execution : Bool := false + +structure FileRight where + /-- The owner's permissions to access the file. -/ + user : AccessRight := {} + /-- The assigned group's permissions to access the file. -/ + group : AccessRight := {} + /-- The permissions that all others have to access the file. -/ + other : AccessRight := {} +``` + +| Name | Type | Description | +| ----------------------- | --------------------------------------- | --------------------------------------------------- | +| `FileRight.flags` | `FileRight → UInt32` | Convert to a raw POSIX bit field (for `chmod`, etc.) | +| `FileRight.ofStatMode` | `UInt64 → FileRight` | Interpret the low 9 permission bits of a raw POSIX `st_mode` | +| `FileRight.default` | `FileRight` | `0o644` — owner read/write; group and other read | +| `FileRight.defaultDir` | `FileRight` | `0o755` — owner read/write/execute; group and other read/execute | + +## File Type + +`File` is a wrapper around `uv_file` with no buffering and no built-in lock. If buffering or locking is needed, wrap with `Mutex (BufferedWriter File)` or call `File.lock`. + +| Function | Type | Description | Operation | +| ------------------------ | ---------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------- | +| `File.openExisting` | `Path → (mode : OpenMode := .readOnly) → IO File` | Open an existing file. Fails if the file does not exist. Default mode is read-only; pass `.readWrite` to open for reading and writing without truncation. | `uv_fs_open` | +| `File.create` | `Path → (mode : OpenMode := .writeCreate) → (perm : FileRight := .default) → IO File` | Create or open a file, applying `perm` if it is newly created. | `uv_fs_open` | +| `File.withFile` | `Path → (mode : OpenMode := .readOnly) → (File → IO α) → IO α` | Open a file, run an action, close in a `finally` block. | +| `File.close` | `File → IO Unit` | Explicitly close the file. Prefer `withFile` or explicit `close`. Closing does not call `fsync`; use `syncAll` before closing for durability. | `uv_fs_close` | +| `File.syncAll` | `File → IO Unit` | Flush data and metadata to the device (`fsync`). | `uv_fs_fsync` | +| `File.syncData` | `File → IO Unit` | Flush data only, skipping metadata (`fdatasync`). Cheaper when durability of timestamps/size is not required. | `uv_fs_fdatasync` | +| `File.sendFile` | `(src dst : File) → (offset : Int64) → (length : USize) → IO USize` | Copy up to `length` bytes from `src` at `offset` into `dst` using OS copy acceleration. Returns the number of bytes actually copied. | `uv_fs_sendfile` | +| `File.lock` | `File → (exclusive : Bool := true) → IO Unit` | Acquire a shared or exclusive lock, blocking the calling thread until available. (Only `lockAsync` needs `uv_queue_work`, to keep the event loop free.) | `LockFileEx` on Windows, `flock` on POSIX | +| `File.tryLock` | `File → (exclusive : Bool := true) → IO Bool` | Try to acquire a lock without blocking. Returns `false` immediately if held by another process. | (`LockFileEx` on Windows, `flock` on POSIX) | +| `File.unlock` | ` File → IO Unit` | Release the lock. Idempotent; succeeds even if no lock is held. | `UnlockFileEx` on Windows, `flock` on POSIX | +| `File.atomically` | `File → (exclusive : Bool := true) → IO α → IO α` | Lock, run action, unlock in `finally`. Uses `File.lock`/`File.unlock`. | | +| `File.read` | `File → (n : USize) → (buf : ByteArray) → IO ByteArray` | Read up to `n` bytes at the current cursor position, advancing it. Bytes are appended after `buf`'s existing content; use the return value, not `buf`, after the call. No bytes appended signals end-of-file. Backs the `Read File` instance. | `uv_fs_read` | +| `File.readAt` | `File → (offset : UInt64) → (n : USize) → (buf : ByteArray) → IO ByteArray` | Read up to `n` bytes at `offset` into `buf` without moving the cursor (`pread`). Returns the filled slice; use the return value, not `buf`, after the call. | `uv_fs_read` | +| `File.writeAt` | `File → (offset : UInt64) → ByteArray → IO Unit` | Write at `offset` (`pwrite`), retrying until every byte is written. | `uv_fs_write` | +| `File.write` | `File → ByteArray → IO Unit` | Write at the current cursor position, retrying until every byte is written. | `uv_fs_write` | +| `File.putStr` | `File → String → IO Unit` | Write a UTF-8 string at the current cursor position. | | +| `File.putStrLn` | `File → String → IO Unit` | Write a UTF-8 string followed by `\n` at the current cursor position. | | +| `File.setLength` | `File → (len : UInt64) → IO Unit` | Truncate or extend the file to exactly `len` bytes. | `uv_fs_ftruncate` | +| `File.metadata` | `File → IO Metadata` | Return metadata for the open file. Avoids TOCTOU vs `Path.metadata`. | `uv_fs_fstat` | +| `File.setPermissions` | `File → FileRight → IO Unit` | Set the file's permission bits. | `uv_fs_fchmod` | +| `File.setTimes` | `File → (accessed : Timestamp) → (modified : Timestamp) → IO Unit` | Set access and modification timestamps. | `uv_fs_futime` | +| `File.chown` | `File → (uid gid : UInt32) → IO Unit` | Change the owner and group of the open file. On Windows this is a noop. | `uv_fs_fchown` | + +## Handle Type + +`Handle` is an open stream endpoint whose *kind is discovered at runtime*: `uv_guess_handle(fd)` +reports `UV_TTY`, `UV_NAMED_PIPE`, or `UV_FILE`, and the kind decides which libuv API is legal for it. +A `Handle` therefore exposes exactly the operations valid for every kind — sequential read, write, +close — and nothing more. + +**Why `Handle` is not a `File`.** The tempting simplification is that on POSIX everything is a file +descriptor, so `Handle` could just be `File` and `Pipe`/`TTY` could disappear. It does not hold: + +- **libuv forbids the mixing.** Regular-file descriptors are always reported ready by `epoll`/`kqueue`, + so readiness polling is meaningless and libuv does not support files as streams: `uv_read_start` is + invalid on a `UV_FILE`, and conversely `uv_fs_read` on a terminal bypasses everything `uv_tty_t` + exists to do. `uv_tty_init` on a non-terminal descriptor returns `EINVAL`. +- **`File`'s API is offset-based; pipes and terminals have no offsets.** `readAt`, `writeAt`, + `setLength`, and `sendFile` all take an offset, and `pread`/`pwrite` on a pipe or terminal fail with + `ESPIPE`. So do `ftruncate` and `flock`, and `fstat` reports nothing useful. Collapsing the types + would produce one whose entire documented surface throws on two of its three kinds. +- **On Windows they are not the same OS object.** `uv_tty_t` wraps a console handle and performs + UTF-16 conversion, ANSI escape emulation, and virtual-terminal mode handling; a pipe is a Named Pipe + driven by overlapped I/O; a file is a `HANDLE` for `ReadFile`. The POSIX intuition does not port. + +The containment runs one way only: a `File` offers a superset of `Handle`'s operations, never the +reverse. No coercion between them is provided, since it would silently discard the +positioned-vs-cursor distinction. + +**Redirected stdio.** `uv_guess_handle` returns `UV_FILE` when stdio is redirected to a regular file +(`./program > out.txt`). The handle then dispatches reads and writes via `uv_fs_read`/`uv_fs_write` +internally, but it stays typed as a `Handle`: the program did not gain the ability to seek or lock its +own stdout just because the shell redirected it. + +```lean +inductive HandleKind where + | file -- `uv_guess_handle` reported `UV_FILE` (redirected stdio) + | tty -- `UV_TTY` + | pipe -- `UV_NAMED_PIPE` +``` + +| Function | Type | Description | libuv | +| ----------------- | --------------------------------------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------ | +| `Handle.ofFd` | `(fd : UInt32) → (readable : Bool) → IO Handle` | Adopt an existing descriptor, dispatching on `uv_guess_handle`: `UV_FILE` is kept as a raw descriptor, `UV_TTY` is initialized with `uv_tty_init`, `UV_NAMED_PIPE` with `uv_pipe_init` + `uv_pipe_open`. `UV_TCP`/`UV_UDP` are rejected — those belong to `Std.Async.TCP`/`UDP`. | `uv_guess_handle` | +| `Handle.kind` | `Handle → BaseIO HandleKind` | The kind reported at construction. | `uv_guess_handle` | +| `Handle.read` | `Handle → (n : USize) → (buf : ByteArray) → IO ByteArray` | Read up to `n` bytes into `buf`, reusing its storage in place when `buf` is uniquely owned. Returns the filled slice; use the return value, not `buf`. Returns `buf` truncated to its original size at EOF. | `uv_read_start` / `uv_fs_read` | +| `Handle.write` | `Handle → ByteArray → IO Unit` | Write bytes. | `uv_write` / `uv_fs_write` | +| `Handle.flush` | `Handle → IO Unit` | Flush any buffered output. No-op for unbuffered handles. | | +| `Handle.close` | `Handle → IO Unit` | Close the handle and release resources. | `uv_close` / `uv_fs_close` | +| `Handle.asTTY?` | `Handle → BaseIO (Option TTY)` | Refine to a `TTY` if the kind is `tty`, so the terminal-only operations become available. | | +| `Handle.asPipe?` | `Handle → BaseIO (Option Pipe)` | Refine to a `Pipe` if the kind is `pipe`. | | +| `Handle.isTty` | `Handle → BaseIO Bool` | `kind == .tty`. Retained as a convenience. | `uv_guess_handle` | +| `Handle.isPipe` | `Handle → BaseIO Bool` | `kind == .pipe`. | `uv_guess_handle` | +| `Handle.isFile` | `Handle → BaseIO Bool` | `kind == .file`. | `uv_guess_handle` | + +The three predicates are mutually exclusive, hence `kind` is the primitive and they are derived from +it. + +`Handle.read`/`write` block the calling thread. For the `tty`/`pipe` kinds the underlying libuv API is +asynchronous (`uv_read_start`/`uv_write`), so the synchronous form is implemented by bridging through a +semaphore that the completion callback posts from the event loop's driver thread. Concurrent +operations on one handle return `EALREADY` rather than interleaving; as with `File`, sharing a +`Handle` across threads requires an explicit `Mutex`. + +## Standard Streams + +`Handle.stdin`, `Handle.stdout`, and `Handle.stderr` are **cached singletons**, built once from +descriptors 0/1/2. They must not be re-initialized: two `uv_tty_init` calls on descriptor 1 produce two +`uv_tty_t` contending for one console. + +They are returned as the distinct types `Stdin`, `Stdout`, and `Stderr`, each wrapping a `Handle` plus +the buffering appropriate to it: + +| Type | Buffering | Rationale | +| -------- | ---------------------------------- | ---------------------------------------------------------------- | +| `Stdin` | `Mutex (BufferedReader Handle)` | Read buffering, with `readLine`. | +| `Stdout` | `RecursiveMutex` + line buffering | Flushes on `\n` so line-oriented output is delivered promptly. | +| `Stderr` | `Mutex Handle`, unbuffered | Diagnostics must survive a crash that never reaches a flush. | + +**They deliberately have no `Close` instance**, and therefore no way to close descriptors 0/1/2. This +follows Rust, where `Stdout` is its own type with no `close` method and dropping a handle leaves the +descriptor open — and departs from Go, Python, and Java, which expose `os.Stdout.Close()` / +`sys.stdout.close()` / `System.out.close()` and let a program disable its own output (silently, in +Java's case). + +The reason to prefer Rust's answer here is specific to this design: `Close` is a *typeclass*, and the +buffered wrappers close what they wrap — `BufferedWriter.close` and `LineWriter.close` both flush and +then call `Close.close` on the inner sink. If the standard streams were ordinary `Close`-able values, +a single `Close.close` reached through a generic cleanup path would close descriptor 1 for the whole +process, with no line of code naming stdout anywhere. Go and Python are not exposed to this because +they have no such polymorphism; removing the instance removes the possibility at the type level rather +than relying on callers to avoid it. + +This is why the buffering above is described by behavior rather than spelled `LineWriter Handle`: +`LineWriter α` and `BufferedWriter α` inherit a `Close` instance from `α`, so the buffering must live +*inside* the newtype rather than the newtype being a type alias for a buffered wrapper. + +Closing a standard descriptor remains possible, but only by naming it: `Handle.ofFd 1 (readable := +false)` yields an ordinary, closable `Handle`. That mirrors Rust's requirement to go through an +explicit owned descriptor. The runtime object additionally carries a no-op-close flag, so an FFI path +that reaches a standard handle by another route still cannot wedge the process's output. + +## Pipe and TTY + +`Pipe` (`uv_pipe_t`) and `TTY` (`uv_tty_t`) are `Handle`s refined by known kind. They share +`Handle`'s read/write/close and exist as distinct types so that kind-specific operations are available +only where they are meaningful: `TTY.setMode .raw` must not typecheck on a stdout that the shell +redirected to a file. + +| Function | Type | Description | libuv | +| -------------------- | ------------------------------------------------------- | ------------------------------------------------------------------------------------------------------------- | ------------------------- | +| `Pipe.read` | `Pipe → (n : USize) → (buf : ByteArray) → IO ByteArray` | Read up to `n` bytes into `buf`; returns the filled slice. | `uv_read_start` | +| `Pipe.write` | `Pipe → ByteArray → IO Unit` | Write bytes to the pipe. | `uv_write` | +| `Pipe.close` | `Pipe → IO Unit` | Close the pipe and release its resources. | `uv_close` | +| `TTY.read` | `TTY → (n : USize) → (buf : ByteArray) → IO ByteArray` | Read up to `n` bytes into `buf`; returns the filled slice. | `uv_read_start` | +| `TTY.write` | `TTY → ByteArray → IO Unit` | Write bytes to the terminal. | `uv_write` | +| `TTY.close` | `TTY → IO Unit` | Close the terminal handle and release its resources. | `uv_close` | +| `TTY.setMode` | `TTY → TTYMode → IO Unit` | Set the terminal input mode. | `uv_tty_set_mode` | +| `TTY.getWinSize` | `TTY → IO (UInt32 × UInt32)` | Return the terminal's width and height in character cells. | `uv_tty_get_winsize` | +| `TTY.vtermState` | `BaseIO VTermState` | Whether the console can process virtual terminal sequences. Process-wide, not per-handle, on Windows. | `uv_tty_get_vterm_state` | + +```lean +inductive TTYMode where + | normal -- initial/normal mode + | raw -- raw input mode + | rawVT -- raw input mode; on Windows also sets `ENABLE_VIRTUAL_TERMINAL_INPUT` + | io -- binary-safe I/O mode for IPC (POSIX only) +``` + +**Raw mode must be reset at process exit.** `uv_tty_reset_mode` is process-wide and restores the +terminal's original settings; without it a program that enters raw mode and then crashes leaves the +user's shell unusable. A handler registered when raw mode is first entered calls it on exit. + +`Pipe` carries no operations of its own for now. libuv offers `uv_pipe_bind2`, `uv_pipe_connect2`, +`uv_pipe_getsockname`/`getpeername`, `uv_pipe_chmod`, and descriptor passing via +`uv_pipe_pending_count`/`pending_type`, but pipe *servers* overlap with what `Std.Async.Process` and +`Std.Async.TCP` already cover; these are deferred until something needs them. + +## Stream + +`Stream` is a record of closures over any readable/writable endpoint. It stays a closure record rather +than becoming a `[Read α] [Write α]` abstraction because `IO.setStdout : FS.Stream → BaseIO FS.Stream` +replaces the current standard output at runtime with a value of a *different* type — capturing to a +buffer, for instance, which is how the language server intercepts stdout. That requires an +existential, which the closure record provides and typeclass polymorphism does not. + +| Field | Type | Description | +| -------------- | ------------------------------------------ | ---------------------------------------------------------------- | +| `Stream.flush` | `IO Unit` | Flush the stream's output buffers. | +| `Stream.read` | `USize → (buf : ByteArray) → IO ByteArray` | Read up to the given number of bytes into `buf`; an empty result signals EOF. | +| `Stream.write` | `ByteArray → IO Unit` | Write the provided bytes. | +| `Stream.close` | `IO Unit` | Release the underlying endpoint. | + +`read` takes a buffer to match `Read.read` and `Handle.read`, so that wrapping a handle in a +`Stream` does not silently give up the buffer-reuse path. `close` is a field rather than an omission, +so a `Stream` over a temporary file or captured pipe can be released; the constructor for a standard +stream supplies a no-op. + +| Constructor | Type | Description | +| ------------------ | -------------------------------- | ------------------------------------------------------------ | +| `Stream.ofHandle` | `Handle → Stream` | | +| `Stream.ofFile` | `File → Stream` | Sequential (cursor-relative) reads and writes only. | +| `Stream.ofBuffer` | `IO.Ref ByteArray → Stream` | In-memory capture; `close` is a no-op. | + +## Buffering + +Buffering is opt-in and layered over the raw types. `BufferedReader` wraps any `Read`able source; +`BufferedWriter` and `LineWriter` wrap any `Write`able sink. + +| Function | Type | Description | +| -------------------------- | ----------------------------------------------------------------- | -------------------------------------------------------------------------------------------------------------- | +| `BufferedReader.new` | `[Read α] → α → (capacity : USize := 4096) → IO (BufferedReader α)` | Wrap a source with a read buffer of the given capacity. | +| `BufferedReader.read` | `[Read α] → BufferedReader α → (n : USize) → IO ByteArray` | Read `n` bytes, looping until `n` are collected or the source is exhausted. A request of at least `capacity` bytes bypasses the buffer. | +| `BufferedReader.readLine` | `[Read α] → BufferedReader α → IO (Option String)` | Read one line including the trailing newline, or `none` at EOF. Fails on invalid UTF-8. | +| `BufferedReader.readToEnd` | `[Read α] → BufferedReader α → IO ByteArray` | Read the remainder of the source into one `ByteArray`. | +| `BufferedReader.close` | `[Close α] → BufferedReader α → IO Unit` | Close the underlying source. Bytes still in the read buffer are discarded. | +| `BufferedWriter.new` | `α → (capacity : USize := 4096) → IO (BufferedWriter α)` | Wrap a sink with a write buffer of the given capacity. | +| `BufferedWriter.write` | `[Write α] → BufferedWriter α → ByteArray → IO Unit` | Buffer bytes, flushing to the sink when the buffer fills. | +| `BufferedWriter.flush` | `[Write α] → BufferedWriter α → IO Unit` | Flush any buffered output to the sink. | +| `BufferedWriter.close` | `[Write α] → [Close α] → BufferedWriter α → IO Unit` | Flush, then close the underlying sink. | +| `LineWriter.new` | `[Write α] → α → IO (LineWriter α)` | Wrap a sink in a line-buffered writer. | +| `LineWriter.write` | `[Write α] → LineWriter α → ByteArray → IO Unit` | Write bytes, flushing up to and including the last newline. | +| `LineWriter.flush` | `[Write α] → LineWriter α → IO Unit` | Flush any buffered output to the sink. | +| `LineWriter.close` | `[Write α] → [Close α] → LineWriter α → IO Unit` | Flush, then close the underlying sink. | + +## Dir + +`Dir` holds a `uv_dir_t`. + +| Function | Type | Description | libuv | +| -------------- | -------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ---------------------------------- | +| `Dir.openExisting` | `Path → IO Dir` | Open a directory for iteration. | `uv_fs_opendir` | +| `Dir.withDir` | `Path → (Dir → IO α) → IO α` | Open a directory, run an action, close in a `finally` block. | `uv_fs_opendir` + `uv_fs_closedir` | +| `Dir.close` | `Dir → IO Unit` | Explicitly close the directory handle. | `uv_fs_closedir` | +| `Dir.next` | `Dir → IO (Option DirEntry)` | Return the next entry, or `none` when exhausted. Order is filesystem-defined. | `uv_fs_readdir` | +| `Dir.drain` | `Dir → IO (Array DirEntry)` | Drain every remaining entry via repeated `next`. Backs `readDir` and `FS.walk`. | `uv_fs_readdir` | +| `Dir.path` | `Dir → Path` | The path the directory was opened at. | | +| `Dir.iter` | `Dir → IO (IterM (α := DirIterator) IO DirEntry)` | Lazy iterator over directory entries. Each step calls `readdir`. Works with `for entry in dir.iter do` and all `IterM` combinators. | `uv_fs_readdir` | +| `Dir.metadata` | `Dir → IO Metadata` | Return metadata for the directory itself. `uv_fs_opendir` does not expose a file descriptor, so this stats `dir.path` rather than the open handle. | `uv_fs_stat` | + +## DirEntry + +`DirEntry` is produced by `Dir.next`. It holds the parent `Dir` so its open methods can construct full paths as `dir.path / entry.fileName`. It already exists as `IO.FS.DirEntry` so it's included here for completeness. + +| Function | Type | Description | libuv | +| ------------------- | ------------------------ | ------------------------------------------------------------------------------------------------------------- | ------------------------------ | +| `DirEntry.dir` | `DirEntry → Dir` | The directory this entry was read from. | | +| `DirEntry.fileName` | `DirEntry → Path.Filename` | The entry name within its parent directory. | | +| `DirEntry.path` | `DirEntry → Path` | Full path, constructed as `dir.path / entry.fileName`. | | +| `DirEntry.fileType` | `DirEntry → IO FileType` | Return the file type *without* following symlinks: a symlink reports `.symlink`, not its target's type. | `uv_fs_lstat` | +| `DirEntry.isDir` | `DirEntry → IO Bool` | Return `true` if the entry is a directory (not a symlink to one). Convenience wrapper around `fileType`. | `uv_fs_lstat` | +| `DirEntry.metadata` | `DirEntry → IO Metadata` | Return full metadata for the entry, following symlinks. Always issues a `stat` call; use `fileType` when only the type is needed. | `uv_fs_stat` | + +## FS Operations + +These functions operate on the filesystem by path. They live in the `FS` namespace rather than `Path` because `Path` is a pure value type for path manipulation; IO operations belong in `FS`. + +| Function | Type | Description | libuv | +| ----------------- | ----------------------------------------------------------------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ----------------------------------------------------------------------- | +| `FS.copyFile` | `Path → Path → IO Unit` | Copy a file. | `uv_fs_copyfile` | +| `FS.removeFile` | `Path → IO Unit` | Delete a file. | `uv_fs_unlink` | +| `FS.removeDir` | `Path → IO Unit` | Remove an empty directory. Fails if the directory is not empty. | `uv_fs_rmdir` | +| `FS.removeDirAll` | `Path → (ignoreErrors : Bool := false) → IO Unit` | Remove a directory and all its contents recursively. If `ignoreErrors`, entries that fail to remove (e.g. permission denied) are skipped instead of aborting, on a best-effort basis. | `FS.readDir` + `uv_fs_unlink` + `uv_fs_rmdir` | +| `FS.createDir` | `Path → (perm : FileRight := .defaultDir) → IO Unit` | Create a directory. Parent must exist. `perm` sets the initial mode bits (default `0o755`). | `uv_fs_mkdir` | +| `FS.createDirAll` | `Path → (perm : FileRight := .defaultDir) → IO Unit` | Create a directory and all missing parent directories. No-op if the directory already exists. `perm` is applied to newly created directories only. | `uv_fs_mkdir` (repeated) | +| `FS.rename` | `Path → Path → IO Unit` | Rename or move a file or directory. | `uv_fs_rename` | +| `FS.hardLink` | `(orig link : Path) → IO Unit` | Create a hard link at `link` pointing to `orig`. Both paths must be on the same filesystem. | `uv_fs_link` | +| `FS.copyDir` | `(src dst : Path) → (ignoreErrors : Bool := false) → IO Unit` | Recursively copy a directory tree from `src` to `dst`. `dst` must not exist; creates it with the same permission bits as `src`. Files are copied via `uv_fs_copyfile`. Symlinks are recreated verbatim rather than followed. If `ignoreErrors`, entries that fail to copy are skipped instead of aborting, on a best-effort basis. | `uv_fs_copyfile` + `FS.readDir` | +| `FS.chown` | `Path → (uid gid : UInt32) → IO Unit` | Change the owner and group of the file or directory at `path`. Follows symlinks. On Windows this is a no-op. | `uv_fs_chown` | +| `FS.lchown` | `Path → (uid gid : UInt32) → IO Unit` | Like `FS.chown` but operates on the symlink itself rather than its target. On Windows this is a no-op. | `uv_fs_lchown` | +| `FS.truncate` | `Path → (len : UInt64) → IO Unit` | Truncate or extend the file at `path` to exactly `len` bytes. Follows symlinks. Complement to `File.setLength` for callers that do not have an open fd; libuv has no path-based `truncate`, so this opens the file `.readWrite` internally. | `uv_fs_open` + `uv_fs_ftruncate` + `uv_fs_close` | + +## Convenience + +| Function | Type | Description | libuv | +| ------------------- | ---------------------------- | --------------------------------------------------------------------------------------------------------- | -------------------------------------------- | +| `FS.readFile` | `Path → IO String` | Read an entire UTF-8 file into a string. Fails on invalid UTF-8. | `uv_fs_open` + `uv_fs_read` + `uv_fs_close` | +| `FS.readBinFile` | `Path → IO ByteArray` | Read an entire file into a `ByteArray`. | `uv_fs_open` + `uv_fs_read` + `uv_fs_close` | +| `FS.lines` | `Path → IO (Array String)` | Read all lines of a UTF-8 file into an array. Implemented via `BufferedReader`. | `uv_fs_open` + `uv_fs_read` + `uv_fs_close` | +| `FS.writeFile` | `Path → String → IO Unit` | Write a UTF-8 string to a file, creating or truncating it. | `uv_fs_open` + `uv_fs_write` + `uv_fs_close` | +| `FS.writeBinFile` | `Path → ByteArray → IO Unit` | Write bytes to a file, creating or truncating it. | `uv_fs_open` + `uv_fs_write` + `uv_fs_close` | +| `FS.appendFile` | `Path → ByteArray → IO Unit` | Append bytes to a file, creating it if it does not exist. | `uv_fs_open` + `uv_fs_write` + `uv_fs_close` | +| `FS.appendTextFile` | `Path → String → IO Unit` | Append a UTF-8 string to a file, creating it if it does not exist. | `uv_fs_open` + `uv_fs_write` + `uv_fs_close` | +| `FS.readDir` | `Path → IO (Array DirEntry)` | List all entries in a directory. Order is filesystem-defined; use `FS.readDirSorted` for stable ordering. | `uv_fs_opendir` + `uv_fs_readdir` + `uv_fs_closedir` | +| `FS.readDirSorted` | `Path → IO (Array DirEntry)` | Like `FS.readDir` but sorted by name. | `uv_fs_opendir` + `uv_fs_readdir` + `uv_fs_closedir` | + +## Temporary Files + +`Std.FS.tempDir` (`IO Path`) resolves the system temp directory (`%TEMP%`/`%TMP%` on Windows, `$TMPDIR` on POSIX, falling back to a platform default), not hardcoded to `"/tmp"`. Following `std::env::temp_dir` + `tempfile`'s `tempdir`/`tempdir_in` split, each operation comes in a plain form (creates in `Std.FS.tempDir`) and an `*In` form (creates inside a caller-supplied `dir`), rather than a single function taking `Option Path`: an always-required `dir` parameter composes with a trailing closure without the caller needing to pass an explicit `none` first. + +| Function | Type | Description | libuv | +| ---------------------- | ---------------------------------- | ---------------------------------------------------------------------------------- | ----------------------------------- | +| `FS.createTempFile` | `IO (File × Path)` | Create a secure temporary file in `Std.FS.tempDir`. Caller is responsible for deleting it. | `uv_fs_mkstemp` | +| `FS.createTempFileIn` | `Path → IO (File × Path)` | Create a secure temporary file inside `dir`. Caller is responsible for deleting it. | `uv_fs_mkstemp` | +| `FS.createTempDir` | `IO Path` | Create a secure temporary directory in `Std.FS.tempDir`. Caller is responsible for deleting it. | `uv_fs_mkdtemp` | +| `FS.createTempDirIn` | `Path → IO Path` | Create a secure temporary directory inside `dir`. Caller is responsible for deleting it. | `uv_fs_mkdtemp` | +| `FS.withTempFile` | `(File → Path → IO α) → IO α` | Create a temporary file in `Std.FS.tempDir`, run an action, delete it in a `finally` block. | `uv_fs_mkstemp` + `uv_fs_unlink` | +| `FS.withTempFileIn` | `Path → (File → Path → IO α) → IO α` | Create a temporary file inside `dir`, run an action, delete it in a `finally` block. | `uv_fs_mkstemp` + `uv_fs_unlink` | +| `FS.withTempDir` | `(Path → IO α) → IO α` | Create a temporary directory in `Std.FS.tempDir`, run an action, delete it recursively in a `finally` block. | `uv_fs_mkdtemp` + `FS.removeDirAll` | +| `FS.withTempDirIn` | `Path → (Path → IO α) → IO α` | Create a temporary directory inside `dir`, run an action, delete it recursively in a `finally` block. | `uv_fs_mkdtemp` + `FS.removeDirAll` | + +## Symlinks + +The current API has `symlinkMetadata` (reads metadata without following the link), but no way to create symlinks or read their targets. `hardLink` is in FS Operations. + +| Function | Type | Description | libuv | +| ------------------ | ------------------------------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ---------------- | +| `FS.createSymlink` | `(target : Path) → (link : Path) → (dir : Bool := false) → IO Unit` | Create a symbolic link at `link` pointing to `target`. `target` is stored verbatim and need not exist at creation time. The `dir` flag is required on Windows (`UV_FS_SYMLINK_DIR`) when the target is a directory; on POSIX it is ignored. | `uv_fs_symlink` | +| `FS.readSymlink` | `Path → IO Path` | Read the raw target of a symbolic link without resolving it. Contrast with `Path.canonicalize` which follows the full chain. | `uv_fs_readlink` | + +## Metadata + +Timestamps use `Std.Time.Timestamp`. `creationTime` is `Option Timestamp` because Linux does not expose file creation time; libuv signals absence by falling back to another timestamp rather than reporting it, so the current implementation always produces `some` and the value is best-effort. + +```lean +structure Metadata where + accessed : Timestamp + modified : Timestamp + creationTime : Option Timestamp + byteSize : UInt64 + type : FileType + numLinks : UInt64 + permissions : FileRight + inode : Option UInt64 -- none on FAT32 and some network filesystems + device : Option UInt64 -- none on FAT32 and some network filesystems + uid : Option UInt32 -- owner user ID; none on Windows + gid : Option UInt32 -- owner group ID; none on Windows +``` + +| Function | Type | Description | libuv | +| ---------------------- | ------------------------------------------------------------------ | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ---------------- | +| `FS.metadata` | `Path → IO Metadata` | Return metadata for a path, following symlinks. | `uv_fs_stat` | +| `FS.symlinkMetadata` | `Path → IO Metadata` | Return metadata for a path without following the final symlink. | `uv_fs_lstat` | +| `FS.isDir` | `Path → BaseIO Bool` | Return `true` if the path exists and is a directory. Returns `false` on any error. | `uv_fs_stat` | +| `FS.isFile` | `Path → BaseIO Bool` | Return `true` if the path exists and is a regular file. Returns `false` on any error. | `uv_fs_stat` | +| `FS.isSymlink` | `Path → BaseIO Bool` | Return `true` if the path is a symbolic link without following it. Returns `false` on any error. | `uv_fs_lstat` | +| `FS.pathExists` | `Path → BaseIO Bool` | Return `true` if the path exists (as any file type). Returns `false` on any error. | `uv_fs_stat` | +| `FS.getPermissions` | `Path → IO FileRight` | Return permission bits by path. Follows symlinks. | `uv_fs_stat` | +| `FS.setPermissions` | `Path → FileRight → IO Unit` | Set permission bits by path. Follows symlinks. | `uv_fs_chmod` | +| `FS.setTimes` | `Path → (accessed : Timestamp) → (modified : Timestamp) → IO Unit` | Set both access and modification timestamps by path. | `uv_fs_utime` | +| `FS.setSymlinkTimes` | `Path → (accessed : Timestamp) → (modified : Timestamp) → IO Unit` | Like `FS.setTimes` but operates on the symlink itself rather than its target. | `uv_fs_lutime` | +| `File.getPermissions` | `File → IO FileRight` | Return the open file's current permission bits. | `uv_fs_fstat` | +| `FS.filesystemStats` | `Path → IO FilesystemStats` | Return filesystem-level statistics (total/free space, inode counts) for the filesystem containing `path`. | `uv_fs_statfs` | +| `Metadata.sameFile` | `Metadata → Metadata → Bool` | Return `true` if two `Metadata` values refer to the same underlying file, compared by `inode` and `device`. Returns `false` if either has no inode (e.g. FAT32). | | + +### FilesystemStats + +```lean +structure FilesystemStats where + type : UInt64 -- filesystem type identifier, as reported by the OS + blockSize : UInt64 -- fundamental block size, in bytes + blocks : UInt64 -- total number of blocks + blocksFree : UInt64 -- free blocks + blocksAvailable : UInt64 -- free blocks available to unprivileged users + files : UInt64 -- total number of file nodes (inodes) + filesFree : UInt64 -- free file nodes +``` + +## Directory Utilities + +| Function | Type | Description | libuv | +| --------- | --------------------------------------------------- | --------------------------------- | -------------------------------------- | +| `FS.walk` | `Path → (ignoreErrors : Bool := false) → IO (IterM (α := WalkIterator) IO DirEntry)` | Lazy recursive directory walk. If `ignoreErrors`, a subtree that fails to open or read (e.g. permission denied) is skipped instead of aborting the whole walk; the directory entry itself is still yielded. The top-level `dir` is not covered by `ignoreErrors` and still raises on failure. | `uv_fs_opendir` + `uv_fs_readdir` + `uv_fs_closedir` | +| `FS.glob` | `Path → String → (ignoreErrors : Bool := false) → IO (Array DirEntry)` | Recursively list all entries beneath `dir` whose full path matches a `/`-separated glob `pattern` (`Path.matchGlob`). Built on `FS.walk`. | `uv_fs_opendir` + `uv_fs_readdir` + `uv_fs_closedir` | + +## Shared Plumbing + +A few conversion helpers are public rather than private so that `Std.Async.FS` can reuse them instead +of duplicating the conversion. They are not part of the intended user-facing surface. + +| Function | Type | Description | +| ------------------------------ | ------------------------------------------- | --------------------------------------------------------------------------- | +| `File.ofInternal` | `Internal.FS.File → File` | Wrap an already-open internal file, for the async open/create/temp helpers. | +| `File.toInternal` | `File → Internal.FS.File` | The underlying internal file (read-only; `File.mk` stays private). | +| `Dir.ofInternal` | `Internal.FS.Dir → Path → Dir` | Wrap an internal directory stream already opened at `path`. | +| `FS.metadataOfStat` | `Internal.FS.Stat → Metadata` | Build a `Metadata` from a raw stat result. | +| `FS.filesystemStatsOfStatFS` | `Internal.FS.StatFS → FilesystemStats` | Build a `FilesystemStats` from a raw statfs result. | +| `FS.timestampToFloatSeconds` | `Timestamp → Float` | Convert to the `Float` seconds that `uv_fs_utime`/`futime` take. | + +# Async Variants + +Everything in `Std.Async.FS` returns `Async α` rather than `IO α`, and lives in the same namespace as +its synchronous counterpart (`Std.FS.File.*Async`, `Std.FS.*Async`). Unless noted, each `*Async` +function has the same signature and semantics as the function it mirrors, with `IO` replaced by +`Async`. + +## File + +| Function | Type | Notes | +| ---------------------------- | ---------------------------------------------------------------------------------------- | ------------------------------------------------------------------------- | +| `File.openExistingAsync` | `Path → (mode : OpenMode := .readOnly) → Async File` | | +| `File.createAsync` | `Path → (mode : OpenMode := .writeCreate) → (perm : FileRight := .default) → Async File` | | +| `File.withFileAsync` | `Path → (mode : OpenMode := .readOnly) → (File → Async α) → Async α` | | +| `File.closeAsync` | `File → Async Unit` | | +| `File.readAtAsync` | `File → (offset : UInt64) → (n : USize) → (_buf : ByteArray) → Async ByteArray` | The async primitive has no buffer-reuse fast path, so `_buf` is accepted only for signature parity and is ignored. | +| `File.writeAtAsync` | `File → (offset : UInt64) → ByteArray → Async Unit` | | +| `File.writeAsync` | `File → ByteArray → Async Unit` | | +| `File.syncAllAsync` | `File → Async Unit` | | +| `File.syncDataAsync` | `File → Async Unit` | | +| `File.sendFileAsync` | `(src dst : File) → (offset : Int64) → (length : USize) → Async USize` | | +| `File.setLengthAsync` | `File → (len : UInt64) → Async Unit` | | +| `File.metadataAsync` | `File → Async Metadata` | | +| `File.getPermissionsAsync` | `File → Async FileRight` | | +| `File.setPermissionsAsync` | `File → FileRight → Async Unit` | | +| `File.setTimesAsync` | `File → (accessed modified : Timestamp) → Async Unit` | | +| `File.chownAsync` | `File → (uid gid : UInt32) → Async Unit` | No-op on Windows. | +| `File.lockAsync` | `File → (exclusive : Bool := true) → Async Unit` | Runs on a dedicated work thread (`uv_queue_work`); see the note below. | +| `File.tryLockAsync` | `File → (exclusive : Bool := true) → Async Bool` | Runs inline; never blocks for an unbounded time. | +| `File.unlockAsync` | `File → Async Unit` | Runs inline; never blocks for an unbounded time. | +| `File.atomicallyAsync` | `File → (exclusive : Bool := true) → Async α → Async α` | | + +`File.putStr`/`File.putStrLn` have no async counterpart; use `writeAsync` with `String.toUTF8`. + +## Handle, Pipe, and TTY + +| Function | Type | Notes | +| ------------------- | ------------------------------------------------------------ | ---------------------------------------------------------------------------- | +| `Handle.readAsync` | `Handle → (n : USize) → Async ByteArray` | Resolves with the bytes read; empty at EOF. | +| `Handle.writeAsync` | `Handle → ByteArray → Async Unit` | | +| `Handle.closeAsync` | `Handle → Async Unit` | | +| `Pipe.readAsync` | `Pipe → (n : USize) → Async ByteArray` | | +| `Pipe.writeAsync` | `Pipe → ByteArray → Async Unit` | | +| `Pipe.closeAsync` | `Pipe → Async Unit` | | +| `TTY.readAsync` | `TTY → (n : USize) → Async ByteArray` | | +| `TTY.writeAsync` | `TTY → ByteArray → Async Unit` | | +| `TTY.closeAsync` | `TTY → Async Unit` | | + +These take no `buf` argument. The synchronous `Handle.read` accepts one because it can hand libuv a +buffer it will fill before the call returns; an async read resolves a `Promise` after the caller has +moved on, so there is no uniquely-owned buffer to reuse and the allocation-avoidance path does not +apply. This matches `File.readAtAsync`, whose `_buf` exists only for signature parity. + +For the `tty` and `pipe` kinds these submit `uv_read_start`/`uv_write` directly and resolve on the +completion callback — no semaphore, no blocked thread. For a `file` kind (redirected stdio) they go +through the same `uv_fs_read`/`uv_fs_write` thread-pool path as `File`'s async operations. + +`TTY.setMode`, `TTY.getWinSize`, and the kind predicates have no async variants: they are +non-blocking calls against local state. + +## Convenience + +| Function | Type | +| ----------------------- | --------------------------------------- | +| `FS.readFileAsync` | `Path → Async String` | +| `FS.readBinFileAsync` | `Path → Async ByteArray` | +| `FS.linesAsync` | `Path → Async (Array String)` | +| `FS.writeFileAsync` | `Path → String → Async Unit` | +| `FS.writeBinFileAsync` | `Path → ByteArray → Async Unit` | +| `FS.appendFileAsync` | `Path → ByteArray → Async Unit` | +| `FS.appendTextFileAsync`| `Path → String → Async Unit` | + +`readBinFileAsync` reads sequentially at the cursor in 64 KiB chunks until EOF, rather than sizing the +buffer from `stat` up front like the synchronous `readBinFile`. + +## FS Operations + +| Function | Type | +| ----------------------- | ----------------------------------------------------------------- | +| `FS.copyFileAsync` | `Path → Path → Async Unit` | +| `FS.removeFileAsync` | `Path → Async Unit` | +| `FS.renameAsync` | `Path → Path → Async Unit` | +| `FS.hardLinkAsync` | `(orig link : Path) → Async Unit` | +| `FS.truncateAsync` | `Path → (len : UInt64) → Async Unit` | +| `FS.chownAsync` | `Path → (uid gid : UInt32) → Async Unit` | +| `FS.lchownAsync` | `Path → (uid gid : UInt32) → Async Unit` | +| `FS.createSymlinkAsync` | `(target link : Path) → (dir : Bool := false) → Async Unit` | +| `FS.readSymlinkAsync` | `Path → Async Path` | +| `FS.resolveAsync` | `Path → Async Path` | + +`FS.resolveAsync` mirrors `Path.resolve` (make absolute and resolve all symlinks) and is backed by +`uv_fs_realpath`. It lives here because there is no async `Path` module. + +## Directories + +| Function | Type | +| ------------------------ | ----------------------------------------------------------------------- | +| `FS.createDirAsync` | `Path → (perm : FileRight := .defaultDir) → Async Unit` | +| `FS.createDirAllAsync` | `Path → (perm : FileRight := .defaultDir) → Async Unit` | +| `FS.removeDirAsync` | `Path → Async Unit` | +| `FS.removeDirAllAsync` | `Path → (ignoreErrors : Bool := false) → Async Unit` | +| `FS.copyDirAsync` | `(src dst : Path) → (ignoreErrors : Bool := false) → Async Unit` | +| `FS.readDirAsync` | `Path → Async (Array DirEntry)` | +| `FS.readDirSortedAsync` | `Path → Async (Array DirEntry)` | +| `FS.walkAsync` | `Path → (ignoreErrors : Bool := false) → Async (Array DirEntry)` | +| `FS.globAsync` | `Path → String → (ignoreErrors : Bool := false) → Async (Array DirEntry)` | + +`Dir` itself has no async surface: there is no `Dir.openExistingAsync`/`nextAsync`/`iterAsync`, so +asynchronous traversal goes through the eager path-keyed helpers above. `walkAsync`/`globAsync` +collect into an `Array` rather than returning a lazy `IterM`, since `Async` has no lazy-iterator +integration yet. + +## Metadata and Permissions + +| Function | Type | +| ---------------------------- | ----------------------------------------------------------------- | +| `FS.metadataAsync` | `Path → Async Metadata` | +| `FS.symlinkMetadataAsync` | `Path → Async Metadata` | +| `FS.isFileAsync` | `Path → Async Bool` | +| `FS.isDirAsync` | `Path → Async Bool` | +| `FS.isSymlinkAsync` | `Path → Async Bool` | +| `FS.pathExistsAsync` | `Path → Async Bool` | +| `FS.getPermissionsAsync` | `Path → Async FileRight` | +| `FS.setPermissionsAsync` | `Path → FileRight → Async Unit` | +| `FS.setTimesAsync` | `Path → (accessed modified : Timestamp) → Async Unit` | +| `FS.setSymlinkTimesAsync` | `Path → (accessed modified : Timestamp) → Async Unit` | +| `FS.filesystemStatsAsync` | `Path → Async FilesystemStats` | + +The four predicates return `Async Bool`, not `BaseIO Bool` as their synchronous counterparts do; they +still swallow every error and answer `false`. + +## Temporary Files + +| Function | Type | +| -------------------------- | ------------------------------------------- | +| `FS.createTempFileAsync` | `Async (File × Path)` | +| `FS.createTempFileInAsync` | `Path → Async (File × Path)` | +| `FS.withTempFileAsync` | `(File → Path → Async α) → Async α` | +| `FS.withTempFileInAsync` | `Path → (File → Path → Async α) → Async α` | +| `FS.createTempDirAsync` | `Async Path` | +| `FS.createTempDirInAsync` | `Path → Async Path` | +| `FS.withTempDirAsync` | `(Path → Async α) → Async α` | +| `FS.withTempDirInAsync` | `Path → (Path → Async α) → Async α` | From f3b18e2f980016dbed5f660bdc51cb6f93dd7deb Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Fri, 24 Jul 2026 14:20:07 -0300 Subject: [PATCH 2/5] feat: add HTTP Pool to be able to reuse connections --- src/Std/Http/Client.lean | 2 +- src/Std/Http/Client/Connector.lean | 80 ++ src/Std/Http/Client/Pool.lean | 297 +++++++ tests/elab/async_http_client_edge_pool.lean | 889 ++++++++++++++++++++ 4 files changed, 1267 insertions(+), 1 deletion(-) create mode 100644 src/Std/Http/Client/Connector.lean create mode 100644 src/Std/Http/Client/Pool.lean create mode 100644 tests/elab/async_http_client_edge_pool.lean diff --git a/src/Std/Http/Client.lean b/src/Std/Http/Client.lean index dfccd3d95046..405fd6b963e4 100644 --- a/src/Std/Http/Client.lean +++ b/src/Std/Http/Client.lean @@ -6,7 +6,7 @@ Authors: Sofia Rodrigues module prelude -public import Std.Http.Client.Agent +public import Std.Http.Client.Pool public section diff --git a/src/Std/Http/Client/Connector.lean b/src/Std/Http/Client/Connector.lean new file mode 100644 index 000000000000..874a9953cbb2 --- /dev/null +++ b/src/Std/Http/Client/Connector.lean @@ -0,0 +1,80 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Std.Http.Client.Session +import Std.Async.DNS + +public section + +/-! +# Connector + +A `Connector` abstracts DNS resolution and TCP/transport connection establishment for the +connection pool. + +The default `Connector.tcp` resolves via the system DNS and dials a raw TCP socket. +-/ + +namespace Std.Http.Client + +open Std Async TCP +open Time + +set_option linter.all true + +/-- +Opens a new transport connection to a target `(scheme, host, port)` and wraps it in a `Session`. + +Supply your own function to customize DNS resolution or transport selection (plain TCP, TLS, +Unix socket). `scheme` is provided so implementations can dispatch between plain and encrypted +transports; `config.proxy` is available for proxy routing. + +Failures are reported as a typed `Error` (usually `Error.connect`). An exception thrown by a +connector is also treated as a connect failure by the pool. +-/ +abbrev Connector := URI.Scheme → URI.Host → UInt16 → Config → Async (Except Error Session) + +/-- +The default connector: resolves `host` via the system DNS, iterates over the returned +addresses, and opens a TCP socket to the first one that succeeds. + +When `config.proxy` is set, the TCP connection is made to the proxy address instead +and the original `host`/`port` are left for the HTTP layer to handle. +-/ +def Connector.tcp : Connector := fun scheme host port config => do + + if scheme.val == "https" then + return .error (.connect "default TCP connector does not support https.") + + if scheme.val != "http" then + return .error (.connect s!"default TCP connector only supports http, got scheme {scheme.val.quote}") + + let (connectHost, connectPort) := config.proxy.getD (toString host, port) + let addrs ← + try DNS.getAddrInfo connectHost (toString connectPort) + catch err => return .error (.connect (toString err)) + + if addrs.isEmpty then + return .error (.connect s!"could not resolve host: {connectHost.quote}") + + let mut lastErr : Error := .connect s!"could not connect to {connectHost.quote}:{connectPort}" + + for ipAddr in addrs do + let socketAddr : Std.Net.SocketAddress := match ipAddr with + | .v4 ip => .v4 ⟨ip, connectPort⟩ + | .v6 ip => .v6 ⟨ip, connectPort⟩ + try + let socket ← Socket.Client.mk + socket.connect socketAddr + return .ok (← Session.new socket config) + catch err => + lastErr := .connect (toString err) + + return .error lastErr + +end Std.Http.Client diff --git a/src/Std/Http/Client/Pool.lean b/src/Std/Http/Client/Pool.lean new file mode 100644 index 000000000000..cb9ebfdf62c1 --- /dev/null +++ b/src/Std/Http/Client/Pool.lean @@ -0,0 +1,297 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Std.Http.Client.Agent +public import Std.Http.Client.Connector +import Init.Data.Array + +public section + +/-! +# Pool + +A simple connection pool that keeps at most one reusable session. + +If the next request targets the current session's origin, the session is reused. If the origin +changes, the current session is retired and a new session is opened for the new origin. + +Use `Pool.new` to create a pool, then call `pool.send` to dispatch requests through managed +sessions. The pool handles redirect following and middlewares. +-/ + +namespace Std.Http.Client + +open Std Async TCP Protocol +open Time + +set_option linter.all true + +/-- +The single reusable session currently held by the pool. +-/ +structure Pool.Slot where + + /-- + Origin this session is connected to. + -/ + origin : URI.Origin + + /-- + The current session. + -/ + session : Session + +/-- +Default number of connection-level retries for pools and clients. One retry absorbs the +stale keep-alive race (the server closed a pooled connection just as it was reused) +without sending any request more than twice. +-/ +def Pool.defaultMaxRetries : Nat := 1 + +/-- +A connection pool that manages one reusable session at a time. +-/ +structure Pool where + + /-- + Current reusable session, if any. + -/ + state : Mutex (Option Pool.Slot) + + /-- + Configuration used when creating new sessions. + -/ + config : Config + + /-- + Monotonically increasing counter for unique session IDs. + -/ + nextId : Mutex UInt64 + + /-- + Middlewares applied (outermost-first) around every request/response hop. + -/ + middlewares : Array Middleware := #[] + + /-- + Function used to open new transport sessions. Supply a custom `Connector` via `Pool.new`. + -/ + connect : Connector := Connector.tcp + + /-- + Maximum number of times to retry a failed request on a fresh connection. `0` disables + retries. + + Retries only apply to connection-level failures (the session died before a response was + received). Application-level errors (4xx, 5xx) are never retried automatically. + + **Only idempotent methods with replayable bodies are retried.** Requests whose method + returns `false` from `Method.isIdempotent` (e.g. `POST`, `PATCH`) are never retried + regardless of this value, to prevent unintended duplicate side-effects. + -/ + maxRetries : Nat := Pool.defaultMaxRetries + +namespace Pool + +/-- +Creates a new, empty connection pool. Supply a custom `connect` function (e.g. a TLS +connector or a mock) to customize how transport sessions are opened. +-/ +def new (config : Config := {}) (connect : Connector := Connector.tcp) + (maxRetries : Nat := Pool.defaultMaxRetries) (middlewares : Array Middleware := #[]) : + Async Pool := do + let state ← Mutex.new (none : Option Pool.Slot) + let nextId ← Mutex.new (1 : UInt64) + pure { state, config, nextId, middlewares, connect, maxRetries } + +/-- +Closes and removes the pool's current session, if any. The pool remains usable: a later +`send` simply opens a fresh connection. +-/ +def close (pool : Pool) : Async Unit := do + let slot ← pool.state.atomically <| modifyGet fun slot => (slot, none) + if let some slot := slot then + discard <| slot.session.close + +/-- +Acquires a fresh unique session ID. +-/ +private def nextSessionId (pool : Pool) : Async UInt64 := + pool.nextId.atomically <| modifyGet fun id => (id, id + 1) + +/-- +Opens a new session for `origin` and assigns it a pool-local ID. The connector runs under +`Config.connectTimeout`, bounding DNS resolution and the transport connect. An exception +thrown by a custom connector is reported as `Error.connect`, keeping every connector-level +failure typed on one path. +-/ +private def openSession (pool : Pool) (origin : URI.Origin) : Async (Except Error Session) := do + let resultChannel : Std.Channel (Except Error Session) ← Std.Channel.new + + let connectTask ← async (t := AsyncTask) do + try + pool.connect origin.scheme origin.host origin.port pool.config + catch err => + pure (.error (.connect (toString err))) + + BaseIO.chainTask connectTask fun + | .ok result => discard <| resultChannel.send result + | .error err => discard <| resultChannel.send (.error (.connect (toString err))) + + let outcome ← Selectable.one #[ + .case resultChannel.recvSelector (fun result => pure (some result)), + .case (← Selector.sleep pool.config.connectTimeout.val) (fun _ => pure none) + ] + + match outcome with + | some (.ok session) => + let id ← nextSessionId pool + return .ok { session with id } + | some (.error e) => return .error e + | none => + -- The connector may still complete after the timeout; drain its result in the + -- background and close the late session so the transport does not leak. + background do + let late ← Selectable.one #[.case resultChannel.recvSelector pure] + if let .ok session := late then + discard <| session.close + return .error (.connect + s!"connecting to {origin.host}:{origin.port} timed out after {pool.config.connectTimeout.val}ms") + +/-- +Returns the pool's single session for `origin`. + +If the current session has the same origin, it is checked out again; HTTP/1.1 requests +queue on the session. If the origin differs, the current session is retired and replaced. + +A new session is opened *outside* the state mutex: DNS resolution and the TCP connect can block, +and holding the lock across them would serialize every other pool operation (including session +retirement). The lock is taken only for the brief fast-path check and to install the freshly +opened session. +-/ +def getOrCreateSession (pool : Pool) (origin : URI.Origin) : Async (Except Error Session) := do + -- Fast path: reuse an existing same-origin session without opening anything. A parked session + -- whose background loop has already shut down (server EOF, idle keep-alive timeout) is evicted + -- instead of returned: handing it out would fail the request even though nothing was ever + -- written to the wire for it. A session can still die between this check and the actual send; + -- that residual race surfaces as a connection error handled by the retry policy in `send`. + let existing ← pool.state.atomically do + match ← get with + | some slot => + if slot.origin == origin then + if ← slot.session.isClosed then + set (none : Option Pool.Slot) + pure none + else + pure (some slot.session) + else + pure none + | none => pure none + if let some session := existing then + return .ok session + + -- Slow path: open a new session with the lock released. + match ← pool.openSession origin with + | .error e => return .error e + | .ok session => + + -- Install it, retiring whatever is parked. If another task installed a same-origin session + -- while we were connecting, keep theirs and discard ours so the pool never holds two live + -- sessions. + let (chosen, evicted) ← pool.state.atomically do + match ← get with + | some slot => + if slot.origin == origin then + pure (slot.session, some session) + else + set (some ({ origin, session } : Pool.Slot)) + pure (session, some slot.session) + | none => + set (some ({ origin, session } : Pool.Slot)) + pure (session, none) + if let some evictedSession := evicted then + discard <| evictedSession.close + return .ok chosen + +/-- +Removes a session from the pool and closes its request channel. +-/ +private def retireSession (pool : Pool) (origin : URI.Origin) (session : Session) : Async Unit := do + pool.state.atomically <| modify fun + | some slot => + if slot.origin == origin && slot.session.id == session.id then none else some slot + | none => none + discard <| session.close + +/-- +Sends a request through the pooled session, following redirects and applying middlewares, +returning the response or the typed `Error` that ended the exchange. +On a retryable connection-level failure (see `Error.isRetryable`), retries up to +`pool.maxRetries` times on fresh connections. Application-level failures (timeouts, +protocol violations, body-size limits) are never retried. + +Session lifecycle is owned by the agent driving the exchange: a failed hop, a cross-origin +redirect swap, or a connection error after the final response hands the session back to the +pool, which retires it. Cross-origin redirects keep the pool to one live origin at a time. +-/ +def trySend {β : Type} [Coe β Body.Any] (pool : Pool) (origin : URI.Origin) (request : Request β) + (overrides : RequestOverrides := {}) : Async (Except Error (Response Body.Stream)) := do + -- Erase the body type once; every layer below the pool works with `Request Body.Any`. + let request : Request Body.Any := { request with } + + -- Non-idempotent methods (POST, PATCH, …) must never be retried; a connection + -- failure after partial delivery could cause duplicate side-effects. + -- The body must also be replayable (`reset?`): the failed attempt may have consumed a + -- streaming body, and retrying would silently send an empty or truncated body. + let reset? := request.body.reset? + let retries := if request.line.method.isIdempotent && reset?.isSome then pool.maxRetries else 0 + + let attempts := retries + 1 + + -- A single attempt: acquire a session and run the exchange. `Agent.trySend` owns session + -- cleanup — every failure path inside it releases the session back to the pool — so the + -- attempt only has to report the typed result to the retry loop below. Connection + -- establishment is part of the attempt so that DNS/TCP failures are retried too. + let attemptOnce : Async (Except Error (Response Body.Stream)) := do + match ← pool.getOrCreateSession origin with + | .error e => return .error e + | .ok session => + Agent.trySend { + session + origin + middlewares := pool.middlewares + release := fun sess o => pool.retireSession o sess + crossOrigin := .follow pool.getOrCreateSession + } request overrides + + for attempt in 0...attempts do + -- A prior attempt may have consumed (part of) the body; rewind it before resending. + if attempt > 0 then + if let some reset := reset? then + reset + match ← attemptOnce with + | .ok response => return .ok response + | .error e => + -- Report on the final attempt or for non-retryable failures; + -- retryable failures fall through to the next attempt. + if ¬e.isRetryable || attempt + 1 ≥ attempts then + return .error e + + -- Unreachable: the loop runs at least once and the final attempt always returns. + return .error (.io (IO.userError "HTTP client retry loop exhausted without returning")) + +/-- +Sends a request through the pooled session, following redirects and applying middlewares. +Use `trySend` to receive failures as a typed `Error` instead of a thrown exception. +-/ +def send {β : Type} [Coe β Body.Any] (pool : Pool) (origin : URI.Origin) (request : Request β) + (overrides : RequestOverrides := {}) : Async (Response Body.Stream) := + pool.trySend origin request overrides >>= Error.throwOrPure + +end Pool +end Std.Http.Client diff --git a/tests/elab/async_http_client_edge_pool.lean b/tests/elab/async_http_client_edge_pool.lean new file mode 100644 index 000000000000..54047f379dda --- /dev/null +++ b/tests/elab/async_http_client_edge_pool.lean @@ -0,0 +1,889 @@ +module + +import Std.Http.Test.Helpers + +open Std.Async +open Std Http Internal +open Test.ClientHelpers + +/-! HTTP client connection-pool, keep-alive, timeout, shutdown, and retry edge cases. -/ + +-- ============================================================ +-- Section 7 — Keep-alive and Connection: close +-- ============================================================ + +-- The simplified pool keeps one session at a time. A same-origin request sent +-- while the previous response body is unread queues on that session and reaches +-- the wire only after the caller closes or drains the previous body. + +#eval show IO _ from runWithTimeout "single-connection pool queues behind unread response body" 4000 <| Async.block do + let (mockClient1, mockServer1) ← Mock.new + let connectCount ← IO.mkRef 0 + + let connect : Client.Connector := fun _ _ _ config => do + let n ← connectCount.get + connectCount.set (n + 1) + match n with + | 0 => return .ok (← Client.Session.new mockServer1 (config := config)) + | _ => throw (IO.userError "pool opened more sessions than expected") + + let pool ← Client.Pool.new {} connect + let some domain := URI.DomainName.ofString? "example.com" + | throw (IO.userError "DomainName parse failed") + let origin : URI.Origin := { + scheme := URI.Scheme.ofString! "http" + host := .name domain + port := 80 + } + + let req1 ← Request.new |>.method .get |>.uri! "/one" + |>.header! "Host" "example.com" |>.empty + let p1 : IO.Promise (Except String (Response Body.Stream)) ← IO.Promise.new + background do + let result ← try + let resp ← pool.send origin req1 + pure (Except.ok resp) + catch e => pure (Except.error (toString e)) + discard <| p1.resolve result + + let _ ← drainRequest mockClient1 + mockClient1.send (rawResp "200 OK" + #[("Content-Length", "5"), ("Connection", "keep-alive")] "hello") + + let resp1 ← match ← await p1.result! with + | Except.error e => throw (IO.userError s!"first pooled request failed: {e}") + | Except.ok resp => pure resp + + let req2 ← Request.new |>.method .get |>.uri! "/two" + |>.header! "Host" "example.com" |>.empty + let p2 : IO.Promise (Except String (Response Body.Stream)) ← IO.Promise.new + background do + let result ← try + let resp ← pool.send origin req2 + pure (Except.ok resp) + catch e => pure (Except.error (toString e)) + discard <| p2.resolve result + + IO.sleep 50 + unless (← connectCount.get) == 1 do + resp1.body.close + mockClient1.close + throw (IO.userError "single-connection pool opened a second same-origin session") + + if let some bytes ← mockClient1.tryRecv? then + resp1.body.close + mockClient1.close + throw (IO.userError s!"queued request reached the wire before the first body was closed:\n{(String.fromUTF8! bytes).quote}") + + resp1.body.close + + let secondBytes ← drainRequest mockClient1 + mockClient1.send (rawResp "200 OK" + #[("Content-Length", "3"), ("Connection", "close")] "two") + + match ← await p2.result! with + | Except.error e => throw (IO.userError s!"second pooled request failed: {e}") + | Except.ok resp2 => + let body ← resp2.body.readAll (α := String) + unless body == "two" do + throw (IO.userError s!"expected second body 'two', got {body.quote}") + + let secondText := String.fromUTF8! secondBytes + unless secondText.startsWith "GET /two" do + throw <| IO.userError s!"second request did not use the queued connection:\n{secondText.quote}" + +-- Once the caller closes an unread pooled response body, the connection loop +-- drains the wire body and reports completion. The pool should then return the +-- session to idle instead of opening another available connection. + +#eval show IO _ from runWithTimeout "pool reuses session after unread response body is closed" 4000 <| Async.block do + let (mockClient1, mockServer1) ← Mock.new + let (_mockClient2, mockServer2) ← Mock.new + let connectCount ← IO.mkRef 0 + + let connect : Client.Connector := fun _ _ _ config => do + let n ← connectCount.get + connectCount.set (n + 1) + match n with + | 0 => return .ok (← Client.Session.new mockServer1 (config := config)) + | 1 => return .ok (← Client.Session.new mockServer2 (config := config)) + | _ => throw (IO.userError "pool opened more sessions than expected") + + let pool ← Client.Pool.new {} connect + let some domain := URI.DomainName.ofString? "example.com" + | throw (IO.userError "DomainName parse failed") + let origin : URI.Origin := { + scheme := URI.Scheme.ofString! "http" + host := .name domain + port := 80 + } + + let req1 ← Request.new |>.method .get |>.uri! "/one" + |>.header! "Host" "example.com" |>.empty + let p1 : IO.Promise (Except String (Response Body.Stream)) ← IO.Promise.new + background do + let result ← try + let resp ← pool.send origin req1 + pure (Except.ok resp) + catch e => pure (Except.error (toString e)) + discard <| p1.resolve result + + let _ ← drainRequest mockClient1 + mockClient1.send (rawResp "200 OK" + #[("Content-Length", "5"), ("Connection", "keep-alive")] "hello") + + let resp1 ← match ← await p1.result! with + | Except.error e => throw (IO.userError s!"first pooled request failed: {e}") + | Except.ok resp => pure resp + + resp1.body.close + IO.sleep 50 + + let req2 ← Request.new |>.method .get |>.uri! "/two" + |>.header! "Host" "example.com" |>.empty + let p2 : IO.Promise (Except String (Response Body.Stream)) ← IO.Promise.new + background do + let result ← try + let resp ← pool.send origin req2 + pure (Except.ok resp) + catch e => pure (Except.error (toString e)) + discard <| p2.resolve result + + IO.sleep 50 + if (← connectCount.get) != 1 then + mockClient1.close + throw (IO.userError "pool opened a second session after the first response body was closed") + + let secondBytes ← drainRequest mockClient1 + mockClient1.send (rawResp "200 OK" + #[("Content-Length", "3"), ("Connection", "close")] "two") + + match ← await p2.result! with + | Except.error e => throw (IO.userError s!"second pooled request failed: {e}") + | Except.ok resp2 => + let body ← resp2.body.readAll (α := String) + unless body == "two" do + throw (IO.userError s!"expected second body 'two', got {body.quote}") + + let secondText := String.fromUTF8! secondBytes + unless secondText.startsWith "GET /two" do + throw <| IO.userError s!"second request did not reuse the first connection:\n{secondText.quote}" + +-- A zero-length pooled response still needs to drive the connection through +-- completion so the session is returned to idle. + +#eval show IO _ from runWithTimeout "pool reuses session after zero-length response body completes" 4000 <| Async.block do + let (mockClient1, mockServer1) ← Mock.new + let (_mockClient2, mockServer2) ← Mock.new + let connectCount ← IO.mkRef 0 + + let connect : Client.Connector := fun _ _ _ config => do + let n ← connectCount.get + connectCount.set (n + 1) + match n with + | 0 => return .ok (← Client.Session.new mockServer1 (config := config)) + | 1 => return .ok (← Client.Session.new mockServer2 (config := config)) + | _ => throw (IO.userError "pool opened more sessions than expected") + + let pool ← Client.Pool.new {} connect + let some domain := URI.DomainName.ofString? "example.com" + | throw (IO.userError "DomainName parse failed") + let origin : URI.Origin := { + scheme := URI.Scheme.ofString! "http" + host := .name domain + port := 80 + } + + let req1 ← Request.new |>.method .get |>.uri! "/empty" + |>.header! "Host" "example.com" |>.empty + let p1 : IO.Promise (Except String (Response Body.Stream)) ← IO.Promise.new + background do + let result ← try + let resp ← pool.send origin req1 + pure (Except.ok resp) + catch e => pure (Except.error (toString e)) + discard <| p1.resolve result + + let _ ← drainRequest mockClient1 + mockClient1.send (rawResp "200 OK" + #[("Content-Length", "0"), ("Connection", "keep-alive")] "") + + match ← await p1.result! with + | Except.error e => throw (IO.userError s!"first pooled request failed: {e}") + | Except.ok resp1 => + let body ← resp1.body.readAll (α := String) + unless body == "" do + throw (IO.userError s!"expected empty first body, got {body.quote}") + + IO.sleep 50 + + let req2 ← Request.new |>.method .get |>.uri! "/two" + |>.header! "Host" "example.com" |>.empty + let p2 : IO.Promise (Except String (Response Body.Stream)) ← IO.Promise.new + background do + let result ← try + let resp ← pool.send origin req2 + pure (Except.ok resp) + catch e => pure (Except.error (toString e)) + discard <| p2.resolve result + + IO.sleep 50 + if (← connectCount.get) != 1 then + mockClient1.close + throw (IO.userError "pool opened a second session after a zero-length response completed") + + let secondBytes ← drainRequest mockClient1 + mockClient1.send (rawResp "200 OK" + #[("Content-Length", "3"), ("Connection", "close")] "two") + + match ← await p2.result! with + | Except.error e => throw (IO.userError s!"second pooled request failed: {e}") + | Except.ok resp2 => + let body ← resp2.body.readAll (α := String) + unless body == "two" do + throw (IO.userError s!"expected second body 'two', got {body.quote}") + + let secondText := String.fromUTF8! secondBytes + unless secondText.startsWith "GET /two" do + throw <| IO.userError s!"second request did not reuse the first connection:\n{secondText.quote}" + +-- A different origin replaces the pool's single current session. + +#eval show IO _ from runWithTimeout "single-connection pool replaces session on origin change" 4000 <| Async.block do + let (mockClient1, mockServer1) ← Mock.new + let (mockClient2, mockServer2) ← Mock.new + let connectCount ← IO.mkRef 0 + + let connect : Client.Connector := fun _ _ _ config => do + let n ← connectCount.get + connectCount.set (n + 1) + match n with + | 0 => return .ok (← Client.Session.new mockServer1 (config := config)) + | 1 => return .ok (← Client.Session.new mockServer2 (config := config)) + | _ => throw (IO.userError "pool opened more sessions than expected") + + let pool ← Client.Pool.new {} connect + let some domain1 := URI.DomainName.ofString? "example.com" + | throw (IO.userError "DomainName parse failed") + let some domain2 := URI.DomainName.ofString? "other.example" + | throw (IO.userError "DomainName parse failed") + let origin1 : URI.Origin := { + scheme := URI.Scheme.ofString! "http" + host := .name domain1 + port := 80 + } + let origin2 : URI.Origin := { + scheme := URI.Scheme.ofString! "http" + host := .name domain2 + port := 80 + } + + let req1 ← Request.new |>.method .get |>.uri! "/one" + |>.header! "Host" "example.com" |>.empty + let p1 : IO.Promise (Except String (Response Body.Stream)) ← IO.Promise.new + background do + let result ← try + let resp ← pool.send origin1 req1 + pure (Except.ok resp) + catch e => pure (Except.error (toString e)) + discard <| p1.resolve result + + let _ ← drainRequest mockClient1 + mockClient1.send (rawResp "200 OK" + #[("Content-Length", "0"), ("Connection", "keep-alive")] "") + + match ← await p1.result! with + | Except.error e => throw (IO.userError s!"first pooled request failed: {e}") + | Except.ok resp1 => + let body ← resp1.body.readAll (α := String) + unless body == "" do + throw (IO.userError s!"expected empty body, got {body.quote}") + + IO.sleep 50 + + let req2 ← Request.new |>.method .get |>.uri! "/two" + |>.header! "Host" "other.example" |>.empty + let p2 : IO.Promise (Except String (Response Body.Stream)) ← IO.Promise.new + background do + let result ← try + let resp ← pool.send origin2 req2 + pure (Except.ok resp) + catch e => pure (Except.error (toString e)) + discard <| p2.resolve result + + match ← mockClient1.recv? with + | none => pure () + | some bytes => + mockClient1.close + mockClient2.close + throw (IO.userError s!"old-origin connection stayed open after origin change:\n{(String.fromUTF8! bytes).quote}") + + let secondBytes ← drainRequest mockClient2 + mockClient2.send (rawResp "200 OK" + #[("Content-Length", "3"), ("Connection", "close")] "two") + + match ← await p2.result! with + | Except.error e => throw (IO.userError s!"second-origin request failed: {e}") + | Except.ok resp2 => + let body ← resp2.body.readAll (α := String) + unless body == "two" do + throw (IO.userError s!"expected second body 'two', got {body.quote}") + + unless (← connectCount.get) == 2 do + throw (IO.userError "origin change did not open exactly one replacement session") + let secondText := String.fromUTF8! secondBytes + unless secondText.startsWith "GET /two" do + throw <| IO.userError s!"second-origin request did not use the replacement connection:\n{secondText.quote}" + +-- If a pooled cross-origin redirect leaves the original origin, the outgoing +-- session is retired instead of being returned idle. A target-acquire failure +-- must close that old session and leave the pool able to open a clean +-- replacement for the original origin. + +#eval show IO _ from runWithTimeout "failed cross-origin redirect retires old session and keeps pool usable" 4000 <| Async.block do + let (mockClient1, mockServer1) ← Mock.new + let (mockClient2, mockServer2) ← Mock.new + let originalConnectCount ← IO.mkRef 0 + + let connect : Client.Connector := fun _scheme host _port config => do + if toString host == "other.example" then + throw (IO.userError s!"redirect target dial failed for {host}") + else + let n ← originalConnectCount.get + originalConnectCount.set (n + 1) + match n with + | 0 => return .ok (← Client.Session.new mockServer1 (config := config)) + | 1 => return .ok (← Client.Session.new mockServer2 (config := config)) + | _ => throw (IO.userError "opened too many original-origin sessions") + + -- Retries are disabled: this test asserts the state the pool is left in after a + -- single failed cross-origin acquire, not the retry policy. + let pool ← Client.Pool.new {} connect (maxRetries := 0) + let some domain := URI.DomainName.ofString? "example.com" + | throw (IO.userError "DomainName parse failed") + let origin : URI.Origin := { + scheme := URI.Scheme.ofString! "http" + host := .name domain + port := 80 + } + + let req1 ← Request.new |>.method .get |>.uri! "/start" + |>.header! "Host" "example.com" |>.empty + let p1 : IO.Promise (Except String (Response Body.Stream)) ← IO.Promise.new + background do + let result ← try + let resp ← pool.send origin req1 + pure (Except.ok resp) + catch e => pure (Except.error (toString e)) + discard <| p1.resolve result + + let _ ← drainRequest mockClient1 + mockClient1.send (rawResp "302 Found" + #[("Location", "http://other.example/landing"), + ("Content-Length", "0"), + ("Connection", "keep-alive")] "") + + match ← await p1.result! with + | Except.ok _ => + mockClient1.close + mockClient2.close + throw (IO.userError "redirect unexpectedly succeeded") + | Except.error e => + unless e.contains "redirect target dial failed" do + mockClient1.close + mockClient2.close + throw (IO.userError s!"unexpected redirect failure: {e}") + + match ← mockClient1.recv? with + | none => pure () + | some bytes => + mockClient1.close + mockClient2.close + throw (IO.userError s!"retired redirect source connection stayed readable:\n{(String.fromUTF8! bytes).quote}") + + let req2 ← Request.new |>.method .get |>.uri! "/again" + |>.header! "Host" "example.com" |>.empty + let p2 : IO.Promise (Except String (Response Body.Stream)) ← IO.Promise.new + background do + let result ← try + let resp ← pool.send origin req2 + pure (Except.ok resp) + catch e => pure (Except.error (toString e)) + discard <| p2.resolve result + + IO.sleep 50 + if (← originalConnectCount.get) != 2 then + mockClient1.close + mockClient2.close + throw (IO.userError "pool did not open a replacement original-origin session for the follow-up request") + + let secondBytes ← drainRequest mockClient2 + mockClient2.send (rawResp "200 OK" + #[("Content-Length", "2"), ("Connection", "close")] "ok") + + match ← await p2.result! with + | Except.error e => throw (IO.userError s!"original session was not reused after failed redirect acquire: {e}") + | Except.ok resp => + let body ← resp.body.readAll (α := String) + unless body == "ok" do + throw (IO.userError s!"expected second response body 'ok', got {body.quote}") + + let secondText := String.fromUTF8! secondBytes + unless secondText.startsWith "GET /again" do + throw <| IO.userError s!"second request did not use the replacement connection:\n{secondText.quote}" + +-- Two sequential requests on the same session must both succeed, exercising the +-- `.next` reset path in the connection state machine. + +#eval show IO _ from runWithTimeout "two sequential GETs on keep-alive succeed" 4000 <| Async.block do + let (mockClient, mockServer) ← Mock.new + let agent ← mkAgent mockServer + + -- First request. + let req1 ← Request.new |>.method .get |>.uri! "/one" + |>.header! "Host" "example.com" |>.empty + let p1 ← sendInBackground agent req1 + + let _ ← drainRequest mockClient + mockClient.send (rawResp "200 OK" + #[("Content-Length", "3"), ("Connection", "keep-alive")] "one") + + match ← await p1.result! with + | Except.error e => throw (IO.userError s!"first request failed: {e}") + | Except.ok resp => + let body ← resp.body.readAll (α := String) + unless body == "one" do + throw (IO.userError s!"expected 'one', got {body.quote}") + + -- Second request on same session must succeed. + let req2 ← Request.new |>.method .get |>.uri! "/two" + |>.header! "Host" "example.com" |>.empty + let p2 ← sendInBackground agent req2 + + let _ ← drainRequest mockClient + mockClient.send (rawResp "200 OK" + #[("Content-Length", "3"), ("Connection", "close")] "two") + + match ← await p2.result! with + | Except.error e => throw (IO.userError s!"second request failed: {e}") + | Except.ok resp => + let body ← resp.body.readAll (α := String) + unless body == "two" do + throw (IO.userError s!"expected 'two', got {body.quote}") + +-- `Connection: close` on the response must close the session; a follow-up request +-- on the same session must error out rather than hang. + +#eval show IO _ from runWithTimeout "Connection: close prevents reuse" 4000 <| Async.block do + let (mockClient, mockServer) ← Mock.new + let agent ← mkAgent mockServer + + let req1 ← Request.new |>.method .get |>.uri! "/" + |>.header! "Host" "example.com" |>.empty + let p1 ← sendInBackground agent req1 + + let _ ← drainRequest mockClient + mockClient.send (rawResp "200 OK" + #[("Content-Length", "2"), ("Connection", "close")] "ok") + + match ← await p1.result! with + | Except.error e => throw (IO.userError s!"first request failed: {e}") + | Except.ok resp => + let _ ← resp.body.readAll (α := String) + + -- Close the mock's receive side so the session observes EOF. + mockClient.close + + -- Second send must not hang; it must fail because the session is closed. + let req2 ← Request.new |>.method .get |>.uri! "/" + |>.header! "Host" "example.com" |>.empty + let p2 ← sendInBackground agent req2 + + match ← await p2.result! with + | Except.ok _ => + throw (IO.userError "second request unexpectedly succeeded after Connection: close") + | Except.error _ => pure () + +-- ============================================================ +-- Section 12 — Request deadline and session close +-- ============================================================ + +-- The absolute `requestTimeout` deadline must abort a response whose body stalls after the headers +-- arrive, surfacing the error to a caller blocked reading the body (rather than hanging until the +-- much larger per-read idle timeout). +#eval show IO _ from runWithTimeout "request deadline aborts a stalled response body" 4000 <| Async.block do + let (mockClient, mockServer) ← Mock.new + let agent ← mkAgent mockServer (config := { requestTimeout := ⟨300, by decide⟩ }) + + let request ← Request.new + |>.method .get + |>.uri! "/slow" + |>.header! "Host" "example.com" + |>.empty + + let resultPromise ← sendInBackground agent request + + let _ ← drainRequest mockClient + -- Promise a 10-byte body but never send it: the exchange must hit the request deadline. + mockClient.send (rawResp "200 OK" + #[("Content-Length", "10"), ("Connection", "close")] "") + + match ← await resultPromise.result! with + | Except.error _ => + -- Deadline surfaced before the headers were returned — still a valid enforcement. + pure () + | Except.ok resp => + let got : Except String String ← try + let s ← resp.body.readAll (α := String) + pure (Except.ok s) + catch e => pure (Except.error (toString e)) + match got with + | Except.error _ => pure () + | Except.ok s => + throw (IO.userError s!"expected request-timeout error on stalled body, read {s.quote}") + +-- Incoming progress must not re-arm the whole-request timeout. A server can keep the idle timer +-- alive by dripping bytes, but the absolute request deadline must still end the exchange. +#eval show IO _ from runWithTimeout "request deadline aborts a slow-drip response body" 4000 <| Async.block do + let (mockClient, mockServer) ← Mock.new + let agent ← mkAgent mockServer (config := { requestTimeout := ⟨250, by decide⟩ }) + + let request ← Request.new |>.method .get |>.uri! "/slow-drip" + |>.header! "Host" "example.com" |>.empty + let resultPromise ← sendInBackground agent request + + let _ ← drainRequest mockClient + mockClient.send (rawResp "200 OK" + #[("Content-Length", "5"), ("Connection", "keep-alive")] "") + background do + for byte in #["a", "b", "c", "d", "e"] do + IO.sleep 100 + try mockClient.send byte.toUTF8 catch _ => pure () + + match ← await resultPromise.result! with + | Except.error _ => pure () + | Except.ok resp => + let result : Except String String ← try + pure (Except.ok (← resp.body.readAll (α := String))) + catch e => pure (Except.error (toString e)) + match result with + | Except.error _ => pure () + | Except.ok body => + throw (IO.userError s!"slow-drip response escaped request deadline with {body.quote}") + +-- `Session.close` must abort an in-flight exchange promptly (via the connection's cancellation +-- context), not leave the caller blocked until the request timeout. The request timeout below is set +-- far beyond the test budget so that only `close` can end the request; without the context wiring the +-- background loop stays parked on the socket and this test times out. +#eval show IO _ from runWithTimeout "session close aborts an in-flight request" 4000 <| Async.block do + let (mockClient, mockServer) ← Mock.new + let agent ← mkAgent mockServer (config := { requestTimeout := ⟨60000, by decide⟩ }) + + let request ← Request.new + |>.method .get + |>.uri! "/never-answered" + |>.header! "Host" "example.com" + |>.empty + + let resultPromise ← sendInBackground agent request + + -- Server receives the request but never responds; only close should end it. + let _ ← drainRequest mockClient + agent.session.close + + match ← await resultPromise.result! with + | Except.error _ => pure () + | Except.ok _ => + throw (IO.userError "expected in-flight request to abort when the session is closed") + +-- Opening a transport must not hold the pool state mutex. The first connector is deliberately +-- blocked; a second-origin acquisition must enter its connector before the first is released. +#eval show IO _ from runWithTimeout "pool does not hold state mutex while connecting" 4000 <| Async.block do + let (_mockClient1, mockServer1) ← Mock.new + let (_mockClient2, mockServer2) ← Mock.new + let calls ← Std.Mutex.new 0 + let firstStarted : IO.Promise Unit ← IO.Promise.new + let releaseFirst : IO.Promise Unit ← IO.Promise.new + let released ← IO.mkRef false + let secondSawReleased ← IO.mkRef true + + let connect : Client.Connector := fun _ _ _ config => do + let callNo ← calls.atomically <| modifyGet fun n => (n, n + 1) + if callNo == 0 then + discard <| firstStarted.resolve () + await releaseFirst.result! + return .ok (← Client.Session.new mockServer1 (config := config)) + else + secondSawReleased.set (← released.get) + return .ok (← Client.Session.new mockServer2 (config := config)) + + let pool ← Client.Pool.new {} connect + let some domainA := URI.DomainName.ofString? "a.example" + | throw (IO.userError "DomainName parse failed") + let some domainB := URI.DomainName.ofString? "b.example" + | throw (IO.userError "DomainName parse failed") + let originA : URI.Origin := { + scheme := URI.Scheme.ofString! "http", host := .name domainA, port := 80 } + let originB : URI.Origin := { + scheme := URI.Scheme.ofString! "http", host := .name domainB, port := 80 } + + let firstDone : IO.Promise Unit ← IO.Promise.new + let secondDone : IO.Promise Unit ← IO.Promise.new + + background do + let .ok session ← pool.getOrCreateSession originA + | throw (IO.userError "first-origin session acquisition failed") + discard <| firstDone.resolve () + session.close + await firstStarted.result! + background do + let .ok session ← pool.getOrCreateSession originB + | throw (IO.userError "second-origin session acquisition failed") + discard <| secondDone.resolve () + session.close + background do + IO.sleep 300 + released.set true + discard <| releaseFirst.resolve () + + await secondDone.result! + if ← secondSawReleased.get then + throw (IO.userError "second connection was blocked behind the pool state mutex") + await firstDone.result! + +-- Idempotent requests retry a connector failure, including a failure before a `Session` exists. +#eval show IO _ from runWithTimeout "GET retries after the first connection attempt fails" 4000 <| Async.block do + let (mockClient, mockServer) ← Mock.new + let calls ← IO.mkRef 0 + let connect : Client.Connector := fun _ _ _ config => do + let callNo ← calls.get + calls.set (callNo + 1) + if callNo == 0 then + throw (IO.userError "synthetic first connect failure") + return .ok (← Client.Session.new mockServer (config := config)) + let pool ← Client.Pool.new {} connect (maxRetries := 1) + let some domain := URI.DomainName.ofString? "example.com" + | throw (IO.userError "DomainName parse failed") + let origin : URI.Origin := { + scheme := URI.Scheme.ofString! "http", host := .name domain, port := 80 } + let request ← Request.new |>.method .get |>.uri! "/retry" + |>.header! "Host" "example.com" |>.empty + let result : IO.Promise (Except String (Response Body.Stream)) ← IO.Promise.new + + background do + let attempt ← try + pure (Except.ok (← pool.send origin request)) + catch e => pure (Except.error (toString e)) + discard <| result.resolve attempt + background do + let _ ← drainRequest mockClient + mockClient.send (rawResp "200 OK" + #[("Content-Length", "2"), ("Connection", "close")] "ok") + + match ← await result.result! with + | Except.error e => throw (IO.userError s!"GET was not retried after connect failure: {e}") + | Except.ok resp => + let body ← resp.body.readAll (α := String) + unless body == "ok" do + throw (IO.userError s!"expected retry body 'ok', got {body.quote}") + unless (← calls.get) == 2 do + throw (IO.userError s!"expected two connection attempts, got {← calls.get}") + +-- A non-idempotent request is never retried after the peer drops the first connection mid-flight. +#eval show IO _ from runWithTimeout "POST is not retried after a mid-flight connection drop" 4000 <| Async.block do + let (mockClient1, mockServer1) ← Mock.new + let (_mockClient2, mockServer2) ← Mock.new + let calls ← IO.mkRef 0 + let connect : Client.Connector := fun _ _ _ config => do + let callNo ← calls.get + calls.set (callNo + 1) + return .ok (← Client.Session.new (if callNo == 0 then mockServer1 else mockServer2) (config := config)) + let pool ← Client.Pool.new {} connect (maxRetries := 3) + let some domain := URI.DomainName.ofString? "example.com" + | throw (IO.userError "DomainName parse failed") + let origin : URI.Origin := { + scheme := URI.Scheme.ofString! "http", host := .name domain, port := 80 } + let request ← Request.new |>.method .post |>.uri! "/side-effect" + |>.header! "Host" "example.com" |>.text "payload" + let result : IO.Promise (Except String (Response Body.Stream)) ← IO.Promise.new + + background do + let attempt ← try + pure (Except.ok (← pool.send origin request)) + catch e => pure (Except.error (toString e)) + discard <| result.resolve attempt + let _ ← drainRequest mockClient1 + mockClient1.close + + match ← await result.result! with + | Except.ok _ => throw (IO.userError "POST unexpectedly succeeded after connection drop") + | Except.error _ => pure () + unless (← calls.get) == 1 do + throw (IO.userError s!"POST was retried; expected one connection attempt, got {← calls.get}") + +-- ============================================================ +-- Section 14 — Retry body integrity and dead-session detection +-- ============================================================ + +-- An idempotent request whose streaming body was consumed by the failed attempt must NOT be +-- retried: the body cannot be replayed, so a retry would silently send an empty body. +#eval show IO _ from runWithTimeout "PUT with non-replayable stream body is not retried" 4000 <| Async.block do + let (mockClient1, mockServer1) ← Mock.new + let (mockClient2, mockServer2) ← Mock.new + let calls ← IO.mkRef 0 + let connect : Client.Connector := fun _ _ _ config => do + let callNo ← calls.get + calls.set (callNo + 1) + return .ok (← Client.Session.new (if callNo == 0 then mockServer1 else mockServer2) (config := config)) + let pool ← Client.Pool.new {} connect (maxRetries := 3) + let some domain := URI.DomainName.ofString? "example.com" + | throw (IO.userError "DomainName parse failed") + let origin : URI.Origin := { + scheme := URI.Scheme.ofString! "http", host := .name domain, port := 80 } + let request ← Request.new |>.method .put |>.uri! "/upload" + |>.header! "Host" "example.com" + |>.stream (fun out => do + out.send (Chunk.ofByteArray "payload".toUTF8) + out.close) + let result : IO.Promise (Except String (Response Body.Stream)) ← IO.Promise.new + + background do + let attempt ← try + pure (Except.ok (← pool.send origin request)) + catch e => pure (Except.error (toString e)) + discard <| result.resolve attempt + + -- Drain the first request fully (chunked or Content-Length framing), then drop the connection + -- without responding, after the body has been consumed from the caller's stream. + let mut firstBytes := ByteArray.empty + repeat + let some chunk ← mockClient1.recv? + | throw (IO.userError "connection closed before first PUT arrived") + firstBytes := firstBytes ++ chunk + let t := String.fromUTF8! firstBytes + if t.endsWith "0\r\n\r\n" || t.endsWith "payload" then break + mockClient1.close + + -- If the client (incorrectly) retries, answer the second connection so the test fails fast on + -- the `calls` assertion instead of timing out. + background do + if (← mockClient2.recv?).isSome then + mockClient2.send (rawResp "200 OK" + #[("Content-Length", "2"), ("Connection", "close")] "ok") + + match ← await result.result! with + | Except.ok _ => + throw (IO.userError "PUT with a consumed stream body unexpectedly succeeded via retry") + | Except.error _ => pure () + unless (← calls.get) == 1 do + throw (IO.userError + s!"PUT with non-replayable body was retried; expected 1 connection attempt, got {← calls.get}") + +-- A replayable (`Body.Full`) request body must be reset before a retry so the second attempt +-- sends the complete payload again, not the consumed remainder. +#eval show IO _ from runWithTimeout "retried PUT resends the full replayable body" 4000 <| Async.block do + let (mockClient1, mockServer1) ← Mock.new + let (mockClient2, mockServer2) ← Mock.new + let calls ← IO.mkRef 0 + let connect : Client.Connector := fun _ _ _ config => do + let callNo ← calls.get + calls.set (callNo + 1) + return .ok (← Client.Session.new (if callNo == 0 then mockServer1 else mockServer2) (config := config)) + let pool ← Client.Pool.new {} connect (maxRetries := 1) + let some domain := URI.DomainName.ofString? "example.com" + | throw (IO.userError "DomainName parse failed") + let origin : URI.Origin := { + scheme := URI.Scheme.ofString! "http", host := .name domain, port := 80 } + let request ← Request.new |>.method .put |>.uri! "/upload" + |>.header! "Host" "example.com" |>.text "payload" + let result : IO.Promise (Except String (Response Body.Stream)) ← IO.Promise.new + + background do + let attempt ← try + pure (Except.ok (← pool.send origin request)) + catch e => pure (Except.error (toString e)) + discard <| result.resolve attempt + + -- First attempt: consume the whole request (headers + body), then drop without responding. + let _ ← drainRequest mockClient1 + mockClient1.close + + -- Second attempt: the retried request must carry the full body again. + let retryBytes ← drainRequest mockClient2 + mockClient2.send (rawResp "200 OK" + #[("Content-Length", "2"), ("Connection", "close")] "ok") + + match ← await result.result! with + | Except.error e => throw (IO.userError s!"retried PUT failed: {e}") + | Except.ok resp => + let _ ← resp.body.readAll (α := String) + unless (← calls.get) == 2 do + throw (IO.userError s!"expected two connection attempts, got {← calls.get}") + let retryText := String.fromUTF8! retryBytes + unless retryText.contains "payload" do + throw <| IO.userError + s!"retried PUT did not resend the request body:\n{retryText.quote}" + +-- A pooled session whose connection has already shut down (idle timeout, server EOF) must not be +-- handed to the next request: the request was never written to the wire, so the pool can safely +-- open a fresh connection — even for non-idempotent methods and with retries disabled. +#eval show IO _ from runWithTimeout "pool discards a dead session instead of failing the next request" 4000 <| Async.block do + let (mockClient1, mockServer1) ← Mock.new + let (mockClient2, mockServer2) ← Mock.new + let calls ← IO.mkRef 0 + let connect : Client.Connector := fun _ _ _ config => do + let callNo ← calls.get + calls.set (callNo + 1) + return .ok (← Client.Session.new (if callNo == 0 then mockServer1 else mockServer2) (config := config)) + let pool ← Client.Pool.new {} connect (maxRetries := 0) + let some domain := URI.DomainName.ofString? "example.com" + | throw (IO.userError "DomainName parse failed") + let origin : URI.Origin := { + scheme := URI.Scheme.ofString! "http", host := .name domain, port := 80 } + + -- First exchange completes cleanly; the session is parked in the pool. + let req1 ← Request.new |>.method .get |>.uri! "/one" + |>.header! "Host" "example.com" |>.empty + let p1 : IO.Promise (Except String (Response Body.Stream)) ← IO.Promise.new + background do + let attempt ← try + pure (Except.ok (← pool.send origin req1)) + catch e => pure (Except.error (toString e)) + discard <| p1.resolve attempt + let _ ← drainRequest mockClient1 + mockClient1.send (rawResp "200 OK" + #[("Content-Length", "5"), ("Connection", "keep-alive")] "hello") + match ← await p1.result! with + | Except.error e => throw (IO.userError s!"first pooled request failed: {e}") + | Except.ok resp => + let _ ← resp.body.readAll (α := String) + + -- The server silently drops the parked connection; give the background loop + -- time to observe EOF and shut down. + mockClient1.close + IO.sleep 200 + + -- The next request (a POST: retries disabled and non-idempotent anyway) must transparently get + -- a fresh connection rather than an error from the dead parked session. + let req2 ← Request.new |>.method .post |>.uri! "/two" + |>.header! "Host" "example.com" |>.text "data" + let p2 : IO.Promise (Except String (Response Body.Stream)) ← IO.Promise.new + background do + let attempt ← try + pure (Except.ok (← pool.send origin req2)) + catch e => pure (Except.error (toString e)) + discard <| p2.resolve attempt + + let secondBytes ← drainRequest mockClient2 + mockClient2.send (rawResp "200 OK" + #[("Content-Length", "2"), ("Connection", "close")] "ok") + + match ← await p2.result! with + | Except.error e => throw (IO.userError s!"POST after dead parked session failed: {e}") + | Except.ok resp => + let _ ← resp.body.readAll (α := String) + unless (← calls.get) == 2 do + throw (IO.userError s!"expected a fresh second connection, got {← calls.get} attempts") + let secondText := String.fromUTF8! secondBytes + unless secondText.startsWith "POST /two" do + throw <| IO.userError s!"unexpected second request:\n{secondText.quote}" From b4ed8796608ab96a061ad84c1d6508e43bf732fd Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Sat, 25 Jul 2026 09:29:17 -0300 Subject: [PATCH 3/5] chore: remove useless file --- FS.md | 666 ---------------------------------------------------------- 1 file changed, 666 deletions(-) delete mode 100644 FS.md diff --git a/FS.md b/FS.md deleted file mode 100644 index c7759c79466f..000000000000 --- a/FS.md +++ /dev/null @@ -1,666 +0,0 @@ -# Summary - -This proposal redesigns Lean's FS and Path API using LibUV, replacing a lot of types, making them more complete and removing the `FILE*` dependency in the C++ side. It also adds directory traversals, metadata inspection, some useful functions like copying without reading the entire file into memory and a way to integrate with `Std.Async` in a clean way. This design changes `FS.Handle` and `FS.Stream` to a layer approach with more low-level changes that requires the user to do synchronization and buffering on the Lean side. - -Since these things will depend on Std abstractions, it lives under `Std.FS` and `Std.Async.FS`. Path-related changes are tracked separately in issue #13922. - -# Migration - -A lot of functions are just going to be moved to other namespaces like `IO.FS.readFile` that goes to `Std.FS.readFile`. The `Handle` type will just be split into multiple low level ones like `File`, `Dir`, `Handle` (a smaller version with `uv_pipe_t` and `uv_tty_t`). - -| Old | New | Notes | -| ----------------------------------------------- | --------------------------------------------- | ------------------------------------------------------ | -| `IO.FS.Handle` | `Std.FS.File` | for regular files opened by path | -| `IO.FS.Handle` | `Std.FS.Dir` | for regular directories opened by path | -| `IO.FS.Handle` | `Std.FS.Handle` | for stdin/stdout/stderr and IPC pipes | -| `IO.FS.Stream` | `Std.FS.Stream` | Keep the abstraction for LSP capture of the Stdout | -| `IO.getStdin` / `getStdout` / `getStderr` | `Handle.stdin` / `.stdout` / `.stderr` | now `Stdin`/`Stdout`/`Stderr`, which have no `close` | -| `IO.FS.Handle.putStr` / `IO.FS.Handle.putStrLn` | `Std.FS.File.putStr` / `Std.FS.File.putStrLn` | same semantics | -| `IO.FS.Handle.isEof` | — | no direct equivalent; `File.readAt` returns empty at EOF | -| `IO.FS.readFile` | `Std.FS.readFile` | same semantics | -| `IO.FS.writeFile` | `Std.FS.writeFile` | same semantics | -| `IO.FS.readBinFile` | `Std.FS.readBinFile` | same semantics | -| `IO.FS.writeBinFile` | `Std.FS.writeBinFile` | same semantics | -| `IO.FS.lines` | `Std.FS.lines` | same semantics | -| `IO.FS.hardLink` | `Std.FS.hardLink` | same semantics | - -## Async Integration - -`uv_fs_*` operations can be used asynchronously and synchronously (by specifying a NULL loop and callback), so with a `Std/Async/FS` we can just add operations in the namespace like `.readAsync` that will return a `Promise` instead of blocking. `Std.Async.FS` gives every `Std.FS`/`Std.FS.File` operation an `*Async` counterpart, including path-keyed convenience helpers (`readFileAsync`, `writeFileAsync`, `appendFileAsync`, …), directory operations (`readDirAsync`, `removeDirAllAsync`, `copyDirAsync`, `walkAsync`, `globAsync`), symlinks, metadata/permissions, and temporary files/directories. The full list is in [Async Variants](#async-variants); everything lives in the same `Std.FS` / `Std.FS.File` namespaces as its synchronous counterpart, so the two are used side by side without extra `open`s. - -The async variants return `Async α` (over `Std.Async`'s `Promise`), not `IO α`. `Handle`, `Pipe`, and `TTY` get async read/write too — for those the asynchronous form is the *primitive* one, since `uv_read_start`/`uv_write` are natively asynchronous and the synchronous variants are what require extra machinery to emulate. `Dir` and the buffered wrappers have no async counterparts: directory iteration is exposed asynchronously only through the eager path-keyed `readDirAsync`/`walkAsync`. - -File locking is the exception: acquiring a contended lock with `flock` (POSIX) or `LockFileEx` (Windows) is a blocking syscall with no libuv equivalent and SHOULDN'T run on the event loop thread, so `File.lockAsync` schedules a dedicated work thread using `uv_queue_work` and resumes a `Promise` once it completes. `File.tryLockAsync` and `File.unlockAsync` are the exception to the exception: a non-blocking `trylock` and releasing a lock never block for an unbounded time, so they run inline rather than needing a work thread. As `flock` is advisory it does not interfere with any of the operations of libuv and thus, is safe to use with another flocks. - -`walkAsync`/`globAsync` collect eagerly into an `Array` rather than returning a lazy `IterM`, since `Async` has no lazy-iterator integration yet (unlike the synchronous `FS.walk`, which returns `IterM (α := WalkIterator) IO DirEntry`). - -## Concurrency Model - -All raw IO types (`File`, `Handle`, `Pipe`, `Dir`) are not thread-safe by default. Concurrency and parallelism safety is achieved through explicit wrappers like `Mutex α` and `RecursiveMutex α`. - -# Core Abstractions - -## Paths and Filesystem Entries - -Path types and path manipulation are specified in issue #13922. This proposal only covers the filesystem abstractions that operate on paths. - -- `Dir`: An open directory handle. -- `DirEntry`: A single filesystem entry produced during directory iteration. -- `Metadata`: Filesystem metadata for files, directories, or special entries. -- `FileType`: Enumeration of entry kinds: `file`, `dir`, `symlink`, `blockDevice`, `charDevice`, `fifo`, `socket`, `unknown`. -- `File`: A thin wrapper around `uv_file`. Not thread-safe by default, concurrent access must be explicitly synchronized using `Mutex`. -- `BufferedReader α`: Buffered wrapper around any readable type. -- `BufferedWriter α`: Buffered writer over any writable type. -- `LineWriter α`: A writer wrapper that flushes automatically on newline characters (`\n`). Used by `Stdout`. -- `FilesystemStats`: Filesystem-level statistics (total/free space, inode counts) for the filesystem containing a path. - -## Handles and Streams - -- `Handle`: A system stream endpoint whose kind (`tty`, `pipe`, or a redirected `file`) is discovered at runtime via `uv_guess_handle`. Exposes only the operations valid for every kind. -- `Pipe`: A `Handle` known by construction to be a `uv_pipe_t`. -- `TTY`: A `Handle` known by construction to be a `uv_tty_t`, adding the terminal-only operations. -- `Stdin` / `Stdout` / `Stderr`: Cached singletons over descriptors 0/1/2, with buffering and *without* a `Close` instance. -- `Stream`: A record of closures that abstracts over any readable/writable endpoint, so stdout can be substituted at runtime. - -## Type Classes - -- `Read`: Typeclass for types that support sequential, cursor-advancing reads; provides `read : α → (n : USize) → ByteArray → IO ByteArray`, which appends up to `n` bytes after `buf`'s existing content. A result with no bytes appended signals end-of-file. Implemented by `File`, `Handle`, `Pipe`, and `TTY`. -- `Write`: Typeclass for types that support writing bytes; provides `write : α → ByteArray → IO Unit`. Implemented by `File`, `Handle`, `Pipe`, `TTY`, `BufferedWriter α`, and `LineWriter α`. -- `Close`: Typeclass for types that hold a resource that must be released; provides `close : α → IO Unit`. Implemented by `File`, `Dir`, `Handle`, `Pipe`, `TTY`, and the buffered wrappers (`BufferedReader`, `BufferedWriter`, `LineWriter`, which flush before delegating to the inner sink's `close`). Lets generic code release whatever `Read`/`Write` source or sink it was handed without depending on its concrete type. `Stdin`/`Stdout`/`Stderr` deliberately have **no** instance, so no generic cleanup path can close descriptors 0/1/2 — see [Standard Streams](#standard-streams). - -# Detailed Explanation - -## Iterators - -Some operations return `IterM` (defined in `Std/Data/Iterators`) rather than eagerly collected `Array`s. - -| Iterator State Type | Element | Used by | -| ------------------- | ---------- | ----------- | -| `DirIterator` | `DirEntry` | `Dir.iter` | -| `WalkIterator` | `DirEntry` | `FS.walk` | - -## FileType - -```lean -inductive FileType where - | file -- regular file - | dir -- directory - | symlink -- symbolic link - | blockDevice -- block device (e.g. disk) - | charDevice -- character device (e.g. /dev/null) - | fifo -- named pipe (FIFO) - | socket -- Unix domain socket - | unknown -- type not reported by the OS (e.g. some network filesystems) -``` - -| Function | Type | Description | -| ----------------------- | ------------------------ | ------------------------------------------------------------------------------------------------------------- | -| `FileType.ofDirentType` | `UInt8 → FileType` | Interpret a raw `uv_dirent_t` type code. | -| `FileType.ofStatMode` | `UInt64 → FileType` | Interpret the `S_IFMT` bits of a raw POSIX `st_mode`, as returned by `stat`/`lstat`/`fstat`. | - -## OpenMode - -`OpenMode` is a struct specifying how a file is opened. The default value opens an existing file -read-only. - -**Fields** - -| Field | Type | Default | Description | -| ---------------------------- | -------------- | ------- | ---------------------------------------------------------- | -| `OpenMode.read` | `Bool` | `true` | Allow reads | -| `OpenMode.write` | `Bool` | `false` | Allow writes | -| `OpenMode.append` | `Bool` | `false` | All writes go to end-of-file; incompatible with `truncate` | -| `OpenMode.truncate` | `Bool` | `false` | Truncate to zero on open; requires `write` | -| `OpenMode.create` | `Bool` | `false` | Create the file if it does not exist (`O_CREAT`) | -| `OpenMode.createNew` | `Bool` | `false` | Create the file, failing if it already exists (`O_CREAT \| O_EXCL`); guarantees exclusive creation | -| `OpenMode.custom` | `Option USize` | `none` | Pass raw OS-level flags directly; merged with the flags derived from the other fields. Use when no predefined field covers the required behavior. | - -**Presets** - -| Name | Value | Description | -| ----------------------- | ------------------------------------------------ | -------------------------------------------------- | -| `OpenMode.readOnly` | `{ read }` | Open an existing file for reading only. | -| `OpenMode.readWrite` | `{ read, write }` | Open an existing file for reading and writing without truncation. | -| `OpenMode.writeCreate` | `{ write, create }` | Create or open a file for writing. | -| `OpenMode.appendCreate` | `{ write, append, create }` | Open a file for appending, creating it if necessary. | - -`OpenMode.rawFlags : OpenMode → UInt32` computes the `uv_fs_open` flag bitmask, merging in `custom`. -It is public so `Std.Async.FS` can share it rather than re-deriving the bits. - -## Permissions - -`AccessRight` and `FileRight` keep the same shape as `IO.AccessRight`/`IO.FileRight` in the current API, moved to `Std.FS`. - -```lean -structure AccessRight where - /-- The file can be read. -/ - read : Bool := false - /-- The file can be written to. -/ - write : Bool := false - /-- The file can be executed. -/ - execution : Bool := false - -structure FileRight where - /-- The owner's permissions to access the file. -/ - user : AccessRight := {} - /-- The assigned group's permissions to access the file. -/ - group : AccessRight := {} - /-- The permissions that all others have to access the file. -/ - other : AccessRight := {} -``` - -| Name | Type | Description | -| ----------------------- | --------------------------------------- | --------------------------------------------------- | -| `FileRight.flags` | `FileRight → UInt32` | Convert to a raw POSIX bit field (for `chmod`, etc.) | -| `FileRight.ofStatMode` | `UInt64 → FileRight` | Interpret the low 9 permission bits of a raw POSIX `st_mode` | -| `FileRight.default` | `FileRight` | `0o644` — owner read/write; group and other read | -| `FileRight.defaultDir` | `FileRight` | `0o755` — owner read/write/execute; group and other read/execute | - -## File Type - -`File` is a wrapper around `uv_file` with no buffering and no built-in lock. If buffering or locking is needed, wrap with `Mutex (BufferedWriter File)` or call `File.lock`. - -| Function | Type | Description | Operation | -| ------------------------ | ---------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------- | -| `File.openExisting` | `Path → (mode : OpenMode := .readOnly) → IO File` | Open an existing file. Fails if the file does not exist. Default mode is read-only; pass `.readWrite` to open for reading and writing without truncation. | `uv_fs_open` | -| `File.create` | `Path → (mode : OpenMode := .writeCreate) → (perm : FileRight := .default) → IO File` | Create or open a file, applying `perm` if it is newly created. | `uv_fs_open` | -| `File.withFile` | `Path → (mode : OpenMode := .readOnly) → (File → IO α) → IO α` | Open a file, run an action, close in a `finally` block. | -| `File.close` | `File → IO Unit` | Explicitly close the file. Prefer `withFile` or explicit `close`. Closing does not call `fsync`; use `syncAll` before closing for durability. | `uv_fs_close` | -| `File.syncAll` | `File → IO Unit` | Flush data and metadata to the device (`fsync`). | `uv_fs_fsync` | -| `File.syncData` | `File → IO Unit` | Flush data only, skipping metadata (`fdatasync`). Cheaper when durability of timestamps/size is not required. | `uv_fs_fdatasync` | -| `File.sendFile` | `(src dst : File) → (offset : Int64) → (length : USize) → IO USize` | Copy up to `length` bytes from `src` at `offset` into `dst` using OS copy acceleration. Returns the number of bytes actually copied. | `uv_fs_sendfile` | -| `File.lock` | `File → (exclusive : Bool := true) → IO Unit` | Acquire a shared or exclusive lock, blocking the calling thread until available. (Only `lockAsync` needs `uv_queue_work`, to keep the event loop free.) | `LockFileEx` on Windows, `flock` on POSIX | -| `File.tryLock` | `File → (exclusive : Bool := true) → IO Bool` | Try to acquire a lock without blocking. Returns `false` immediately if held by another process. | (`LockFileEx` on Windows, `flock` on POSIX) | -| `File.unlock` | ` File → IO Unit` | Release the lock. Idempotent; succeeds even if no lock is held. | `UnlockFileEx` on Windows, `flock` on POSIX | -| `File.atomically` | `File → (exclusive : Bool := true) → IO α → IO α` | Lock, run action, unlock in `finally`. Uses `File.lock`/`File.unlock`. | | -| `File.read` | `File → (n : USize) → (buf : ByteArray) → IO ByteArray` | Read up to `n` bytes at the current cursor position, advancing it. Bytes are appended after `buf`'s existing content; use the return value, not `buf`, after the call. No bytes appended signals end-of-file. Backs the `Read File` instance. | `uv_fs_read` | -| `File.readAt` | `File → (offset : UInt64) → (n : USize) → (buf : ByteArray) → IO ByteArray` | Read up to `n` bytes at `offset` into `buf` without moving the cursor (`pread`). Returns the filled slice; use the return value, not `buf`, after the call. | `uv_fs_read` | -| `File.writeAt` | `File → (offset : UInt64) → ByteArray → IO Unit` | Write at `offset` (`pwrite`), retrying until every byte is written. | `uv_fs_write` | -| `File.write` | `File → ByteArray → IO Unit` | Write at the current cursor position, retrying until every byte is written. | `uv_fs_write` | -| `File.putStr` | `File → String → IO Unit` | Write a UTF-8 string at the current cursor position. | | -| `File.putStrLn` | `File → String → IO Unit` | Write a UTF-8 string followed by `\n` at the current cursor position. | | -| `File.setLength` | `File → (len : UInt64) → IO Unit` | Truncate or extend the file to exactly `len` bytes. | `uv_fs_ftruncate` | -| `File.metadata` | `File → IO Metadata` | Return metadata for the open file. Avoids TOCTOU vs `Path.metadata`. | `uv_fs_fstat` | -| `File.setPermissions` | `File → FileRight → IO Unit` | Set the file's permission bits. | `uv_fs_fchmod` | -| `File.setTimes` | `File → (accessed : Timestamp) → (modified : Timestamp) → IO Unit` | Set access and modification timestamps. | `uv_fs_futime` | -| `File.chown` | `File → (uid gid : UInt32) → IO Unit` | Change the owner and group of the open file. On Windows this is a noop. | `uv_fs_fchown` | - -## Handle Type - -`Handle` is an open stream endpoint whose *kind is discovered at runtime*: `uv_guess_handle(fd)` -reports `UV_TTY`, `UV_NAMED_PIPE`, or `UV_FILE`, and the kind decides which libuv API is legal for it. -A `Handle` therefore exposes exactly the operations valid for every kind — sequential read, write, -close — and nothing more. - -**Why `Handle` is not a `File`.** The tempting simplification is that on POSIX everything is a file -descriptor, so `Handle` could just be `File` and `Pipe`/`TTY` could disappear. It does not hold: - -- **libuv forbids the mixing.** Regular-file descriptors are always reported ready by `epoll`/`kqueue`, - so readiness polling is meaningless and libuv does not support files as streams: `uv_read_start` is - invalid on a `UV_FILE`, and conversely `uv_fs_read` on a terminal bypasses everything `uv_tty_t` - exists to do. `uv_tty_init` on a non-terminal descriptor returns `EINVAL`. -- **`File`'s API is offset-based; pipes and terminals have no offsets.** `readAt`, `writeAt`, - `setLength`, and `sendFile` all take an offset, and `pread`/`pwrite` on a pipe or terminal fail with - `ESPIPE`. So do `ftruncate` and `flock`, and `fstat` reports nothing useful. Collapsing the types - would produce one whose entire documented surface throws on two of its three kinds. -- **On Windows they are not the same OS object.** `uv_tty_t` wraps a console handle and performs - UTF-16 conversion, ANSI escape emulation, and virtual-terminal mode handling; a pipe is a Named Pipe - driven by overlapped I/O; a file is a `HANDLE` for `ReadFile`. The POSIX intuition does not port. - -The containment runs one way only: a `File` offers a superset of `Handle`'s operations, never the -reverse. No coercion between them is provided, since it would silently discard the -positioned-vs-cursor distinction. - -**Redirected stdio.** `uv_guess_handle` returns `UV_FILE` when stdio is redirected to a regular file -(`./program > out.txt`). The handle then dispatches reads and writes via `uv_fs_read`/`uv_fs_write` -internally, but it stays typed as a `Handle`: the program did not gain the ability to seek or lock its -own stdout just because the shell redirected it. - -```lean -inductive HandleKind where - | file -- `uv_guess_handle` reported `UV_FILE` (redirected stdio) - | tty -- `UV_TTY` - | pipe -- `UV_NAMED_PIPE` -``` - -| Function | Type | Description | libuv | -| ----------------- | --------------------------------------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------ | -| `Handle.ofFd` | `(fd : UInt32) → (readable : Bool) → IO Handle` | Adopt an existing descriptor, dispatching on `uv_guess_handle`: `UV_FILE` is kept as a raw descriptor, `UV_TTY` is initialized with `uv_tty_init`, `UV_NAMED_PIPE` with `uv_pipe_init` + `uv_pipe_open`. `UV_TCP`/`UV_UDP` are rejected — those belong to `Std.Async.TCP`/`UDP`. | `uv_guess_handle` | -| `Handle.kind` | `Handle → BaseIO HandleKind` | The kind reported at construction. | `uv_guess_handle` | -| `Handle.read` | `Handle → (n : USize) → (buf : ByteArray) → IO ByteArray` | Read up to `n` bytes into `buf`, reusing its storage in place when `buf` is uniquely owned. Returns the filled slice; use the return value, not `buf`. Returns `buf` truncated to its original size at EOF. | `uv_read_start` / `uv_fs_read` | -| `Handle.write` | `Handle → ByteArray → IO Unit` | Write bytes. | `uv_write` / `uv_fs_write` | -| `Handle.flush` | `Handle → IO Unit` | Flush any buffered output. No-op for unbuffered handles. | | -| `Handle.close` | `Handle → IO Unit` | Close the handle and release resources. | `uv_close` / `uv_fs_close` | -| `Handle.asTTY?` | `Handle → BaseIO (Option TTY)` | Refine to a `TTY` if the kind is `tty`, so the terminal-only operations become available. | | -| `Handle.asPipe?` | `Handle → BaseIO (Option Pipe)` | Refine to a `Pipe` if the kind is `pipe`. | | -| `Handle.isTty` | `Handle → BaseIO Bool` | `kind == .tty`. Retained as a convenience. | `uv_guess_handle` | -| `Handle.isPipe` | `Handle → BaseIO Bool` | `kind == .pipe`. | `uv_guess_handle` | -| `Handle.isFile` | `Handle → BaseIO Bool` | `kind == .file`. | `uv_guess_handle` | - -The three predicates are mutually exclusive, hence `kind` is the primitive and they are derived from -it. - -`Handle.read`/`write` block the calling thread. For the `tty`/`pipe` kinds the underlying libuv API is -asynchronous (`uv_read_start`/`uv_write`), so the synchronous form is implemented by bridging through a -semaphore that the completion callback posts from the event loop's driver thread. Concurrent -operations on one handle return `EALREADY` rather than interleaving; as with `File`, sharing a -`Handle` across threads requires an explicit `Mutex`. - -## Standard Streams - -`Handle.stdin`, `Handle.stdout`, and `Handle.stderr` are **cached singletons**, built once from -descriptors 0/1/2. They must not be re-initialized: two `uv_tty_init` calls on descriptor 1 produce two -`uv_tty_t` contending for one console. - -They are returned as the distinct types `Stdin`, `Stdout`, and `Stderr`, each wrapping a `Handle` plus -the buffering appropriate to it: - -| Type | Buffering | Rationale | -| -------- | ---------------------------------- | ---------------------------------------------------------------- | -| `Stdin` | `Mutex (BufferedReader Handle)` | Read buffering, with `readLine`. | -| `Stdout` | `RecursiveMutex` + line buffering | Flushes on `\n` so line-oriented output is delivered promptly. | -| `Stderr` | `Mutex Handle`, unbuffered | Diagnostics must survive a crash that never reaches a flush. | - -**They deliberately have no `Close` instance**, and therefore no way to close descriptors 0/1/2. This -follows Rust, where `Stdout` is its own type with no `close` method and dropping a handle leaves the -descriptor open — and departs from Go, Python, and Java, which expose `os.Stdout.Close()` / -`sys.stdout.close()` / `System.out.close()` and let a program disable its own output (silently, in -Java's case). - -The reason to prefer Rust's answer here is specific to this design: `Close` is a *typeclass*, and the -buffered wrappers close what they wrap — `BufferedWriter.close` and `LineWriter.close` both flush and -then call `Close.close` on the inner sink. If the standard streams were ordinary `Close`-able values, -a single `Close.close` reached through a generic cleanup path would close descriptor 1 for the whole -process, with no line of code naming stdout anywhere. Go and Python are not exposed to this because -they have no such polymorphism; removing the instance removes the possibility at the type level rather -than relying on callers to avoid it. - -This is why the buffering above is described by behavior rather than spelled `LineWriter Handle`: -`LineWriter α` and `BufferedWriter α` inherit a `Close` instance from `α`, so the buffering must live -*inside* the newtype rather than the newtype being a type alias for a buffered wrapper. - -Closing a standard descriptor remains possible, but only by naming it: `Handle.ofFd 1 (readable := -false)` yields an ordinary, closable `Handle`. That mirrors Rust's requirement to go through an -explicit owned descriptor. The runtime object additionally carries a no-op-close flag, so an FFI path -that reaches a standard handle by another route still cannot wedge the process's output. - -## Pipe and TTY - -`Pipe` (`uv_pipe_t`) and `TTY` (`uv_tty_t`) are `Handle`s refined by known kind. They share -`Handle`'s read/write/close and exist as distinct types so that kind-specific operations are available -only where they are meaningful: `TTY.setMode .raw` must not typecheck on a stdout that the shell -redirected to a file. - -| Function | Type | Description | libuv | -| -------------------- | ------------------------------------------------------- | ------------------------------------------------------------------------------------------------------------- | ------------------------- | -| `Pipe.read` | `Pipe → (n : USize) → (buf : ByteArray) → IO ByteArray` | Read up to `n` bytes into `buf`; returns the filled slice. | `uv_read_start` | -| `Pipe.write` | `Pipe → ByteArray → IO Unit` | Write bytes to the pipe. | `uv_write` | -| `Pipe.close` | `Pipe → IO Unit` | Close the pipe and release its resources. | `uv_close` | -| `TTY.read` | `TTY → (n : USize) → (buf : ByteArray) → IO ByteArray` | Read up to `n` bytes into `buf`; returns the filled slice. | `uv_read_start` | -| `TTY.write` | `TTY → ByteArray → IO Unit` | Write bytes to the terminal. | `uv_write` | -| `TTY.close` | `TTY → IO Unit` | Close the terminal handle and release its resources. | `uv_close` | -| `TTY.setMode` | `TTY → TTYMode → IO Unit` | Set the terminal input mode. | `uv_tty_set_mode` | -| `TTY.getWinSize` | `TTY → IO (UInt32 × UInt32)` | Return the terminal's width and height in character cells. | `uv_tty_get_winsize` | -| `TTY.vtermState` | `BaseIO VTermState` | Whether the console can process virtual terminal sequences. Process-wide, not per-handle, on Windows. | `uv_tty_get_vterm_state` | - -```lean -inductive TTYMode where - | normal -- initial/normal mode - | raw -- raw input mode - | rawVT -- raw input mode; on Windows also sets `ENABLE_VIRTUAL_TERMINAL_INPUT` - | io -- binary-safe I/O mode for IPC (POSIX only) -``` - -**Raw mode must be reset at process exit.** `uv_tty_reset_mode` is process-wide and restores the -terminal's original settings; without it a program that enters raw mode and then crashes leaves the -user's shell unusable. A handler registered when raw mode is first entered calls it on exit. - -`Pipe` carries no operations of its own for now. libuv offers `uv_pipe_bind2`, `uv_pipe_connect2`, -`uv_pipe_getsockname`/`getpeername`, `uv_pipe_chmod`, and descriptor passing via -`uv_pipe_pending_count`/`pending_type`, but pipe *servers* overlap with what `Std.Async.Process` and -`Std.Async.TCP` already cover; these are deferred until something needs them. - -## Stream - -`Stream` is a record of closures over any readable/writable endpoint. It stays a closure record rather -than becoming a `[Read α] [Write α]` abstraction because `IO.setStdout : FS.Stream → BaseIO FS.Stream` -replaces the current standard output at runtime with a value of a *different* type — capturing to a -buffer, for instance, which is how the language server intercepts stdout. That requires an -existential, which the closure record provides and typeclass polymorphism does not. - -| Field | Type | Description | -| -------------- | ------------------------------------------ | ---------------------------------------------------------------- | -| `Stream.flush` | `IO Unit` | Flush the stream's output buffers. | -| `Stream.read` | `USize → (buf : ByteArray) → IO ByteArray` | Read up to the given number of bytes into `buf`; an empty result signals EOF. | -| `Stream.write` | `ByteArray → IO Unit` | Write the provided bytes. | -| `Stream.close` | `IO Unit` | Release the underlying endpoint. | - -`read` takes a buffer to match `Read.read` and `Handle.read`, so that wrapping a handle in a -`Stream` does not silently give up the buffer-reuse path. `close` is a field rather than an omission, -so a `Stream` over a temporary file or captured pipe can be released; the constructor for a standard -stream supplies a no-op. - -| Constructor | Type | Description | -| ------------------ | -------------------------------- | ------------------------------------------------------------ | -| `Stream.ofHandle` | `Handle → Stream` | | -| `Stream.ofFile` | `File → Stream` | Sequential (cursor-relative) reads and writes only. | -| `Stream.ofBuffer` | `IO.Ref ByteArray → Stream` | In-memory capture; `close` is a no-op. | - -## Buffering - -Buffering is opt-in and layered over the raw types. `BufferedReader` wraps any `Read`able source; -`BufferedWriter` and `LineWriter` wrap any `Write`able sink. - -| Function | Type | Description | -| -------------------------- | ----------------------------------------------------------------- | -------------------------------------------------------------------------------------------------------------- | -| `BufferedReader.new` | `[Read α] → α → (capacity : USize := 4096) → IO (BufferedReader α)` | Wrap a source with a read buffer of the given capacity. | -| `BufferedReader.read` | `[Read α] → BufferedReader α → (n : USize) → IO ByteArray` | Read `n` bytes, looping until `n` are collected or the source is exhausted. A request of at least `capacity` bytes bypasses the buffer. | -| `BufferedReader.readLine` | `[Read α] → BufferedReader α → IO (Option String)` | Read one line including the trailing newline, or `none` at EOF. Fails on invalid UTF-8. | -| `BufferedReader.readToEnd` | `[Read α] → BufferedReader α → IO ByteArray` | Read the remainder of the source into one `ByteArray`. | -| `BufferedReader.close` | `[Close α] → BufferedReader α → IO Unit` | Close the underlying source. Bytes still in the read buffer are discarded. | -| `BufferedWriter.new` | `α → (capacity : USize := 4096) → IO (BufferedWriter α)` | Wrap a sink with a write buffer of the given capacity. | -| `BufferedWriter.write` | `[Write α] → BufferedWriter α → ByteArray → IO Unit` | Buffer bytes, flushing to the sink when the buffer fills. | -| `BufferedWriter.flush` | `[Write α] → BufferedWriter α → IO Unit` | Flush any buffered output to the sink. | -| `BufferedWriter.close` | `[Write α] → [Close α] → BufferedWriter α → IO Unit` | Flush, then close the underlying sink. | -| `LineWriter.new` | `[Write α] → α → IO (LineWriter α)` | Wrap a sink in a line-buffered writer. | -| `LineWriter.write` | `[Write α] → LineWriter α → ByteArray → IO Unit` | Write bytes, flushing up to and including the last newline. | -| `LineWriter.flush` | `[Write α] → LineWriter α → IO Unit` | Flush any buffered output to the sink. | -| `LineWriter.close` | `[Write α] → [Close α] → LineWriter α → IO Unit` | Flush, then close the underlying sink. | - -## Dir - -`Dir` holds a `uv_dir_t`. - -| Function | Type | Description | libuv | -| -------------- | -------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ---------------------------------- | -| `Dir.openExisting` | `Path → IO Dir` | Open a directory for iteration. | `uv_fs_opendir` | -| `Dir.withDir` | `Path → (Dir → IO α) → IO α` | Open a directory, run an action, close in a `finally` block. | `uv_fs_opendir` + `uv_fs_closedir` | -| `Dir.close` | `Dir → IO Unit` | Explicitly close the directory handle. | `uv_fs_closedir` | -| `Dir.next` | `Dir → IO (Option DirEntry)` | Return the next entry, or `none` when exhausted. Order is filesystem-defined. | `uv_fs_readdir` | -| `Dir.drain` | `Dir → IO (Array DirEntry)` | Drain every remaining entry via repeated `next`. Backs `readDir` and `FS.walk`. | `uv_fs_readdir` | -| `Dir.path` | `Dir → Path` | The path the directory was opened at. | | -| `Dir.iter` | `Dir → IO (IterM (α := DirIterator) IO DirEntry)` | Lazy iterator over directory entries. Each step calls `readdir`. Works with `for entry in dir.iter do` and all `IterM` combinators. | `uv_fs_readdir` | -| `Dir.metadata` | `Dir → IO Metadata` | Return metadata for the directory itself. `uv_fs_opendir` does not expose a file descriptor, so this stats `dir.path` rather than the open handle. | `uv_fs_stat` | - -## DirEntry - -`DirEntry` is produced by `Dir.next`. It holds the parent `Dir` so its open methods can construct full paths as `dir.path / entry.fileName`. It already exists as `IO.FS.DirEntry` so it's included here for completeness. - -| Function | Type | Description | libuv | -| ------------------- | ------------------------ | ------------------------------------------------------------------------------------------------------------- | ------------------------------ | -| `DirEntry.dir` | `DirEntry → Dir` | The directory this entry was read from. | | -| `DirEntry.fileName` | `DirEntry → Path.Filename` | The entry name within its parent directory. | | -| `DirEntry.path` | `DirEntry → Path` | Full path, constructed as `dir.path / entry.fileName`. | | -| `DirEntry.fileType` | `DirEntry → IO FileType` | Return the file type *without* following symlinks: a symlink reports `.symlink`, not its target's type. | `uv_fs_lstat` | -| `DirEntry.isDir` | `DirEntry → IO Bool` | Return `true` if the entry is a directory (not a symlink to one). Convenience wrapper around `fileType`. | `uv_fs_lstat` | -| `DirEntry.metadata` | `DirEntry → IO Metadata` | Return full metadata for the entry, following symlinks. Always issues a `stat` call; use `fileType` when only the type is needed. | `uv_fs_stat` | - -## FS Operations - -These functions operate on the filesystem by path. They live in the `FS` namespace rather than `Path` because `Path` is a pure value type for path manipulation; IO operations belong in `FS`. - -| Function | Type | Description | libuv | -| ----------------- | ----------------------------------------------------------------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ----------------------------------------------------------------------- | -| `FS.copyFile` | `Path → Path → IO Unit` | Copy a file. | `uv_fs_copyfile` | -| `FS.removeFile` | `Path → IO Unit` | Delete a file. | `uv_fs_unlink` | -| `FS.removeDir` | `Path → IO Unit` | Remove an empty directory. Fails if the directory is not empty. | `uv_fs_rmdir` | -| `FS.removeDirAll` | `Path → (ignoreErrors : Bool := false) → IO Unit` | Remove a directory and all its contents recursively. If `ignoreErrors`, entries that fail to remove (e.g. permission denied) are skipped instead of aborting, on a best-effort basis. | `FS.readDir` + `uv_fs_unlink` + `uv_fs_rmdir` | -| `FS.createDir` | `Path → (perm : FileRight := .defaultDir) → IO Unit` | Create a directory. Parent must exist. `perm` sets the initial mode bits (default `0o755`). | `uv_fs_mkdir` | -| `FS.createDirAll` | `Path → (perm : FileRight := .defaultDir) → IO Unit` | Create a directory and all missing parent directories. No-op if the directory already exists. `perm` is applied to newly created directories only. | `uv_fs_mkdir` (repeated) | -| `FS.rename` | `Path → Path → IO Unit` | Rename or move a file or directory. | `uv_fs_rename` | -| `FS.hardLink` | `(orig link : Path) → IO Unit` | Create a hard link at `link` pointing to `orig`. Both paths must be on the same filesystem. | `uv_fs_link` | -| `FS.copyDir` | `(src dst : Path) → (ignoreErrors : Bool := false) → IO Unit` | Recursively copy a directory tree from `src` to `dst`. `dst` must not exist; creates it with the same permission bits as `src`. Files are copied via `uv_fs_copyfile`. Symlinks are recreated verbatim rather than followed. If `ignoreErrors`, entries that fail to copy are skipped instead of aborting, on a best-effort basis. | `uv_fs_copyfile` + `FS.readDir` | -| `FS.chown` | `Path → (uid gid : UInt32) → IO Unit` | Change the owner and group of the file or directory at `path`. Follows symlinks. On Windows this is a no-op. | `uv_fs_chown` | -| `FS.lchown` | `Path → (uid gid : UInt32) → IO Unit` | Like `FS.chown` but operates on the symlink itself rather than its target. On Windows this is a no-op. | `uv_fs_lchown` | -| `FS.truncate` | `Path → (len : UInt64) → IO Unit` | Truncate or extend the file at `path` to exactly `len` bytes. Follows symlinks. Complement to `File.setLength` for callers that do not have an open fd; libuv has no path-based `truncate`, so this opens the file `.readWrite` internally. | `uv_fs_open` + `uv_fs_ftruncate` + `uv_fs_close` | - -## Convenience - -| Function | Type | Description | libuv | -| ------------------- | ---------------------------- | --------------------------------------------------------------------------------------------------------- | -------------------------------------------- | -| `FS.readFile` | `Path → IO String` | Read an entire UTF-8 file into a string. Fails on invalid UTF-8. | `uv_fs_open` + `uv_fs_read` + `uv_fs_close` | -| `FS.readBinFile` | `Path → IO ByteArray` | Read an entire file into a `ByteArray`. | `uv_fs_open` + `uv_fs_read` + `uv_fs_close` | -| `FS.lines` | `Path → IO (Array String)` | Read all lines of a UTF-8 file into an array. Implemented via `BufferedReader`. | `uv_fs_open` + `uv_fs_read` + `uv_fs_close` | -| `FS.writeFile` | `Path → String → IO Unit` | Write a UTF-8 string to a file, creating or truncating it. | `uv_fs_open` + `uv_fs_write` + `uv_fs_close` | -| `FS.writeBinFile` | `Path → ByteArray → IO Unit` | Write bytes to a file, creating or truncating it. | `uv_fs_open` + `uv_fs_write` + `uv_fs_close` | -| `FS.appendFile` | `Path → ByteArray → IO Unit` | Append bytes to a file, creating it if it does not exist. | `uv_fs_open` + `uv_fs_write` + `uv_fs_close` | -| `FS.appendTextFile` | `Path → String → IO Unit` | Append a UTF-8 string to a file, creating it if it does not exist. | `uv_fs_open` + `uv_fs_write` + `uv_fs_close` | -| `FS.readDir` | `Path → IO (Array DirEntry)` | List all entries in a directory. Order is filesystem-defined; use `FS.readDirSorted` for stable ordering. | `uv_fs_opendir` + `uv_fs_readdir` + `uv_fs_closedir` | -| `FS.readDirSorted` | `Path → IO (Array DirEntry)` | Like `FS.readDir` but sorted by name. | `uv_fs_opendir` + `uv_fs_readdir` + `uv_fs_closedir` | - -## Temporary Files - -`Std.FS.tempDir` (`IO Path`) resolves the system temp directory (`%TEMP%`/`%TMP%` on Windows, `$TMPDIR` on POSIX, falling back to a platform default), not hardcoded to `"/tmp"`. Following `std::env::temp_dir` + `tempfile`'s `tempdir`/`tempdir_in` split, each operation comes in a plain form (creates in `Std.FS.tempDir`) and an `*In` form (creates inside a caller-supplied `dir`), rather than a single function taking `Option Path`: an always-required `dir` parameter composes with a trailing closure without the caller needing to pass an explicit `none` first. - -| Function | Type | Description | libuv | -| ---------------------- | ---------------------------------- | ---------------------------------------------------------------------------------- | ----------------------------------- | -| `FS.createTempFile` | `IO (File × Path)` | Create a secure temporary file in `Std.FS.tempDir`. Caller is responsible for deleting it. | `uv_fs_mkstemp` | -| `FS.createTempFileIn` | `Path → IO (File × Path)` | Create a secure temporary file inside `dir`. Caller is responsible for deleting it. | `uv_fs_mkstemp` | -| `FS.createTempDir` | `IO Path` | Create a secure temporary directory in `Std.FS.tempDir`. Caller is responsible for deleting it. | `uv_fs_mkdtemp` | -| `FS.createTempDirIn` | `Path → IO Path` | Create a secure temporary directory inside `dir`. Caller is responsible for deleting it. | `uv_fs_mkdtemp` | -| `FS.withTempFile` | `(File → Path → IO α) → IO α` | Create a temporary file in `Std.FS.tempDir`, run an action, delete it in a `finally` block. | `uv_fs_mkstemp` + `uv_fs_unlink` | -| `FS.withTempFileIn` | `Path → (File → Path → IO α) → IO α` | Create a temporary file inside `dir`, run an action, delete it in a `finally` block. | `uv_fs_mkstemp` + `uv_fs_unlink` | -| `FS.withTempDir` | `(Path → IO α) → IO α` | Create a temporary directory in `Std.FS.tempDir`, run an action, delete it recursively in a `finally` block. | `uv_fs_mkdtemp` + `FS.removeDirAll` | -| `FS.withTempDirIn` | `Path → (Path → IO α) → IO α` | Create a temporary directory inside `dir`, run an action, delete it recursively in a `finally` block. | `uv_fs_mkdtemp` + `FS.removeDirAll` | - -## Symlinks - -The current API has `symlinkMetadata` (reads metadata without following the link), but no way to create symlinks or read their targets. `hardLink` is in FS Operations. - -| Function | Type | Description | libuv | -| ------------------ | ------------------------------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ---------------- | -| `FS.createSymlink` | `(target : Path) → (link : Path) → (dir : Bool := false) → IO Unit` | Create a symbolic link at `link` pointing to `target`. `target` is stored verbatim and need not exist at creation time. The `dir` flag is required on Windows (`UV_FS_SYMLINK_DIR`) when the target is a directory; on POSIX it is ignored. | `uv_fs_symlink` | -| `FS.readSymlink` | `Path → IO Path` | Read the raw target of a symbolic link without resolving it. Contrast with `Path.canonicalize` which follows the full chain. | `uv_fs_readlink` | - -## Metadata - -Timestamps use `Std.Time.Timestamp`. `creationTime` is `Option Timestamp` because Linux does not expose file creation time; libuv signals absence by falling back to another timestamp rather than reporting it, so the current implementation always produces `some` and the value is best-effort. - -```lean -structure Metadata where - accessed : Timestamp - modified : Timestamp - creationTime : Option Timestamp - byteSize : UInt64 - type : FileType - numLinks : UInt64 - permissions : FileRight - inode : Option UInt64 -- none on FAT32 and some network filesystems - device : Option UInt64 -- none on FAT32 and some network filesystems - uid : Option UInt32 -- owner user ID; none on Windows - gid : Option UInt32 -- owner group ID; none on Windows -``` - -| Function | Type | Description | libuv | -| ---------------------- | ------------------------------------------------------------------ | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ---------------- | -| `FS.metadata` | `Path → IO Metadata` | Return metadata for a path, following symlinks. | `uv_fs_stat` | -| `FS.symlinkMetadata` | `Path → IO Metadata` | Return metadata for a path without following the final symlink. | `uv_fs_lstat` | -| `FS.isDir` | `Path → BaseIO Bool` | Return `true` if the path exists and is a directory. Returns `false` on any error. | `uv_fs_stat` | -| `FS.isFile` | `Path → BaseIO Bool` | Return `true` if the path exists and is a regular file. Returns `false` on any error. | `uv_fs_stat` | -| `FS.isSymlink` | `Path → BaseIO Bool` | Return `true` if the path is a symbolic link without following it. Returns `false` on any error. | `uv_fs_lstat` | -| `FS.pathExists` | `Path → BaseIO Bool` | Return `true` if the path exists (as any file type). Returns `false` on any error. | `uv_fs_stat` | -| `FS.getPermissions` | `Path → IO FileRight` | Return permission bits by path. Follows symlinks. | `uv_fs_stat` | -| `FS.setPermissions` | `Path → FileRight → IO Unit` | Set permission bits by path. Follows symlinks. | `uv_fs_chmod` | -| `FS.setTimes` | `Path → (accessed : Timestamp) → (modified : Timestamp) → IO Unit` | Set both access and modification timestamps by path. | `uv_fs_utime` | -| `FS.setSymlinkTimes` | `Path → (accessed : Timestamp) → (modified : Timestamp) → IO Unit` | Like `FS.setTimes` but operates on the symlink itself rather than its target. | `uv_fs_lutime` | -| `File.getPermissions` | `File → IO FileRight` | Return the open file's current permission bits. | `uv_fs_fstat` | -| `FS.filesystemStats` | `Path → IO FilesystemStats` | Return filesystem-level statistics (total/free space, inode counts) for the filesystem containing `path`. | `uv_fs_statfs` | -| `Metadata.sameFile` | `Metadata → Metadata → Bool` | Return `true` if two `Metadata` values refer to the same underlying file, compared by `inode` and `device`. Returns `false` if either has no inode (e.g. FAT32). | | - -### FilesystemStats - -```lean -structure FilesystemStats where - type : UInt64 -- filesystem type identifier, as reported by the OS - blockSize : UInt64 -- fundamental block size, in bytes - blocks : UInt64 -- total number of blocks - blocksFree : UInt64 -- free blocks - blocksAvailable : UInt64 -- free blocks available to unprivileged users - files : UInt64 -- total number of file nodes (inodes) - filesFree : UInt64 -- free file nodes -``` - -## Directory Utilities - -| Function | Type | Description | libuv | -| --------- | --------------------------------------------------- | --------------------------------- | -------------------------------------- | -| `FS.walk` | `Path → (ignoreErrors : Bool := false) → IO (IterM (α := WalkIterator) IO DirEntry)` | Lazy recursive directory walk. If `ignoreErrors`, a subtree that fails to open or read (e.g. permission denied) is skipped instead of aborting the whole walk; the directory entry itself is still yielded. The top-level `dir` is not covered by `ignoreErrors` and still raises on failure. | `uv_fs_opendir` + `uv_fs_readdir` + `uv_fs_closedir` | -| `FS.glob` | `Path → String → (ignoreErrors : Bool := false) → IO (Array DirEntry)` | Recursively list all entries beneath `dir` whose full path matches a `/`-separated glob `pattern` (`Path.matchGlob`). Built on `FS.walk`. | `uv_fs_opendir` + `uv_fs_readdir` + `uv_fs_closedir` | - -## Shared Plumbing - -A few conversion helpers are public rather than private so that `Std.Async.FS` can reuse them instead -of duplicating the conversion. They are not part of the intended user-facing surface. - -| Function | Type | Description | -| ------------------------------ | ------------------------------------------- | --------------------------------------------------------------------------- | -| `File.ofInternal` | `Internal.FS.File → File` | Wrap an already-open internal file, for the async open/create/temp helpers. | -| `File.toInternal` | `File → Internal.FS.File` | The underlying internal file (read-only; `File.mk` stays private). | -| `Dir.ofInternal` | `Internal.FS.Dir → Path → Dir` | Wrap an internal directory stream already opened at `path`. | -| `FS.metadataOfStat` | `Internal.FS.Stat → Metadata` | Build a `Metadata` from a raw stat result. | -| `FS.filesystemStatsOfStatFS` | `Internal.FS.StatFS → FilesystemStats` | Build a `FilesystemStats` from a raw statfs result. | -| `FS.timestampToFloatSeconds` | `Timestamp → Float` | Convert to the `Float` seconds that `uv_fs_utime`/`futime` take. | - -# Async Variants - -Everything in `Std.Async.FS` returns `Async α` rather than `IO α`, and lives in the same namespace as -its synchronous counterpart (`Std.FS.File.*Async`, `Std.FS.*Async`). Unless noted, each `*Async` -function has the same signature and semantics as the function it mirrors, with `IO` replaced by -`Async`. - -## File - -| Function | Type | Notes | -| ---------------------------- | ---------------------------------------------------------------------------------------- | ------------------------------------------------------------------------- | -| `File.openExistingAsync` | `Path → (mode : OpenMode := .readOnly) → Async File` | | -| `File.createAsync` | `Path → (mode : OpenMode := .writeCreate) → (perm : FileRight := .default) → Async File` | | -| `File.withFileAsync` | `Path → (mode : OpenMode := .readOnly) → (File → Async α) → Async α` | | -| `File.closeAsync` | `File → Async Unit` | | -| `File.readAtAsync` | `File → (offset : UInt64) → (n : USize) → (_buf : ByteArray) → Async ByteArray` | The async primitive has no buffer-reuse fast path, so `_buf` is accepted only for signature parity and is ignored. | -| `File.writeAtAsync` | `File → (offset : UInt64) → ByteArray → Async Unit` | | -| `File.writeAsync` | `File → ByteArray → Async Unit` | | -| `File.syncAllAsync` | `File → Async Unit` | | -| `File.syncDataAsync` | `File → Async Unit` | | -| `File.sendFileAsync` | `(src dst : File) → (offset : Int64) → (length : USize) → Async USize` | | -| `File.setLengthAsync` | `File → (len : UInt64) → Async Unit` | | -| `File.metadataAsync` | `File → Async Metadata` | | -| `File.getPermissionsAsync` | `File → Async FileRight` | | -| `File.setPermissionsAsync` | `File → FileRight → Async Unit` | | -| `File.setTimesAsync` | `File → (accessed modified : Timestamp) → Async Unit` | | -| `File.chownAsync` | `File → (uid gid : UInt32) → Async Unit` | No-op on Windows. | -| `File.lockAsync` | `File → (exclusive : Bool := true) → Async Unit` | Runs on a dedicated work thread (`uv_queue_work`); see the note below. | -| `File.tryLockAsync` | `File → (exclusive : Bool := true) → Async Bool` | Runs inline; never blocks for an unbounded time. | -| `File.unlockAsync` | `File → Async Unit` | Runs inline; never blocks for an unbounded time. | -| `File.atomicallyAsync` | `File → (exclusive : Bool := true) → Async α → Async α` | | - -`File.putStr`/`File.putStrLn` have no async counterpart; use `writeAsync` with `String.toUTF8`. - -## Handle, Pipe, and TTY - -| Function | Type | Notes | -| ------------------- | ------------------------------------------------------------ | ---------------------------------------------------------------------------- | -| `Handle.readAsync` | `Handle → (n : USize) → Async ByteArray` | Resolves with the bytes read; empty at EOF. | -| `Handle.writeAsync` | `Handle → ByteArray → Async Unit` | | -| `Handle.closeAsync` | `Handle → Async Unit` | | -| `Pipe.readAsync` | `Pipe → (n : USize) → Async ByteArray` | | -| `Pipe.writeAsync` | `Pipe → ByteArray → Async Unit` | | -| `Pipe.closeAsync` | `Pipe → Async Unit` | | -| `TTY.readAsync` | `TTY → (n : USize) → Async ByteArray` | | -| `TTY.writeAsync` | `TTY → ByteArray → Async Unit` | | -| `TTY.closeAsync` | `TTY → Async Unit` | | - -These take no `buf` argument. The synchronous `Handle.read` accepts one because it can hand libuv a -buffer it will fill before the call returns; an async read resolves a `Promise` after the caller has -moved on, so there is no uniquely-owned buffer to reuse and the allocation-avoidance path does not -apply. This matches `File.readAtAsync`, whose `_buf` exists only for signature parity. - -For the `tty` and `pipe` kinds these submit `uv_read_start`/`uv_write` directly and resolve on the -completion callback — no semaphore, no blocked thread. For a `file` kind (redirected stdio) they go -through the same `uv_fs_read`/`uv_fs_write` thread-pool path as `File`'s async operations. - -`TTY.setMode`, `TTY.getWinSize`, and the kind predicates have no async variants: they are -non-blocking calls against local state. - -## Convenience - -| Function | Type | -| ----------------------- | --------------------------------------- | -| `FS.readFileAsync` | `Path → Async String` | -| `FS.readBinFileAsync` | `Path → Async ByteArray` | -| `FS.linesAsync` | `Path → Async (Array String)` | -| `FS.writeFileAsync` | `Path → String → Async Unit` | -| `FS.writeBinFileAsync` | `Path → ByteArray → Async Unit` | -| `FS.appendFileAsync` | `Path → ByteArray → Async Unit` | -| `FS.appendTextFileAsync`| `Path → String → Async Unit` | - -`readBinFileAsync` reads sequentially at the cursor in 64 KiB chunks until EOF, rather than sizing the -buffer from `stat` up front like the synchronous `readBinFile`. - -## FS Operations - -| Function | Type | -| ----------------------- | ----------------------------------------------------------------- | -| `FS.copyFileAsync` | `Path → Path → Async Unit` | -| `FS.removeFileAsync` | `Path → Async Unit` | -| `FS.renameAsync` | `Path → Path → Async Unit` | -| `FS.hardLinkAsync` | `(orig link : Path) → Async Unit` | -| `FS.truncateAsync` | `Path → (len : UInt64) → Async Unit` | -| `FS.chownAsync` | `Path → (uid gid : UInt32) → Async Unit` | -| `FS.lchownAsync` | `Path → (uid gid : UInt32) → Async Unit` | -| `FS.createSymlinkAsync` | `(target link : Path) → (dir : Bool := false) → Async Unit` | -| `FS.readSymlinkAsync` | `Path → Async Path` | -| `FS.resolveAsync` | `Path → Async Path` | - -`FS.resolveAsync` mirrors `Path.resolve` (make absolute and resolve all symlinks) and is backed by -`uv_fs_realpath`. It lives here because there is no async `Path` module. - -## Directories - -| Function | Type | -| ------------------------ | ----------------------------------------------------------------------- | -| `FS.createDirAsync` | `Path → (perm : FileRight := .defaultDir) → Async Unit` | -| `FS.createDirAllAsync` | `Path → (perm : FileRight := .defaultDir) → Async Unit` | -| `FS.removeDirAsync` | `Path → Async Unit` | -| `FS.removeDirAllAsync` | `Path → (ignoreErrors : Bool := false) → Async Unit` | -| `FS.copyDirAsync` | `(src dst : Path) → (ignoreErrors : Bool := false) → Async Unit` | -| `FS.readDirAsync` | `Path → Async (Array DirEntry)` | -| `FS.readDirSortedAsync` | `Path → Async (Array DirEntry)` | -| `FS.walkAsync` | `Path → (ignoreErrors : Bool := false) → Async (Array DirEntry)` | -| `FS.globAsync` | `Path → String → (ignoreErrors : Bool := false) → Async (Array DirEntry)` | - -`Dir` itself has no async surface: there is no `Dir.openExistingAsync`/`nextAsync`/`iterAsync`, so -asynchronous traversal goes through the eager path-keyed helpers above. `walkAsync`/`globAsync` -collect into an `Array` rather than returning a lazy `IterM`, since `Async` has no lazy-iterator -integration yet. - -## Metadata and Permissions - -| Function | Type | -| ---------------------------- | ----------------------------------------------------------------- | -| `FS.metadataAsync` | `Path → Async Metadata` | -| `FS.symlinkMetadataAsync` | `Path → Async Metadata` | -| `FS.isFileAsync` | `Path → Async Bool` | -| `FS.isDirAsync` | `Path → Async Bool` | -| `FS.isSymlinkAsync` | `Path → Async Bool` | -| `FS.pathExistsAsync` | `Path → Async Bool` | -| `FS.getPermissionsAsync` | `Path → Async FileRight` | -| `FS.setPermissionsAsync` | `Path → FileRight → Async Unit` | -| `FS.setTimesAsync` | `Path → (accessed modified : Timestamp) → Async Unit` | -| `FS.setSymlinkTimesAsync` | `Path → (accessed modified : Timestamp) → Async Unit` | -| `FS.filesystemStatsAsync` | `Path → Async FilesystemStats` | - -The four predicates return `Async Bool`, not `BaseIO Bool` as their synchronous counterparts do; they -still swallow every error and answer `false`. - -## Temporary Files - -| Function | Type | -| -------------------------- | ------------------------------------------- | -| `FS.createTempFileAsync` | `Async (File × Path)` | -| `FS.createTempFileInAsync` | `Path → Async (File × Path)` | -| `FS.withTempFileAsync` | `(File → Path → Async α) → Async α` | -| `FS.withTempFileInAsync` | `Path → (File → Path → Async α) → Async α` | -| `FS.createTempDirAsync` | `Async Path` | -| `FS.createTempDirInAsync` | `Path → Async Path` | -| `FS.withTempDirAsync` | `(Path → Async α) → Async α` | -| `FS.withTempDirInAsync` | `Path → (Path → Async α) → Async α` | From 2f0426e46f412f956090b078a00528afcd6388d7 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Tue, 4 Aug 2026 19:56:43 -0300 Subject: [PATCH 4/5] fix: adapt to agent --- src/Std/Http/Client/Connector.lean | 11 +- src/Std/Http/Client/Pool.lean | 148 +++++++------- tests/elab/async_http_client_edge_pool.lean | 204 ++++++++++++-------- 3 files changed, 201 insertions(+), 162 deletions(-) diff --git a/src/Std/Http/Client/Connector.lean b/src/Std/Http/Client/Connector.lean index 874a9953cbb2..259af4f1ecc6 100644 --- a/src/Std/Http/Client/Connector.lean +++ b/src/Std/Http/Client/Connector.lean @@ -6,7 +6,7 @@ Authors: Sofia Rodrigues module prelude -public import Std.Http.Client.Session +public import Std.Http.Client.Connection import Std.Async.DNS public section @@ -28,7 +28,7 @@ open Time set_option linter.all true /-- -Opens a new transport connection to a target `(scheme, host, port)` and wraps it in a `Session`. +Opens a new transport connection to a target `(scheme, host, port)` and wraps it in a `Connection`. Supply your own function to customize DNS resolution or transport selection (plain TCP, TLS, Unix socket). `scheme` is provided so implementations can dispatch between plain and encrypted @@ -37,7 +37,7 @@ transports; `config.proxy` is available for proxy routing. Failures are reported as a typed `Error` (usually `Error.connect`). An exception thrown by a connector is also treated as a connect failure by the pool. -/ -abbrev Connector := URI.Scheme → URI.Host → UInt16 → Config → Async (Except Error Session) +abbrev Connector := URI.Scheme → URI.Host → UInt16 → Config → Async (Except Error Connection) /-- The default connector: resolves `host` via the system DNS, iterates over the returned @@ -52,7 +52,8 @@ def Connector.tcp : Connector := fun scheme host port config => do return .error (.connect "default TCP connector does not support https.") if scheme.val != "http" then - return .error (.connect s!"default TCP connector only supports http, got scheme {scheme.val.quote}") + return .error (.connect + s!"default TCP connector only supports http, got scheme {scheme.val.quote}") let (connectHost, connectPort) := config.proxy.getD (toString host, port) let addrs ← @@ -71,7 +72,7 @@ def Connector.tcp : Connector := fun scheme host port config => do try let socket ← Socket.Client.mk socket.connect socketAddr - return .ok (← Session.new socket config) + return .ok (← Connection.new socket config) catch err => lastErr := .connect (toString err) diff --git a/src/Std/Http/Client/Pool.lean b/src/Std/Http/Client/Pool.lean index cb9ebfdf62c1..d855a2aad22a 100644 --- a/src/Std/Http/Client/Pool.lean +++ b/src/Std/Http/Client/Pool.lean @@ -15,13 +15,13 @@ public section /-! # Pool -A simple connection pool that keeps at most one reusable session. +A simple connection pool that keeps at most one reusable connection. -If the next request targets the current session's origin, the session is reused. If the origin -changes, the current session is retired and a new session is opened for the new origin. +If the next request targets the current connection's origin, the connection is reused. If the origin +changes, the current connection is retired and a new one is opened for the new origin. Use `Pool.new` to create a pool, then call `pool.send` to dispatch requests through managed -sessions. The pool handles redirect following and middlewares. +connections. The pool handles redirect following and middlewares. -/ namespace Std.Http.Client @@ -32,19 +32,18 @@ open Time set_option linter.all true /-- -The single reusable session currently held by the pool. +The single reusable connection currently held by the pool. -/ structure Pool.Slot where - /-- - Origin this session is connected to. + Origin this connection is connected to. -/ origin : URI.Origin /-- - The current session. + The current connection. -/ - session : Session + connection : Connection /-- Default number of connection-level retries for pools and clients. One retry absorbs the @@ -54,22 +53,21 @@ without sending any request more than twice. def Pool.defaultMaxRetries : Nat := 1 /-- -A connection pool that manages one reusable session at a time. +A connection pool that manages one reusable connection at a time. -/ structure Pool where - /-- - Current reusable session, if any. + Current reusable connection, if any. -/ state : Mutex (Option Pool.Slot) /-- - Configuration used when creating new sessions. + Configuration used when creating new connections. -/ config : Config /-- - Monotonically increasing counter for unique session IDs. + Monotonically increasing counter for unique connection IDs. -/ nextId : Mutex UInt64 @@ -79,7 +77,7 @@ structure Pool where middlewares : Array Middleware := #[] /-- - Function used to open new transport sessions. Supply a custom `Connector` via `Pool.new`. + Function used to open new transport connections. Supply a custom `Connector` via `Pool.new`. -/ connect : Connector := Connector.tcp @@ -87,7 +85,7 @@ structure Pool where Maximum number of times to retry a failed request on a fresh connection. `0` disables retries. - Retries only apply to connection-level failures (the session died before a response was + Retries only apply to connection-level failures (the connection died before a response was received). Application-level errors (4xx, 5xx) are never retried automatically. **Only idempotent methods with replayable bodies are retried.** Requests whose method @@ -100,7 +98,7 @@ namespace Pool /-- Creates a new, empty connection pool. Supply a custom `connect` function (e.g. a TLS -connector or a mock) to customize how transport sessions are opened. +connector or a mock) to customize how transport connections are opened. -/ def new (config : Config := {}) (connect : Connector := Connector.tcp) (maxRetries : Nat := Pool.defaultMaxRetries) (middlewares : Array Middleware := #[]) : @@ -110,28 +108,29 @@ def new (config : Config := {}) (connect : Connector := Connector.tcp) pure { state, config, nextId, middlewares, connect, maxRetries } /-- -Closes and removes the pool's current session, if any. The pool remains usable: a later +Closes and removes the pool's current connection, if any. The pool remains usable: a later `send` simply opens a fresh connection. -/ def close (pool : Pool) : Async Unit := do let slot ← pool.state.atomically <| modifyGet fun slot => (slot, none) if let some slot := slot then - discard <| slot.session.close + slot.connection.close /-- -Acquires a fresh unique session ID. +Acquires a fresh unique connection ID. -/ -private def nextSessionId (pool : Pool) : Async UInt64 := +private def nextConnectionId (pool : Pool) : Async UInt64 := pool.nextId.atomically <| modifyGet fun id => (id, id + 1) /-- -Opens a new session for `origin` and assigns it a pool-local ID. The connector runs under +Opens a new connection for `origin` and assigns it a pool-local ID. The connector runs under `Config.connectTimeout`, bounding DNS resolution and the transport connect. An exception thrown by a custom connector is reported as `Error.connect`, keeping every connector-level failure typed on one path. -/ -private def openSession (pool : Pool) (origin : URI.Origin) : Async (Except Error Session) := do - let resultChannel : Std.Channel (Except Error Session) ← Std.Channel.new +private def openConnection (pool : Pool) (origin : URI.Origin) : + Async (Except Error Connection) := do + let resultChannel : Std.Channel (Except Error Connection) ← Std.Channel.new let connectTask ← async (t := AsyncTask) do try @@ -149,94 +148,97 @@ private def openSession (pool : Pool) (origin : URI.Origin) : Async (Except Erro ] match outcome with - | some (.ok session) => - let id ← nextSessionId pool - return .ok { session with id } + | some (.ok connection) => + let id ← nextConnectionId pool + return .ok { connection with id } | some (.error e) => return .error e | none => -- The connector may still complete after the timeout; drain its result in the - -- background and close the late session so the transport does not leak. + -- background and close the late connection so the transport does not leak. background do let late ← Selectable.one #[.case resultChannel.recvSelector pure] - if let .ok session := late then - discard <| session.close + if let .ok connection := late then + connection.close + let timeout := pool.config.connectTimeout.val return .error (.connect - s!"connecting to {origin.host}:{origin.port} timed out after {pool.config.connectTimeout.val}ms") + s!"connecting to {origin.host}:{origin.port} timed out after {timeout}ms") /-- -Returns the pool's single session for `origin`. +Returns the pool's single connection for `origin`. -If the current session has the same origin, it is checked out again; HTTP/1.1 requests -queue on the session. If the origin differs, the current session is retired and replaced. +If the current connection has the same origin, it is checked out again; HTTP/1.1 requests +queue on the connection. If the origin differs, the current connection is retired and replaced. -A new session is opened *outside* the state mutex: DNS resolution and the TCP connect can block, -and holding the lock across them would serialize every other pool operation (including session +A new connection is opened *outside* the state mutex: DNS resolution and the TCP connect can block, +and holding the lock across them would serialize every other pool operation (including connection retirement). The lock is taken only for the brief fast-path check and to install the freshly -opened session. +opened connection. -/ -def getOrCreateSession (pool : Pool) (origin : URI.Origin) : Async (Except Error Session) := do - -- Fast path: reuse an existing same-origin session without opening anything. A parked session - -- whose background loop has already shut down (server EOF, idle keep-alive timeout) is evicted - -- instead of returned: handing it out would fail the request even though nothing was ever - -- written to the wire for it. A session can still die between this check and the actual send; +def getOrCreateConnection (pool : Pool) (origin : URI.Origin) : + Async (Except Error Connection) := do + -- Fast path: reuse an existing same-origin connection without opening anything. A parked + -- connection whose background loop has already shut down (server EOF, idle keep-alive timeout) is + -- evicted instead of returned: handing it out would fail the request even though nothing was ever + -- written to the wire for it. A connection can still die between this check and the actual send; -- that residual race surfaces as a connection error handled by the retry policy in `send`. let existing ← pool.state.atomically do match ← get with | some slot => if slot.origin == origin then - if ← slot.session.isClosed then + if ← slot.connection.isClosed then set (none : Option Pool.Slot) pure none else - pure (some slot.session) + pure (some slot.connection) else pure none | none => pure none - if let some session := existing then - return .ok session + if let some connection := existing then + return .ok connection - -- Slow path: open a new session with the lock released. - match ← pool.openSession origin with + -- Slow path: open a new connection with the lock released. + match ← pool.openConnection origin with | .error e => return .error e - | .ok session => + | .ok connection => - -- Install it, retiring whatever is parked. If another task installed a same-origin session + -- Install it, retiring whatever is parked. If another task installed a same-origin connection -- while we were connecting, keep theirs and discard ours so the pool never holds two live - -- sessions. + -- connections. let (chosen, evicted) ← pool.state.atomically do match ← get with | some slot => if slot.origin == origin then - pure (slot.session, some session) + pure (slot.connection, some connection) else - set (some ({ origin, session } : Pool.Slot)) - pure (session, some slot.session) + set (some ({ origin, connection } : Pool.Slot)) + pure (connection, some slot.connection) | none => - set (some ({ origin, session } : Pool.Slot)) - pure (session, none) - if let some evictedSession := evicted then - discard <| evictedSession.close + set (some ({ origin, connection } : Pool.Slot)) + pure (connection, none) + if let some evictedConnection := evicted then + evictedConnection.close return .ok chosen /-- -Removes a session from the pool and closes its request channel. +Removes a connection from the pool and closes its request channel. -/ -private def retireSession (pool : Pool) (origin : URI.Origin) (session : Session) : Async Unit := do +private def retireConnection (pool : Pool) (connection : Connection) (origin : URI.Origin) : + Async Unit := do pool.state.atomically <| modify fun | some slot => - if slot.origin == origin && slot.session.id == session.id then none else some slot + if slot.origin == origin && slot.connection.id == connection.id then none else some slot | none => none - discard <| session.close + connection.close /-- -Sends a request through the pooled session, following redirects and applying middlewares, +Sends a request through the pooled connection, following redirects and applying middlewares, returning the response or the typed `Error` that ended the exchange. On a retryable connection-level failure (see `Error.isRetryable`), retries up to `pool.maxRetries` times on fresh connections. Application-level failures (timeouts, protocol violations, body-size limits) are never retried. -Session lifecycle is owned by the agent driving the exchange: a failed hop, a cross-origin -redirect swap, or a connection error after the final response hands the session back to the +Connection lifecycle is owned by the agent driving the exchange: a failed hop, a cross-origin +redirect swap, or a connection error after the final response hands the connection back to the pool, which retires it. Cross-origin redirects keep the pool to one live origin at a time. -/ def trySend {β : Type} [Coe β Body.Any] (pool : Pool) (origin : URI.Origin) (request : Request β) @@ -253,20 +255,20 @@ def trySend {β : Type} [Coe β Body.Any] (pool : Pool) (origin : URI.Origin) (r let attempts := retries + 1 - -- A single attempt: acquire a session and run the exchange. `Agent.trySend` owns session - -- cleanup — every failure path inside it releases the session back to the pool — so the + -- A single attempt: acquire a connection and run the exchange. `Agent.trySend` owns connection + -- cleanup — every failure path inside it releases the connection back to the pool — so the -- attempt only has to report the typed result to the retry loop below. Connection -- establishment is part of the attempt so that DNS/TCP failures are retried too. let attemptOnce : Async (Except Error (Response Body.Stream)) := do - match ← pool.getOrCreateSession origin with + match ← pool.getOrCreateConnection origin with | .error e => return .error e - | .ok session => + | .ok connection => Agent.trySend { - session + connection origin middlewares := pool.middlewares - release := fun sess o => pool.retireSession o sess - crossOrigin := .follow pool.getOrCreateSession + release := pool.retireConnection + crossOrigin := .follow pool.getOrCreateConnection } request overrides for attempt in 0...attempts do @@ -286,7 +288,7 @@ def trySend {β : Type} [Coe β Body.Any] (pool : Pool) (origin : URI.Origin) (r return .error (.io (IO.userError "HTTP client retry loop exhausted without returning")) /-- -Sends a request through the pooled session, following redirects and applying middlewares. +Sends a request through the pooled connection, following redirects and applying middlewares. Use `trySend` to receive failures as a typed `Error` instead of a thrown exception. -/ def send {β : Type} [Coe β Body.Any] (pool : Pool) (origin : URI.Origin) (request : Request β) diff --git a/tests/elab/async_http_client_edge_pool.lean b/tests/elab/async_http_client_edge_pool.lean index 54047f379dda..fcac16d0fc93 100644 --- a/tests/elab/async_http_client_edge_pool.lean +++ b/tests/elab/async_http_client_edge_pool.lean @@ -2,21 +2,23 @@ module import Std.Http.Test.Helpers +/-! HTTP client connection-pool, keep-alive, timeout, shutdown, and retry edge cases. -/ + open Std.Async open Std Http Internal open Test.ClientHelpers -/-! HTTP client connection-pool, keep-alive, timeout, shutdown, and retry edge cases. -/ - -- ============================================================ -- Section 7 — Keep-alive and Connection: close -- ============================================================ --- The simplified pool keeps one session at a time. A same-origin request sent --- while the previous response body is unread queues on that session and reaches +-- The simplified pool keeps one connection at a time. A same-origin request sent +-- while the previous response body is unread queues on that connection and reaches -- the wire only after the caller closes or drains the previous body. -#eval show IO _ from runWithTimeout "single-connection pool queues behind unread response body" 4000 <| Async.block do +#eval show IO _ from + runWithTimeout "single-connection pool queues behind unread response body" 4000 <| + Async.block do let (mockClient1, mockServer1) ← Mock.new let connectCount ← IO.mkRef 0 @@ -24,8 +26,8 @@ open Test.ClientHelpers let n ← connectCount.get connectCount.set (n + 1) match n with - | 0 => return .ok (← Client.Session.new mockServer1 (config := config)) - | _ => throw (IO.userError "pool opened more sessions than expected") + | 0 => return .ok (← Client.Connection.new mockServer1 (config := config)) + | _ => throw (IO.userError "pool opened more connections than expected") let pool ← Client.Pool.new {} connect let some domain := URI.DomainName.ofString? "example.com" @@ -68,12 +70,14 @@ open Test.ClientHelpers unless (← connectCount.get) == 1 do resp1.body.close mockClient1.close - throw (IO.userError "single-connection pool opened a second same-origin session") + throw (IO.userError "single-connection pool opened a second same-origin connection") if let some bytes ← mockClient1.tryRecv? then resp1.body.close mockClient1.close - throw (IO.userError s!"queued request reached the wire before the first body was closed:\n{(String.fromUTF8! bytes).quote}") + let text := String.fromUTF8! bytes + throw (IO.userError + s!"queued request reached the wire before the first body was closed:\n{text.quote}") resp1.body.close @@ -93,10 +97,12 @@ open Test.ClientHelpers throw <| IO.userError s!"second request did not use the queued connection:\n{secondText.quote}" -- Once the caller closes an unread pooled response body, the connection loop --- drains the wire body and reports completion. The pool should then return the --- session to idle instead of opening another available connection. +-- drains the wire body and reports completion. The pool should then park the +-- connection as idle instead of opening a new one. -#eval show IO _ from runWithTimeout "pool reuses session after unread response body is closed" 4000 <| Async.block do +#eval show IO _ from + runWithTimeout "pool reuses connection after unread response body is closed" 4000 <| + Async.block do let (mockClient1, mockServer1) ← Mock.new let (_mockClient2, mockServer2) ← Mock.new let connectCount ← IO.mkRef 0 @@ -105,9 +111,9 @@ open Test.ClientHelpers let n ← connectCount.get connectCount.set (n + 1) match n with - | 0 => return .ok (← Client.Session.new mockServer1 (config := config)) - | 1 => return .ok (← Client.Session.new mockServer2 (config := config)) - | _ => throw (IO.userError "pool opened more sessions than expected") + | 0 => return .ok (← Client.Connection.new mockServer1 (config := config)) + | 1 => return .ok (← Client.Connection.new mockServer2 (config := config)) + | _ => throw (IO.userError "pool opened more connections than expected") let pool ← Client.Pool.new {} connect let some domain := URI.DomainName.ofString? "example.com" @@ -152,7 +158,7 @@ open Test.ClientHelpers IO.sleep 50 if (← connectCount.get) != 1 then mockClient1.close - throw (IO.userError "pool opened a second session after the first response body was closed") + throw (IO.userError "pool opened a second connection after the first response body was closed") let secondBytes ← drainRequest mockClient1 mockClient1.send (rawResp "200 OK" @@ -170,9 +176,11 @@ open Test.ClientHelpers throw <| IO.userError s!"second request did not reuse the first connection:\n{secondText.quote}" -- A zero-length pooled response still needs to drive the connection through --- completion so the session is returned to idle. +-- completion so the connection is returned to idle. -#eval show IO _ from runWithTimeout "pool reuses session after zero-length response body completes" 4000 <| Async.block do +#eval show IO _ from + runWithTimeout "pool reuses connection after zero-length response body completes" 4000 <| + Async.block do let (mockClient1, mockServer1) ← Mock.new let (_mockClient2, mockServer2) ← Mock.new let connectCount ← IO.mkRef 0 @@ -181,9 +189,9 @@ open Test.ClientHelpers let n ← connectCount.get connectCount.set (n + 1) match n with - | 0 => return .ok (← Client.Session.new mockServer1 (config := config)) - | 1 => return .ok (← Client.Session.new mockServer2 (config := config)) - | _ => throw (IO.userError "pool opened more sessions than expected") + | 0 => return .ok (← Client.Connection.new mockServer1 (config := config)) + | 1 => return .ok (← Client.Connection.new mockServer2 (config := config)) + | _ => throw (IO.userError "pool opened more connections than expected") let pool ← Client.Pool.new {} connect let some domain := URI.DomainName.ofString? "example.com" @@ -230,7 +238,7 @@ open Test.ClientHelpers IO.sleep 50 if (← connectCount.get) != 1 then mockClient1.close - throw (IO.userError "pool opened a second session after a zero-length response completed") + throw (IO.userError "pool opened a second connection after a zero-length response completed") let secondBytes ← drainRequest mockClient1 mockClient1.send (rawResp "200 OK" @@ -247,9 +255,11 @@ open Test.ClientHelpers unless secondText.startsWith "GET /two" do throw <| IO.userError s!"second request did not reuse the first connection:\n{secondText.quote}" --- A different origin replaces the pool's single current session. +-- A different origin replaces the pool's single current connection. -#eval show IO _ from runWithTimeout "single-connection pool replaces session on origin change" 4000 <| Async.block do +#eval show IO _ from + runWithTimeout "single-connection pool replaces connection on origin change" 4000 <| + Async.block do let (mockClient1, mockServer1) ← Mock.new let (mockClient2, mockServer2) ← Mock.new let connectCount ← IO.mkRef 0 @@ -258,9 +268,9 @@ open Test.ClientHelpers let n ← connectCount.get connectCount.set (n + 1) match n with - | 0 => return .ok (← Client.Session.new mockServer1 (config := config)) - | 1 => return .ok (← Client.Session.new mockServer2 (config := config)) - | _ => throw (IO.userError "pool opened more sessions than expected") + | 0 => return .ok (← Client.Connection.new mockServer1 (config := config)) + | 1 => return .ok (← Client.Connection.new mockServer2 (config := config)) + | _ => throw (IO.userError "pool opened more connections than expected") let pool ← Client.Pool.new {} connect let some domain1 := URI.DomainName.ofString? "example.com" @@ -316,7 +326,8 @@ open Test.ClientHelpers | some bytes => mockClient1.close mockClient2.close - throw (IO.userError s!"old-origin connection stayed open after origin change:\n{(String.fromUTF8! bytes).quote}") + throw (IO.userError + s!"old-origin connection stayed open after origin change:\n{(String.fromUTF8! bytes).quote}") let secondBytes ← drainRequest mockClient2 mockClient2.send (rawResp "200 OK" @@ -330,17 +341,20 @@ open Test.ClientHelpers throw (IO.userError s!"expected second body 'two', got {body.quote}") unless (← connectCount.get) == 2 do - throw (IO.userError "origin change did not open exactly one replacement session") + throw (IO.userError "origin change did not open exactly one replacement connection") let secondText := String.fromUTF8! secondBytes unless secondText.startsWith "GET /two" do - throw <| IO.userError s!"second-origin request did not use the replacement connection:\n{secondText.quote}" + throw <| IO.userError + s!"second-origin request did not use the replacement connection:\n{secondText.quote}" -- If a pooled cross-origin redirect leaves the original origin, the outgoing --- session is retired instead of being returned idle. A target-acquire failure --- must close that old session and leave the pool able to open a clean +-- connection is retired instead of being returned idle. A target-acquire failure +-- must close that old connection and leave the pool able to open a clean -- replacement for the original origin. -#eval show IO _ from runWithTimeout "failed cross-origin redirect retires old session and keeps pool usable" 4000 <| Async.block do +#eval show IO _ from + runWithTimeout "failed cross-origin redirect retires old connection and keeps pool usable" 4000 <| + Async.block do let (mockClient1, mockServer1) ← Mock.new let (mockClient2, mockServer2) ← Mock.new let originalConnectCount ← IO.mkRef 0 @@ -352,9 +366,9 @@ open Test.ClientHelpers let n ← originalConnectCount.get originalConnectCount.set (n + 1) match n with - | 0 => return .ok (← Client.Session.new mockServer1 (config := config)) - | 1 => return .ok (← Client.Session.new mockServer2 (config := config)) - | _ => throw (IO.userError "opened too many original-origin sessions") + | 0 => return .ok (← Client.Connection.new mockServer1 (config := config)) + | 1 => return .ok (← Client.Connection.new mockServer2 (config := config)) + | _ => throw (IO.userError "opened too many original-origin connections") -- Retries are disabled: this test asserts the state the pool is left in after a -- single failed cross-origin acquire, not the retry policy. @@ -399,7 +413,8 @@ open Test.ClientHelpers | some bytes => mockClient1.close mockClient2.close - throw (IO.userError s!"retired redirect source connection stayed readable:\n{(String.fromUTF8! bytes).quote}") + throw (IO.userError + s!"retired redirect source connection stayed readable:\n{(String.fromUTF8! bytes).quote}") let req2 ← Request.new |>.method .get |>.uri! "/again" |>.header! "Host" "example.com" |>.empty @@ -415,14 +430,17 @@ open Test.ClientHelpers if (← originalConnectCount.get) != 2 then mockClient1.close mockClient2.close - throw (IO.userError "pool did not open a replacement original-origin session for the follow-up request") + throw (IO.userError + "pool did not open a replacement original-origin connection for the follow-up request") let secondBytes ← drainRequest mockClient2 mockClient2.send (rawResp "200 OK" #[("Content-Length", "2"), ("Connection", "close")] "ok") match ← await p2.result! with - | Except.error e => throw (IO.userError s!"original session was not reused after failed redirect acquire: {e}") + | Except.error e => + throw (IO.userError + s!"original connection was not reused after failed redirect acquire: {e}") | Except.ok resp => let body ← resp.body.readAll (α := String) unless body == "ok" do @@ -430,12 +448,14 @@ open Test.ClientHelpers let secondText := String.fromUTF8! secondBytes unless secondText.startsWith "GET /again" do - throw <| IO.userError s!"second request did not use the replacement connection:\n{secondText.quote}" + throw <| IO.userError + s!"second request did not use the replacement connection:\n{secondText.quote}" --- Two sequential requests on the same session must both succeed, exercising the +-- Two sequential requests on the same connection must both succeed, exercising the -- `.next` reset path in the connection state machine. -#eval show IO _ from runWithTimeout "two sequential GETs on keep-alive succeed" 4000 <| Async.block do +#eval show IO _ from runWithTimeout "two sequential GETs on keep-alive succeed" 4000 <| + Async.block do let (mockClient, mockServer) ← Mock.new let agent ← mkAgent mockServer @@ -455,7 +475,7 @@ open Test.ClientHelpers unless body == "one" do throw (IO.userError s!"expected 'one', got {body.quote}") - -- Second request on same session must succeed. + -- Second request on same connection must succeed. let req2 ← Request.new |>.method .get |>.uri! "/two" |>.header! "Host" "example.com" |>.empty let p2 ← sendInBackground agent req2 @@ -471,8 +491,8 @@ open Test.ClientHelpers unless body == "two" do throw (IO.userError s!"expected 'two', got {body.quote}") --- `Connection: close` on the response must close the session; a follow-up request --- on the same session must error out rather than hang. +-- `Connection: close` on the response must close the connection; a follow-up request +-- on the same connection must error out rather than hang. #eval show IO _ from runWithTimeout "Connection: close prevents reuse" 4000 <| Async.block do let (mockClient, mockServer) ← Mock.new @@ -491,10 +511,10 @@ open Test.ClientHelpers | Except.ok resp => let _ ← resp.body.readAll (α := String) - -- Close the mock's receive side so the session observes EOF. + -- Close the mock's receive side so the connection observes EOF. mockClient.close - -- Second send must not hang; it must fail because the session is closed. + -- Second send must not hang; it must fail because the connection is closed. let req2 ← Request.new |>.method .get |>.uri! "/" |>.header! "Host" "example.com" |>.empty let p2 ← sendInBackground agent req2 @@ -505,13 +525,14 @@ open Test.ClientHelpers | Except.error _ => pure () -- ============================================================ --- Section 12 — Request deadline and session close +-- Section 12 — Request deadline and connection close -- ============================================================ -- The absolute `requestTimeout` deadline must abort a response whose body stalls after the headers -- arrive, surfacing the error to a caller blocked reading the body (rather than hanging until the -- much larger per-read idle timeout). -#eval show IO _ from runWithTimeout "request deadline aborts a stalled response body" 4000 <| Async.block do +#eval show IO _ from runWithTimeout "request deadline aborts a stalled response body" 4000 <| + Async.block do let (mockClient, mockServer) ← Mock.new let agent ← mkAgent mockServer (config := { requestTimeout := ⟨300, by decide⟩ }) @@ -544,7 +565,8 @@ open Test.ClientHelpers -- Incoming progress must not re-arm the whole-request timeout. A server can keep the idle timer -- alive by dripping bytes, but the absolute request deadline must still end the exchange. -#eval show IO _ from runWithTimeout "request deadline aborts a slow-drip response body" 4000 <| Async.block do +#eval show IO _ from runWithTimeout "request deadline aborts a slow-drip response body" 4000 <| + Async.block do let (mockClient, mockServer) ← Mock.new let agent ← mkAgent mockServer (config := { requestTimeout := ⟨250, by decide⟩ }) @@ -571,11 +593,12 @@ open Test.ClientHelpers | Except.ok body => throw (IO.userError s!"slow-drip response escaped request deadline with {body.quote}") --- `Session.close` must abort an in-flight exchange promptly (via the connection's cancellation --- context), not leave the caller blocked until the request timeout. The request timeout below is set --- far beyond the test budget so that only `close` can end the request; without the context wiring the --- background loop stays parked on the socket and this test times out. -#eval show IO _ from runWithTimeout "session close aborts an in-flight request" 4000 <| Async.block do +-- `Connection.close` must abort an in-flight exchange promptly (via the connection's cancellation +-- context), not leave the caller blocked until the request timeout. The request timeout below is +-- set far beyond the test budget so that only `close` can end the request; without the context +-- wiring the background loop stays parked on the socket and this test times out. +#eval show IO _ from runWithTimeout "connection close aborts an in-flight request" 4000 <| + Async.block do let (mockClient, mockServer) ← Mock.new let agent ← mkAgent mockServer (config := { requestTimeout := ⟨60000, by decide⟩ }) @@ -589,16 +612,17 @@ open Test.ClientHelpers -- Server receives the request but never responds; only close should end it. let _ ← drainRequest mockClient - agent.session.close + agent.connection.close match ← await resultPromise.result! with | Except.error _ => pure () | Except.ok _ => - throw (IO.userError "expected in-flight request to abort when the session is closed") + throw (IO.userError "expected in-flight request to abort when the connection is closed") -- Opening a transport must not hold the pool state mutex. The first connector is deliberately -- blocked; a second-origin acquisition must enter its connector before the first is released. -#eval show IO _ from runWithTimeout "pool does not hold state mutex while connecting" 4000 <| Async.block do +#eval show IO _ from runWithTimeout "pool does not hold state mutex while connecting" 4000 <| + Async.block do let (_mockClient1, mockServer1) ← Mock.new let (_mockClient2, mockServer2) ← Mock.new let calls ← Std.Mutex.new 0 @@ -612,10 +636,10 @@ open Test.ClientHelpers if callNo == 0 then discard <| firstStarted.resolve () await releaseFirst.result! - return .ok (← Client.Session.new mockServer1 (config := config)) + return .ok (← Client.Connection.new mockServer1 (config := config)) else secondSawReleased.set (← released.get) - return .ok (← Client.Session.new mockServer2 (config := config)) + return .ok (← Client.Connection.new mockServer2 (config := config)) let pool ← Client.Pool.new {} connect let some domainA := URI.DomainName.ofString? "a.example" @@ -631,16 +655,16 @@ open Test.ClientHelpers let secondDone : IO.Promise Unit ← IO.Promise.new background do - let .ok session ← pool.getOrCreateSession originA - | throw (IO.userError "first-origin session acquisition failed") + let .ok connection ← pool.getOrCreateConnection originA + | throw (IO.userError "first-origin connection acquisition failed") discard <| firstDone.resolve () - session.close + connection.close await firstStarted.result! background do - let .ok session ← pool.getOrCreateSession originB - | throw (IO.userError "second-origin session acquisition failed") + let .ok connection ← pool.getOrCreateConnection originB + | throw (IO.userError "second-origin connection acquisition failed") discard <| secondDone.resolve () - session.close + connection.close background do IO.sleep 300 released.set true @@ -651,8 +675,9 @@ open Test.ClientHelpers throw (IO.userError "second connection was blocked behind the pool state mutex") await firstDone.result! --- Idempotent requests retry a connector failure, including a failure before a `Session` exists. -#eval show IO _ from runWithTimeout "GET retries after the first connection attempt fails" 4000 <| Async.block do +-- Idempotent requests retry a connector failure, including a failure before a `Connection` exists. +#eval show IO _ from runWithTimeout "GET retries after the first connection attempt fails" 4000 <| + Async.block do let (mockClient, mockServer) ← Mock.new let calls ← IO.mkRef 0 let connect : Client.Connector := fun _ _ _ config => do @@ -660,7 +685,7 @@ open Test.ClientHelpers calls.set (callNo + 1) if callNo == 0 then throw (IO.userError "synthetic first connect failure") - return .ok (← Client.Session.new mockServer (config := config)) + return .ok (← Client.Connection.new mockServer (config := config)) let pool ← Client.Pool.new {} connect (maxRetries := 1) let some domain := URI.DomainName.ofString? "example.com" | throw (IO.userError "DomainName parse failed") @@ -690,14 +715,16 @@ open Test.ClientHelpers throw (IO.userError s!"expected two connection attempts, got {← calls.get}") -- A non-idempotent request is never retried after the peer drops the first connection mid-flight. -#eval show IO _ from runWithTimeout "POST is not retried after a mid-flight connection drop" 4000 <| Async.block do +#eval show IO _ from runWithTimeout "POST is not retried after a mid-flight connection drop" 4000 <| + Async.block do let (mockClient1, mockServer1) ← Mock.new let (_mockClient2, mockServer2) ← Mock.new let calls ← IO.mkRef 0 let connect : Client.Connector := fun _ _ _ config => do let callNo ← calls.get calls.set (callNo + 1) - return .ok (← Client.Session.new (if callNo == 0 then mockServer1 else mockServer2) (config := config)) + let mockServer := if callNo == 0 then mockServer1 else mockServer2 + return .ok (← Client.Connection.new mockServer (config := config)) let pool ← Client.Pool.new {} connect (maxRetries := 3) let some domain := URI.DomainName.ofString? "example.com" | throw (IO.userError "DomainName parse failed") @@ -722,19 +749,21 @@ open Test.ClientHelpers throw (IO.userError s!"POST was retried; expected one connection attempt, got {← calls.get}") -- ============================================================ --- Section 14 — Retry body integrity and dead-session detection +-- Section 14 — Retry body integrity and dead-connection detection -- ============================================================ -- An idempotent request whose streaming body was consumed by the failed attempt must NOT be -- retried: the body cannot be replayed, so a retry would silently send an empty body. -#eval show IO _ from runWithTimeout "PUT with non-replayable stream body is not retried" 4000 <| Async.block do +#eval show IO _ from runWithTimeout "PUT with non-replayable stream body is not retried" 4000 <| + Async.block do let (mockClient1, mockServer1) ← Mock.new let (mockClient2, mockServer2) ← Mock.new let calls ← IO.mkRef 0 let connect : Client.Connector := fun _ _ _ config => do let callNo ← calls.get calls.set (callNo + 1) - return .ok (← Client.Session.new (if callNo == 0 then mockServer1 else mockServer2) (config := config)) + let mockServer := if callNo == 0 then mockServer1 else mockServer2 + return .ok (← Client.Connection.new mockServer (config := config)) let pool ← Client.Pool.new {} connect (maxRetries := 3) let some domain := URI.DomainName.ofString? "example.com" | throw (IO.userError "DomainName parse failed") @@ -775,20 +804,23 @@ open Test.ClientHelpers | Except.ok _ => throw (IO.userError "PUT with a consumed stream body unexpectedly succeeded via retry") | Except.error _ => pure () - unless (← calls.get) == 1 do + let attempts ← calls.get + unless attempts == 1 do throw (IO.userError - s!"PUT with non-replayable body was retried; expected 1 connection attempt, got {← calls.get}") + s!"PUT with non-replayable body was retried; expected 1 attempt, got {attempts}") -- A replayable (`Body.Full`) request body must be reset before a retry so the second attempt -- sends the complete payload again, not the consumed remainder. -#eval show IO _ from runWithTimeout "retried PUT resends the full replayable body" 4000 <| Async.block do +#eval show IO _ from runWithTimeout "retried PUT resends the full replayable body" 4000 <| + Async.block do let (mockClient1, mockServer1) ← Mock.new let (mockClient2, mockServer2) ← Mock.new let calls ← IO.mkRef 0 let connect : Client.Connector := fun _ _ _ config => do let callNo ← calls.get calls.set (callNo + 1) - return .ok (← Client.Session.new (if callNo == 0 then mockServer1 else mockServer2) (config := config)) + let mockServer := if callNo == 0 then mockServer1 else mockServer2 + return .ok (← Client.Connection.new mockServer (config := config)) let pool ← Client.Pool.new {} connect (maxRetries := 1) let some domain := URI.DomainName.ofString? "example.com" | throw (IO.userError "DomainName parse failed") @@ -824,24 +856,28 @@ open Test.ClientHelpers throw <| IO.userError s!"retried PUT did not resend the request body:\n{retryText.quote}" --- A pooled session whose connection has already shut down (idle timeout, server EOF) must not be +-- A pooled connection whose background loop has already shut down (idle timeout, server EOF) must +-- not be -- handed to the next request: the request was never written to the wire, so the pool can safely -- open a fresh connection — even for non-idempotent methods and with retries disabled. -#eval show IO _ from runWithTimeout "pool discards a dead session instead of failing the next request" 4000 <| Async.block do +#eval show IO _ from + runWithTimeout "pool discards a dead connection instead of failing the next request" 4000 <| + Async.block do let (mockClient1, mockServer1) ← Mock.new let (mockClient2, mockServer2) ← Mock.new let calls ← IO.mkRef 0 let connect : Client.Connector := fun _ _ _ config => do let callNo ← calls.get calls.set (callNo + 1) - return .ok (← Client.Session.new (if callNo == 0 then mockServer1 else mockServer2) (config := config)) + let mockServer := if callNo == 0 then mockServer1 else mockServer2 + return .ok (← Client.Connection.new mockServer (config := config)) let pool ← Client.Pool.new {} connect (maxRetries := 0) let some domain := URI.DomainName.ofString? "example.com" | throw (IO.userError "DomainName parse failed") let origin : URI.Origin := { scheme := URI.Scheme.ofString! "http", host := .name domain, port := 80 } - -- First exchange completes cleanly; the session is parked in the pool. + -- First exchange completes cleanly; the connection is parked in the pool. let req1 ← Request.new |>.method .get |>.uri! "/one" |>.header! "Host" "example.com" |>.empty let p1 : IO.Promise (Except String (Response Body.Stream)) ← IO.Promise.new @@ -864,7 +900,7 @@ open Test.ClientHelpers IO.sleep 200 -- The next request (a POST: retries disabled and non-idempotent anyway) must transparently get - -- a fresh connection rather than an error from the dead parked session. + -- a fresh connection rather than an error from the dead parked connection. let req2 ← Request.new |>.method .post |>.uri! "/two" |>.header! "Host" "example.com" |>.text "data" let p2 : IO.Promise (Except String (Response Body.Stream)) ← IO.Promise.new @@ -879,7 +915,7 @@ open Test.ClientHelpers #[("Content-Length", "2"), ("Connection", "close")] "ok") match ← await p2.result! with - | Except.error e => throw (IO.userError s!"POST after dead parked session failed: {e}") + | Except.error e => throw (IO.userError s!"POST after dead parked connection failed: {e}") | Except.ok resp => let _ ← resp.body.readAll (α := String) unless (← calls.get) == 2 do From a615e23d30f8f3e85173ab108ee4acb396f7b8f7 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Wed, 5 Aug 2026 11:54:54 -0300 Subject: [PATCH 5/5] test: fix assertions --- tests/elab/async_http_client_edge_pool.lean | 32 ++++++++++++++++----- 1 file changed, 25 insertions(+), 7 deletions(-) diff --git a/tests/elab/async_http_client_edge_pool.lean b/tests/elab/async_http_client_edge_pool.lean index fcac16d0fc93..a47b4ca32ec1 100644 --- a/tests/elab/async_http_client_edge_pool.lean +++ b/tests/elab/async_http_client_edge_pool.lean @@ -321,13 +321,15 @@ open Test.ClientHelpers catch e => pure (Except.error (toString e)) discard <| p2.resolve result + -- `recv?` returns `none` only once the old connection's transport is closed, so this doubles as + -- the retirement check: an old connection left open makes the test run out its wall clock here. match ← mockClient1.recv? with | none => pure () | some bytes => mockClient1.close mockClient2.close throw (IO.userError - s!"old-origin connection stayed open after origin change:\n{(String.fromUTF8! bytes).quote}") + s!"the new origin's request was written to the old connection:\n{(String.fromUTF8! bytes).quote}") let secondBytes ← drainRequest mockClient2 mockClient2.send (rawResp "200 OK" @@ -408,13 +410,15 @@ open Test.ClientHelpers mockClient2.close throw (IO.userError s!"unexpected redirect failure: {e}") + -- As above, `none` means the transport was closed; a source connection left open instead ends + -- this test on its wall clock. match ← mockClient1.recv? with | none => pure () | some bytes => mockClient1.close mockClient2.close throw (IO.userError - s!"retired redirect source connection stayed readable:\n{(String.fromUTF8! bytes).quote}") + s!"a request was written to the retired redirect source connection:\n{(String.fromUTF8! bytes).quote}") let req2 ← Request.new |>.method .get |>.uri! "/again" |>.header! "Host" "example.com" |>.empty @@ -511,19 +515,32 @@ open Test.ClientHelpers | Except.ok resp => let _ ← resp.body.readAll (α := String) - -- Close the mock's receive side so the connection observes EOF. - mockClient.close + -- The response itself must retire the connection. Closing the mock here instead would fail the + -- second request through a dead transport whether or not `Connection: close` was honoured. + let mut retired := false + for _ in [0:50] do + if ← agent.connection.isClosed then + retired := true + break + IO.sleep 20 + unless retired do + mockClient.close + throw (IO.userError "the connection was still open after a Connection: close response") -- Second send must not hang; it must fail because the connection is closed. let req2 ← Request.new |>.method .get |>.uri! "/" |>.header! "Host" "example.com" |>.empty let p2 ← sendInBackground agent req2 + -- Nothing reaches the wire either: a retired connection *is* one whose request channel is closed + -- (`Connection.isClosed` reads that channel), so the send above failed before writing anything. match ← await p2.result! with | Except.ok _ => throw (IO.userError "second request unexpectedly succeeded after Connection: close") | Except.error _ => pure () + mockClient.close + -- ============================================================ -- Section 12 — Request deadline and connection close -- ============================================================ @@ -549,10 +566,11 @@ open Test.ClientHelpers mockClient.send (rawResp "200 OK" #[("Content-Length", "10"), ("Connection", "close")] "") + -- The head arrives immediately and the deadline is 300ms away, so it must reach the caller; + -- accepting an up-front error here would hide a regression that withholds the head. match ← await resultPromise.result! with - | Except.error _ => - -- Deadline surfaced before the headers were returned — still a valid enforcement. - pure () + | Except.error e => + throw (IO.userError s!"the response head was not delivered before the deadline: {e}") | Except.ok resp => let got : Except String String ← try let s ← resp.body.readAll (α := String)