Skip to content

fix: always use last active lean editor as active client#750

Merged
mhuisi merged 1 commit intoleanprover:masterfrom
mhuisi:push-lkkxzuvmzsty
Mar 31, 2026
Merged

fix: always use last active lean editor as active client#750
mhuisi merged 1 commit intoleanprover:masterfrom
mhuisi:push-lkkxzuvmzsty

Conversation

@mhuisi
Copy link
Copy Markdown
Collaborator

@mhuisi mhuisi commented Mar 31, 2026

This PR ensures that the client provider always uses the last active lean editor for its active client instead of attempting to manage this state by itself. This fixes a bug where the active client of the client provider could sometimes de-sync from the actual lean file that the user is looking at.

The following analysis by Claude on the bug fixed by this PR is fully accurate:

Root Cause

The bug is that onDidOpenLeanDocument (line 86 of clientProvider.ts) calls ensureClient for every Lean document that VS Code opens, including invisible/background documents. This silently
overwrites activeClient even though the user's active editor hasn't changed.

The onDidChangeActiveLeanEditor handler (line 71) would correct this by calling ensureClient for the project file — but it only fires when the active editor actually changes. Since
invisible document opens don't change the active editor, the correction never happens.

And when the invisible document is subsequently closed, updateActiveTextEditor is called, but since the active editor is still the same project file editor object, updateActiveLeanEditor
short-circuits at line 242 (equalsWithUndefined returns true) and the event doesn't fire.

How It Happens

The didOpen middleware comment at leanclient.ts:900-904 documents this exact behavior:

▎ holding Ctrl while hovering over an identifier will quickly emit a didOpen and then a didClose notification for the document the identifier is in

When a user Ctrl+hovers over a standard library symbol in their project file, VS Code preloads the definition's source file (inside ~/.elan/toolchains/.../src/lean/). This fires
workspace.onDidOpenTextDocument → onDidOpenLeanDocument → ensureClient(coreUri). If a core client already exists (from a previous go-to-definition), ensureClient immediately sets
activeClient to the core client (line 268). Nothing restores it.

Reproduction Steps

1. Open a Lean 4 project in VS Code (with lakefile.toml and lean-toolchain)
2. Open a .lean file and wait for the server to fully start
3. Go to Definition (F12) on any standard library symbol (e.g., List.map) — this navigates to a file in ~/.elan and creates a core client
4. Navigate back to your project file — activeClient is restored to the project client
5. Ctrl+hover over any standard library symbol (just hold Ctrl and move the mouse over List.map or similar, without clicking) — VS Code invisibly opens the core source file, ensureClient
silently overwrites activeClient to the core client
6. Run "Lean 4: Build Project" — it uses the core client, tries lake build in the toolchain directory, and fails because there's no lakefile

The user never leaves their project file. Step 5 is the invisible trigger — activeClient is silently switched by a background document open, and nothing switches it back because the active
editor never changed.

@mhuisi mhuisi merged commit 39b9340 into leanprover:master Mar 31, 2026
5 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant