Repository navigation
Keep Lake setup output out of the startup protocol and recover cancelled initialization - #823
Conversation
Route dependency hook progress to the Lean log before protocol startup and allow Stop followed by retry while initialization is pending. Include the process-tree termination helper so cancellation does not wait for a dependency hook to finish.
Codex Review Summary: ✅ CompletedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: f88b65bb98
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| } | ||
| this.pending = Buffer.concat([this.pending, chunk]) | ||
| const text = this.pending.toString('latin1') | ||
| const header = /Content-Length:[ \t]*[0-9]+\r\n/i.exec(text) |
There was a problem hiding this comment.
When a dependency hook writes an HTTP-style line such as Content-Length: 123\r\n (for example, curl -i output) before Lean starts, this regex treats that hook output as the first LSP header. The branch then permanently sets protocolStarted and forwards the hook's response/body to StreamMessageReader, so the cold server startup fails before the real Lean header arrives. Since these hooks can emit arbitrary stdout, wait for a complete frame and validate that it is JSON-RPC before switching modes.
Useful? React with 👍 / 👎.
Hook output can contain HTTP-style Content-Length headers. Validate a bounded complete JSON-RPC body before switching readers, and keep searching later candidates when an earlier hook frame is incomplete.
Summary
Cold
lake servestartup can run dependencypost_updatehooks before the Lean server starts. Their ordinary stdout then reaches the JSON-RPC reader ahead of its firstContent-Lengthheader, leaving initialization stuck. Stopping that client previously did nothing because it was not yet running.Changes
IO.printwithout a newline and carriage-return progress.terminateProcess.shin the extension bundle and VSIX with executable permissions. Without this asset, its delayed process-tree cleanup silently fails on Unix.Testing
extension/dist/terminateProcess.shhas mode0755and bytes identical to the dependency's helper.The language-client library still logs initialization/connection errors when a pending startup is deliberately terminated; cancellation settles and a subsequent restart succeeds.