experiment: remove #align and benchmark

[semorrison]

Not a proposal to actually do this, rather for comparison with the benchmarking results at #8199

---

[semorrison]

!bench

[leanprover-bot]

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

[semorrison]

!bench

[leanprover-bot]

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

[semorrison]

!bench

[leanprover-bot]

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

[semorrison]

!bench

[leanprover-bot]

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

[semorrison]

!bench

[leanprover-bot]

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

[semorrison]

!bench

[leanprover-bot]

Here are the benchmark results for commit 58b94ba.
There were significant changes against commit ce4b7e4:

  Benchmark      Metric           Change
  ======================================
+ build          interpretation   -18.1%
+ open Mathlib   instructions     -24.2%
+ open Mathlib   wall-clock       -13.8%
+ size           .lean            -10.1%