From 624aa3d7081fd9c394ec9e22cf46b04bb06dc61f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 28 Jan 2026 22:44:06 +0100 Subject: [PATCH] test: LSP server verso tests 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 --- .github/workflows/copyright-header.yml | 2 +- .gitignore | 1 + doc/UsersGuide/Releases/v4_28_0.lean | 1 - src/tests/TestMain.lean | 13 ++- src/tests/interactive/README.md | 38 +++++++ src/tests/interactive/common.sh | 107 ++++++++++++++++++ src/tests/interactive/run.lean | 3 + src/tests/interactive/run_interactive.sh | 67 +++++++++++ .../test-cases/completion_inline.lean | 18 +++ .../completion_inline.lean.expected.out | 8 ++ .../interactive/test-cases/inline_goals.lean | 24 ++++ .../test-cases/inline_goals.lean.expected.out | 22 ++++ .../interactive/test-cases/math_hover.lean | 12 ++ .../test-cases/math_hover.lean.expected.out | 8 ++ src/tests/interactive/test_single.sh | 12 ++ 15 files changed, 333 insertions(+), 3 deletions(-) create mode 100644 src/tests/interactive/README.md create mode 100644 src/tests/interactive/common.sh create mode 100644 src/tests/interactive/run.lean create mode 100755 src/tests/interactive/run_interactive.sh create mode 100644 src/tests/interactive/test-cases/completion_inline.lean create mode 100644 src/tests/interactive/test-cases/completion_inline.lean.expected.out create mode 100644 src/tests/interactive/test-cases/inline_goals.lean create mode 100644 src/tests/interactive/test-cases/inline_goals.lean.expected.out create mode 100644 src/tests/interactive/test-cases/math_hover.lean create mode 100644 src/tests/interactive/test-cases/math_hover.lean.expected.out create mode 100755 src/tests/interactive/test_single.sh diff --git a/.github/workflows/copyright-header.yml b/.github/workflows/copyright-header.yml index 1c56f849..01daeefc 100644 --- a/.github/workflows/copyright-header.yml +++ b/.github/workflows/copyright-header.yml @@ -15,7 +15,7 @@ jobs: - name: Verify .lean files start with a copyright header. run: | - FILES=$(find ./src ./test-projects -type f -name "*.lean" -exec perl -ne 'BEGIN { $/ = undef; } print "$ARGV\n" if !m{\A/-\nCopyright}; exit;' {} \;) + FILES=$(find ./src ./test-projects -path ./src/tests/interactive -prune -type f -name "*.lean" -exec perl -ne 'BEGIN { $/ = undef; } print "$ARGV\n" if !m{\A/-\nCopyright}; exit;' {} \;) if [ -n "$FILES" ]; then echo "Found .lean files which do not have a copyright header:" echo "$FILES" diff --git a/.gitignore b/.gitignore index ca0b1808..a9f40f6f 100644 --- a/.gitignore +++ b/.gitignore @@ -20,3 +20,4 @@ profile.json.gz multi.json single.json *.html +*.produced.out diff --git a/doc/UsersGuide/Releases/v4_28_0.lean b/doc/UsersGuide/Releases/v4_28_0.lean index 72f300d3..9558138e 100644 --- a/doc/UsersGuide/Releases/v4_28_0.lean +++ b/doc/UsersGuide/Releases/v4_28_0.lean @@ -18,4 +18,3 @@ file := "v4.28.0" %%% * Add Release Notes / Changelog to Verso Users guide (@ejgallego, #708) - diff --git a/src/tests/TestMain.lean b/src/tests/TestMain.lean index fea930f4..22534291 100644 --- a/src/tests/TestMain.lean +++ b/src/tests/TestMain.lean @@ -153,6 +153,16 @@ def testBlog (_ : Config) : IO Unit := do if fails > 0 then throw <| .userError s!"{fails} blog tests failed" +-- Interactive tests via the LSP server +def testInteractive (_ : Config) : IO Unit := do + IO.println "Running interactive (LSP) tests..." + IO.println s!"current dir: {(← IO.Process.getCurrentDir)}" + -- We use the lower-level Process.spawn, which causes the subprocess to inherit the stdio + let child ← IO.Process.spawn { cmd := "src/tests/interactive/run_interactive.sh" } + let exitCode ← child.wait + if exitCode != 0 then + throw <| IO.userError s!"Interactive LSP tests failed with exit code {exitCode}" + open Verso.Integration in def tests := [ testSerialization, @@ -165,7 +175,8 @@ def tests := [ (extraFiles := [("src/tests/integration/extra-files-doc/test-data/shared", "shared")]) (extraFilesTeX := [("src/tests/integration/extra-files-doc/test-data/TeX-only", "TeX-only")]), testTexOutput "front-matter-doc" FrontMatter.doc, - testZip + testZip, + testInteractive ] def getConfig (config : Config) : List String → IO Config diff --git a/src/tests/interactive/README.md b/src/tests/interactive/README.md new file mode 100644 index 00000000..3ef897c8 --- /dev/null +++ b/src/tests/interactive/README.md @@ -0,0 +1,38 @@ +# LSP Server Tests for Verso + +This directory contains the infrastructure and test cases for Verso +LSP tests. + +See +[Lean's LSP testing documentation](https://github.com/leanprover/lean4/blob/master/doc/dev/testing.md#test-suite-organization) +for more information about how to test Lean's LSP server in Verso. + +## Adding test cases + +To add a test case, add two files to `test-cases` directory: + +- A `test.lean` file, with your test case according to the upstream + documentation. +- A `test.lean.expected.out` that contains the expected test output. + This can be produced by first creating `test.lean`, running it, and + verifying that `test.lean.produced.out` has the expected content. + Then, `test.lean.produced.out` can be copied to + `test.lean.expected.out` and committed. + +## Running individual tests + +Do `./src/tests/interactive/run_single.sh $test_case` from Verso's +root directory. + +## Runner architecture + +The runner architecture lies in a small custom script +`./run_interactive.sh`. This script will call the upstream runner for +each file in `test-cases`. The script is called from the main Verso +test runner, in `src/tests/TestMain.lean`. + +Files from upstream: + +- `run.lean`: main runner +- `test_single.sh`: test a single file +- `common.sh`: diff and miscellaneous testing utilities diff --git a/src/tests/interactive/common.sh b/src/tests/interactive/common.sh new file mode 100644 index 00000000..45e61db1 --- /dev/null +++ b/src/tests/interactive/common.sh @@ -0,0 +1,107 @@ +set -euo pipefail + +ulimit -s ${MAIN_STACK_SIZE:-8192} +DIFF=diff +if diff --color --help >/dev/null 2>&1; then + DIFF="diff --color"; +fi + +function fail { + echo $1 + exit 1 +} + +INTERACTIVE=no +if [ $1 == "-i" ]; then + INTERACTIVE=yes + shift +fi +f="$1" +shift +[ $# -eq 0 ] || fail "Usage: test_single.sh [-i] test-file.lean" + +function lean_has_llvm_support { + lean --features | grep -q "LLVM" +} + +function compile_lean_c_backend { + lean --c="$f.c" "$f" || fail "Failed to compile $f into C file" + leanc ${LEANC_OPTS-} -O3 -DNDEBUG -o "$f.out" "$@" "$f.c" || fail "Failed to compile C file $f.c" +} + +function compile_lean_llvm_backend { + set -o xtrace + rm "*.ll" || true # remove debugging files. + rm "*.bc" || true # remove bitcode files + rm "*.o" || true # remove object files + lean --bc="$f.linked.bc" "$f" || fail "Failed to compile $f into bitcode file" + leanc ${LEANC_OPTS-} -O3 -DNDEBUG -o "$f.out" "$@" "$f.linked.bc" || fail "Failed to link object file '$f.linked.bc'" + set +o xtrace +} + +function exec_capture_raw { + # backtraces are system-specific, strip them (might be captured in `#guard_msgs`) + LEAN_BACKTRACE=0 "$@" 2>&1 > "$f.produced.out" +} + +# produces filtered output intended for usage with `diff_produced` +function exec_capture { + # backtraces are system-specific, strip them + # mvar suffixes like in `?m.123` are deterministic but prone to change on minor changes, so strip them + # similarly, links to the language reference may have URL components depending on the toolchain, so normalize those + LEAN_BACKTRACE=0 "$@" 2>&1 \ + | perl -pe 's/(\?(\w|_\w+))\.[0-9]+/\1/g' \ + | perl -pe 's/https:\/\/lean-lang\.org\/doc\/reference\/(v?[0-9.]+(-rc[0-9]+)?|latest)/REFERENCE/g' > "$f.produced.out" +} + + +# Remark: `${var+x}` is a parameter expansion which evaluates to nothing if `var` is unset, and substitutes the string `x` otherwise. +function check_ret { + [ -n "${expected_ret+x}" ] || expected_ret=0 + [ -f "$f.expected.ret" ] && expected_ret=$(< "$f.expected.ret") + if [ -n "$expected_ret" ] && [ $ret -ne $expected_ret ]; then + echo "Unexpected return code $ret executing '$@'; expected $expected_ret. Output:" + cat "$f.produced.out" + exit 1 + fi +} + +function exec_check_raw { + ret=0 + exec_capture_raw "$@" || ret=$? + check_ret "$@" +} + +# produces filtered output intended for usage with `diff_produced` +function exec_check { + ret=0 + exec_capture "$@" || ret=$? + check_ret "$@" +} + +function diff_produced { + if test -f "$f.expected.out"; then + if $DIFF -au --strip-trailing-cr -I "executing external script" "$f.expected.out" "$f.produced.out"; then + : + else + echo "ERROR: file $f.produced.out does not match $f.expected.out" + if [ $INTERACTIVE == "yes" ]; then + meld "$f.produced.out" "$f.expected.out" + if diff -I "executing external script" "$f.expected.out" "$f.produced.out"; then + echo "-- mismatch was fixed" + fi + fi + exit 1 + fi + else + echo "ERROR: file $f.expected.out does not exist" + if [ $INTERACTIVE == "yes" ]; then + read -p "copy $f.produced.out (y/n)? " + if [ $REPLY == "y" ]; then + cp -- "$f.produced.out" "$f.expected.out" + echo "-- copied $f.produced.out --> $f.expected.out" + fi + fi + exit 1 + fi +} diff --git a/src/tests/interactive/run.lean b/src/tests/interactive/run.lean new file mode 100644 index 00000000..a8927a2b --- /dev/null +++ b/src/tests/interactive/run.lean @@ -0,0 +1,3 @@ +import Lean.Server.Test.Runner + +def main := Lean.Server.Test.Runner.main diff --git a/src/tests/interactive/run_interactive.sh b/src/tests/interactive/run_interactive.sh new file mode 100755 index 00000000..400d553c --- /dev/null +++ b/src/tests/interactive/run_interactive.sh @@ -0,0 +1,67 @@ +#!/bin/bash + +RUN_DIR=src/tests/interactive + +# Configuration +TEST_DIR="$RUN_DIR/test-cases" +RUNNER="$RUN_DIR/test_single.sh" +PASS_COUNT=0 +FAIL_COUNT=0 +FAILED_TESTS=() + +# Check if the runner exists and is executable +if [[ ! -x "$RUNNER" ]]; then + echo "Error: Runner script '$RUNNER' not found or not executable." + exit 1 +fi + +echo "------------------------------------------------" +echo " Starting Verso Interactive Test Suite: $(date) " +echo "------------------------------------------------" + +# Loop through every file in the test directory +for test_file in "$TEST_DIR"/*.lean; do + # Skip if it's not a file (e.g., a subdirectory) + [[ -f "$test_file" ]] || continue + + echo -n "Running test: $(basename "$test_file")... " + + # Capture both stdout and stderr into a variable + # This allows us to hide it on PASS and show it on FAIL + TEST_OUTPUT=$("$RUNNER" "$test_file" 2>&1) + EXIT_CODE=$? + + if [ $EXIT_CODE -eq 0 ]; then + echo "✅ PASS" + ((PASS_COUNT++)) + else + echo "❌ FAIL (Exit Code: $EXIT_CODE)" + echo "--- FAILURE LOG: $(basename "$test_file") ---" + echo "$TEST_OUTPUT" + echo "-----------------------------------------------" + + ((FAIL_COUNT++)) + FAILED_TESTS+=("$(basename "$test_file")") + fi +done + +# --- Summary Output --- +echo "-----------------------------------------------" +echo "Test Summary:" +echo " Total: $((PASS_COUNT + FAIL_COUNT))" +echo " Passed: $PASS_COUNT" +echo " Failed: $FAIL_COUNT" + +if [[ $FAIL_COUNT -gt 0 ]]; then + echo "-----------------------------------------------" + echo "Failed Tests:" + for failed in "${FAILED_TESTS[@]}"; do + echo " - $failed" + done + echo "-----------------------------------------------" + exit 1 +else + echo "All tests passed successfully!" + echo "-----------------------------------------------" + exit 0 +fi diff --git a/src/tests/interactive/test-cases/completion_inline.lean b/src/tests/interactive/test-cases/completion_inline.lean new file mode 100644 index 00000000..991b5927 --- /dev/null +++ b/src/tests/interactive/test-cases/completion_inline.lean @@ -0,0 +1,18 @@ +import Verso +import VersoManual + +open Verso.Genre Manual InlineLean + +#doc (Manual) "Test for Completion in Inline Lean" => + +```lean +theorem test : ∀ (n : Nat), n = n := by + intros + --^ textDocument/completion + rfl + +def a : Nat := Nat.add 3 2 + --^ textDocument/completion + +#print a +``` diff --git a/src/tests/interactive/test-cases/completion_inline.lean.expected.out b/src/tests/interactive/test-cases/completion_inline.lean.expected.out new file mode 100644 index 00000000..cc93f0b3 --- /dev/null +++ b/src/tests/interactive/test-cases/completion_inline.lean.expected.out @@ -0,0 +1,8 @@ +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/completion_inline.lean"}, + "position": {"line": 9, "character": 7}} +{"items": [], "isIncomplete": true} +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/completion_inline.lean"}, + "position": {"line": 13, "character": 18}} +{"items": [], "isIncomplete": true} diff --git a/src/tests/interactive/test-cases/inline_goals.lean b/src/tests/interactive/test-cases/inline_goals.lean new file mode 100644 index 00000000..1f6735fe --- /dev/null +++ b/src/tests/interactive/test-cases/inline_goals.lean @@ -0,0 +1,24 @@ +import Verso +import VersoManual + +theorem test0 : ∀ (n : Nat), n = n := by + intros + --^ textDocument/hover + rfl + +open Verso.Genre Manual InlineLean + +#doc (Manual) "Test for Goals in Inline Lean" => + +We ship two tests for inline lean codeblocks: + +- show hover info over the constant in the codeblock +- shows goals info on a proof + +```lean + --^ textDocument/hover +theorem test : ∀ (n : Nat), n = n := by + intros + --^ $/lean/plainGoal + rfl +``` diff --git a/src/tests/interactive/test-cases/inline_goals.lean.expected.out b/src/tests/interactive/test-cases/inline_goals.lean.expected.out new file mode 100644 index 00000000..241b490a --- /dev/null +++ b/src/tests/interactive/test-cases/inline_goals.lean.expected.out @@ -0,0 +1,22 @@ +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/inline_goals.lean"}, + "position": {"line": 4, "character": 7}} +{"range": + {"start": {"line": 4, "character": 2}, "end": {"line": 4, "character": 8}}, + "contents": + {"value": + "`intros` repeatedly applies `intro` to introduce zero or more hypotheses\nuntil the goal is no longer a *binding expression*\n(i.e., a universal quantifier, function type, implication, or `have`/`let`),\nwithout performing any definitional reductions (no unfolding, beta, eta, etc.).\nThe introduced hypotheses receive inaccessible (hygienic) names.\n\n`intros x y z` is equivalent to `intro x y z` and exists only for historical reasons.\nThe `intro` tactic should be preferred in this case.\n\n## Properties and relations\n\n- `intros` succeeds even when it introduces no hypotheses.\n\n- `repeat intro` is like `intros`, but it performs definitional reductions\n to expose binders, and as such it may introduce more hypotheses than `intros`.\n\n- `intros` is equivalent to `intro _ _ … _`,\n with the fewest trailing `_` placeholders needed so that the goal is no longer a binding expression.\n The trailing introductions do not perform any definitional reductions.\n\n## Examples\n\nImplications:\n```lean\nexample (p q : Prop) : p → q → p := by\n intros\n /- Tactic state\n a✝¹ : p\n a✝ : q\n ⊢ p -/\n assumption\n```\n\nLet-bindings:\n```lean\nexample : let n := 1; let k := 2; n + k = 3 := by\n intros\n /- n✝ : Nat := 1\n k✝ : Nat := 2\n ⊢ n✝ + k✝ = 3 -/\n rfl\n```\n\nDoes not unfold definitions:\n```lean\ndef AllEven (f : Nat → Nat) := ∀ n, f n % 2 = 0\n\nexample : ∀ (f : Nat → Nat), AllEven f → AllEven (fun k => f (k + 1)) := by\n intros\n /- Tactic state\n f✝ : Nat → Nat\n a✝ : AllEven f✝\n ⊢ AllEven fun k => f✝ (k + 1) -/\n sorry\n```\n", + "kind": "markdown"}} +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/inline_goals.lean"}, + "position": {"line": 17, "character": 4}} +{"range": + {"start": {"line": 17, "character": 3}, "end": {"line": 17, "character": 7}}, + "contents": + {"value": + "Code block `Verso.Genre.Manual.InlineLean.lean`\n\nNamed: `name : Ident` (optional) — a name\n\nFlags:\n* `show` (default `true`) - Flag\n* `keep` (default `true`) - Flag\n* `error` (default `false`) - Flag\n* `fresh` (default `false`) - Flag\n\n\nElaborates the provided Lean command in the context of the current Verso module.\n", + "kind": "markdown"}} +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/inline_goals.lean"}, + "position": {"line": 20, "character": 7}} +null diff --git a/src/tests/interactive/test-cases/math_hover.lean b/src/tests/interactive/test-cases/math_hover.lean new file mode 100644 index 00000000..bff3732e --- /dev/null +++ b/src/tests/interactive/test-cases/math_hover.lean @@ -0,0 +1,12 @@ +import Verso +import VersoManual + +open Verso.Genre Manual + +#doc (Manual) "Test for Infoview over Inline Math" => + +$`\sum_i x_i \cdot y_i = \sum_i y_i \cdot x_i` + --^ $/lean/plainGoal + +$$`\sum_i x_i + y_i = \sum_i y_i + x_i` + --^ $/lean/plainGoal diff --git a/src/tests/interactive/test-cases/math_hover.lean.expected.out b/src/tests/interactive/test-cases/math_hover.lean.expected.out new file mode 100644 index 00000000..9a7640e5 --- /dev/null +++ b/src/tests/interactive/test-cases/math_hover.lean.expected.out @@ -0,0 +1,8 @@ +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/math_hover.lean"}, + "position": {"line": 7, "character": 6}} +null +{"textDocument": + {"uri": "file:///src/tests/interactive/test-cases/math_hover.lean"}, + "position": {"line": 10, "character": 6}} +null diff --git a/src/tests/interactive/test_single.sh b/src/tests/interactive/test_single.sh new file mode 100755 index 00000000..9c5bd117 --- /dev/null +++ b/src/tests/interactive/test_single.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash +RUN_DIR=src/tests/interactive + +source $RUN_DIR/common.sh + +# IO.Process.exit (used by the file worker) seems to be incompatible with LSAN +# TODO: investigate or work around +export ASAN_OPTIONS=detect_leaks=0 + +# these tests don't have to succeed +exec_capture lean -Dlinter.all=false --run "$RUN_DIR/run.lean" -p "$f" || true +diff_produced