From ca23ed0c171b583dd797158ec1e7510391daa1fa Mon Sep 17 00:00:00 2001 From: Garmelon Date: Mon, 1 Dec 2025 17:20:34 +0100 Subject: [PATCH] chore: fix "tests/compiler//sum binary sizes" benchmark (#11444) The bench script expected no output on stdout from `compile.sh`, which was not always the case. Now, it separates the compilation and size measurement steps. --- tests/bench/speedcenter.exec.velcom.yaml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml index 9048954141..564633306e 100644 --- a/tests/bench/speedcenter.exec.velcom.yaml +++ b/tests/bench/speedcenter.exec.velcom.yaml @@ -98,8 +98,9 @@ cwd: ../compiler/ cmd: | set -eu + for f in *.lean; do ../bench/compile.sh $f > /dev/null; done printf 'sum binary sizes: ' - for f in *.lean; do ../bench/compile.sh $f; printf '%s\0' "$f.out"; done | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1 + for f in *.lean; do printf '%s\0' "$f.out"; done | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1 max_runs: 1 runner: output - attributes: