Skip to content

Commit 6bdf8a5

Browse files
ejgallegodavid-christiansen
ejgallego
and
david-christiansen
committed
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]>
1 parent 5a3b5c0 commit 6bdf8a5

File tree

14 files changed

+328
-2
lines changed

14 files changed

+328
-2
lines changed

‎.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,3 +20,4 @@ profile.json.gz
2020
multi.json
2121
single.json
2222
*.html
23+
*.produced.out

‎doc/UsersGuide/Releases/v4_28_0.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,4 +18,4 @@ file := "v4.28.0"
1818
%%%
1919

2020
* Add Release Notes / Changelog to Verso Users guide (@ejgallego, #708)
21-
21+
* Add LSP testing infrastructure for Verso documents (@ejgallego, #707)

‎src/tests/TestMain.lean‎

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -153,6 +153,19 @@ def testBlog (_ : Config) : IO Unit := do
153153
if fails > 0 then
154154
throw <| .userError s!"{fails} blog tests failed"
155155

156+
-- Interactive tests via the LSP server
157+
def testInteractive (_ : Config) : IO Unit := do
158+
IO.println "Running interactive (LSP) tests..."
159+
IO.println s!"current dir: {(← IO.Process.getCurrentDir)}"
160+
-- We use the lower-level Process.spawn not to buffer the test output
161+
-- Is this OK on windows ?
162+
let child ← IO.Process.spawn { cmd := "src/tests/interactive/run_interactive.sh" }
163+
let exitCode ← child.wait
164+
if exitCode != 0 then
165+
throw <| IO.userError s!"[!!!] interactive tests failed!"
166+
-- Likely a more friendly rule on non-Unix
167+
-- IO.Process.run { cmd := "bash", args := #["src/tests/interactive/run_interactive.sh"] } >>= IO.println
168+
156169
open Verso.Integration in
157170
def tests := [
158171
testSerialization,
@@ -165,7 +178,8 @@ def tests := [
165178
(extraFiles := [("src/tests/integration/extra-files-doc/test-data/shared", "shared")])
166179
(extraFilesTeX := [("src/tests/integration/extra-files-doc/test-data/TeX-only", "TeX-only")]),
167180
testTexOutput "front-matter-doc" FrontMatter.doc,
168-
testZip
181+
testZip,
182+
testInteractive
169183
]
170184

171185
def getConfig (config : Config) : List String → IO Config

‎src/tests/interactive/README.md‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
LSP Server Tests for Verso
2+
--------------------------
3+
4+
This directory contains the infrastructure and test cases for Verso LSP tests.
5+
6+
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.
7+
8+
## Adding test cases
9+
10+
To add a test case, add two files to `test-cases` directory:
11+
12+
- A `test.lean` file, with your test case according to the upstream documentation.
13+
- A `test.lean.expected.out` that contains the expected test output.
14+
15+
## Running individual tests
16+
17+
Do `./src/tests/interactive/run_single.sh $test_case` from Verso's root directory.
18+
19+
## Runner architecture
20+
21+
The runner architecture lies in a small custom script
22+
`./run_interactive.sh`. This script will call the upstream runner for
23+
each file in `test-cases`. The script is called from the main Verso
24+
test runner, in `src/tests/TestMain.lean`.
25+
26+
Files from upstream:
27+
28+
- `run.lean`: main runner
29+
- `test_single.sh`: test a single file
30+
- `common.sh`: diff and miscellaneous testing utilities

‎src/tests/interactive/common.sh‎

Lines changed: 107 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,107 @@
1+
set -euo pipefail
2+
3+
ulimit -s ${MAIN_STACK_SIZE:-8192}
4+
DIFF=diff
5+
if diff --color --help >/dev/null 2>&1; then
6+
DIFF="diff --color";
7+
fi
8+
9+
function fail {
10+
echo $1
11+
exit 1
12+
}
13+
14+
INTERACTIVE=no
15+
if [ $1 == "-i" ]; then
16+
INTERACTIVE=yes
17+
shift
18+
fi
19+
f="$1"
20+
shift
21+
[ $# -eq 0 ] || fail "Usage: test_single.sh [-i] test-file.lean"
22+
23+
function lean_has_llvm_support {
24+
lean --features | grep -q "LLVM"
25+
}
26+
27+
function compile_lean_c_backend {
28+
lean --c="$f.c" "$f" || fail "Failed to compile $f into C file"
29+
leanc ${LEANC_OPTS-} -O3 -DNDEBUG -o "$f.out" "$@" "$f.c" || fail "Failed to compile C file $f.c"
30+
}
31+
32+
function compile_lean_llvm_backend {
33+
set -o xtrace
34+
rm "*.ll" || true # remove debugging files.
35+
rm "*.bc" || true # remove bitcode files
36+
rm "*.o" || true # remove object files
37+
lean --bc="$f.linked.bc" "$f" || fail "Failed to compile $f into bitcode file"
38+
leanc ${LEANC_OPTS-} -O3 -DNDEBUG -o "$f.out" "$@" "$f.linked.bc" || fail "Failed to link object file '$f.linked.bc'"
39+
set +o xtrace
40+
}
41+
42+
function exec_capture_raw {
43+
# backtraces are system-specific, strip them (might be captured in `#guard_msgs`)
44+
LEAN_BACKTRACE=0 "$@" 2>&1 > "$f.produced.out"
45+
}
46+
47+
# produces filtered output intended for usage with `diff_produced`
48+
function exec_capture {
49+
# backtraces are system-specific, strip them
50+
# mvar suffixes like in `?m.123` are deterministic but prone to change on minor changes, so strip them
51+
# similarly, links to the language reference may have URL components depending on the toolchain, so normalize those
52+
LEAN_BACKTRACE=0 "$@" 2>&1 \
53+
| perl -pe 's/(\?(\w|_\w+))\.[0-9]+/\1/g' \
54+
| perl -pe 's/https:\/\/lean-lang\.org\/doc\/reference\/(v?[0-9.]+(-rc[0-9]+)?|latest)/REFERENCE/g' > "$f.produced.out"
55+
}
56+
57+
58+
# Remark: `${var+x}` is a parameter expansion which evaluates to nothing if `var` is unset, and substitutes the string `x` otherwise.
59+
function check_ret {
60+
[ -n "${expected_ret+x}" ] || expected_ret=0
61+
[ -f "$f.expected.ret" ] && expected_ret=$(< "$f.expected.ret")
62+
if [ -n "$expected_ret" ] && [ $ret -ne $expected_ret ]; then
63+
echo "Unexpected return code $ret executing '$@'; expected $expected_ret. Output:"
64+
cat "$f.produced.out"
65+
exit 1
66+
fi
67+
}
68+
69+
function exec_check_raw {
70+
ret=0
71+
exec_capture_raw "$@" || ret=$?
72+
check_ret "$@"
73+
}
74+
75+
# produces filtered output intended for usage with `diff_produced`
76+
function exec_check {
77+
ret=0
78+
exec_capture "$@" || ret=$?
79+
check_ret "$@"
80+
}
81+
82+
function diff_produced {
83+
if test -f "$f.expected.out"; then
84+
if $DIFF -au --strip-trailing-cr -I "executing external script" "$f.expected.out" "$f.produced.out"; then
85+
:
86+
else
87+
echo "ERROR: file $f.produced.out does not match $f.expected.out"
88+
if [ $INTERACTIVE == "yes" ]; then
89+
meld "$f.produced.out" "$f.expected.out"
90+
if diff -I "executing external script" "$f.expected.out" "$f.produced.out"; then
91+
echo "-- mismatch was fixed"
92+
fi
93+
fi
94+
exit 1
95+
fi
96+
else
97+
echo "ERROR: file $f.expected.out does not exist"
98+
if [ $INTERACTIVE == "yes" ]; then
99+
read -p "copy $f.produced.out (y/n)? "
100+
if [ $REPLY == "y" ]; then
101+
cp -- "$f.produced.out" "$f.expected.out"
102+
echo "-- copied $f.produced.out --> $f.expected.out"
103+
fi
104+
fi
105+
exit 1
106+
fi
107+
}

‎src/tests/interactive/run.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
import Lean.Server.Test.Runner
2+
3+
def main := Lean.Server.Test.Runner.main

‎src/tests/interactive/run_interactive.sh‎

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
#!/bin/bash
2+
3+
RUN_DIR=src/tests/interactive
4+
5+
# Configuration
6+
TEST_DIR="$RUN_DIR/test-cases"
7+
RUNNER="$RUN_DIR/test_single.sh"
8+
PASS_COUNT=0
9+
FAIL_COUNT=0
10+
FAILED_TESTS=()
11+
12+
# Check if the runner exists and is executable
13+
if [[ ! -x "$RUNNER" ]]; then
14+
echo "Error: Runner script '$RUNNER' not found or not executable."
15+
exit 1
16+
fi
17+
18+
echo "------------------------------------------------"
19+
echo " Starting Verso Interactive Test Suite: $(date) "
20+
echo "------------------------------------------------"
21+
22+
# Loop through every file in the test directory
23+
for test_file in "$TEST_DIR"/*.lean; do
24+
# Skip if it's not a file (e.g., a subdirectory)
25+
[[ -f "$test_file" ]] || continue
26+
27+
echo -n "Running test: $(basename "$test_file")... "
28+
29+
# Capture both stdout and stderr into a variable
30+
# This allows us to hide it on PASS and show it on FAIL
31+
TEST_OUTPUT=$("$RUNNER" "$test_file" 2>&1)
32+
EXIT_CODE=$?
33+
34+
if [ $EXIT_CODE -eq 0 ]; then
35+
echo "✅ PASS"
36+
((PASS_COUNT++))
37+
else
38+
echo "❌ FAIL (Exit Code: $EXIT_CODE)"
39+
echo "--- FAILURE LOG: $(basename "$test_file") ---"
40+
echo "$TEST_OUTPUT"
41+
echo "-----------------------------------------------"
42+
43+
((FAIL_COUNT++))
44+
FAILED_TESTS+=("$(basename "$test_file")")
45+
fi
46+
done
47+
48+
# --- Summary Output ---
49+
echo "-----------------------------------------------"
50+
echo "Test Summary:"
51+
echo " Total: $((PASS_COUNT + FAIL_COUNT))"
52+
echo " Passed: $PASS_COUNT"
53+
echo " Failed: $FAIL_COUNT"
54+
55+
if [[ $FAIL_COUNT -gt 0 ]]; then
56+
echo "-----------------------------------------------"
57+
echo "Failed Tests:"
58+
for failed in "${FAILED_TESTS[@]}"; do
59+
echo " - $failed"
60+
done
61+
echo "-----------------------------------------------"
62+
exit 1
63+
else
64+
echo "All tests passed successfully!"
65+
echo "-----------------------------------------------"
66+
exit 0
67+
fi

‎src/tests/interactive/test-cases/completion_inline.lean‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
import Verso
2+
import VersoManual
3+
4+
open Verso.Genre Manual InlineLean
5+
6+
#doc (Manual) "Test for Completion in Inline Lean" =>
7+
8+
```lean
9+
theorem test : ∀ (n : Nat), n = n := by
10+
intros
11+
--^ textDocument/completion
12+
rfl
13+
14+
def a : Nat := Nat.add 3 2
15+
--^ textDocument/completion
16+
17+
#print a
18+
```

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
{"textDocument":
2+
{"uri": "file:///src/tests/interactive/test-cases/completion_inline.lean"},
3+
"position": {"line": 9, "character": 7}}
4+
{"items": [], "isIncomplete": true}
5+
{"textDocument":
6+
{"uri": "file:///src/tests/interactive/test-cases/completion_inline.lean"},
7+
"position": {"line": 13, "character": 18}}
8+
{"items": [], "isIncomplete": true}

‎src/tests/interactive/test-cases/inline_goals.lean‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
import Verso
2+
import VersoManual
3+
4+
theorem test0 : ∀ (n : Nat), n = n := by
5+
intros
6+
--^ textDocument/hover
7+
rfl
8+
9+
open Verso.Genre Manual InlineLean
10+
11+
#doc (Manual) "Test for Goals in Inline Lean" =>
12+
13+
We ship two tests for inline lean codeblocks:
14+
15+
- show hover info over the constant in the codeblock
16+
- shows goals info on a proof
17+
18+
```lean
19+
--^ textDocument/hover
20+
theorem test : ∀ (n : Nat), n = n := by
21+
intros
22+
--^ $/lean/plainGoal
23+
rfl
24+
```

0 commit comments

Comments
 (0)