#!/usr/bin/env bash
set -euxo pipefail

"$BENCH_DIR/repeatedly.py" -n 5 -o "$OUTPUT_FILE" -- \
  "$BENCH_DIR/measure.py" -t open-mathlib -d -a -o "$OUTPUT_FILE" -- \
  lake lean Mathlib.lean
