wip

Author: ejgallego

CHANGELOG.md

@@ -1,8 +1,10 @@
 unreleased
 ----------
 
-(Changes that can break existing programs are marked with a "*")
+(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/interactive/inline_goals.lean

@@ -2,13 +2,18 @@ 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" =>
 
-```lean
+```leann
 theorem test : ∀ (n : Nat), n = n := by
   intros
-      --^ $/lean/plainGoal
+     --^ $/lean/plainGoal
   rfl
 ```

src/tests/run_interactive.sh

@@ -2,9 +2,12 @@
 
 # set -ex
 
+cd ../..
+RUN_DIR=src/tests/
+
 # Configuration
-TEST_DIR="interactive"
-RUNNER="./test_single.sh"
+TEST_DIR="$RUN_DIR/interactive"
+RUNNER="$RUN_DIR/test_single.sh"
 PASS_COUNT=0
 FAIL_COUNT=0
 FAILED_TESTS=()

src/tests/test_single.sh

@@ -1,10 +1,12 @@
 #!/usr/bin/env bash
-source ./common.sh
+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.lean "$f" || true
+exec_capture lean -Dlinter.all=false --run "$RUN_DIR/run.lean" -p "$f" || true
 diff_produced