test: LSP server verso tests by ejgallego · Pull Request #699 · leanprover/verso

ejgallego · 2026-01-13T21:34:03Z

We add LSP tests for Verso documents; we reuse the core LSP testing infrastructure from lean4 upstream. See doc/dev/testing.md there for more details.

This is a draft PR, some comments:

maybe we should make the effort and use the lake test runner instead of the ad-hoc test runner here
location of files / entry point to be debated
we need to ship more tests

CHANGELOG.md

ejgallego · 2026-01-14T13:20:30Z

Summary of PR review discussion with David:

run test-runner via lake, maybe update test runner upstream to support -d
make tests run from lake test
note which files are copied from lean upstream
test all Verso LSP extensions
move changelog to manual, à la reference manual

david-christiansen · 2026-01-15T16:06:08Z

test all Verso LSP extensions

I think this one isn't really necessary for a merge here. It's important, but so is avoiding bitrot and getting value from the test that's already here. One or two more should suffice to validate the approach.

ejgallego · 2026-01-15T16:15:56Z

update test runner upstream to support -d option

Upstream is happy with this so I'll proceed with that plan.

This avoids spurious infoview display of the internal elaborated constant type. This bug is only observable after applying the fix in leanprover#700 ; will wait for leanprover#700 and leanprover#699 to merge this so we can properly provide a test. Co-authored-by: David Thrane Christiansen <david@lean-fro.org>

ejgallego · 2026-01-28T21:47:24Z

Summary of PR review discussion with David:

run test-runner via lake, maybe update test runner upstream to support -d

make tests run from lake test

note which files are copied from lean upstream

test all Verso LSP extensions

move changelog to manual, à la reference manual

Points addressed, except for "test all Verso LSP extensions".

I added a custom pass on Verso test runner to run the tests, would be nice to have a fancier test runner at some point so we can run the tests in parallel for example.

This avoids spurious infoview display of the internal elaborated constant type. This bug is only observable after applying the fix in leanprover#700 ; will wait for leanprover#700 and leanprover#699 to merge this so we can properly provide a test. Co-authored-by: David Thrane Christiansen <david@lean-fro.org>

doc/UsersGuide/Releases/v4_28_0.lean

src/tests/interactive/test-cases/completion_inline.lean.expected.out

src/tests/interactive/README.md

david-christiansen · 2026-01-30T05:28:31Z

src/tests/TestMain.lean

+  IO.println "Running interactive (LSP) tests..."
+  IO.println s!"current dir: {(← IO.Process.getCurrentDir)}"
+  -- We use the lower-level Process.spawn not to buffer the test output
+  -- Is this OK on windows ?


Should we set up a Windows runner so you can be sure? No core Verso developer runs Windows, and all sorts of things are different over there; it'd be nice to know that we can build and test everything.

Happy to setup a windows runner, I think it is a key platform.

See #724 for a (low-prio) attempt to add Windows CI; I propose to keep things as they are until the Windows env to run CI is settled down.

src/tests/TestMain.lean

ejgallego · 2026-01-30T14:19:36Z

Thanks for the reviews @david-christiansen , I've incorporated your feedback. Open points:

add a changelog entry for this PR?
keep tests that showcase a bug, or move them to the fix PR?
are we happy with using IO.Process.spawn { cmd := "src/tests/interactive/run_interactive.sh" } for now?

We add LSP tests for Verso documents; we reuse the core LSP testing infrastructure from lean4 upstream. See `doc/dev/testing.md` there for more details. Co-authored-by: David Thrane Christiansen <david@lean-fro.org>

david-christiansen · 2026-01-30T22:02:50Z

My opinions:

add a changelog entry for this PR?

No, we should save that for user-visible things.

keep tests that showcase a bug, or move them to the fix PR?

Keep 'em, and fix them in that PR :)

are we happy with using IO.Process.spawn { cmd := "src/tests/interactive/run_interactive.sh" } for now?

Yes

ejgallego · 2026-01-30T22:07:19Z

Thanks, we should then be ready to go.

This avoids spurious infoview display of the internal elaborated constant type. This bug is only observable after applying the fix in leanprover#700 ; will wait for leanprover#700 and leanprover#699 to merge this so we can properly provide a test. Co-authored-by: David Thrane Christiansen <david@lean-fro.org>

…#707) This avoids spurious infoview display of the internal elaborated constant type. This bug is only observable after applying the fix in #700 ; will wait for #700 and #699 to merge this so we can properly provide a test. Co-authored-by: David Thrane Christiansen <david@lean-fro.org> --------- Co-authored-by: David Thrane Christiansen <david@lean-fro.org>

ejgallego mentioned this pull request Jan 13, 2026

fix: create well-spanned syntax on verso blocks #700

Merged

david-christiansen reviewed Jan 14, 2026

View reviewed changes

CHANGELOG.md Outdated Show resolved Hide resolved

ejgallego force-pushed the test_lsp branch 3 times, most recently from 9e3f79d to 70158ef Compare January 15, 2026 16:39

ejgallego mentioned this pull request Jan 22, 2026

fix: Don't include syntax information in elaboration of math elements #707

Merged

ejgallego force-pushed the test_lsp branch 3 times, most recently from 0cb4ad2 to 6bdf8a5 Compare January 28, 2026 21:44

ejgallego force-pushed the test_lsp branch from 6bdf8a5 to b317553 Compare January 28, 2026 21:52

ejgallego force-pushed the test_lsp branch from b317553 to f35ef3f Compare January 29, 2026 17:13

ejgallego marked this pull request as ready for review January 29, 2026 17:14

ejgallego requested a review from david-christiansen January 29, 2026 17:14