From 01a05247498461e265805d6c8dda71d09d4a2f3a Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 11 Jun 2025 14:27:06 +0200
Subject: [PATCH] chore: move benchmarking script to this repo (#8718)

Corresponding to
https://github.com/Kha/lean-bench/commit/d3f39f8343e0df237ad5c91ecdfd5168ae0fbc64
---
 script/bench.sh | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100755 script/bench.sh

diff --git a/script/bench.sh b/script/bench.sh
new file mode 100755
index 0000000000..99adffa6b0
--- /dev/null
+++ b/script/bench.sh
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+# We benchmark against stage 2 to test new optimizations.
+timeout -s KILL 1h time bash -c 'mkdir -p build/release; cd build/release; cmake ../.. && make -j$(nproc) stage2' 1>&2
+export PATH=$PWD/build/release/stage2/bin:$PATH
+cd tests/bench
+timeout -s KILL 1h time temci exec --config speedcenter.yaml --in speedcenter.exec.velcom.yaml 1>&2
+temci report run_output.yaml --reporter codespeed2