tree 558625c5bebd90fb688a82dd1bf83b3ceeccaa54
parent b318ba539353a8653bc7465e5f3f3229ab7758d2
author Leonardo de Moura <leomoura@amazon.com> 1789848431 +0000
committer Leonardo de Moura <leomoura@amazon.com> 1789848431 +0000

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>