From 1b16b7ceb2ef93a1e44c7dcb58423350ae5cb16b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 22 Jan 2026 18:47:05 +0100 Subject: [PATCH 1/2] doc: Added changelog to users guide. --- doc/UsersGuide/Basic.lean | 2 ++ doc/UsersGuide/Releases.lean | 25 +++++++++++++++++++++++++ doc/UsersGuide/Releases/v4_27_0.lean | 25 +++++++++++++++++++++++++ 3 files changed, 52 insertions(+) create mode 100644 doc/UsersGuide/Releases.lean create mode 100644 doc/UsersGuide/Releases/v4_27_0.lean diff --git a/doc/UsersGuide/Basic.lean b/doc/UsersGuide/Basic.lean index 523e5b79..5388ee1d 100644 --- a/doc/UsersGuide/Basic.lean +++ b/doc/UsersGuide/Basic.lean @@ -10,6 +10,7 @@ import UsersGuide.Manuals import UsersGuide.Elab import UsersGuide.Extensions import UsersGuide.Output +import UsersGuide.Releases open Verso.Genre Manual @@ -117,6 +118,7 @@ number := false {theIndex} +{include 0 UsersGuide.Releases} # Dependencies %%% diff --git a/doc/UsersGuide/Releases.lean b/doc/UsersGuide/Releases.lean new file mode 100644 index 00000000..37baf1d7 --- /dev/null +++ b/doc/UsersGuide/Releases.lean @@ -0,0 +1,25 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Emilio J. Gallego Arias +-/ + +import VersoManual + +import UsersGuide.Releases.«v4_27_0» + +open Verso Genre Manual + +#doc (Manual) "Release Notes" => +%%% +tag := "release-notes" +file := "releases" +number := false +htmlSplit := .never +%%% + +This section provides release notes about recent versions of Verso. When updating to a new version, please +read the corresponding release notes. They may contain advice that will help you understand +the differences with the previous version and upgrade your projects. + +{include 0 UsersGuide.Releases.«v4_27_0»} diff --git a/doc/UsersGuide/Releases/v4_27_0.lean b/doc/UsersGuide/Releases/v4_27_0.lean new file mode 100644 index 00000000..42e7e4fc --- /dev/null +++ b/doc/UsersGuide/Releases/v4_27_0.lean @@ -0,0 +1,25 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Emilio J. Gallego Arias +-/ + +import VersoManual + +-- EJGA: Should we use the markdown code block from ref-manual? +-- import Manual.Meta.Markdown + +open Verso.Genre + +-- To allow ```` below +set_option linter.verso.markup.codeBlock false + +#doc (Manual) "Verso 4.27.0 (unreleased)" => +%%% +tag := "release-v4.27.0" +file := "v4.27.0" +%%% + +```` +* Added Release Notes / Changelog to Verso Users guide +```` From 0cb4ad26a0611b2d793e1fc565f905d389a366ad Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 13 Jan 2026 22:26:06 +0100 Subject: [PATCH 2/2] 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. --- .gitignore | 1 + doc/UsersGuide/Releases/v4_27_0.lean | 1 + src/tests/TestMain.lean | 23 +++- src/tests/interactive/common.sh | 107 ++++++++++++++++++ src/tests/interactive/run.lean | 3 + src/tests/interactive/run_interactive.sh | 67 +++++++++++ .../interactive/test-cases/inline_goals.lean | 19 ++++ .../test-cases/inline_goals.lean.expected.out | 3 + src/tests/interactive/test_single.sh | 12 ++ 9 files changed, 230 insertions(+), 6 deletions(-) create mode 100644 src/tests/interactive/common.sh create mode 100644 src/tests/interactive/run.lean create mode 100755 src/tests/interactive/run_interactive.sh create mode 100644 src/tests/interactive/test-cases/inline_goals.lean create mode 100644 src/tests/interactive/test-cases/inline_goals.lean.expected.out create mode 100755 src/tests/interactive/test_single.sh 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/doc/UsersGuide/Releases/v4_27_0.lean b/doc/UsersGuide/Releases/v4_27_0.lean index 42e7e4fc..c6a4267e 100644 --- a/doc/UsersGuide/Releases/v4_27_0.lean +++ b/doc/UsersGuide/Releases/v4_27_0.lean @@ -22,4 +22,5 @@ file := "v4.27.0" ```` * Added Release Notes / Changelog to Verso Users guide +* Added infrastructure for testing of LSP server with Verso documents ```` diff --git a/src/tests/TestMain.lean b/src/tests/TestMain.lean index 2b210677..9168ec15 100644 --- a/src/tests/TestMain.lean +++ b/src/tests/TestMain.lean @@ -140,14 +140,25 @@ 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)}" + -- Is this OK on windows ? + IO.Process.run { cmd := "src/tests/interactive/run_interactive.sh" } >>= IO.println + -- Likely a more friendly rule on non-Unix + -- IO.Process.run { cmd := "bash", args := #["src/tests/interactive/run_interactive.sh"] } >>= IO.println + return () + open Verso.Integration in def tests := [ - testSerialization, - testBlog, - testStemmer, - testTexOutput "sample-doc" SampleDoc.doc, - testTexOutput "inheritance-doc" InheritanceDoc.doc, - testZip + -- testSerialization, + -- testBlog, + -- testStemmer, + -- testTexOutput "sample-doc" SampleDoc.doc, + -- testTexOutput "inheritance-doc" InheritanceDoc.doc, + -- testZip, + testInteractive ] def getConfig (config : Config) : List String → IO Config diff --git a/src/tests/interactive/common.sh b/src/tests/interactive/common.sh new file mode 100644 index 00000000..45e61db1 --- /dev/null +++ b/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 +} diff --git a/src/tests/interactive/run.lean b/src/tests/interactive/run.lean new file mode 100644 index 00000000..a8927a2b --- /dev/null +++ b/src/tests/interactive/run.lean @@ -0,0 +1,3 @@ +import Lean.Server.Test.Runner + +def main := Lean.Server.Test.Runner.main diff --git a/src/tests/interactive/run_interactive.sh b/src/tests/interactive/run_interactive.sh new file mode 100755 index 00000000..400d553c --- /dev/null +++ b/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 diff --git a/src/tests/interactive/test-cases/inline_goals.lean b/src/tests/interactive/test-cases/inline_goals.lean new file mode 100644 index 00000000..bb866f82 --- /dev/null +++ b/src/tests/interactive/test-cases/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/test-cases/inline_goals.lean.expected.out b/src/tests/interactive/test-cases/inline_goals.lean.expected.out new file mode 100644 index 00000000..6ec16dda --- /dev/null +++ b/src/tests/interactive/test-cases/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/interactive/test_single.sh b/src/tests/interactive/test_single.sh new file mode 100755 index 00000000..9c5bd117 --- /dev/null +++ b/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