)]}'
{
  "commit": "a70727a255fa42d5ebbd3d8a57312c6b20c76d3b",
  "tree": "558625c5bebd90fb688a82dd1bf83b3ceeccaa54",
  "parents": [
    "b318ba539353a8653bc7465e5f3f3229ab7758d2"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sat Sep 19 20:07:11 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sat Sep 19 20:07:11 2026 +0000"
  },
  "message": "perf: avoid per-command array copies in the frontend\n\nThis 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.\n\nThe 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.\n\nThe 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\n\n    TEST_BENCH\u003d1 tests/with_stage1_bench_env.sh tests/elab_bench/run_bench.sh many_commands.lean\n\nbefore this change:\n\n    measurement: cmds_16000 18.911000 s\n    measurement: cmds_32000 60.130000 s\n\nand after:\n\n    measurement: cmds_16000 11.660000 s\n    measurement: cmds_32000 23.801000 s\n\n| Commands | Before | After | Speedup |\n|---|---|---|---|\n| 16,000 | 18.9 s | 11.7 s | 1.6x |\n| 32,000 | 60.1 s | 23.8 s | 2.5x |\n\nCo-Authored-By: Claude Fable 5.1 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "d1bb776105eda72d35b591e5fa781eedc8939224",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Command.lean",
      "new_id": "3964d8f751ed13409146cf92b39690dc35890536",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Command.lean"
    },
    {
      "type": "modify",
      "old_id": "8ec4fec2088b6910a05dc44894e33dd606761333",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Frontend.lean",
      "new_id": "54b7ea5e49733b3330203b891bd19b829531d9c4",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Frontend.lean"
    },
    {
      "type": "modify",
      "old_id": "d5bdd00f7821327940d49248e38c24b37af06e1c",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/GuardMsgs.lean",
      "new_id": "0896af430116a13b0e5060bb25c42bdbb48234f2",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/GuardMsgs.lean"
    },
    {
      "type": "modify",
      "old_id": "889378c986c99f6b1a9eee32f86de09e5e648588",
      "old_mode": 33188,
      "old_path": "src/Lean/Language/Lean.lean",
      "new_id": "d593f6562c480fd986974ffbc31c8f25374c79ab",
      "new_mode": 33188,
      "new_path": "src/Lean/Language/Lean.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "274c35a395b83ee3b380eaa656c82dd105a50f14",
      "new_mode": 33188,
      "new_path": "tests/elab_bench/many_commands.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "0bec1774765a74b92dd6923b1f137375476b2172",
      "new_mode": 33188,
      "new_path": "tests/elab_bench/many_commands.lean.out.expected"
    },
    {
      "type": "modify",
      "old_id": "aefb905753fc27283784757bb94562188a4ad4a5",
      "old_mode": 33188,
      "old_path": "tests/pkg/code_quality_log/CQTest/Linters.lean",
      "new_id": "e71fbcbe39c3d1c6a0a58fead9c179690bd7bca1",
      "new_mode": 33188,
      "new_path": "tests/pkg/code_quality_log/CQTest/Linters.lean"
    }
  ]
}