From 4f5054424283f5d185f8103dac66f4d3e91118fa Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 17 Apr 2024 20:10:32 +0200 Subject: [PATCH] chore: Nat.repr microbenchmark (#3888) --- tests/bench/nat_repr.lean | 8 ++++++++ tests/bench/nat_repr.lean.args | 1 + tests/bench/nat_repr.lean.expected.out | 1 + tests/bench/speedcenter.exec.velcom.yaml | 8 ++++++++ 4 files changed, 18 insertions(+) create mode 100644 tests/bench/nat_repr.lean create mode 100644 tests/bench/nat_repr.lean.args create mode 100644 tests/bench/nat_repr.lean.expected.out diff --git a/tests/bench/nat_repr.lean b/tests/bench/nat_repr.lean new file mode 100644 index 0000000000..76c2dabb3d --- /dev/null +++ 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 new file mode 100644 index 0000000000..e9c02dad18 --- /dev/null +++ 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 new file mode 100644 index 0000000000..4345f9e626 --- /dev/null +++ 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 index 6855d1131d..247a4f8689 100644 --- 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]