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