perf: avoid per-command array copies in the frontend
This PR fixes a per-command overhead in the frontend that grew linearly with the position of the command in the file, making files with many commands quadratic.
The state threaded through the per-command loop of the frontend contains two arrays that receive one entry per command: the code quality entries of the linters (#14914) and the list of commands for the module linters (#13917). The state is captured by the tasks spawned for each command, so an older version of each array is still referenced when the next command pushes, and the push copies the whole array. Both arrays are now `PersistentArray`s, whose push shares structure with the previous version instead of copying it.
The new benchmark `tests/elab_bench/many_commands.lean` elaborates 16,000 and 32,000 generated trivial theorems with the options of the command line driver. The time for 32,000 commands should stay at about twice the time for 16,000. Measured with
TEST_BENCH=1 tests/with_stage1_bench_env.sh tests/elab_bench/run_bench.sh many_commands.lean
before this change:
measurement: cmds_16000 18.911000 s
measurement: cmds_32000 60.130000 s
and after:
measurement: cmds_16000 11.660000 s
measurement: cmds_32000 23.801000 s
| Commands | Before | After | Speedup |
|---|---|---|---|
| 16,000 | 18.9 s | 11.7 s | 1.6x |
| 32,000 | 60.1 s | 23.8 s | 2.5x |
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.