Lean language server can't find local modules imported by current module

[glocq]

Summary

Lean language server fails when trying to import a module from another.

Reproduction Steps

What I Did

• Create a new project with lake new myproject
• Create a new module in myproject:
  • Create a new module with cd myproject && touch Myproject/Mymodule.lean
  • Add Myproject.Mymodule to the import list of Myproject.lean
  • Import Mymodule from the Basic module by adding import Myproject.Mymodule at the top of Myproject/Basic.lean
  • Build your project by running lake build
  • Open Helix from myproject's root, and open Myproject/Basic.lean

What happened

An error arises:

unknown module prefix 'Myproject'

No directory 'Myproject' or file 'Myproject.olean' in the search path entries:
/home/glocq/.elan/toolchains/leanprover--lean4---v4.22.0/lib/lean

(If you can't see the error, put your cursor at the very beginning of the first line of the file)

The rest of the code gets ignored, e.g. putting the cursor on hello, then pressing Space then k (for "Show docs for item under cursor") does not result in anything.

What Should Have Happened

The LSP server is able to access Mymodule. Actions such as "Show docs for item under cursor" bring up relevant info.

Probable Cause

From what I understand, the lean executable (which provides the LSP server) is not in charge of looking for the modules, that's the responsibility of the lake executable.

Fix

(tested, it works!)

In languages.toml, replace the line

lean = { command = "lean", args = ["--server"] }

with

lean = { command = "lake", args = ["serve"] }

Helix log

~/.cache/helix/helix.log

2025-09-03T15:45:23.602 helix_term::application [ERROR] Language Server: Method workspace/semanticTokens/refresh not found in request 0
2025-09-03T15:45:25.606 helix_term::application [ERROR] Language Server: Method workspace/semanticTokens/refresh not found in request 1

Platform

Linux

Terminal Emulator

GNOME Terminal 3.52.0 using VTE 0.76.0 +BIDI +GNUTLS +ICU +SYSTEMD and zellij 0.41.2

Installation Method

APT

Helix Version

helix 24.7 (079f544)