chore: migrate more tests to new test suite

.gitattributes

@@ -5,9 +5,3 @@ stage0/** binary linguist-generated
 # The following file is often manually edited, so do show it in diffs
 stage0/src/stdlib_flags.h -binary -linguist-generated
 doc/std/grove/GroveStdlib/Generated/** linguist-generated
-# These files should not have line endings translated on Windows, because
-# it throws off parser tests. Later lines override earlier ones, so the
-# runner code is still treated as ordinary text.
-tests/lean/docparse/* eol=lf
-tests/lean/docparse/*.lean eol=auto
-tests/lean/docparse/*.sh eol=auto

doc/examples/.gitignore

@@ -0,0 +1,2 @@
+*.out.produced
+*.exit.produced

doc/examples/bintree.lean.out.expected

@@ -0,0 +1,2 @@
+Tree.node (Tree.node (Tree.leaf) 1 "one" (Tree.leaf)) 2 "two" (Tree.node (Tree.leaf) 3 "three" (Tree.leaf))
+[(1, "one"), (2, "two"), (3, "three")]

doc/examples/compiler/run_test

@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+source ../../../tests/env_test.sh
+source "$TEST_DIR/util.sh"
+
+leanmake --always-make bin
+
+exec_capture test.lean \
+  ./build/bin/test hello world
+
+check_exit test.lean
+check_out test.lean

doc/examples/compiler/test.lean.out.expected

@@ -0,0 +1 @@
+[hello, world]

doc/examples/interp.lean.out.expected

@@ -0,0 +1,3 @@
+30
+interp.lean:146:4: warning: declaration uses `sorry`
+3628800

doc/examples/palindromes.lean.out.expected

@@ -0,0 +1,2 @@
+true
+false

doc/examples/phoas.lean.out.expected

@@ -0,0 +1,2 @@
+"(((fun x_1 => (fun x_2 => (x_1 + x_2))) 1) 2)"
+"((((fun x_1 => (fun x_2 => (x_1 + x_2))) 1) 2) + 5)"

doc/examples/run_test

@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+source ../../tests/env_test.sh
+source "$TEST_DIR/util.sh"
+
+exec_capture "$1" \
+  lean -Dlinter.all=false "$1"
+
+check_exit "$1"
+check_out "$1"

src/Lean/Server/Test/Runner.lean

@@ -265,7 +265,7 @@ def ident : Parser Name := do
   return xs.foldl .str $ .mkSimple head
 
 def patchUri (s : String) : IO String := do
-  let patterns := #["/src/Init/", "/src/Lean/", "/src/Std/", "/tests/lean/interactive/"]
+  let patterns := #["/src/Init/", "/src/Lean/", "/src/Std/", "/tests/misc_dir/"]
   let some path := System.Uri.fileUriToPath? s
     | return s
   let path ← try