perf: faster Nat.repr implementation in C

[nomeata]

Nat.repr was implemented by generating a list of Chars, each created by a 10-way if-then-else. This can cause significant slow down in some particular use cases.

Now Nat.repr is implemented_by a faster implementation that uses C++’s std::to_string on small numbers (< USize.size) and maintains an array of pre-allocated strings for the first 128 numbers.

The handling of big numbers (≥ USize.size) remains as before.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❌ Mathlib branch lean-pr-testing-3876 built against this PR, but linting failed. (2024-04-10 22:24:17) View Log
• ❌ Mathlib branch lean-pr-testing-3876 built against this PR, but linting failed. (2024-04-10 22:44:08) View Log
• ✅ Mathlib branch lean-pr-testing-3876 has successfully built against this PR. (2024-04-11 07:15:58) View Log
• ✅ Mathlib branch lean-pr-testing-3876 has successfully built against this PR. (2024-04-11 07:58:01) View Log
• ✅ Mathlib branch lean-pr-testing-3876 has successfully built against this PR. (2024-04-11 15:36:22) View Log
• ✅ Mathlib branch lean-pr-testing-3876 has successfully built against this PR. (2024-04-11 23:22:44) View Log
• 🟡 Mathlib branch lean-pr-testing-3876 build this PR didn't complete normally. (2024-04-12 10:13:39) View Log
• ✅ Mathlib branch lean-pr-testing-3876 has successfully built against this PR. (2024-04-12 12:56:24) View Log
• ✅ Mathlib branch lean-pr-testing-3876 has successfully built against this PR. (2024-04-12 15:43:39) View Log
• ✅ Mathlib branch lean-pr-testing-3876 has successfully built against this PR. (2024-04-12 16:59:12) View Log
• ✅ Mathlib branch lean-pr-testing-3876 has successfully built against this PR. (2024-04-12 21:06:58) View Log
• ✅ Mathlib branch lean-pr-testing-3876 has successfully built against this PR. (2024-04-12 23:02:43) View Log

[nomeata]

!bench

[leanprover-bot]

Here are the benchmark results for commit 76c6249d7ad13b2a11bb45961d89d6e33e1a9681. There were no significant changes against commit 892bfe2c5fdd964405d94f0adb0e178fe2b485af.

[nomeata]

!bench

[nomeata]

!bench

[leanprover-bot]

Here are the benchmark results for commit 99cbe00ed3bc95ab59a81d839442cb9bf2a47e51. There were significant changes against commit 892bfe2c5fdd964405d94f0adb0e178fe2b485af:

  Benchmark                  Metric         Change
  ============================================================
- tests/bench/ interpreted   instructions    80.9% (19859.8 σ)
- tests/bench/ interpreted   task-clock      35.0%    (27.2 σ)
- tests/bench/ interpreted   wall-clock      56.3%    (30.7 σ)

[leanprover-bot]

Here are the benchmark results for commit 3e32e3585d23cff61e14d896aee82e375f43e9c5. There were significant changes against commit 892bfe2c5fdd964405d94f0adb0e178fe2b485af:

  Benchmark                  Metric             Change
  ===============================================================
+ stdlib                     tactic execution    -3.5%  (-37.5 σ)
+ stdlib                     type checking       -1.9%  (-31.0 σ)
- tests/bench/ interpreted   instructions        62.4% (1872.7 σ)
- tests/bench/ interpreted   task-clock          26.9%   (20.1 σ)
- tests/bench/ interpreted   wall-clock          43.8%   (37.3 σ)

[nomeata]

!bench

[leanprover-bot]

Here are the benchmark results for commit 199c811f1472627722c40c390a80ef7c687a3242. The entire run failed. Found no significant differences.

[nomeata]

!bench

[leanprover-bot]

Here are the benchmark results for commit d116a9a6410da2b800807ffff600e054ef0fcef5. There were significant changes against commit 892bfe2c5fdd964405d94f0adb0e178fe2b485af:

  Benchmark                  Metric          Change
  =============================================================
+ stdlib                     type checking    -1.4%  (-457.7 σ)
- tests/bench/ interpreted   instructions     62.3% (38683.5 σ)
- tests/bench/ interpreted   task-clock       25.3%    (37.9 σ)
- tests/bench/ interpreted   wall-clock       41.1%    (38.6 σ)

[nomeata]

!bench

[nomeata]

!bench

[nomeata]

!bench

[leanprover-bot]

Here are the benchmark results for commit 57cf9ae6e5babeeca4e57e88cd1f78b1d9d1dd9a. The entire run failed. Found no significant differences.

[leanprover-bot]

Here are the benchmark results for commit 32adde56d1035e97153a1533107dff803a60e65d.Found no runs to compare against.

[nomeata]

!bench

[leanprover-bot]

Here are the benchmark results for commit ed05fb09f210a09327ca31768702d68f68577683. There were significant changes against commit b0183a64d0b41a75ce5abfabe039de8c1d57f3d1:

  Benchmark                  Metric          Change
  ==============================================================
+ nat_repr                   branch-misses    -8.3%    (-10.2 σ)
+ nat_repr                   branches        -69.7% (-81916.4 σ)
+ nat_repr                   instructions    -70.8% (-70325.4 σ)
+ nat_repr                   task-clock      -63.8%    (-62.5 σ)
+ nat_repr                   wall-clock      -63.8%    (-62.3 σ)
+ stdlib                     task-clock       -1.1%    (-22.0 σ)
+ tests/bench/ interpreted   instructions     -3.7%  (-2746.6 σ)

[nomeata]

Impact on mathlib: http://speed.lean-fro.org/mathlib4/compare/a93fa055-e732-498b-8c1f-fd5ab4f48b05/to/4457e6c3-ba82-4273-b390-de8345e68c5f

[nomeata]

Don't know. Is that something we should look at now, or when it seems to become a problem?

[hargoniX]

The latter I think, it would only be an issue if we end up improving this even more.