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 <[email protected]>

Author: ejgallego

.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"

.gitignore

@@ -20,3 +20,4 @@ profile.json.gz
 multi.json
 single.json
 *.html
+*.produced.out

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)
-

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

src/tests/interactive/README.md

@@ -0,0 +1,39 @@
+# 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

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
+}

src/tests/interactive/run.lean

@@ -0,0 +1,3 @@
+import Lean.Server.Test.Runner
+
+def main := Lean.Server.Test.Runner.main

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

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
+```

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}