perf: reduce allocations in Json.compress

[hargoniX]

1. Remove the need to allocate an intermediate String for literally every character in a JSON String.
2. Use a single String buffer in the entire Json.compress machinery.
3. Use toListAppend

Number 1 is doing most of the lifting in the perf diff, the rest are some minor but measurable improvements.

[hargoniX]

!bench

[leanprover-bot]

Here are the benchmark results for commit 0c983e9.
There were significant changes against commit e04a40d:

  Benchmark         Metric             Change
  =======================================================
- const_fold        task-clock           3.4%    (12.3 σ)
- const_fold        wall-clock           3.3%    (12.1 σ)
+ ilean roundtrip   branch-misses      -18.6%   (-17.0 σ)
+ ilean roundtrip   branches           -25.7% (-2771.6 σ)
+ ilean roundtrip   compress           -29.9%  (-117.7 σ)
+ ilean roundtrip   instructions       -26.3% (-3135.0 σ)
+ ilean roundtrip   maxrss              -3.2%   (-67.7 σ)
+ ilean roundtrip   task-clock         -21.2%   (-57.6 σ)
+ ilean roundtrip   wall-clock         -21.2%   (-57.6 σ)
+ stdlib            tactic execution    -1.3%   (-99.0 σ)

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e04a40ddc1ff598ea91f41b3e0ec62ccd6293a9d --onto 9ce15fb0c61e3a1bee17fd81647ed4d02b4f6c6d. (2024-08-31 22:15:19)

[hargoniX]

!bench

[leanprover-bot]

Here are the benchmark results for commit 601ce86.
There were significant changes against commit e04a40d:

  Benchmark         Metric          Change
  ====================================================
+ binarytrees.st    task-clock       -1.4%   (-10.8 σ)
+ binarytrees.st    wall-clock       -1.4%   (-10.7 σ)
+ ilean roundtrip   branches        -26.8% (-5154.8 σ)
+ ilean roundtrip   compress        -31.4%   (-87.7 σ)
+ ilean roundtrip   instructions    -27.3% (-3574.7 σ)
+ ilean roundtrip   maxrss           -3.2%   (-77.1 σ)
+ ilean roundtrip   task-clock      -22.4%  (-112.0 σ)
+ ilean roundtrip   wall-clock      -22.4%  (-111.3 σ)
+ import Lean       task-clock       -8.7%   (-14.5 σ)
+ import Lean       wall-clock       -8.7%   (-13.2 σ)
- stdlib            type checking     2.0%   (163.4 σ)