diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c0c1ab9a..9d151f26 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/.gitignore b/.gitignore index 1dee1865..a8a70761 100644 --- a/.gitignore +++ b/.gitignore @@ -12,3 +12,4 @@ _out *.hash profile.json profile.json.gz +*.produced.out diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 index 00000000..72322f10 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,10 @@ +unreleased +---------- + +(Changes that can break existing programs are marked with a "(!)") + +### Tests + +- Added infrastructure for testing of LSP server and Verso documents + +* Changed BlockConfig diff --git a/src/tests/common.sh b/src/tests/common.sh new file mode 100644 index 00000000..45e61db1 --- /dev/null +++ b/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 +} diff --git a/src/tests/interactive/inline_goals.lean b/src/tests/interactive/inline_goals.lean new file mode 100644 index 00000000..bb866f82 --- /dev/null +++ b/src/tests/interactive/inline_goals.lean @@ -0,0 +1,19 @@ +import Verso +import VersoManual +import VersoBlueprint + +theorem test0 : ∀ (n : Nat), n = n := by + intros + --^ textDocument/hover + rfl +no +open Verso.Genre Manual + +#doc (Manual) "Test for Goals in Inline Lean" => + +```leann +theorem test : ∀ (n : Nat), n = n := by + intros + --^ $/lean/plainGoal + rfl +``` diff --git a/src/tests/interactive/inline_goals.lean.expected.out b/src/tests/interactive/inline_goals.lean.expected.out new file mode 100644 index 00000000..6ec16dda --- /dev/null +++ b/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 diff --git a/src/tests/run.lean b/src/tests/run.lean new file mode 100644 index 00000000..a8927a2b --- /dev/null +++ b/src/tests/run.lean @@ -0,0 +1,3 @@ +import Lean.Server.Test.Runner + +def main := Lean.Server.Test.Runner.main diff --git a/src/tests/run_interactive.sh b/src/tests/run_interactive.sh new file mode 100755 index 00000000..14784eee --- /dev/null +++ b/src/tests/run_interactive.sh @@ -0,0 +1,70 @@ +#!/bin/bash + +# set -ex + +cd ../.. +RUN_DIR=src/tests/ + +# Configuration +TEST_DIR="$RUN_DIR/interactive" +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/test_single.sh b/src/tests/test_single.sh new file mode 100755 index 00000000..063c2c7a --- /dev/null +++ b/src/tests/test_single.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash +RUN_DIR=src/tests/ + +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