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.

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

Author: ejgallego

.github/workflows/ci.yml

@@ -68,6 +68,10 @@ jobs:
               run: |
                   lake test
 
+            - name: Run LSP tests
+              run: |
+                cd src/tests && ./run_interactive.sh
+
             - name: Generate the test website
               run: |
                   lake exe demosite --output _out/test-projects/demosite

.gitignore

@@ -12,3 +12,4 @@ _out
 *.hash
 profile.json
 profile.json.gz
+*.produced.out

CHANGELOG.md

@@ -0,0 +1,8 @@
+unreleased
+----------
+
+(Changes that can break existing programs are marked with a "*")
+
+### Tests
+
+- Added infrastructure for testing of LSP server and Verso documents

src/tests/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/inline_goals.lean

@@ -0,0 +1,14 @@
+import Verso
+import VersoManual
+import VersoBlueprint
+
+open Verso.Genre Manual
+
+#doc (Manual) "Test for Goals in Inline Lean" =>
+
+```lean
+theorem test : ∀ (n : Nat), n = n := by
+  intros
+      --^ $/lean/plainGoal
+  rfl
+```

src/tests/interactive/inline_goals.lean.expected.out

@@ -0,0 +1,3 @@
+{"textDocument": {"uri": "file:///interactive/inline_goals.lean"},
+ "position": {"line": 10, "character": 8}}
+null

src/tests/run.lean

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

src/tests/run_interactive.sh

@@ -0,0 +1,67 @@
+#!/bin/bash
+
+# set -ex
+
+# Configuration
+TEST_DIR="interactive"
+RUNNER="./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/test_single.sh

@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+source ./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.lean "$f" || true
+diff_produced