chore: Nat.repr microbenchmark (#3888)
This commit is contained in:
parent
627a0f308b
commit
4f50544242
4 changed files with 18 additions and 0 deletions
8
tests/bench/nat_repr.lean
Normal file
8
tests/bench/nat_repr.lean
Normal file
|
|
@ -0,0 +1,8 @@
|
|||
def main : List String → IO Unit
|
||||
| [n] => do
|
||||
let mut s := 0
|
||||
for i in [0:n.toNat!] do
|
||||
for j in [:i] do
|
||||
s := s + j.repr.length
|
||||
IO.println s
|
||||
| _ => throw $ IO.userError "give upper bound"
|
||||
1
tests/bench/nat_repr.lean.args
Normal file
1
tests/bench/nat_repr.lean.args
Normal file
|
|
@ -0,0 +1 @@
|
|||
5000
|
||||
1
tests/bench/nat_repr.lean.expected.out
Normal file
1
tests/bench/nat_repr.lean.expected.out
Normal file
|
|
@ -0,0 +1 @@
|
|||
44945605
|
||||
|
|
@ -302,6 +302,14 @@
|
|||
run_config:
|
||||
<<: *time
|
||||
cmd: lean reduceMatch.lean
|
||||
- attributes:
|
||||
description: nat_repr
|
||||
tags: [fast, suite]
|
||||
run_config:
|
||||
<<: *time
|
||||
cmd: ./nat_repr.lean.out 5000
|
||||
build_config:
|
||||
cmd: ./compile.sh nat_repr.lean
|
||||
- attributes:
|
||||
description: unionfind
|
||||
tags: [fast, suite]
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue