Skip to content

Commit 9486421

Browse files
authored
chore: tame some slow benchmarks (#8352)
No single-topic benchmark should take half as long as stdlib. Bench run time reduced from 27min to 21min.
1 parent d69a8ef commit 9486421

File tree

2 files changed

+7
-2
lines changed

2 files changed

+7
-2
lines changed

tests/bench/channel.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ Note that we will stick exclusively to the sync interface for this as there is n
2121
reaped from async in this benchmark so we might as well just block.
2222
-/
2323

24-
def MESSAGES : Nat := 1_000_000
24+
def MESSAGES : Nat := 100_000
2525
def THREADS : Nat := 4
2626

2727
def seq (ch : Std.CloseableChannel.Sync Nat) (amount : Nat) : IO Unit := do

tests/bench/speedcenter.exec.velcom.yaml

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -145,7 +145,7 @@
145145
lean --run ${f%.args} $(cat $f)
146146
done
147147
'
148-
max_runs: 5
148+
max_runs: 2
149149
- attributes:
150150
description: binarytrees
151151
tags: [fast, suite]
@@ -191,6 +191,7 @@
191191
lake -flakefile-clean.lean clean
192192
lake -flakefile-clean.lean build
193193
"
194+
max_runs: 2
194195
build_config:
195196
cmd: |
196197
bash -c "
@@ -412,6 +413,7 @@
412413
run_config:
413414
<<: *time
414415
cmd: lean workspaceSymbols.lean
416+
max_runs: 2
415417
- attributes:
416418
description: bv_decide_realworld
417419
tags: [fast]
@@ -430,12 +432,14 @@
430432
run_config:
431433
<<: *time
432434
cmd: lean bv_decide_mod.lean
435+
max_runs: 2
433436
- attributes:
434437
description: bv_decide_inequality.lean
435438
tags: [fast]
436439
run_config:
437440
<<: *time
438441
cmd: lean bv_decide_inequality.lean
442+
max_runs: 2
439443
- attributes:
440444
description: bv_decide_large_aig.lean
441445
tags: [fast]
@@ -481,3 +485,4 @@
481485
run_config:
482486
<<: *time
483487
cmd: lean riscv-ast.lean
488+
max_runs: 2

0 commit comments

Comments
 (0)