Commit Graph
4 Commits
Author SHA1 Message Date
Michael Panchenko 7392d65b00 Tests: removed unnecessary and failing test for empty symbol not being cached 2026-04-17 09:32:03 +02:00
d32c053c55 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>
2026-04-16 19:19:23 +02:00
Michael Panchenko 0bbd9e375e Reformat (minor, after replacing black with ruff)
Black dependency created a dependabot warning and couldn't be bumped since it collided with pathspec dependencies. Since ruff can also format, black is not needed. But we now have these small format changes, mostly in test files
2026-03-23 21:10:41 +01:00
Dan Rosen 09c007d1e1 Add Lean 4 language support (#1137) 2026-03-12 11:32:31 +01:00