diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md
index 8036dba4fb..1ce0336f35 100644
--- a/.claude/CLAUDE.md
+++ b/.claude/CLAUDE.md
@@ -20,7 +20,8 @@ CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
 make -C build/release -j "$(nproc)" test ARGS='--rerun-failed'
 
 # Single test from tests/foo/bar/ (quick check during development)
-cd tests/foo/bar && ./run_test example_test.lean
+CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
+make -C build/release -j "$(nproc)" test ARGS=-R testname'
 ```
 
 ## Testing stage 2
diff --git a/doc/examples/compiler/run_test b/doc/examples/compiler/run_test.sh
old mode 100755
new mode 100644
similarity index 64%
rename from doc/examples/compiler/run_test
rename to doc/examples/compiler/run_test.sh
index affefd3b37..000aabbbdb
--- a/doc/examples/compiler/run_test
+++ b/doc/examples/compiler/run_test.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../../tests/env_test.sh
-
 leanmake --always-make bin
 
 capture ./build/bin/test hello world
diff --git a/doc/examples/run_test b/doc/examples/run_test.sh
old mode 100755
new mode 100644
similarity index 62%
rename from doc/examples/run_test
rename to doc/examples/run_test.sh
index e7a00a4351..40a81bc83b
--- a/doc/examples/run_test
+++ b/doc/examples/run_test.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../tests/env_test.sh
-
 capture_only "$1" \
   lean -Dlinter.all=false "$1"
 check_exit_is_success
diff --git a/tests/.gitignore b/tests/.gitignore
index 24d50cc1bd..1f28d50dc9 100644
--- a/tests/.gitignore
+++ b/tests/.gitignore
@@ -1,6 +1,5 @@
 # Generated by cmake
-/env_test.sh
-/env_bench.sh
+/with_*_env.sh
 
 # Created by test suite
 *.out.produced
diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
index d306742c44..d0a43a6c90 100644
--- a/tests/CMakeLists.txt
+++ b/tests/CMakeLists.txt
@@ -38,12 +38,15 @@ string(APPEND TEST_VARS " LEANC_OPTS='${LEANC_OPTS}'")
 # LEANC_OPTS in CXX is necessary for macOS c++ to find its headers
 string(APPEND TEST_VARS " CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}'")
 
+set(WITH_TEST_ENV "${CMAKE_CURRENT_SOURCE_DIR}/with_stage${STAGE}_test_env.sh")
+set(WITH_BENCH_ENV "${CMAKE_CURRENT_SOURCE_DIR}/with_stage${STAGE}_bench_env.sh")
+
 string(APPEND TEST_VARS " TEST_BENCH=")
-configure_file(env.sh.in "${CMAKE_CURRENT_SOURCE_DIR}/env_test.sh")
+configure_file(with_env.sh.in "${WITH_TEST_ENV}")
 
 block()
   string(APPEND TEST_VARS " TEST_BENCH=1")
-  configure_file(env.sh.in "${CMAKE_CURRENT_SOURCE_DIR}/env_bench.sh")
+  configure_file(with_env.sh.in "${WITH_BENCH_ENV}")
 endblock()
 
 ######################
@@ -69,8 +72,8 @@ function(glob_except OUT DIR GLOB)
 endfunction()
 
 function(check_test_bench_scripts DIR)
-  set(RUN_TEST "${DIR}/run_test")
-  set(RUN_BENCH "${DIR}/run_bench")
+  set(RUN_TEST "${DIR}/run_test.sh")
+  set(RUN_BENCH "${DIR}/run_bench.sh")
 
   set(RUN_TEST_EXISTS FALSE)
   set(RUN_BENCH_EXISTS FALSE)
@@ -125,10 +128,10 @@ endfunction()
 # represents a separate test (or benchmark). The directory may also contain
 # additional files or subdirectories required by the individual test files.
 #
-# If a run_test script is present, each test file will be added as a test. Tests
+# If a run_test.sh script is present, each test file will be added as a test. Tests
 # can be disabled on a per-file basis by creating a `<file>.no_test` file.
 #
-# If a run_bench script is present, each test file will be added as a benchmark.
+# If a run_bench.sh script is present, each test file will be added as a benchmark.
 # Benchmarks can be disabled on a per-file basis by creating a `<file>.no_bench`
 # file. CMake expects the bench script to produce a `<file>.measurements.jsonl`
 # file next to the test file. The individual measurements will be combined into
@@ -160,7 +163,7 @@ function(add_test_pile DIR GLOB)
         NAME "${FILE_IN_SOURCE_DIR}"
         WORKING_DIRECTORY "${DIR}"
         # On Windows, we can't call the file directly, hence we always use bash.
-        COMMAND bash "${RUN_TEST}" "${FILE_IN_DIR}"
+        COMMAND bash "${WITH_TEST_ENV}" "${RUN_TEST}" "${FILE_IN_DIR}"
       )
     endif()
 
@@ -172,7 +175,7 @@ function(add_test_pile DIR GLOB)
         WORKING_DIRECTORY "${DIR}"
         COMMAND "${CMAKE_COMMAND}" -E remove -f "${MEASUREMENTS_FILE}"
         # On Windows, we can't call the file directly, hence we always use bash.
-        COMMAND bash "${RUN_BENCH}" "${FILE_IN_DIR}"
+        COMMAND bash "${WITH_BENCH_ENV}" "${RUN_BENCH}" "${FILE_IN_DIR}"
       )
     endif()
   endforeach()
@@ -202,7 +205,7 @@ function(add_test_dir DIR)
       NAME "${DIR_IN_SOURCE_DIR}"
       WORKING_DIRECTORY "${DIR}"
       # On Windows, we can't call the file directly, hence we always use bash.
-      COMMAND bash "${RUN_TEST}"
+      COMMAND bash "${WITH_TEST_ENV}" "${RUN_TEST}"
     )
   endif()
 
@@ -216,7 +219,7 @@ function(add_test_dir DIR)
       WORKING_DIRECTORY "${DIR}"
       COMMAND "${CMAKE_COMMAND}" -E remove -f "${MEASUREMENTS_FILE}"
       # On Windows, we can't call the file directly, hence we always use bash.
-      COMMAND bash "${RUN_BENCH}"
+      COMMAND bash "${WITH_BENCH_ENV}" "${RUN_BENCH}"
     )
   endif()
 endfunction()
diff --git a/tests/README.md b/tests/README.md
index 5891ccf484..13db992206 100644
--- a/tests/README.md
+++ b/tests/README.md
@@ -4,11 +4,11 @@ This directory contains the lean test and benchmark suite.
 
 The test suite consists of two types of directories: Test directories and test piles.
 
-A **test directory** is a directory containing a `run_test` and/or a `run_bench` script.
+A **test directory** is a directory containing a `run_test.sh` and/or a `run_bench.sh` script.
 It represents a single test or benchmark, depending on which script is present.
 The run scripts are executed once with their working directory set to the test directory.
 
-A **test pile** is also a directory containing a `run_test` and/or a `run_bench` script.
+A **test pile** is also a directory containing a `run_test.sh` and/or a `run_bench.sh` script.
 Here however, each file of a directory-specific extension (usually `.lean`) represents a single test or benchmark.
 The run scripts are executed once for each test file with their working directory set to the pile directory.
 Often, additional supplementary files are placed next to the test files and interpreted by the run scripts.
@@ -70,11 +70,19 @@ CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
 make -C build/release -j "$(nproc)" test ARGS="--rerun-failed"
 ```
 
-Run an individual test by `cd`-ing into its directory and then using
+Run an individual test using one of these commands:
 
 ```sh
-./run_test # in a test directory
-./run_test testfile # in a test pile
+CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
+make -C build/release -j "$(nproc)" test ARGS="-R <regex>"
+
+# For a specific stage
+CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
+make -C build/release/stage1 -j "$(nproc)" test ARGS="-R <regex>"
+
+# Manually, without ctest
+tests/with_stage1_test_env.sh path/to/test/directory/run_test.sh
+tests/with_stage1_test_env.sh path/to/test/pile/run_test.sh testfile
 ```
 
 ## How to run the bench suite?
@@ -95,11 +103,11 @@ make -C build/release -j "$(nproc)" bench-part2 # produces tests/part2.measureme
 
 Make sure not to specify `-j "$(nproc)"` when running the bench suite manually inside `build/release/stage<n>`.
 
-Run an individual benchmark by `cd`-ing into its directory and then using
+Run an individual benchmark manually using
 
 ```sh
-./run_bench # in a test directory
-./run_bench testfile # in a test pile
+tests/with_stage1_bench_env.sh path/to/test/directory/run_bench.sh
+tests/with_stage1_bench_env.sh path/to/test/pile/run_bench.sh testfile
 ```
 
 ## How to write a test?
@@ -120,7 +128,7 @@ If your test should be part of one of the existing test directories:
 Otherwise, create a new test directory or pile:
 
 1. Decide on a place to put the new directory.
-2. Write a `run_test` and/or `run_bench` script.
+2. Write a `run_test.sh` and/or `run_bench.sh` script.
 3. Add the directory to the [`CMakeLists.txt`](CMakeLists.txt) file,
    next to the other tests near the bottom.
 4. Document the new directory in this readme file
@@ -130,7 +138,7 @@ Otherwise, create a new test directory or pile:
 ## How to write a benchmark?
 
 When writing a benchmark, consider that most benchmarks are also executed as tests.
-You can check that this is the case if a `run_test` script exists next to the `run_bench` script in the directory.
+You can check that this is the case if a `run_test.sh` script exists next to the `run_bench.sh` script in the directory.
 When run as benchmark, the problem instance should be large enough to result in reliable measurements.
 When run as test, the problem instance should be as small as possible, but large enough to still test the different code paths.
 
@@ -167,33 +175,29 @@ Some test directories or test piles strip or modify certain flaky or nondetermin
 
 ## How to write a test or bench run script?
 
-Test and bench scripts must be named `run_test` and `run_bench` respectively.
-They must be executable and start with the shebang `#!/usr/bin/env bash`.
-Immediately afterwards, they must source `env_test.sh` or `env_bench.sh` respectively
-using a relative path.
+Test and bench scripts must be named `run_test.sh` and `run_bench.sh` respectively.
+They are sourced by the `with_*_env.sh` script,
+which provides a set of environment variables and definitions.
+Because of this, they require no shebang and should not be executable.
 
-The `env_*.sh` files set some build related environment variables,
-plus a set of test suite related environment variables
-document at the top of [`CMakeLists.txt`](CMakeLists.txt).
-The most notable ones are:
+The most notable environment variables are:
 
 - `TEST_DIR`: Absolute path to the `tests` directory.
 - `SCRIPT_DIR`: Absolute path to the `script` directory.
 - `TEST_BENCH`: Set to `1` if we're currently executing a benchmark, unset otherwise.
 
-It also sources `"$TEST_DIR/util.sh"`,
+The definitions come from `util.sh`,
 which provides a few utility functions and also uses `set` to set sensible bash defaults.
-See `util.sh` for the available utility functions.
 
 The run scripts are always executed with their working directory set to their surrounding directory.
-Inside a test pile, `run_test` and `run_bench` receive
+Inside a test pile, `run_test.sh` and `run_bench.sh` receive
 a relative path to the file under test as their first (and only) argument.
 Inside a test directory, they receive no arguments.
 
-A test succeeds iff the `run_test` script exits with exit code 0.
+A test succeeds iff the `run_test.sh` script exits with exit code 0.
 A benchmark additionally must produce a measurements file:
-Inside a test pile, `run_bench testfile` is expected to produce a `testfile.measurments.jsonl` file.
-Inside a test directory, `run_bench` is expected to produce a `measurements.jsonl` file.
+Inside a test pile, `run_bench.sh` is expected to produce a `<testfile>.measurments.jsonl` file.
+Inside a test directory, `run_bench.sh` is expected to produce a `measurements.jsonl` file.
 
 ## The `elab*` test pile
 
diff --git a/tests/bench/build/lakeprof_report_upload.py b/tests/bench/build/lakeprof_report_upload.py
index a847c96ba3..9038b4711c 100755
--- a/tests/bench/build/lakeprof_report_upload.py
+++ b/tests/bench/build/lakeprof_report_upload.py
@@ -22,7 +22,7 @@ def run_stdout(*command: str, cwd: Path | None = None) -> str:
 
 sha = run_stdout("git", "rev-parse", "@", cwd=src_dir).strip()
 base_url = f"https://speed.lean-lang.org/lean4-out/{sha}"
-report = run_stdout("lakeprof", "report", "-prc", cwd=src_dir)
+report = (src_dir / "lakeprof_report.txt").read_text()
 
 template = template_file.read_text()
 template = template.replace("__BASE_URL__", json.dumps(base_url))
diff --git a/tests/bench/build/run_bench b/tests/bench/build/run_bench.sh
old mode 100755
new mode 100644
similarity index 64%
rename from tests/bench/build/run_bench
rename to tests/bench/build/run_bench.sh
index c4160a6768..4388163a91
--- a/tests/bench/build/run_bench
+++ b/tests/bench/build/run_bench.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../env_bench.sh
-
 STAGE_THIS="stage$STAGE"
 STAGE_NEXT="stage$((STAGE + 1))"
 
@@ -17,19 +14,7 @@ echo ">"
 echo "> Configuring $STAGE_NEXT..."
 echo ">"
 
-# Building a stage mostly affects files in that stage's build directory.
-# However, the bench suite runs inside the source directory for developer UX
-# reasons, so some stage-specific bench suite files are generated in the source
-# directory (namely the env_*.sh files).
-#
-# To avoid messing up the rest of the bench suite, we restore those files to
-# STAGE_THIS's versions immediately after we configure STAGE_NEXT. Yes, this is
-# a big hack, but it allows running the build benchmark as part of the bench
-# suite instead of completely separately.
-#
-# Configuring STAGE_NEXT also builds all stages up to and including STAGE_THIS.
 make -C "$BUILD_ROOT" -j"$(nproc)" "$STAGE_NEXT-configure"
-make -C "$BUILD_ROOT" -j"$(nproc)" "$STAGE_THIS-configure"
 
 
 
@@ -66,6 +51,7 @@ echo ">"
 # calling lake in its current working directory.
 mv lakeprof.log "$SRC_DIR"
 pushd "$SRC_DIR"
+lakeprof report -prc > lakeprof_report.txt
 lakeprof report -pj | jq '{metric: "build/lakeprof/longest build path//wall-clock", value: .[-1][2], unit: "s"}' -c >> "$OUT"
 lakeprof report -rj | jq '{metric: "build/lakeprof/longest rebuild path//wall-clock", value: .[-1][2], unit: "s"}' -c >> "$OUT"
 popd
diff --git a/tests/bench/build/run_upload_lakeprof_report b/tests/bench/build/run_upload_lakeprof_report
deleted file mode 100755
index 0d12ce7108..0000000000
--- a/tests/bench/build/run_upload_lakeprof_report
+++ /dev/null
@@ -1,11 +0,0 @@
-#!/usr/bin/env bash
-source ../../env_bench.sh
-
-# This should run in the same environment as run_bench, otherwise `lakeprof`
-# will use the `lake` from the global system `elan` install and not the one from
-# the current commit.
-#
-# Once an elan with support for relative toolchains has been widely released and
-# been adopted by this repo, this wrapper script should no longer be necessary
-# and the upload script can be called directly.
-./lakeprof_report_upload.py
diff --git a/tests/bench/dag_hassorry_issue.lean.expected.out b/tests/bench/dag_hassorry_issue.lean.out.expected
similarity index 100%
rename from tests/bench/dag_hassorry_issue.lean.expected.out
rename to tests/bench/dag_hassorry_issue.lean.out.expected
diff --git a/tests/bench/mvcgen/sym/run_bench b/tests/bench/mvcgen/sym/run_bench.sh
old mode 100755
new mode 100644
similarity index 95%
rename from tests/bench/mvcgen/sym/run_bench
rename to tests/bench/mvcgen/sym/run_bench.sh
index bfdb851cfc..32a9115a24
--- a/tests/bench/mvcgen/sym/run_bench
+++ b/tests/bench/mvcgen/sym/run_bench.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../../env_bench.sh
-
 rm -f measurements.jsonl
 
 # Build dependencies first so their compilation isn't measured.
diff --git a/tests/bench/mvcgen/sym/run_test b/tests/bench/mvcgen/sym/run_test.sh
old mode 100755
new mode 100644
similarity index 67%
rename from tests/bench/mvcgen/sym/run_test
rename to tests/bench/mvcgen/sym/run_test.sh
index 071e59c541..b228532fcb
--- a/tests/bench/mvcgen/sym/run_test
+++ b/tests/bench/mvcgen/sym/run_test.sh
@@ -1,5 +1,2 @@
-#!/usr/bin/env bash
-source ../../../env_test.sh
-
 # Limit threads to avoid exhausting memory with the large thread stack.
 LEAN_NUM_THREADS=1 lake test
diff --git a/tests/bench/size/run_bench b/tests/bench/size/run_bench.sh
old mode 100755
new mode 100644
similarity index 76%
rename from tests/bench/size/run_bench
rename to tests/bench/size/run_bench.sh
index ebb5f26b72..f14e88bdde
--- a/tests/bench/size/run_bench
+++ b/tests/bench/size/run_bench.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../env_bench.sh
-
 make -C "$BUILD_DIR" install DESTDIR="$(realpath install)"
 python measure_sizes.py "$SRC_DIR" "$BUILD_DIR" install measurements.jsonl
 rm -rf install
diff --git a/tests/compile/run_bench b/tests/compile/run_bench.sh
old mode 100755
new mode 100644
similarity index 94%
rename from tests/compile/run_bench
rename to tests/compile/run_bench.sh
index 2bebbde972..0c37663e0a
--- a/tests/compile/run_bench
+++ b/tests/compile/run_bench.sh
@@ -1,5 +1,3 @@
-#!/usr/bin/env bash
-source ../env_bench.sh
 source_init "$1"
 
 if [[ -f "$1.do_compile_bench" ]]; then DO_COMPILE=1
diff --git a/tests/compile/run_test b/tests/compile/run_test.sh
old mode 100755
new mode 100644
similarity index 96%
rename from tests/compile/run_test
rename to tests/compile/run_test.sh
index 6fb1ada12f..bbb8f8b985
--- a/tests/compile/run_test
+++ b/tests/compile/run_test.sh
@@ -1,5 +1,3 @@
-#!/usr/bin/env bash
-source ../env_test.sh
 source_init "$1"
 
 if [[ -f "$1.do_compile_test" ]]; then DO_COMPILE=1
diff --git a/tests/compile_bench/run_bench b/tests/compile_bench/run_bench.sh
old mode 100755
new mode 100644
similarity index 97%
rename from tests/compile_bench/run_bench
rename to tests/compile_bench/run_bench.sh
index e677d6819d..297051f61a
--- a/tests/compile_bench/run_bench
+++ b/tests/compile_bench/run_bench.sh
@@ -1,5 +1,3 @@
-#!/usr/bin/env bash
-source ../env_bench.sh
 source_init "$1"
 
 if [[ -f "$1.do_compile_bench" ]]; then DO_COMPILE=1
diff --git a/tests/compile_bench/run_test b/tests/compile_bench/run_test
deleted file mode 120000
index a8a41fecb0..0000000000
--- a/tests/compile_bench/run_test
+++ /dev/null
@@ -1 +0,0 @@
-../compile/run_test
\ No newline at end of file
diff --git a/tests/compile_bench/run_test.sh b/tests/compile_bench/run_test.sh
new file mode 120000
index 0000000000..6d82e16c8c
--- /dev/null
+++ b/tests/compile_bench/run_test.sh
@@ -0,0 +1 @@
+../compile/run_test.sh
\ No newline at end of file
diff --git a/tests/docparse/run_test b/tests/docparse/run_test.sh
old mode 100755
new mode 100644
similarity index 85%
rename from tests/docparse/run_test
rename to tests/docparse/run_test.sh
index 52d30e0eaa..4616e3d4ea
--- a/tests/docparse/run_test
+++ b/tests/docparse/run_test.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../env_test.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
diff --git a/tests/elab/run_test b/tests/elab/run_test.sh
old mode 100755
new mode 100644
similarity index 90%
rename from tests/elab/run_test
rename to tests/elab/run_test.sh
index 19811b1b9f..41772406bb
--- a/tests/elab/run_test
+++ b/tests/elab/run_test.sh
@@ -1,7 +1,4 @@
-#!/usr/bin/env bash
-source ../env_test.sh
 source_init "$1"
-
 run_before "$1"
 
 # `--root` to infer same private names as in the server
diff --git a/tests/elab_bench/run_bench b/tests/elab_bench/run_bench.sh
old mode 100755
new mode 100644
similarity index 92%
rename from tests/elab_bench/run_bench
rename to tests/elab_bench/run_bench.sh
index 877a5ddc38..fa0a846ef7
--- a/tests/elab_bench/run_bench
+++ b/tests/elab_bench/run_bench.sh
@@ -1,7 +1,4 @@
-#!/usr/bin/env bash
-source ../env_bench.sh
 source_init "$1"
-
 run_before "$1"
 
 TOPIC="elab/$(basename "$1" .lean)"
diff --git a/tests/elab_bench/run_test b/tests/elab_bench/run_test
deleted file mode 120000
index 98ed3a9119..0000000000
--- a/tests/elab_bench/run_test
+++ /dev/null
@@ -1 +0,0 @@
-../elab/run_test
\ No newline at end of file
diff --git a/tests/elab_bench/run_test.sh b/tests/elab_bench/run_test.sh
new file mode 120000
index 0000000000..603161cda3
--- /dev/null
+++ b/tests/elab_bench/run_test.sh
@@ -0,0 +1 @@
+../elab/run_test.sh
\ No newline at end of file
diff --git a/tests/elab_fail/run_test b/tests/elab_fail/run_test.sh
old mode 100755
new mode 100644
similarity index 90%
rename from tests/elab_fail/run_test
rename to tests/elab_fail/run_test.sh
index d91b551aaa..91081b9756
--- a/tests/elab_fail/run_test
+++ b/tests/elab_fail/run_test.sh
@@ -1,7 +1,4 @@
-#!/usr/bin/env bash
-source ../env_test.sh
 source_init "$1"
-
 run_before "$1"
 
 # `--root` to infer same private names as in the server
diff --git a/tests/lake_bench/inundation/run_bench b/tests/lake_bench/inundation/run_bench.sh
old mode 100755
new mode 100644
similarity index 96%
rename from tests/lake_bench/inundation/run_bench
rename to tests/lake_bench/inundation/run_bench.sh
index 07349b03b2..de4fc902b8
--- a/tests/lake_bench/inundation/run_bench
+++ b/tests/lake_bench/inundation/run_bench.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../env_bench.sh
-
 PREFIX="lake/inundation"
 rm -f measurements.jsonl
 
diff --git a/tests/lint.py b/tests/lint.py
index 34bdefc52c..ab6f942eeb 100755
--- a/tests/lint.py
+++ b/tests/lint.py
@@ -20,8 +20,17 @@ def nag(reason: str, path: Path, fatal: bool = True) -> None:
 
 # Files and directories that will no longer work.
 
-for file in Path().glob("tests/speedcenter.exec.velcom.yaml"):
-    nag("removed file", file)
+for pattern in (
+    "**/*.exit.expected",
+    "**/*.expected.out",
+    "**/*.expected.ret",
+    "**/*.no_interpreter",
+    "**/run_bench",
+    "**/run_test",
+    "tests/speedcenter.exec.velcom.yaml",
+):
+    for file in Path().glob(pattern):
+        nag("removed file", file)
 
 for dir in (
     "tests/bench-radar",
@@ -39,12 +48,12 @@ for dir in (
         nag("removed dir", file)
 
 for dir in ("tests/lean",):
-    for glob in (
+    for pattern in (
         f"{dir}/*.lean",
         f"{dir}/*.expected.out",
         f"{dir}/*.expected.ret",
     ):
-        for file in Path().glob(glob):
+        for file in Path().glob(pattern):
             nag("removed dir", file)
 
 
@@ -63,18 +72,18 @@ for dir in (
     "tests/server",
     "tests/server_interactive",
 ):
-    for glob in (
+    for pattern in (
         f"{dir}/*.no_interpreter",
         f"{dir}/*.expected.out",
         f"{dir}/*.expected.ret",
     ):
-        for file in Path().glob(glob):
+        for file in Path().glob(pattern):
             nag("old suffix", file)
 
 
 # Files that expect a corresponding base file
 
-for glob, drop in (
+for pattern, drop in (
     ("**/*.no_test", 1),
     ("**/*.no_bench", 1),
     ("**/*.do_compile", 1),
@@ -96,13 +105,8 @@ for glob, drop in (
     ("**/*.after.sh", 2),
     ("**/*.out.expected", 2),
     ("**/*.out.ignored", 2),
-    ("**/*.exit.expected", 2),
-    # Old naming convention
-    ("**/*.no_interpreter", 1),
-    ("**/*.expected.out", 2),
-    ("**/*.expected.ret", 2),
 ):
-    for file in Path().glob(glob):
+    for file in Path().glob(pattern):
         basefile = file
         for _ in range(drop):
             basefile = basefile.with_suffix("")
@@ -117,13 +121,12 @@ for glob, drop in (
 
 # Files that shouldn't be empty
 
-for glob in (
+for pattern in (
     "**/*.init.sh",
     "**/*.before.sh",
     "**/*.after.sh",
-    "**/*.exit.expected",
 ):
-    for file in Path().glob(glob):
+    for file in Path().glob(pattern):
         if file.read_text().strip():
             continue
         nag("empty", file)
@@ -153,40 +156,14 @@ for file in Path().glob("**/*.no_test"):
 
 # Special rules for certain directories
 
-for glob in (
+for pattern in (
     "tests/compile_bench/*.no_bench",
-    "tests/elab/*.exit.expected",
     "tests/elab_bench/*.no_bench",
     "tests/misc_bench/*.no_bench",
 ):
-    for file in Path().glob(glob):
+    for file in Path().glob(pattern):
         nag("forbidden", file)
 
-for file in Path().glob("tests/elab_fail/*.exit.expected"):
-    if file.read_text().strip() == "0":
-        nag("must be != 0", file)
-
-
-# Run scripts sourcing incorrectly
-
-for file in Path().glob("**/run_test"):
-    if file.is_symlink():
-        continue
-    text = file.read_text()
-    if "env_test.sh" not in text:
-        nag("no env_test.sh", file)
-    if "env_bench.sh" in text:
-        nag("has env_bench.sh", file)
-
-for file in Path().glob("**/run_bench"):
-    if file.is_symlink():
-        continue
-    text = file.read_text()
-    if "env_bench.sh" not in text:
-        nag("no env_bench.sh", file)
-    if "env_test.sh" in text:
-        nag("has env_test.sh", file)
-
 
 # File confusion by case insensitive filesystems
 
diff --git a/tests/misc/run_test b/tests/misc/run_test.sh
old mode 100755
new mode 100644
similarity index 51%
rename from tests/misc/run_test
rename to tests/misc/run_test.sh
index 01356a79f4..1d455adb0f
--- a/tests/misc/run_test
+++ b/tests/misc/run_test.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../env_test.sh
-
 NAME="$1"
 FILE="$(realpath "$1")"
 source "$1"
diff --git a/tests/misc_bench/run_bench b/tests/misc_bench/run_bench.sh
old mode 100755
new mode 100644
similarity index 71%
rename from tests/misc_bench/run_bench
rename to tests/misc_bench/run_bench.sh
index 71ca5de6fe..af41c221e3
--- a/tests/misc_bench/run_bench
+++ b/tests/misc_bench/run_bench.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../env_bench.sh
-
 NAME="$1"
 FILE="$(realpath "$1")"
 OUT="$FILE.measurements.jsonl"
diff --git a/tests/misc_dir/plugin/run_test b/tests/misc_dir/plugin/run_test.sh
old mode 100755
new mode 100644
similarity index 88%
rename from tests/misc_dir/plugin/run_test
rename to tests/misc_dir/plugin/run_test.sh
index 240a02b7d3..efd8108411
--- a/tests/misc_dir/plugin/run_test
+++ b/tests/misc_dir/plugin/run_test.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
 # LEAN_EXPORTING needs to be defined for .c files included in shared libraries
 lean --c=SnakeLinter.c SnakeLinter.lean
 leanc ${LEANC_OPTS-} -O3 -DNDEBUG -DLEAN_EXPORTING -shared -o SnakeLinter.so SnakeLinter.c
diff --git a/tests/misc_dir/server_project/run_test b/tests/misc_dir/server_project/run_test.sh
old mode 100755
new mode 100644
similarity index 87%
rename from tests/misc_dir/server_project/run_test
rename to tests/misc_dir/server_project/run_test.sh
index 1bc4269629..822e70a589
--- a/tests/misc_dir/server_project/run_test
+++ b/tests/misc_dir/server_project/run_test.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../env_test.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
diff --git a/tests/pkg/builtin_attr/run_test b/tests/pkg/builtin_attr/run_test
deleted file mode 100755
index 8278b89b81..0000000000
--- a/tests/pkg/builtin_attr/run_test
+++ /dev/null
@@ -1,5 +0,0 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
-rm -rf .lake/build
-lake build
diff --git a/tests/pkg/builtin_attr/run_test.sh b/tests/pkg/builtin_attr/run_test.sh
new file mode 100644
index 0000000000..b911bf4de8
--- /dev/null
+++ b/tests/pkg/builtin_attr/run_test.sh
@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build
diff --git a/tests/pkg/cbv_attr/run_test b/tests/pkg/cbv_attr/run_test
deleted file mode 100755
index 8278b89b81..0000000000
--- a/tests/pkg/cbv_attr/run_test
+++ /dev/null
@@ -1,5 +0,0 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
-rm -rf .lake/build
-lake build
diff --git a/tests/pkg/cbv_attr/run_test.sh b/tests/pkg/cbv_attr/run_test.sh
new file mode 100644
index 0000000000..b911bf4de8
--- /dev/null
+++ b/tests/pkg/cbv_attr/run_test.sh
@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build
diff --git a/tests/pkg/debug/run_test b/tests/pkg/debug/run_test.sh
old mode 100755
new mode 100644
similarity index 58%
rename from tests/pkg/debug/run_test
rename to tests/pkg/debug/run_test.sh
index 19d85f1fd0..fd1762db3c
--- a/tests/pkg/debug/run_test
+++ b/tests/pkg/debug/run_test.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
 rm -rf .lake/build
 
 run lake exe release
diff --git a/tests/pkg/def_clash/run_test b/tests/pkg/def_clash/run_test.sh
old mode 100755
new mode 100644
similarity index 96%
rename from tests/pkg/def_clash/run_test
rename to tests/pkg/def_clash/run_test.sh
index 9cb1784d9a..7c8508520c
--- a/tests/pkg/def_clash/run_test
+++ b/tests/pkg/def_clash/run_test.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
 # The test covers the behavior of transitively importing multiple modules
 # that have a definition with the same name.
 
diff --git a/tests/pkg/deriving/run_test b/tests/pkg/deriving/run_test
deleted file mode 100755
index 8278b89b81..0000000000
--- a/tests/pkg/deriving/run_test
+++ /dev/null
@@ -1,5 +0,0 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
-rm -rf .lake/build
-lake build
diff --git a/tests/pkg/deriving/run_test.sh b/tests/pkg/deriving/run_test.sh
new file mode 100644
index 0000000000..b911bf4de8
--- /dev/null
+++ b/tests/pkg/deriving/run_test.sh
@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build
diff --git a/tests/pkg/frontend/run_test b/tests/pkg/frontend/run_test.sh
old mode 100755
new mode 100644
similarity index 96%
rename from tests/pkg/frontend/run_test
rename to tests/pkg/frontend/run_test.sh
index b5d30bfb72..a544fcdf3d
--- a/tests/pkg/frontend/run_test
+++ b/tests/pkg/frontend/run_test.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
 rm -rf .lake/build
 lake build
 
diff --git a/tests/pkg/initialize/run_test b/tests/pkg/initialize/run_test
deleted file mode 100755
index 8278b89b81..0000000000
--- a/tests/pkg/initialize/run_test
+++ /dev/null
@@ -1,5 +0,0 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
-rm -rf .lake/build
-lake build
diff --git a/tests/pkg/initialize/run_test.sh b/tests/pkg/initialize/run_test.sh
new file mode 100644
index 0000000000..b911bf4de8
--- /dev/null
+++ b/tests/pkg/initialize/run_test.sh
@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build
diff --git a/tests/pkg/leanchecker/run_test b/tests/pkg/leanchecker/run_test.sh
old mode 100755
new mode 100644
similarity index 93%
rename from tests/pkg/leanchecker/run_test
rename to tests/pkg/leanchecker/run_test.sh
index a49bb21a80..44f41a4240
--- a/tests/pkg/leanchecker/run_test
+++ b/tests/pkg/leanchecker/run_test.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
 rm -rf .lake/build
 lake build
 
diff --git a/tests/pkg/linter_set/run_test b/tests/pkg/linter_set/run_test
deleted file mode 100755
index 8278b89b81..0000000000
--- a/tests/pkg/linter_set/run_test
+++ /dev/null
@@ -1,5 +0,0 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
-rm -rf .lake/build
-lake build
diff --git a/tests/pkg/linter_set/run_test.sh b/tests/pkg/linter_set/run_test.sh
new file mode 100644
index 0000000000..b911bf4de8
--- /dev/null
+++ b/tests/pkg/linter_set/run_test.sh
@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build
diff --git a/tests/pkg/misc/run_test b/tests/pkg/misc/run_test
deleted file mode 100755
index 8278b89b81..0000000000
--- a/tests/pkg/misc/run_test
+++ /dev/null
@@ -1,5 +0,0 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
-rm -rf .lake/build
-lake build
diff --git a/tests/pkg/misc/run_test.sh b/tests/pkg/misc/run_test.sh
new file mode 100644
index 0000000000..b911bf4de8
--- /dev/null
+++ b/tests/pkg/misc/run_test.sh
@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build
diff --git a/tests/pkg/mod_clash/run_test b/tests/pkg/mod_clash/run_test.sh
old mode 100755
new mode 100644
similarity index 92%
rename from tests/pkg/mod_clash/run_test
rename to tests/pkg/mod_clash/run_test.sh
index 25e08975dd..8a7a638fe9
--- a/tests/pkg/mod_clash/run_test
+++ b/tests/pkg/mod_clash/run_test.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
 # This test covers importing modules which are defined in multiple packages
 # (with the same original package name).
 
diff --git a/tests/pkg/module/run_test b/tests/pkg/module/run_test.sh
old mode 100755
new mode 100644
similarity index 76%
rename from tests/pkg/module/run_test
rename to tests/pkg/module/run_test.sh
index b6f08e23c2..de377ac1ca
--- a/tests/pkg/module/run_test
+++ b/tests/pkg/module/run_test.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
 rm -rf .lake/build
 LEAN_ABORT_ON_PANIC=1 lake build
 
diff --git a/tests/pkg/path with spaces/run_test b/tests/pkg/path with spaces/run_test.sh
old mode 100755
new mode 100644
similarity index 77%
rename from tests/pkg/path with spaces/run_test
rename to tests/pkg/path with spaces/run_test.sh
index c64021cc62..7044f45e6f
--- a/tests/pkg/path with spaces/run_test	
+++ b/tests/pkg/path with spaces/run_test.sh	
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
 rm -rf .lake/build
 lake exe "path with spaces"
 # presence of this file should not break process spawn
diff --git a/tests/pkg/prv/run_test b/tests/pkg/prv/run_test
deleted file mode 100755
index 8278b89b81..0000000000
--- a/tests/pkg/prv/run_test
+++ /dev/null
@@ -1,5 +0,0 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
-rm -rf .lake/build
-lake build
diff --git a/tests/pkg/prv/run_test.sh b/tests/pkg/prv/run_test.sh
new file mode 100644
index 0000000000..b911bf4de8
--- /dev/null
+++ b/tests/pkg/prv/run_test.sh
@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build
diff --git a/tests/pkg/rebuild/run_test b/tests/pkg/rebuild/run_test.sh
old mode 100755
new mode 100644
similarity index 97%
rename from tests/pkg/rebuild/run_test
rename to tests/pkg/rebuild/run_test.sh
index 9cb6dcd63d..048158d210
--- a/tests/pkg/rebuild/run_test
+++ b/tests/pkg/rebuild/run_test.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
 rm -rf .lake/build
 
 mkdir -p Rebuild
diff --git a/tests/pkg/setup/run_test b/tests/pkg/setup/run_test.sh
old mode 100755
new mode 100644
similarity index 73%
rename from tests/pkg/setup/run_test
rename to tests/pkg/setup/run_test.sh
index 6b61853497..cb6f0494a3
--- a/tests/pkg/setup/run_test
+++ b/tests/pkg/setup/run_test.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
 # Test that Lean will use the specified olean from `setup.json`
 lean Dep.lean -o Dep.olean
 lean Test.lean --setup setup.json
diff --git a/tests/pkg/signal/run_test b/tests/pkg/signal/run_test.sh
old mode 100755
new mode 100644
similarity index 95%
rename from tests/pkg/signal/run_test
rename to tests/pkg/signal/run_test.sh
index d4c2730686..e99ea33b6d
--- a/tests/pkg/signal/run_test
+++ b/tests/pkg/signal/run_test.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
 rm -rf .lake/build
 lake build release
 
diff --git a/tests/pkg/structure_docstrings/run_test b/tests/pkg/structure_docstrings/run_test.sh
old mode 100755
new mode 100644
similarity index 53%
rename from tests/pkg/structure_docstrings/run_test
rename to tests/pkg/structure_docstrings/run_test.sh
index 134dcc7476..86adafe999
--- a/tests/pkg/structure_docstrings/run_test
+++ b/tests/pkg/structure_docstrings/run_test.sh
@@ -1,5 +1,2 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
 rm -rf .lake/build
 LEAN_ABORT_ON_PANIC=1 lake build
diff --git a/tests/pkg/test_extern/run_test b/tests/pkg/test_extern/run_test.sh
old mode 100755
new mode 100644
similarity index 96%
rename from tests/pkg/test_extern/run_test
rename to tests/pkg/test_extern/run_test.sh
index 272fbe7c8e..178d67f395
--- a/tests/pkg/test_extern/run_test
+++ b/tests/pkg/test_extern/run_test.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
 # We need a package test because we need multiple files with imports.
 # Currently the other package tests all succeed,
 # but here we need to check for a particular error message.
diff --git a/tests/pkg/user_attr/run_test b/tests/pkg/user_attr/run_test
deleted file mode 100755
index 8278b89b81..0000000000
--- a/tests/pkg/user_attr/run_test
+++ /dev/null
@@ -1,5 +0,0 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
-rm -rf .lake/build
-lake build
diff --git a/tests/pkg/user_attr/run_test.sh b/tests/pkg/user_attr/run_test.sh
new file mode 100644
index 0000000000..b911bf4de8
--- /dev/null
+++ b/tests/pkg/user_attr/run_test.sh
@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build
diff --git a/tests/pkg/user_attr_app/run_test b/tests/pkg/user_attr_app/run_test
deleted file mode 100755
index d50e34e8c8..0000000000
--- a/tests/pkg/user_attr_app/run_test
+++ /dev/null
@@ -1,5 +0,0 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
-rm -rf .lake/build
-lake exe user_attr
diff --git a/tests/pkg/user_attr_app/run_test.sh b/tests/pkg/user_attr_app/run_test.sh
new file mode 100644
index 0000000000..e119dfff42
--- /dev/null
+++ b/tests/pkg/user_attr_app/run_test.sh
@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake exe user_attr
diff --git a/tests/pkg/user_ext/run_test b/tests/pkg/user_ext/run_test.sh
old mode 100755
new mode 100644
similarity index 64%
rename from tests/pkg/user_ext/run_test
rename to tests/pkg/user_ext/run_test.sh
index b75a6205cf..26263062c4
--- a/tests/pkg/user_ext/run_test
+++ b/tests/pkg/user_ext/run_test.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
 rm -rf .lake/build
 
 capture lake build -v
diff --git a/tests/pkg/user_opt/run_test b/tests/pkg/user_opt/run_test
deleted file mode 100755
index 8278b89b81..0000000000
--- a/tests/pkg/user_opt/run_test
+++ /dev/null
@@ -1,5 +0,0 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
-rm -rf .lake/build
-lake build
diff --git a/tests/pkg/user_opt/run_test.sh b/tests/pkg/user_opt/run_test.sh
new file mode 100644
index 0000000000..b911bf4de8
--- /dev/null
+++ b/tests/pkg/user_opt/run_test.sh
@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build
diff --git a/tests/pkg/user_plugin/run_test b/tests/pkg/user_plugin/run_test.sh
old mode 100755
new mode 100644
similarity index 97%
rename from tests/pkg/user_plugin/run_test
rename to tests/pkg/user_plugin/run_test.sh
index 77788f3d94..911a5876c3
--- a/tests/pkg/user_plugin/run_test
+++ b/tests/pkg/user_plugin/run_test.sh
@@ -1,5 +1,3 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
 set -euo pipefail
 
 # Deermine shared library extension
diff --git a/tests/pkg/ver_clash/run_test b/tests/pkg/ver_clash/run_test.sh
old mode 100755
new mode 100644
similarity index 98%
rename from tests/pkg/ver_clash/run_test
rename to tests/pkg/ver_clash/run_test.sh
index 3db66f5717..7b22adf8e7
--- a/tests/pkg/ver_clash/run_test
+++ b/tests/pkg/ver_clash/run_test.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
 # This directory contains a unified version of the "ring example"
 # developed by Kim across the following 4 repositories:
 #
diff --git a/tests/server/run_test b/tests/server/run_test.sh
old mode 100755
new mode 100644
similarity index 74%
rename from tests/server/run_test
rename to tests/server/run_test.sh
index 03c01443c9..19b5e82fb6
--- a/tests/server/run_test
+++ b/tests/server/run_test.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../env_test.sh
-
 run_before "$1"
 
 capture_only "$1" \
diff --git a/tests/server_interactive/run_test b/tests/server_interactive/run_test.sh
old mode 100755
new mode 100644
similarity index 88%
rename from tests/server_interactive/run_test
rename to tests/server_interactive/run_test.sh
index 541be16224..31e9dbc8e1
--- a/tests/server_interactive/run_test
+++ b/tests/server_interactive/run_test.sh
@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../env_test.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
diff --git a/tests/with_env.sh.in b/tests/with_env.sh.in
new file mode 100755
index 0000000000..b6c12814e3
--- /dev/null
+++ b/tests/with_env.sh.in
@@ -0,0 +1,7 @@
+#!/usr/bin/env bash
+export ${TEST_VARS}
+source "$TEST_DIR/util.sh"
+
+TEST_SCRIPT="$1"; shift
+cd "$(dirname "$TEST_SCRIPT")"
+source "$(basename "$TEST_SCRIPT")"