chore: Nat.repr microbenchmark (#3888)

leanprover · Apr 17, 2024 · 4f50544 · 4f50544
1 parent 627a0f3
commit 4f50544
Show file tree

Hide file tree

Showing 4 changed files with 18 additions and 0 deletions.
diff --git a/tests/bench/nat_repr.lean b/tests/bench/nat_repr.lean
@@ -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"
diff --git a/tests/bench/nat_repr.lean.args b/tests/bench/nat_repr.lean.args
@@ -0,0 +1 @@
+5000
diff --git a/tests/bench/nat_repr.lean.expected.out b/tests/bench/nat_repr.lean.expected.out
@@ -0,0 +1 @@
+44945605
diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml
@@ -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]