From bb5ed7396857c9873a8a329e898b7d19517ce87a Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 23 Oct 2024 01:20:15 -0700 Subject: [PATCH] test: add a benchmark that is slow to elaborate (#5656) Add an example Lean file that includes an unusually large definition that takes a long time to elaborate. It may be that it's difficult to process it more efficiently, but perhaps someone will discover a way to improve it if it's in the benchmark suite. Improved performance on this benchmark will likely make some program analysis and verification tasks within Lean more feasible. --------- Co-authored-by: Sebastian Ullrich --- tests/bench/big_do.lean | 459 +++++++++++++++++++++++ tests/bench/speedcenter.exec.velcom.yaml | 6 + 2 files changed, 465 insertions(+) create mode 100644 tests/bench/big_do.lean diff --git a/tests/bench/big_do.lean b/tests/bench/big_do.lean new file mode 100644 index 000000000000..41319f1aaa66 --- /dev/null +++ b/tests/bench/big_do.lean @@ -0,0 +1,459 @@ +/-! +This benchmark exercises +* general elaboration, likely from many nested lambdas +* code generation, ditto +-/ + +set_option maxRecDepth 10000 + +def addALot (x: Nat) : StateM Nat Nat := do + set x + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + modifyGet (λ y => ((), y + x)) + let y <- get + pure y + +#eval StateT.run' (addALot 2) 0 diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml index ce08a96f6a0d..4282be76702a 100644 --- a/tests/bench/speedcenter.exec.velcom.yaml +++ b/tests/bench/speedcenter.exec.velcom.yaml @@ -362,3 +362,9 @@ run_config: <<: *time cmd: lean bv_decide_inequality.lean +- attributes: + description: big_do + tags: [fast] + run_config: + <<: *time + cmd: lean big_do.lean