oraios/serena · error · RuntimeError

lean is not installed or not in PATH. Please install Lean 4

Error message

lean is not installed or not in PATH.
Please install Lean 4 via elan: https://github.com/leanprover/elan
  curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
After installation, make sure 'lean' is available on your PATH.

What it means

Raised when the Lean 4 language server is requested but the `lean` executable cannot be found on PATH via shutil.which. Unlike many servers in this library, Lean is not auto-installed; the user must install Lean 4 themselves via elan. The error includes the exact elan install command.

Source

Thrown at src/solidlsp/language_servers/lean4_language_server.py:33

log = logging.getLogger(__name__)


class Lean4LanguageServer(SolidLanguageServer):
    """
    Provides Lean 4 specific instantiation of the LanguageServer class.
    Uses the built-in Lean 4 language server invoked via ``lean --server``.
    Requires ``lean`` to be installed and available on PATH (typically via elan).
    """

    class DependencyProvider(LanguageServerDependencyProviderSinglePath):
        def __init__(self, custom_settings: SolidLSPSettings.CustomLSSettings, ls_resources_dir: str, repository_root_path: str):
            super().__init__(custom_settings, ls_resources_dir)
            self._repository_root_path = repository_root_path

        def _get_or_install_core_dependency(self) -> str:
            lean_path = shutil.which("lean")
            if lean_path is None:
                raise RuntimeError(
                    "lean is not installed or not in PATH.\n"
                    "Please install Lean 4 via elan: https://github.com/leanprover/elan\n"
                    "  curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh\n"
                    "After installation, make sure 'lean' is available on your PATH."
                )
            return lean_path

        def _create_launch_command(self, core_path: str) -> list[str]:
            return [core_path, "--server"]

        @override
        def create_launch_command_env(self) -> dict[str, str]:
            """Provides LEAN_PATH and LEAN_SRC_PATH from ``lake env`` for cross-file references."""
            env: dict[str, str] = {}
            lake_path = shutil.which("lake")
            if lake_path is None:
                log.warning("lake not found on PATH; cross-file references may not work")

View on GitHub (pinned to 7fcbca7e62)

Solutions

Install Lean 4 via elan: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
Ensure ~/.elan/bin is on PATH (source ~/.profile or add export PATH="$HOME/.elan/bin:$PATH")
Verify with `which lean` / `lean --version` in the same shell that runs the library
In Docker/CI, add the elan install step to the image before running tests

Example fix

// before
RUN pip install multilspy  # no lean toolchain
// after
RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y \
 && ENV PATH="/root/.elan/bin:${PATH}"

Defensive patterns

Strategy: validation

Validate before calling

import shutil, sys
if shutil.which("lean") is None:
    sys.exit("Lean 4 not found. Install via elan: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh")

Try / catch

try:
    server = SolidLSP(...lean config...)
except RuntimeError as e:
    if "lean is not installed" in str(e):
        install_elan_and_retry()  # subprocess elan-init, then re-exec with updated PATH
    else:
        raise

Prevention

Bake elan installation into Dockerfiles/devcontainers
Add ~/.elan/bin to PATH in shell profiles and CI env
Run `lean --version` as a CI preflight step
Use the same shell environment for installation and test execution

When it happens

Trigger: Creating the Lean4 language server (solidlsp Lean4) on a machine where `lean` was never installed, installed via a package manager that only ships `leanpkg`, installed in a non-login shell/conda env where PATH does not include ~/.elan/bin, or in Docker images without elan.

Common situations: Fresh CI containers, devcontainers without Lean toolchain, installing elan in one shell but running tests from another with a different PATH, Windows users who installed Lean but did not add elan's bin dir to PATH.

Related errors

AI-assisted analysis of oraios/serena@7fcbca7e62 (2026-08-29). Data as JSON: /api/errors/15d463fa05bc2a8c. Report an issue: GitHub.