chore: fix ci for new test suite (#12704)

.github/workflows/build-template.yml

@@ -234,14 +234,16 @@ jobs:
       - name: Build Stage 2
         run: |
           make -C build -j$NPROC stage2
-        if: matrix.test-speedcenter
+        if: matrix.test-bench
       - name: Check Stage 3
         run: |
           make -C build -j$NPROC check-stage3
         if: matrix.check-stage3
-      - name: Test Speedcenter Benchmarks
-        run: nix shell github:Kha/lakeprof -c make -C build -j$NPROC bench
-        if: matrix.test-speedcenter
+      - name: Test Benchmarks
+        run: |
+          cd tests
+          nix develop -c make -C ../build -j$NPROC bench
+        if: matrix.test-bench
       - name: Check rebootstrap
         run: |
           set -e

.github/workflows/ci.yml

@@ -258,8 +258,8 @@ jobs:
                 "check-rebootstrap": level >= 1,
                 "check-stage3": level >= 2,
                 "test": true,
-                // NOTE: `test-speedcenter` currently seems to be broken on `ubuntu-latest`
-                "test-speedcenter": large && level >= 2,
+                // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`
+                "test-bench": large && level >= 2,
                 // We are not warning-free yet on all platforms, start here
                 "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror",
               },
@@ -269,6 +269,8 @@ jobs:
                 "enabled": level >= 2,
                 "test": true,
                 "CMAKE_PRESET": "reldebug",
+                // * `elab_bench/big_do` crashes with exit code 134
+                "CTEST_OPTIONS": "-E 'elab_bench/big_do'",
               },
               {
                 "name": "Linux fsanitize",

.gitignore

@@ -1,7 +1,6 @@
 *~
 \#*
 .#*
-*.lock
 .lake
 lake-manifest.json
 /build

CMakePresets.json

@@ -41,7 +41,7 @@
         "SMALL_ALLOCATOR": "OFF",
         "USE_MIMALLOC": "OFF",
         "BSYMBOLIC": "OFF",
-        "LEAN_TEST_VARS": "MAIN_STACK_SIZE=16000 LSAN_OPTIONS=max_leaks=10"
+        "LEAN_TEST_VARS": "MAIN_STACK_SIZE=16000 TEST_STACK_SIZE=16000 LSAN_OPTIONS=max_leaks=10"
       },
       "generator": "Unix Makefiles",
       "binaryDir": "${sourceDir}/build/sanitize"

tests/CMakeLists.txt

@@ -2,17 +2,33 @@
 ## Environment ##
 #################
 
-# MSYS2 bash usually handles Windows paths relatively well, but not when putting them in the PATH
-string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")
+# MSYS2 bash usually handles Windows paths relatively well, but not in all situations.
+# Thus, rewrite C:/foo/bar to /C/foo/bar on Windows.
+function(mangle_windows_path OUT PATH)
+  if(WIN32)
+    string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" RESULT "${PATH}")
+    # Replace with return(PROPAGATE) if we ever update to cmake 3.25+
+    set("${OUT}" "${RESULT}" PARENT_SCOPE)
+  else()
+    # Replace with return(PROPAGATE) if we ever update to cmake 3.25+
+    set("${OUT}" "${PATH}" PARENT_SCOPE)
+  endif()
+endfunction()
+
+mangle_windows_path(MANGLED_BINARY_DIR "${CMAKE_BINARY_DIR}")
+mangle_windows_path(MANGLED_SOURCE_DIR "${CMAKE_SOURCE_DIR}")
+mangle_windows_path(MANGLED_CURRENT_SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}")
+
+set(LEAN_BIN "${MANGLED_BINARY_DIR}/bin")
 
 set(TEST_VARS "${LEAN_TEST_VARS}")
 
 # Test scripts can use these to find other parts of the repo, e.g. "$TEST_DIR/measure.py"
 string(APPEND TEST_VARS " STAGE='${STAGE}'") # Using this should not normally be necessary
-string(APPEND TEST_VARS " SRC_DIR='${CMAKE_SOURCE_DIR}'")
-string(APPEND TEST_VARS " TEST_DIR='${CMAKE_CURRENT_SOURCE_DIR}'")
-string(APPEND TEST_VARS " BUILD_DIR='${CMAKE_BINARY_DIR}'")
-string(APPEND TEST_VARS " SCRIPT_DIR='${CMAKE_SOURCE_DIR}/../script'")
+string(APPEND TEST_VARS " SRC_DIR='${MANGLED_SOURCE_DIR}'")
+string(APPEND TEST_VARS " TEST_DIR='${MANGLED_CURRENT_SOURCE_DIR}'")
+string(APPEND TEST_VARS " BUILD_DIR='${MANGLED_BINARY_DIR}'")
+string(APPEND TEST_VARS " SCRIPT_DIR='${MANGLED_SOURCE_DIR}/../script'")
 
 # Use the current stage's lean binary instead of whatever lake thinks we want
 string(APPEND TEST_VARS " PATH='${LEAN_BIN}':\"$PATH\"")
@@ -117,7 +133,12 @@ function(add_test_pile DIR GLOB)
     cmake_path(RELATIVE_PATH FILE_ABS BASE_DIRECTORY "${DIR_ABS}" OUTPUT_VARIABLE FILE_NAME)
 
     if(RUN_TEST_EXISTS AND NOT EXISTS "${FILE_ABS}.no_test")
-      add_test(NAME "${FILE}" WORKING_DIRECTORY "${DIR_ABS}" COMMAND "${RUN_TEST}" "${FILE_NAME}")
+      add_test(
+        NAME "${FILE}"
+        WORKING_DIRECTORY "${DIR_ABS}"
+        # On Windows, we can't call the file directly, hence we always use bash.
+        COMMAND bash "${RUN_TEST}" "${FILE_NAME}"
+      )
     endif()
 
     if(RUN_BENCH_EXISTS AND NOT EXISTS "${FILE_ABS}.no_bench")
@@ -127,7 +148,8 @@ function(add_test_pile DIR GLOB)
         OUTPUT "${MEASUREMENTS_FILE}"
         WORKING_DIRECTORY "${DIR_ABS}"
         COMMAND "${CMAKE_COMMAND}" -E remove -f "${MEASUREMENTS_FILE}"
-        COMMAND "${RUN_BENCH}" "${FILE_NAME}"
+        # On Windows, we can't call the file directly, hence we always use bash.
+        COMMAND bash "${RUN_BENCH}" "${FILE_NAME}"
       )
     endif()
   endforeach()
@@ -152,7 +174,12 @@ function(add_test_dir DIR)
 
   # Add as test
   if(RUN_TEST_EXISTS)
-    add_test(NAME "${DIR}" WORKING_DIRECTORY "${DIR_ABS}" COMMAND "${RUN_TEST}")
+    add_test(
+      NAME "${DIR}"
+      WORKING_DIRECTORY "${DIR_ABS}"
+      # On Windows, we can't call the file directly, hence we always use bash.
+      COMMAND bash "${RUN_TEST}"
+    )
   endif()
 
   # Add as benchmark
@@ -164,7 +191,8 @@ function(add_test_dir DIR)
       OUTPUT "${MEASUREMENTS_FILE}"
       WORKING_DIRECTORY "${DIR_ABS}"
       COMMAND "${CMAKE_COMMAND}" -E remove -f "${MEASUREMENTS_FILE}"
-      COMMAND "${RUN_BENCH}"
+      # On Windows, we can't call the file directly, hence we always use bash.
+      COMMAND bash "${RUN_BENCH}"
     )
   endif()
 endfunction()

tests/README.md

@@ -193,6 +193,7 @@ These files are available to configure a test:
 - `<file>.exit.expected`:
   The test fails if its exit code doesn't match this file's contents.
   If this file isn't present, the pile's default exit code is used instead.
+  If this file contains the text `nonzero`, the test's exit code must not be 0.
 
 These bash variables (set via `<file>.init.sh`) are used by the run script:
 
@@ -234,6 +235,7 @@ These files are available to configure a test:
 - `<file>.exit.expected`:
   The test fails if its exit code doesn't match this file's contents.
   If this file isn't present, the test's exit code must be 0.
+  If this file contains the text `nonzero`, the test's exit code must not be 0.
 
 These bash variables (set via `<file>.init.sh`) are used by the run script:
 

tests/compile/StackOverflow.lean.exit.expected

@@ -1 +1 @@
-134
+nonzero

tests/compile/StackOverflowTask.lean.exit.expected

@@ -1 +1 @@
-134
+nonzero

tests/compile_bench/const_fold.lean.init.sh

@@ -4,4 +4,4 @@ if [[ -n $TEST_BENCH ]]; then
   TEST_ARGS=( 23 )
 fi
 
-ulimit -s unlimited
+set_stack_size_to_maximum

tests/elab/async_systems_info.lean.out.expected

@@ -1 +0,0 @@
-18446744073709551615

tests/elab/handleLocking.lean

@@ -2,7 +2,7 @@
 This test covers the file handle locking functionality in `IO`.
 -/
 
-def testFile := "handleLocking.lock"
+def testFile := "handleLocking.lean.lock"
 
 /-- Test an exclusive lock. -/
 def test1 : IO Unit := do

tests/elab/handleLocking.lean.after.sh

@@ -0,0 +1 @@
+rm -f handleLocking.lean.lock

tests/elab/realPath.lean

@@ -9,6 +9,7 @@ This test will need to be updated once that issue is fixed.
 
 def realPathTest : IO Unit := do
   unless System.Platform.isWindows do
+    IO.println "This test only does something on Windows."
     return
   let dir ← IO.currentDir
   let tmpDir := dir / "tmp_realpath_test_dir"

tests/flake.lock

@@ -0,0 +1,82 @@
+{
+  "nodes": {
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1731533236,
+        "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "lakeprof": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": [
+          "nixpkgs"
+        ]
+      },
+      "locked": {
+        "lastModified": 1769693345,
+        "narHash": "sha256-Q4mH0gbXVqhbnEGISkqhCeLmS83cbz4h9AlkdELAFbk=",
+        "owner": "Kha",
+        "repo": "lakeprof",
+        "rev": "4b79b5554baff187c93054385ecb030e83cc4607",
+        "type": "github"
+      },
+      "original": {
+        "owner": "Kha",
+        "repo": "lakeprof",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1771923393,
+        "narHash": "sha256-Fy0+UXELv9hOE8WjYhJt8fMDLYTU2Dqn3cX4BwoGBos=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "ea7f1f06811ce7fcc81d6c6fd4213150c23edcf2",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixpkgs-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "lakeprof": "lakeprof",
+        "nixpkgs": "nixpkgs"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}

tests/flake.nix

@@ -0,0 +1,27 @@
+{
+  inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
+
+  inputs.lakeprof.url = "github:Kha/lakeprof";
+  inputs.lakeprof.inputs.nixpkgs.follows = "nixpkgs";
+
+  outputs =
+    inputs:
+    let
+      lib = inputs.nixpkgs.lib;
+      forAllSystems = lib.genAttrs lib.systems.flakeExposed;
+    in
+    {
+      devShells = forAllSystems (
+        system:
+        let
+          pkgs = inputs.nixpkgs.legacyPackages.${system};
+          lakeprof = inputs.lakeprof.packages.${system}.lakeprof;
+        in
+        {
+          default = pkgs.mkShellNoCC {
+            packages = [ lakeprof ] ++ lib.optional pkgs.stdenv.isLinux pkgs.perf;
+          };
+        }
+      );
+    };
+}

tests/misc/lint.sh

@@ -1 +1 @@
-"$TEST_DIR/lint.py"
+python "$TEST_DIR/lint.py"

tests/util.sh

@@ -1,6 +1,7 @@
 set -eu
 
-DIFF="diff -u --color=always"
+DIFF="diff -au --strip-trailing-cr --color=always"
+ulimit -S -s ${TEST_STACK_SIZE:-8192}
 
 function fail {
   echo "$1"
@@ -40,9 +41,19 @@ function exec_capture {
 
 function check_exit {
   if [[ -f "$1.exit.expected" ]]; then
-    $DIFF -- "$1.exit.expected" "$1.exit.produced" || fail "$1: Unexpected exit code"
+    EXPECTED="$(< "$1.exit.expected")"
   else
-    echo "${2:-0}" | $DIFF -- - "$1.exit.produced" || fail "$1: Unexpected exit code"
+    EXPECTED="${2:-0}"
+  fi
+
+  ACTUAL="$(< "$1.exit.produced")"
+
+  if [[ "$EXPECTED" == "nonzero" ]]; then
+    if [[ "$ACTUAL" == "0" ]]; then
+      fail "$1: Expected nonzero exit code, got 0"
+    fi
+  elif [[ "$EXPECTED" != "$ACTUAL" ]]; then
+    fail "$1: Expected exit code $EXPECTED, got $ACTUAL"
   fi
 }
 
@@ -58,16 +69,18 @@ function check_out {
 
 # mvar suffixes like in `?m.123` are deterministic but prone to change on minor changes, so strip them
 function normalize_mvar_suffixes {
-  sed -i -E 's/(\?(\w|_\w+))\.[0-9]+/\1/g' "$1.out.produced"
+  # Sed on macOS does not support \w.
+  perl -p -i -e 's/(\?(\w|_\w+))\.[0-9]+/\1/g' "$1.out.produced"
 }
 
 # similarly, links to the language reference may have URL components depending on the toolchain, so normalize those
 function normalize_reference_urls {
-  sed -i -E 's#https://lean-lang\.org/doc/reference/(v?[0-9.]+(-rc[0-9]+)?|latest)#REFERENCE#g' "$1.out.produced"
+  perl -p -i -e 's#https://lean-lang\.org/doc/reference/(v?[0-9.]+(-rc[0-9]+)?|latest)#REFERENCE#g' "$1.out.produced"
 }
 
 function normalize_measurements {
-  sed -i -E 's/^measurement: (\S+) \S+( \S+)?$/measurement: \1 .../' "$1.out.produced"
+  # Sed on macOS does not support \S.
+  perl -p -i -e 's/^measurement: (\S+) \S+( \S+)?$/measurement: \1 .../' "$1.out.produced"
 }
 
 function extract_measurements {
@@ -77,3 +90,10 @@ function extract_measurements {
 
   normalize_measurements "$1"
 }
+
+function set_stack_size_to_maximum {
+  # On macOS, `ulimit -s unlimited` fails with `Operation not permitted` because
+  # the hard limit is a certain number, not `unlimited` like on Linux.
+  echo "Setting stack size to $(ulimit -H -s)"
+  ulimit -s "$(ulimit -H -s)"
+}