chore: add import Lean (cold) benchmark (#14121)

Co-authored-by: Joscha <joscha@plugh.de>

Author: Kha

tests/evict.py

@@ -0,0 +1,34 @@
+#!/usr/bin/env python3
+
+import argparse
+import glob
+import os
+import sys
+
+
+def evict(patterns: list[str]) -> None:
+    evicted = 0
+    for pattern in patterns:
+        for path in glob.glob(pattern, recursive=True):
+            if not os.path.isfile(path):
+                continue
+            fd = os.open(path, os.O_RDONLY)
+            try:
+                os.posix_fadvise(fd, 0, 0, os.POSIX_FADV_DONTNEED)
+            finally:
+                os.close(fd)
+            evicted += 1
+    if evicted == 0:
+        sys.exit(f"error: evicted no files, globs matched nothing: {patterns}")
+
+
+if __name__ == "__main__":
+    parser = argparse.ArgumentParser(description="Evict files from the page cache.")
+    parser.add_argument(
+        "globs",
+        nargs="+",
+        metavar="GLOB",
+        help="glob patterns to evict (`**` is recursive)",
+    )
+    args = parser.parse_args()
+    evict(args.globs)

tests/misc_bench/import Lean cold.sh

@@ -0,0 +1,5 @@
+cd ../../src
+# Like `import Lean`, but drop the built library files from the page cache first for a cold-cache run.
+"$TEST_DIR/evict.py" "$BUILD_DIR/lib/lean/**/*"
+"$TEST_DIR/measure.py" -t "$TOPIC" -d -o "$OUT" -- \
+  lean --setup="$BUILD_DIR/lib/temp/Lean.setup.json" Lean.lean