From 09c007d1e1b3900ea2b75192eb9f43e3e69623d9 Mon Sep 17 00:00:00 2001 From: Dan Rosen Date: Thu, 12 Mar 2026 06:32:31 -0400 Subject: [PATCH] Add Lean 4 language support (#1137) --- .github/workflows/pytest.yml | 4 + .gitignore | 3 + CHANGELOG.md | 1 + README.md | 2 +- docs/01-about/020_programming-languages.md | 3 + pyproject.toml | 1 + .../language_servers/lean4_language_server.py | 175 ++++++++++++++++++ src/solidlsp/ls_config.py | 7 + .../repos/lean4/test_repo/Helper.lean | 16 ++ .../resources/repos/lean4/test_repo/Main.lean | 24 +++ .../repos/lean4/test_repo/lake-manifest.json | 5 + .../repos/lean4/test_repo/lakefile.lean | 9 + .../repos/lean4/test_repo/lean-toolchain | 1 + test/serena/test_serena_agent.py | 3 + test/solidlsp/lean4/test_lean4_basic.py | 164 ++++++++++++++++ 15 files changed, 417 insertions(+), 1 deletion(-) create mode 100644 src/solidlsp/language_servers/lean4_language_server.py create mode 100644 test/resources/repos/lean4/test_repo/Helper.lean create mode 100644 test/resources/repos/lean4/test_repo/Main.lean create mode 100644 test/resources/repos/lean4/test_repo/lake-manifest.json create mode 100644 test/resources/repos/lean4/test_repo/lakefile.lean create mode 100644 test/resources/repos/lean4/test_repo/lean-toolchain create mode 100644 test/solidlsp/lean4/test_lean4_basic.py diff --git a/.github/workflows/pytest.yml b/.github/workflows/pytest.yml index 77f241fe..c3c0b95b 100644 --- a/.github/workflows/pytest.yml +++ b/.github/workflows/pytest.yml @@ -544,6 +544,10 @@ jobs: echo "ERROR: FPCDIR does not exist: $FPCDIR" exit 1 fi + - name: Build Lean 4 test project + uses: leanprover/lean-action@v1 + with: + lake-package-directory: test/resources/repos/lean4/test_repo - name: Cache language servers id: cache-language-servers uses: actions/cache@v3 diff --git a/.gitignore b/.gitignore index f156e0f6..213894d5 100644 --- a/.gitignore +++ b/.gitignore @@ -259,5 +259,8 @@ dist-newstyle/ cabal.project.local* .ghc.environment.* +# Lean 4 +.lake/ + zz-misc/ vue-implementation/ diff --git a/CHANGELOG.md b/CHANGELOG.md index e74f715a..1c6cae01 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -49,6 +49,7 @@ Status of the `main` branch. Changes prior to the next official version change w * Language support: + * **Add support for Lean 4** via built-in `lean --server` with cross-file reference support (requires `lean` and `lake` via [elan](https://github.com/leanprover/elan)) * **Add support for OCaml** via ocaml-lsp-server with cross-file reference support on OCaml 5.2+ (requires opam; see [setup guide](docs/03-special-guides/ocaml_setup_guide_for_serena.md)) * **Add Phpactor as alternative PHP language server** (specify `php_phpactor` as language; requires PHP 8.1+) * **Add support for Fortran** via fortls language server (requires `pip install fortls`) diff --git a/README.md b/README.md index be511138..2b65ea9d 100644 --- a/README.md +++ b/README.md @@ -82,7 +82,7 @@ that implement the language server protocol (LSP). The underlying language servers are typically open-source projects (like Serena) or at least freely available for use. With Serena's LSP library, we provide **support for over 30 programming languages**, including -AL, Bash, C#, C/C++, Clojure, Dart, Elixir, Elm, Erlang, Fortran, GLSL, Go, Groovy (partial support), Haskell, HLSL, Java, Javascript, Julia, Kotlin, Lua, Markdown, MATLAB, Nix, OCaml, Perl, PHP, PowerShell, Python, R, Ruby, Rust, Scala, Swift, TOML, TypeScript, WGSL, YAML, and Zig. +AL, Bash, C#, C/C++, Clojure, Dart, Elixir, Elm, Erlang, Fortran, GLSL, Go, Groovy (partial support), Haskell, HLSL, Java, Javascript, Julia, Kotlin, Lean 4, Lua, Markdown, MATLAB, Nix, OCaml, Perl, PHP, PowerShell, Python, R, Ruby, Rust, Scala, Swift, TOML, TypeScript, WGSL, YAML, and Zig. > [!IMPORTANT] > Some language servers require additional dependencies to be installed; see the [Language Support](https://oraios.github.io/serena/01-about/020_programming-languages.html) page for details. diff --git a/docs/01-about/020_programming-languages.md b/docs/01-about/020_programming-languages.md index 94d617e2..e70fd450 100644 --- a/docs/01-about/020_programming-languages.md +++ b/docs/01-about/020_programming-languages.md @@ -64,6 +64,9 @@ Some languages require additional installations or setup steps, as noted. * **Julia** * **Kotlin** (uses the pre-alpha [official kotlin LS](https://github.com/Kotlin/kotlin-lsp), some issues may appear) +* **Lean 4** + (requires `lean` and `lake` installed via [elan](https://github.com/leanprover/elan); uses the built-in Lean 4 LSP; + the project must be a Lake project with `lake build` run before use) * **Lua** * **Markdown** (must explicitly enable language `markdown`, primarily useful for documentation-heavy projects) diff --git a/pyproject.toml b/pyproject.toml index b1f9448e..a204b050 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -328,6 +328,7 @@ markers = [ "matlab: language server running for MATLAB (requires MATLAB R2021b+)", "systemverilog: language server running for SystemVerilog (uses verible-verilog-ls)", "hlsl: language server running for HLSL shaders (uses shader-language-server)", + "lean4: language server running for Lean 4", ] [tool.codespell] diff --git a/src/solidlsp/language_servers/lean4_language_server.py b/src/solidlsp/language_servers/lean4_language_server.py new file mode 100644 index 00000000..463e4992 --- /dev/null +++ b/src/solidlsp/language_servers/lean4_language_server.py @@ -0,0 +1,175 @@ +""" +Provides Lean 4 specific instantiation of the LanguageServer class. +Uses the built-in Lean 4 language server (lean --server). +""" + +import logging +import os +import pathlib +import shutil +import subprocess +from typing import cast + +from overrides import override + +from solidlsp.ls import LanguageServerDependencyProvider, LanguageServerDependencyProviderSinglePath, SolidLanguageServer +from solidlsp.ls_config import LanguageServerConfig +from solidlsp.lsp_protocol_handler.lsp_types import InitializeParams +from solidlsp.settings import SolidLSPSettings + +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") + return env + try: + result = subprocess.run( + [lake_path, "env"], + check=False, + cwd=self._repository_root_path, + capture_output=True, + text=True, + timeout=30, + ) + if result.returncode == 0: + for line in result.stdout.splitlines(): + if "=" in line: + key, _, value = line.partition("=") + if key in ("LEAN_PATH", "LEAN_SRC_PATH"): + env[key] = value + log.info(f"Lake env: {key}={value}") + else: + log.warning(f"lake env failed (exit {result.returncode}): {result.stderr[:200]}") + except Exception as e: + log.warning(f"Failed to run lake env: {e}") + return env + + def __init__(self, config: LanguageServerConfig, repository_root_path: str, solidlsp_settings: SolidLSPSettings): + """ + Creates a Lean4LanguageServer instance. This class is not meant to be + instantiated directly. Use LanguageServer.create() instead. + """ + super().__init__( + config, + repository_root_path, + None, + "lean4", + solidlsp_settings, + ) + + def _create_dependency_provider(self) -> LanguageServerDependencyProvider: + return self.DependencyProvider(self._custom_settings, self._ls_resources_dir, self.repository_root_path) + + @override + def is_ignored_dirname(self, dirname: str) -> bool: + return super().is_ignored_dirname(dirname) or dirname in [".lake", "build"] + + @staticmethod + def _get_initialize_params(repository_absolute_path: str) -> InitializeParams: + """ + Returns the initialize params for the Lean 4 Language Server. + """ + root_uri = pathlib.Path(repository_absolute_path).as_uri() + initialize_params = { + "processId": os.getpid(), + "rootPath": repository_absolute_path, + "rootUri": root_uri, + "capabilities": { + "textDocument": { + "synchronization": {"didSave": True, "dynamicRegistration": True}, + "definition": {"dynamicRegistration": True, "linkSupport": True}, + "references": {"dynamicRegistration": True}, + "documentSymbol": { + "dynamicRegistration": True, + "hierarchicalDocumentSymbolSupport": True, + "symbolKind": {"valueSet": list(range(1, 27))}, + }, + "hover": {"dynamicRegistration": True, "contentFormat": ["markdown", "plaintext"]}, + "completion": { + "dynamicRegistration": True, + "completionItem": { + "snippetSupport": True, + "documentationFormat": ["markdown", "plaintext"], + }, + }, + }, + "workspace": { + "workspaceFolders": True, + "didChangeConfiguration": {"dynamicRegistration": True}, + }, + }, + "workspaceFolders": [ + { + "uri": root_uri, + "name": os.path.basename(repository_absolute_path), + } + ], + } + return cast(InitializeParams, initialize_params) + + def _start_server(self) -> None: + """Start the Lean 4 language server process.""" + + def register_capability_handler(_params: dict) -> None: + return + + def window_log_message(msg: dict) -> None: + log.info(f"LSP: window/logMessage: {msg}") + + def do_nothing(_params: dict) -> None: + return + + self.server.on_request("client/registerCapability", register_capability_handler) + self.server.on_notification("window/logMessage", window_log_message) + self.server.on_notification("$/progress", do_nothing) + self.server.on_notification("textDocument/publishDiagnostics", do_nothing) + self.server.on_notification("$/lean/fileProgress", do_nothing) + + log.info("Starting Lean 4 language server process") + self.server.start() + initialize_params = self._get_initialize_params(self.repository_root_path) + + log.info("Sending initialize request from LSP client to LSP server and awaiting response") + init_response = self.server.send.initialize(initialize_params) + + capabilities = init_response.get("capabilities", {}) + log.info(f"Lean 4 LSP capabilities: {list(capabilities.keys())}") + + self.server.notify.initialized({}) + + @override + def _get_wait_time_for_cross_file_referencing(self) -> float: + """Lean 4 projects need time to compile and build cross-file references.""" + return 10.0 diff --git a/src/solidlsp/ls_config.py b/src/solidlsp/ls_config.py index c4d33522..00be0c7c 100644 --- a/src/solidlsp/ls_config.py +++ b/src/solidlsp/ls_config.py @@ -63,6 +63,7 @@ class Language(str, Enum): JULIA = "julia" FORTRAN = "fortran" HASKELL = "haskell" + LEAN4 = "lean4" GROOVY = "groovy" VUE = "vue" POWERSHELL = "powershell" @@ -244,6 +245,8 @@ class Language(str, Enum): ) case self.HASKELL: return FilenameMatcher("*.hs", "*.lhs") + case self.LEAN4: + return FilenameMatcher("*.lean") case self.VUE: path_patterns = ["*.vue"] for prefix in ["c", "m", ""]: @@ -444,6 +447,10 @@ class Language(str, Enum): from solidlsp.language_servers.haskell_language_server import HaskellLanguageServer return HaskellLanguageServer + case self.LEAN4: + from solidlsp.language_servers.lean4_language_server import Lean4LanguageServer + + return Lean4LanguageServer case self.FSHARP: from solidlsp.language_servers.fsharp_language_server import FSharpLanguageServer diff --git a/test/resources/repos/lean4/test_repo/Helper.lean b/test/resources/repos/lean4/test_repo/Helper.lean new file mode 100644 index 00000000..6112bfcd --- /dev/null +++ b/test/resources/repos/lean4/test_repo/Helper.lean @@ -0,0 +1,16 @@ +structure Calculator where + name : String + version : Nat + deriving Repr + +def add (x y : Nat) : Nat := + x + y + +def subtract (x y : Nat) : Int := + Int.ofNat x - Int.ofNat y + +def isPositive (x : Int) : Bool := + x > 0 + +def absolute (x : Int) : Int := + if isPositive x then x else -x diff --git a/test/resources/repos/lean4/test_repo/Main.lean b/test/resources/repos/lean4/test_repo/Main.lean new file mode 100644 index 00000000..261ef8ff --- /dev/null +++ b/test/resources/repos/lean4/test_repo/Main.lean @@ -0,0 +1,24 @@ +import Helper + +def multiply (x y : Nat) : Nat := + x * y + +def calculate (c : Calculator) (op : String) (x y : Nat) : Option Int := + match op with + | "add" => some (Int.ofNat (add x y)) + | "subtract" => some (subtract x y) + | "multiply" => some (Int.ofNat (multiply x y)) + | _ => none + +def main : IO Unit := do + let c : Calculator := { name := "TestCalc", version := 1 } + IO.println s!"Using {c.name} version {c.version}" + let result1 := add 5 3 + IO.println s!"5 + 3 = {result1}" + let result2 := subtract 10 4 + IO.println s!"10 - 4 = {result2}" + match calculate c "multiply" 6 7 with + | some result => IO.println s!"6 * 7 = {result}" + | none => IO.println "Calculation failed" + IO.println s!"Is 5 positive? {isPositive 5}" + IO.println s!"Absolute of -10: {absolute (-10)}" diff --git a/test/resources/repos/lean4/test_repo/lake-manifest.json b/test/resources/repos/lean4/test_repo/lake-manifest.json new file mode 100644 index 00000000..5a610bd8 --- /dev/null +++ b/test/resources/repos/lean4/test_repo/lake-manifest.json @@ -0,0 +1,5 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "test_repo", + "lakeDir": ".lake"} diff --git a/test/resources/repos/lean4/test_repo/lakefile.lean b/test/resources/repos/lean4/test_repo/lakefile.lean new file mode 100644 index 00000000..cb410f19 --- /dev/null +++ b/test/resources/repos/lean4/test_repo/lakefile.lean @@ -0,0 +1,9 @@ +import Lake +open Lake DSL + +package «test_repo» where + leanOptions := #[⟨`autoImplicit, false⟩] + +@[default_target] +lean_lib «Main» where + roots := #[`Main, `Helper] diff --git a/test/resources/repos/lean4/test_repo/lean-toolchain b/test/resources/repos/lean4/test_repo/lean-toolchain new file mode 100644 index 00000000..7638861c --- /dev/null +++ b/test/resources/repos/lean4/test_repo/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:stable diff --git a/test/serena/test_serena_agent.py b/test/serena/test_serena_agent.py index 7b2d3147..33c204b8 100644 --- a/test/serena/test_serena_agent.py +++ b/test/serena/test_serena_agent.py @@ -38,6 +38,7 @@ def serena_config(): Language.FSHARP, Language.POWERSHELL, Language.CPP_CCLS, + Language.LEAN4, ]: repo_path = get_repo_path(language) if repo_path.exists(): @@ -164,6 +165,7 @@ class TestSerenaAgent: pytest.param(Language.CSHARP, "Calculator", "Class", "Program.cs", marks=pytest.mark.csharp), pytest.param(Language.POWERSHELL, "function Greet-User ()", "Function", "main.ps1", marks=pytest.mark.powershell), pytest.param(Language.CPP_CCLS, "add", "Function", "b.cpp", marks=pytest.mark.cpp), + pytest.param(Language.LEAN4, "add", "Method", "Helper.lean", marks=pytest.mark.lean4), ], indirect=["serena_agent"], ) @@ -264,6 +266,7 @@ class TestSerenaAgent: pytest.param(Language.CSHARP, "Calculator", "Program.cs", "Program.cs", marks=pytest.mark.csharp), pytest.param(Language.POWERSHELL, "function Greet-User ()", "main.ps1", "main.ps1", marks=pytest.mark.powershell), pytest.param(Language.CPP_CCLS, "add", "b.cpp", "a.cpp", marks=pytest.mark.cpp), + pytest.param(Language.LEAN4, "add", "Helper.lean", "Main.lean", marks=pytest.mark.lean4), ], indirect=["serena_agent"], ) diff --git a/test/solidlsp/lean4/test_lean4_basic.py b/test/solidlsp/lean4/test_lean4_basic.py new file mode 100644 index 00000000..5ec40572 --- /dev/null +++ b/test/solidlsp/lean4/test_lean4_basic.py @@ -0,0 +1,164 @@ +""" +Tests for Lean 4 Language Server integration with Serena. + +Tests prove that Serena's symbol tools can: +1. Start the Lean 4 language server +2. Discover all expected symbols with precise matching +3. Track within-file references +4. Track cross-file references + +Test Repository Structure: +- Helper.lean: Calculator structure, arithmetic functions (add, subtract), predicates (isPositive, absolute) +- Main.lean: Main entry point using Helper, plus multiply and calculate functions +""" + +import pytest + +from solidlsp.ls import SolidLanguageServer +from solidlsp.ls_config import Language + + +@pytest.mark.lean4 +class TestLean4LanguageServer: + @pytest.mark.parametrize("language_server", [Language.LEAN4], indirect=True) + def test_ls_is_running(self, language_server: SolidLanguageServer) -> None: + """Test that the Lean 4 language server starts successfully.""" + assert language_server.is_running() + + @pytest.mark.parametrize("language_server", [Language.LEAN4], indirect=True) + def test_helper_symbols(self, language_server: SolidLanguageServer) -> None: + """ + Test symbol discovery in Helper.lean. + + Verifies that Serena can identify: + - Structure definition (Calculator) + - All functions (add, subtract, isPositive, absolute) + """ + all_symbols, _ = language_server.request_document_symbols("Helper.lean").get_all_symbols_and_roots() + symbol_names = {s["name"] for s in all_symbols} + + expected_symbols = { + "Calculator", + "add", + "subtract", + "isPositive", + "absolute", + } + + missing = expected_symbols - symbol_names + assert not missing, f"Missing expected symbols in Helper.lean: {missing}" + + @pytest.mark.parametrize("language_server", [Language.LEAN4], indirect=True) + def test_main_symbols(self, language_server: SolidLanguageServer) -> None: + """ + Test symbol discovery in Main.lean. + + Verifies that Serena can identify locally defined functions. + """ + all_symbols, _ = language_server.request_document_symbols("Main.lean").get_all_symbols_and_roots() + symbol_names = {s["name"] for s in all_symbols} + + expected_symbols = { + "multiply", + "calculate", + "main", + } + + missing = expected_symbols - symbol_names + assert not missing, f"Missing expected symbols in Main.lean: {missing}" + + @pytest.mark.parametrize("language_server", [Language.LEAN4], indirect=True) + def test_within_file_references(self, language_server: SolidLanguageServer) -> None: + """ + Test within-file reference tracking for isPositive. + + isPositive is defined in Helper.lean line 11 (0-indexed) and used by absolute on line 15. + """ + # isPositive defined at line 11, column 4 + references = language_server.request_references("Helper.lean", line=11, column=4) + + assert len(references) >= 1, f"Expected at least 1 reference to isPositive (used in absolute), got {len(references)}" + + # Check that isPositive is referenced within Helper.lean at line 15 (absolute calls isPositive) + ref_locations = [(ref["relativePath"], ref["range"]["start"]["line"]) for ref in references] + helper_refs = [(path, line) for path, line in ref_locations if "Helper.lean" in path] + assert any( + line == 15 for _, line in helper_refs + ), f"Expected isPositive reference at Helper.lean:15 (in absolute), got: {ref_locations}" + + @pytest.mark.parametrize("language_server", [Language.LEAN4], indirect=True) + def test_cross_file_references_add(self, language_server: SolidLanguageServer) -> None: + """ + Test cross-file reference tracking for add function. + + add is defined in Helper.lean line 5 (0-indexed) and used in Main.lean on lines 7 and 15. + """ + # add defined at line 5, column 4 + references = language_server.request_references("Helper.lean", line=5, column=4) + + assert len(references) >= 1, f"Expected at least 1 reference to add in Main.lean, got {len(references)}" + + # Check for references in Main.lean with specific lines + ref_locations = [(ref["relativePath"], ref["range"]["start"]["line"]) for ref in references] + main_refs = [(path, line) for path, line in ref_locations if "Main.lean" in path] + assert len(main_refs) >= 1, f"Expected at least 1 reference to add in Main.lean, got: {ref_locations}" + main_ref_lines = {line for _, line in main_refs} + # add is used in Main.lean line 7 (in calculate) and line 15 (in main) + assert ( + 7 in main_ref_lines or 15 in main_ref_lines + ), f"Expected add references at Main.lean lines 7 or 15, got lines: {main_ref_lines}" + + @pytest.mark.parametrize("language_server", [Language.LEAN4], indirect=True) + def test_cross_file_references_calculator(self, language_server: SolidLanguageServer) -> None: + """ + Test cross-file reference tracking for Calculator structure. + + Calculator is defined in Helper.lean line 0 (0-indexed) and used in Main.lean lines 5 and 13. + """ + # Calculator defined at line 0, column 10 + references = language_server.request_references("Helper.lean", line=0, column=10) + + assert len(references) >= 1, f"Expected at least 1 reference to Calculator in Main.lean, got {len(references)}" + + ref_locations = [(ref["relativePath"], ref["range"]["start"]["line"]) for ref in references] + main_refs = [(path, line) for path, line in ref_locations if "Main.lean" in path] + assert len(main_refs) >= 1, f"Expected at least 1 reference to Calculator in Main.lean, got: {ref_locations}" + main_ref_lines = {line for _, line in main_refs} + # Calculator is used in Main.lean line 5 (calculate signature) and line 13 (let c : Calculator) + assert ( + 5 in main_ref_lines or 13 in main_ref_lines + ), f"Expected Calculator references at Main.lean lines 5 or 13, got lines: {main_ref_lines}" + + @pytest.mark.parametrize("language_server", [Language.LEAN4], indirect=True) + def test_go_to_definition_within_file(self, language_server: SolidLanguageServer) -> None: + """ + Test go-to-definition within a file. + + In Main.lean line 19, calculate is called: 'match calculate c "multiply" 6 7 with'. + calculate is defined at Main.lean line 5. + """ + # calculate usage in Main.lean line 19, 'calculate' starts at col 8 + definitions = language_server.request_definition("Main.lean", line=19, column=8) + + assert len(definitions) >= 1, f"Expected at least 1 definition for calculate, got {len(definitions)}" + + def_location = definitions[0] + assert def_location["uri"].endswith("Main.lean"), f"Expected definition in Main.lean, got: {def_location['uri']}" + assert def_location["range"]["start"]["line"] == 5, f"Expected definition at line 5, got: {def_location['range']['start']['line']}" + + @pytest.mark.parametrize("language_server", [Language.LEAN4], indirect=True) + def test_go_to_definition_across_files(self, language_server: SolidLanguageServer) -> None: + """ + Test go-to-definition across files. + + In Main.lean line 15, add is called: 'add 5 3'. + add is defined in Helper.lean line 5. + """ + # add usage in Main.lean line 15, 'add' starts at col 19 + definitions = language_server.request_definition("Main.lean", line=15, column=19) + + assert len(definitions) >= 1, f"Expected at least 1 definition for add, got {len(definitions)}" + + def_location = definitions[0] + assert def_location["uri"].endswith("Helper.lean"), f"Expected definition in Helper.lean, got: {def_location['uri']}" + assert def_location["range"]["start"]["line"] == 5, f"Expected definition at line 5, got: {def_location['range']['start']['line']}"