test: LSP server verso tests

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

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}

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

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

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

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

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