Two focused contributions to Oliver Dressler’s Lean LSP MCP server. Explore what happens when build phases reset, requests overlap, and the last waiter leaves.
Synthetic events only · no server connection
Lake’s job count may repeat, grow, or restart. Each reported notification still advances the request’s counter by one.
Try repeated counts and phase resets. The bright line keeps climbing.
No notifications emitted
This experiment illustrates the monotonic-progress branch only. A fresh request starts a fresh counter. Lake counts stay in message text; total is unspecified.
Every new request supersedes the previous build. In share mode, earlier waiters follow the replacement.
Cleanup starts when a build is superseded or loses its last waiter.
A simplified POSIX state model, not running Python or Lake. Cleanup waits are advanced by you, not wall-clock timers. The “allow” mode, which permits independent builds, is outside this lab.
A build can pass through clean, cache, and compilation phases. Their local job counts do not form one stable measuring stick.
The contribution increments a runner-local counter across notifications, sends no total, and retains Lake’s original counts in the message. Repeated counts and new phases no longer move the MCP progress value backward.
Read monotonic progress change 38b7e1cA cancelled request must release its own interest. In share mode, another interested request keeps the latest build alive. With no waiters left, that build is cancelled and its cleanup is drained.
A replacement starts only after the predecessor’s cleanup finishes. Repeated cancellation must not interrupt that drain, including when intermediate builds never started.
Read bounded cleanup change f73dcf6The guarantee follows the process group the runner owns.
These are focused contributions in Alok’s public fork of Oliver Dressler’s Lean LSP MCP, an MIT-licensed server connecting AI assistants with Lean’s language server. This page does not claim authorship of the whole project.
The two pinned branch snapshots are independent. The cancellation snapshot does not incorporate the monotonic-progress change. This site makes no claim of an upstream pull request, acceptance, or merge.
The public source includes tests for progress resets, notification failures, cancellation, and pipe-holding descendants. These describe intended behavior. Local checks and review do not establish public CI status. This exhibit runs only original JavaScript simulations with invented events; it never starts processes, builds Lean code, reads files, or contacts an MCP server.