Update run_test and run_bench scripts

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

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

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"
 
 
 

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.

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

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

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

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

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

tests/compile_bench/run_test

@@ -1 +0,0 @@
-../compile/run_test

tests/compile_bench/run_test.sh

@@ -0,0 +1 @@
+../compile/run_test.sh

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

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

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)"

tests/elab_bench/run_test

@@ -1 +0,0 @@
-../elab/run_test

tests/elab_bench/run_test.sh

@@ -0,0 +1 @@
+../elab/run_test.sh

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

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
 

tests/misc/run_test.sh

@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../env_test.sh
-
 NAME="$1"
 FILE="$(realpath "$1")"
 source "$1"

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"

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

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

tests/pkg/builtin_attr/run_test

@@ -1,5 +0,0 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
-rm -rf .lake/build
-lake build

tests/pkg/builtin_attr/run_test.sh

@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build

tests/pkg/cbv_attr/run_test

@@ -1,5 +0,0 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
-rm -rf .lake/build
-lake build

tests/pkg/cbv_attr/run_test.sh

@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build

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

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.
 

tests/pkg/deriving/run_test

@@ -1,5 +0,0 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
-rm -rf .lake/build
-lake build

tests/pkg/deriving/run_test.sh

@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build

tests/pkg/frontend/run_test.sh

@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
 rm -rf .lake/build
 lake build
 

tests/pkg/initialize/run_test

@@ -1,5 +0,0 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
-rm -rf .lake/build
-lake build

tests/pkg/initialize/run_test.sh

@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build

tests/pkg/leanchecker/run_test.sh

@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
 rm -rf .lake/build
 lake build
 

tests/pkg/linter_set/run_test

@@ -1,5 +0,0 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
-rm -rf .lake/build
-lake build

tests/pkg/linter_set/run_test.sh

@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build

tests/pkg/misc/run_test

@@ -1,5 +0,0 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
-rm -rf .lake/build
-lake build

tests/pkg/misc/run_test.sh

@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build

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

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
 

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

tests/pkg/prv/run_test

@@ -1,5 +0,0 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
-rm -rf .lake/build
-lake build

tests/pkg/prv/run_test.sh

@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build

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

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

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
 

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

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.

tests/pkg/user_attr/run_test

@@ -1,5 +0,0 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
-rm -rf .lake/build
-lake build

tests/pkg/user_attr/run_test.sh

@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build

tests/pkg/user_attr_app/run_test

@@ -1,5 +0,0 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
-rm -rf .lake/build
-lake exe user_attr

tests/pkg/user_attr_app/run_test.sh

@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake exe user_attr

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

tests/pkg/user_opt/run_test

@@ -1,5 +0,0 @@
-#!/usr/bin/env bash
-source ../../env_test.sh
-
-rm -rf .lake/build
-lake build

tests/pkg/user_opt/run_test.sh

@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build

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

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:
 #

tests/server/run_test.sh

@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../env_test.sh
-
 run_before "$1"
 
 capture_only "$1" \

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