chore: add import Lean (cold) benchmark

Author: Kha

tests/measure.py

@@ -1,6 +1,7 @@
 #!/usr/bin/env python3
 
 import argparse
+import glob
 import json
 import os
 import resource
@@ -155,17 +156,38 @@ def get_rusage_result(rusage: resource.struct_rusage, metric: str) -> Result:
     return Result(category=metric, value=value, unit=info.unit)
 
 
+def evict_caches(patterns: list[str]) -> None:
+    evicted = False
+    for pattern in patterns:
+        for path in glob.glob(pattern, recursive=True):
+            try:
+                fd = os.open(path, os.O_RDONLY)
+            except OSError:
+                continue
+            try:
+                os.posix_fadvise(fd, 0, 0, os.POSIX_FADV_DONTNEED)
+                evicted = True
+            finally:
+                os.close(fd)
+    if patterns and not evicted:
+        print(f"warning: --evict matched no files: {patterns}", file=sys.stderr)
+
+
 def main(
     cmd: list[str],
     output: Path,
     topics: list[str],
     metrics: set[str],
     append: bool = True,
     capture: bool = False,
+    evict: list[str] | None = None,
 ) -> tuple[str, str]:
     perf_metrics, rusage_metrics = resolve_metrics(metrics)
     perf_events = {PERF_METRICS[metric].event for metric in perf_metrics}
 
+    if evict:
+        evict_caches(evict)
+
     measured = measure_perf(cmd, perf_events, capture=capture)
     perf = measured.perf
     rusage = resource.getrusage(resource.RUSAGE_CHILDREN)
@@ -191,6 +213,7 @@ class Args(Namespace):
     default_metrics: bool
     output: Path
     append: bool
+    evict: list[str]
     cmd: str
     args: list[str]
 
@@ -233,6 +256,13 @@ class Args(Namespace):
         action="store_true",
         help="append to the output file instead of overwriting it",
     )
+    parser.add_argument(
+        "--evict",
+        action="append",
+        default=[],
+        metavar="GLOB",
+        help="drop files matching GLOB from the page cache before measuring, for a cold-cache run. Repeatable.",
+    )
     parser.add_argument(
         "cmd",
         help="command to measure the resource usage of",
@@ -255,4 +285,5 @@ class Args(Namespace):
         topics=args.topic,
         metrics=metrics,
         append=args.append,
+        evict=args.evict,
     )

tests/misc_bench/import Lean (cold).sh

@@ -0,0 +1,4 @@
+cd ../../src
+# Like `import Lean`, but with `--evict`
+"$TEST_DIR/measure.py" -t "$TOPIC" -d -o "$OUT" --evict "$BUILD_DIR/lib/lean/**/*" -- \
+  lean --setup="$BUILD_DIR/lib/temp/Lean.setup.json" Lean.lean