fix: create well-spanned syntax on verso blocks

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

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

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

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

src/verso/Verso/Doc/Concrete.lean

@@ -161,8 +161,8 @@ elab "#doc" "(" genre:term ")" title:str "=>" text:completeDocument eoi : term =
   Term.elabTerm (← `( ($(doc) : Part $genre))) none
 
 
-scoped syntax (name := addBlockCmd) block term:max : command
-scoped syntax (name := addLastBlockCmd) block term:max str : command
+scoped syntax (name := addBlockCmd) block : command
+scoped syntax (name := addLastBlockCmd) block : command
 
 /-!
 Unlike `#doc` expressions and `#docs` commands, which are elaborated all at once, `#doc` commands
@@ -246,7 +246,7 @@ private meta partial def getTailContext? (source : String) (stx : Syntax) : Opti
 Parses each top-level block as either an `addBlockCmd` or an `addLastBlockCmd`. (This is what
 Verso uses to replace the command parser.)
 -/
-private meta def versoBlockCommandFn (genre : Term) (title : String) : ParserFn := fun c s =>
+private meta def versoBlockCommandFn : ParserFn := fun c s =>
   let iniSz  := s.stackSize
   let lastPos? := lastVersoEndPosExt.getState c.env
   let s := lastPos? |>.map s.setPos |>.getD s
@@ -255,10 +255,8 @@ private meta def versoBlockCommandFn (genre : Term) (title : String) : ParserFn
   else
     let s := ignoreFn (manyFn blankLine) c s
     let s := updateTrailing c s
-    let s := s.pushSyntax genre
     let i := s.pos
     if c.atEnd i then
-      let s := s.pushSyntax (Syntax.mkStrLit title)
       s.mkNode ``addLastBlockCmd iniSz
     else
       s.mkNode ``addBlockCmd iniSz
@@ -281,6 +279,7 @@ be used to thread state between the separate top level blocks. These environment
 the state that needs to exist across top-level-block parsing events.
 -/
 public meta structure DocElabEnvironment where
+  genreSyntax : Term := ⟨.missing⟩
   ctx : DocElabContext := ⟨.missing, mkConst ``Unit, .always, .none⟩
   docState : DocElabM.State := { highlightDeduplicationTable := some {} }
   partState : PartElabM.State := .init (.node .none nullKind #[])
@@ -323,18 +322,17 @@ in `elabDoc` across three functions: the prelude in `startDoc`, the loop body in
 and the postlude in `finishDoc`.
 -/
 
-private meta def startDoc (genreSyntax : Term) (title: StrLit) : Command.CommandElabM String := do
+private meta def startDoc (genreSyntax : Term) (title: StrLit) : Command.CommandElabM Unit := do
   let env ← getEnv
   let titleParts ← stringToInlines title
   let titleString := inlinesToString env titleParts
   let ctx ← Command.runTermElabM fun _ => DocElabContext.fromGenreTerm genreSyntax
   let initDocState : DocElabM.State := { highlightDeduplicationTable := .some {} }
   let initPartState : PartElabM.State := .init (.node .none nullKind titleParts)
 
-  modifyEnv (docEnvironmentExt.setState · ⟨ctx, initDocState, initPartState⟩)
+  modifyEnv (docEnvironmentExt.setState · ⟨genreSyntax, ctx, initDocState, initPartState⟩)
   runPartElabInEnv <| do
     PartElabM.setTitle titleString (← titleParts.mapM (elabInline ⟨·⟩))
-  return titleString
 
 private meta def runVersoBlock (block : TSyntax `block) : Command.CommandElabM Unit := do
   runPartElabInEnv <| partCommand block
@@ -344,29 +342,30 @@ private meta def runVersoBlock (block : TSyntax `block) : Command.CommandElabM U
   saveRefsInEnv
 
 open PartElabM in
-private meta def finishDoc (genreSyntax : Term) (title : StrLit) : Command.CommandElabM Unit:= do
+private meta def finishDoc : Command.CommandElabM Unit:= do
   let endPos := (← getFileMap).source.rawEndPos
   runPartElabInEnv <| do closePartsUntil 0 endPos
 
   let versoEnv := docEnvironmentExt.getState (← getEnv)
   let finished := versoEnv.partState.partContext.toPartFrame.close endPos
 
-  let n := mkIdentFrom title (← currentDocName)
-  let doc ← Command.runTermElabM fun _ => finished.toVersoDoc genreSyntax versoEnv.ctx versoEnv.docState versoEnv.partState
-  let ty ← ``(VersoDoc $genreSyntax)
+  let n := mkIdent (← currentDocName)
+  let doc ← Command.runTermElabM fun _ => finished.toVersoDoc versoEnv.genreSyntax versoEnv.ctx versoEnv.docState versoEnv.partState
+
+  let ty ← ``(VersoDoc $versoEnv.genreSyntax)
   Command.elabCommand (← `(def $n : $ty := $doc))
 
 syntax (name := replaceDoc) "#doc " "(" term ") " str " =>" : command
 elab_rules : command
   | `(command|#doc ( $genreSyntax:term ) $title:str =>%$tok) => open Lean Parser Elab Command in do
   elabCommand <| ← `(open scoped Lean.Doc.Syntax)
 
-  let titleString ← startDoc genreSyntax title
+  startDoc genreSyntax title
 
   -- Sets up basic incremental evaluation of documents by replacing Lean's command-by-command parser
   -- with a top-level-block parser.
   modifyEnv fun env => originalCatParserExt.setState env (categoryParserFnExtension.getState env)
-  replaceCategoryParser `command (versoBlockCommandFn genreSyntax titleString)
+  replaceCategoryParser `command versoBlockCommandFn
 
   if let some stopPos := tok.getTailPos? then
     let txt ← getFileMap
@@ -387,7 +386,7 @@ elab_rules : command
     -- Edge case: if there's no blocks after the =>, the replacement command parser won't get called,
     -- so we detect that case and call finishDoc.
     if stopPos.extract txt.source txt.source.rawEndPos |>.all Char.isWhitespace then
-      finishDoc genreSyntax title
+      finishDoc
 
 open Command in
 /--
@@ -403,16 +402,16 @@ private meta def updatePos (b : TSyntax `block) : CommandElabM Unit := do
 
 @[command_elab addBlockCmd]
 public meta def elabVersoBlock : Command.CommandElab
-  | `(addBlockCmd| $b:block $_:term) => do
+  | `(addBlockCmd| $b:block) => do
     updatePos b
     runVersoBlock b
   | _ => throwUnsupportedSyntax
 
 @[command_elab addLastBlockCmd]
 public meta def elabVersoLastBlock : Command.CommandElab
-  | `(addLastBlockCmd| $b:block $genre:term $title:str) => do
+  | `(addLastBlockCmd| $b:block) => do
     updatePos b
     runVersoBlock b
     -- Finish up the document
-    finishDoc genre title
+    finishDoc
   | _ => throwUnsupportedSyntax