{"record":{"id":"15d463fa05bc2a8c","repo":"oraios/serena","slug":"lean-is-not-installed-or-not-in-path-please-insta","errorCode":null,"errorMessage":"lean is not installed or not in PATH.\nPlease install Lean 4 via elan: https://github.com/leanprover/elan\n  curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh\nAfter installation, make sure 'lean' is available on your PATH.","messagePattern":"lean is not installed or not in PATH\\.\nPlease install Lean 4 via elan: https://github\\.com/leanprover/elan\n  curl https://raw\\.githubusercontent\\.com/leanprover/elan/master/elan-init\\.sh -sSf \\| sh\nAfter installation, make sure 'lean' is available on your PATH\\.","errorType":"exception","errorClass":"RuntimeError","httpStatus":null,"severity":"error","filePath":"src/solidlsp/language_servers/lean4_language_server.py","lineNumber":33,"sourceCode":"\nlog = logging.getLogger(__name__)\n\n\nclass Lean4LanguageServer(SolidLanguageServer):\n    \"\"\"\n    Provides Lean 4 specific instantiation of the LanguageServer class.\n    Uses the built-in Lean 4 language server invoked via ``lean --server``.\n    Requires ``lean`` to be installed and available on PATH (typically via elan).\n    \"\"\"\n\n    class DependencyProvider(LanguageServerDependencyProviderSinglePath):\n        def __init__(self, custom_settings: SolidLSPSettings.CustomLSSettings, ls_resources_dir: str, repository_root_path: str):\n            super().__init__(custom_settings, ls_resources_dir)\n            self._repository_root_path = repository_root_path\n\n        def _get_or_install_core_dependency(self) -> str:\n            lean_path = shutil.which(\"lean\")\n            if lean_path is None:\n                raise RuntimeError(\n                    \"lean is not installed or not in PATH.\\n\"\n                    \"Please install Lean 4 via elan: https://github.com/leanprover/elan\\n\"\n                    \"  curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh\\n\"\n                    \"After installation, make sure 'lean' is available on your PATH.\"\n                )\n            return lean_path\n\n        def _create_launch_command(self, core_path: str) -> list[str]:\n            return [core_path, \"--server\"]\n\n        @override\n        def create_launch_command_env(self) -> dict[str, str]:\n            \"\"\"Provides LEAN_PATH and LEAN_SRC_PATH from ``lake env`` for cross-file references.\"\"\"\n            env: dict[str, str] = {}\n            lake_path = shutil.which(\"lake\")\n            if lake_path is None:\n                log.warning(\"lake not found on PATH; cross-file references may not work\")","sourceCodeStart":15,"sourceCodeEnd":51,"githubUrl":"https://github.com/oraios/serena/blob/7fcbca7e62555ec2287ddb2f083caee805848ea6/src/solidlsp/language_servers/lean4_language_server.py#L15-L51","documentation":"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.","triggerScenarios":"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.","commonSituations":"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.","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"],"exampleFix":"// before\nRUN pip install multilspy  # no lean toolchain\n// after\nRUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y \\\n && ENV PATH=\"/root/.elan/bin:${PATH}\"","handlingStrategy":"validation","validationCode":"import shutil, sys\nif shutil.which(\"lean\") is None:\n    sys.exit(\"Lean 4 not found. Install via elan: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh\")","typeGuard":null,"tryCatchPattern":"try:\n    server = SolidLSP(...lean config...)\nexcept RuntimeError as e:\n    if \"lean is not installed\" in str(e):\n        install_elan_and_retry()  # subprocess elan-init, then re-exec with updated PATH\n    else:\n        raise","preventionTips":["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"],"tags":["lean","missing-dependency","path","installation"],"backgroundTag":"executable-not-on-path","analyzedSha":"7fcbca7e62555ec2287ddb2f083caee805848ea6","analyzedAt":"2026-08-29T00:04:09.619Z","schemaVersion":2},"datasetVersion":"2026-08-29T02:17:18.158Z"}