LSP development setup problem

Stream: new members

[ptrl]

I’m interested in Lean’s LSP and would like to fix some bugs or add new features. I followed the configuration steps outlined in these two documents Development Workflow and Lean Server Readme, and attempted to modify the LSP code (by commenting out the logic in the handleRequest functions in Watchdog.lean and FileWorker.lean). However, after recompiling the source code and restarting VS Code, the changes I made to the LSP code didn’t take effect. Could anybody help me understand why this is happening? Below are the steps I took.

1. open workspace

code lean.code-workspace

2. setup toolchain

elan toolchain link lean4 build/release/stage1
elan toolchain link lean4-stage0 build/release/stage0

3. comment out handleRequest

-- Watchdog.lean
def handleRequest (id : RequestID) (method : String) (params : Json) : ServerM Unit := do
  return
-- FileWorker.lean
def handleRequest (id : RequestID) (method : String) (params : Json)
      : WorkerM Unit := do
    return

4. build lean

cd build/release
make -j6

5. reload
   Refresh File Dependencies
   Restart Server

Even after following these steps, I expected the LSP to stop functioning properly (for example, “Go to Definition” shouldn’t work), but the LSP is still working as usual. When I checked the Lean version using the ps command, I noticed it was running stage0. From what I understand, stage0 shouldn’t include the compiled Lean server. Could this be related to the issue?

$ps aux | grep lean
luoyangze        22456   0.0  0.2 412147840  78624   ??  S     4:48PM   0:01.66 /Users/luoyangze/.elan/toolchains/lean4-stage0/bin/lean --server /Users/luoyangze/lean/lean4/src
luoyangze        34849   0.0  1.0 412193424 369552   ??  Ss    4:59PM   0:02.47 /Users/luoyangze/lean/lean4/build/release/stage0/bin/lean --worker file:///Users/luoyangze/lean/lean4/src/Lean/Server/Watchdog.lean
luoyangze        34842   0.0  1.1 412372000 403488   ??  Ss    4:59PM   0:04.46 /Users/luoyangze/lean/lean4/build/release/stage0/bin/lean --worker file:///Users/luoyangze/lean/lean4/src/Lean/Server/FileWorker.lean

[Sebastian Ullrich]

Stage 0 is used to both build and while editing src/ - otherwise we couldn't do any editing before a first successful build. If you want to test changes, you should do it in tests/, which uses stage 1. I usually keep an untracked file tests/scratch.lean around for experimentation

[ptrl]

Sebastian Ullrich said:

Stage 0 is used to both build and while editing src/ - otherwise we couldn't do any editing before a first successful build. If you want to test changes, you should do it in tests/, which uses stage 1. I usually keep an untracked file tests/scratch.lean around for experimentation

I want to see the effects of my changes to the Lean/Server code in VS Code (for example, if I modify the semantic highlight logic, I want to see the color changes in VS Code). I found a somewhat hacky solution: I modified the code in vscode-lean to force the LSP to run from a specific path, changing it to build/release/stage1/bin/lean, and that works. Although it’s a bit cumbersome, it does the job. Is there a better way to achieve this?

[Sebastian Ullrich]

You can temporarily change src/lean-toolchain to lean4 and restart the server