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.

Author: Garmelon

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: