From d32c053c55c8216803cad21fbd81e2ce52f4b0e9 Mon Sep 17 00:00:00 2001
From: Koushik-Salammagari
 <138836560+Koushik-Salammagari@users.noreply.github.com>
Date: Thu, 16 Apr 2026 10:19:23 -0700
Subject: [PATCH] Fix Lean4 stale cache: skip caching empty document symbol
 responses (#1356)

* Fix Lean4 stale cache: skip caching empty document symbol responses

When the Lean language server is queried before `lake build` completes,
it returns empty symbol lists. Previously these were written to the
persistent cache, permanently hiding symbols even after the build
finished. Now only non-empty responses are cached.

Adds a unit test that verifies empty responses from the LSP layer are
never written to _raw_document_symbols_cache.

Fixes #1217

* fix: run poe format and add changelog entry for #1356

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

---------

Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
Co-authored-by: Michael Panchenko <35432522+MischaPanch@users.noreply.github.com>
---
 CHANGELOG.md                            |  1 +
 src/solidlsp/ls.py                      |  9 ++++++---
 test/solidlsp/lean4/test_lean4_basic.py | 25 +++++++++++++++++++++++++
 3 files changed, 32 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2cf145fe..64349290 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -14,6 +14,7 @@ Status of the `main` branch. Changes prior to the next official version change w
 * Language Servers:
   - Fix: clangd capability checks now tolerate valid initialize response shape differences and invalidate cached C++ document symbols when clangd/compile commands context changes #1359                                                                                                                                                                                                            
   - Fix: `rename_symbol` for Vue files now correctly propagates edits to the TypeScript server, enabling cross-file renames in `.vue` files 
+  - Fix: Lean4 stale cache — empty document symbol responses (returned before `lake build` completes) are no longer persisted, preventing symbols from being permanently hidden #1356
 
 
 # v1.1.2 (2026-04-14)
diff --git a/src/solidlsp/ls.py b/src/solidlsp/ls.py
index 4a1f5986..5b679ce9 100644
--- a/src/solidlsp/ls.py
+++ b/src/solidlsp/ls.py
@@ -1331,9 +1331,12 @@ class SolidLanguageServer(ABC):
                 {"textDocument": {"uri": pathlib.Path(os.path.join(self.repository_root_path, relative_file_path)).as_uri()}}
             )
 
-            # update cache
-            self._raw_document_symbols_cache[cache_key] = (fd.content_hash, response)
-            self._raw_document_symbols_cache_is_modified = True
+            # Only cache non-empty results. An empty or None response can occur when the language server
+            # has not yet finished indexing or building the project (e.g. Lean 4 before `lake build`),
+            # and caching it would permanently serve stale data even after the project is ready.
+            if response:
+                self._raw_document_symbols_cache[cache_key] = (fd.content_hash, response)
+                self._raw_document_symbols_cache_is_modified = True
 
             return response
 
diff --git a/test/solidlsp/lean4/test_lean4_basic.py b/test/solidlsp/lean4/test_lean4_basic.py
index b8f35efa..a20a32cd 100644
--- a/test/solidlsp/lean4/test_lean4_basic.py
+++ b/test/solidlsp/lean4/test_lean4_basic.py
@@ -12,6 +12,8 @@ Test Repository Structure:
 - Main.lean: Main entry point using Helper, plus multiply and calculate functions
 """
 
+from unittest.mock import patch
+
 import pytest
 
 from solidlsp.ls import SolidLanguageServer
@@ -146,6 +148,29 @@ class TestLean4LanguageServer:
         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_empty_symbol_response_not_cached(self, language_server: SolidLanguageServer) -> None:
+        """
+        Test that an empty document symbol response is not written to the cache.
+
+        This guards against the scenario where the Lean language server returns no symbols
+        before `lake build` has completed. If the empty result were cached, subsequent
+        requests after the build would still return empty symbols even though the LS now
+        has the full build artifacts available.
+        """
+        file_path = "Helper.lean"
+
+        # Patch the LSP server to return an empty list, simulating a pre-build response.
+        with patch.object(language_server.server.send, "document_symbol", return_value=[]):
+            result = language_server._request_document_symbols(file_path, None)
+            assert result == [], "Expected the (mocked) empty response to be returned as-is"
+
+        # The empty result must NOT have been written to the cache.
+        assert file_path not in language_server._raw_document_symbols_cache, (
+            "Empty symbol response must not be stored in the cache; "
+            "it would permanently hide symbols that become available after `lake build`"
+        )
+
     @pytest.mark.parametrize("language_server", [Language.LEAN4], indirect=True)
     def test_go_to_definition_across_files(self, language_server: SolidLanguageServer) -> None:
         """