)]}'
{
  "commit": "a3d2ef4333746d00cd5360be8d9262e2eff5d318",
  "tree": "e7926d1f31986dc9e23b500db6f93ca82c7eb5f1",
  "parents": [
    "963b1e4a7bd00a3f606edae8d1244c3439eadf00"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sun Sep 20 06:07:36 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sun Sep 20 06:07:36 2026 +0000"
  },
  "message": "perf: make environment extension replay proportional to the number of new entries\n\nThis PR makes the cost of realizing a constant (e.g. the equation lemmas needed by `simp only [f]`) independent of the size of the current file. Previously, files with many such realizations slowed down quadratically: on a file with 4,000 definition/theorem pairs elaboration time drops from 99 s to 32 s, and the time per pair is now constant.\n\nEvery `realizeConst` replays the extension changes it made onto the kernel environment, and all replays of a file run serially on the `checked` task chain. Several `replay?` implementations computed the new entries with `newState.take (newState.length - oldState.length)`, which walks all entries the extension accumulated in the file, and `LCNF.PhaseExt.replayFn` folded over the whole map of compiled declarations. The new `takeNewEntriesRev`/`takeNewEntries` helpers find the old list inside the new one by pointer equality, since entries are only ever consed onto it, and fall back to the length computation otherwise. `AbstractDeclExtState` now also records its keys in insertion order so the LCNF declaration and signature extensions replay only the new keys.\n\nThe new benchmark `tests/elab_bench/realizations.lean` measures this scenario.\n\nCo-Authored-By: Claude Fable 5.1 \u003cnoreply@anthropic.com\u003e\nClaude-Session: https://claude.ai/code/session_01QvNV36NuY94c36fRECjLFK\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "20b7acf5d684789ab52b81dda7def4b19568213c",
      "old_mode": 33188,
      "old_path": "src/Lean/Compiler/ClosedTermCache.lean",
      "new_id": "4bd9ab78a0de5c2e49915b6dbec9f2ea063ed7a5",
      "new_mode": 33188,
      "new_path": "src/Lean/Compiler/ClosedTermCache.lean"
    },
    {
      "type": "modify",
      "old_id": "5149b8060c01dbd9721ee36ead44c9cde16a8bef",
      "old_mode": 33188,
      "old_path": "src/Lean/Compiler/LCNF/CompilerM.lean",
      "new_id": "cc667d5237f25125f5e519da29a3871a869b11e6",
      "new_mode": 33188,
      "new_path": "src/Lean/Compiler/LCNF/CompilerM.lean"
    },
    {
      "type": "modify",
      "old_id": "1c0e61d8124bf88bb531439297ccee0b62f01065",
      "old_mode": 33188,
      "old_path": "src/Lean/Compiler/LCNF/PhaseExt.lean",
      "new_id": "d6ecce2213aae602be50bab2a3405ac148324225",
      "new_mode": 33188,
      "new_path": "src/Lean/Compiler/LCNF/PhaseExt.lean"
    },
    {
      "type": "modify",
      "old_id": "21a9cf775db6d0167bba79c6a68f59638f802271",
      "old_mode": 33188,
      "old_path": "src/Lean/Compiler/LCNF/PublicDeclsExt.lean",
      "new_id": "8089a83471326a4d552de5dbdf01799e6cd40cb1",
      "new_mode": 33188,
      "new_path": "src/Lean/Compiler/LCNF/PublicDeclsExt.lean"
    },
    {
      "type": "modify",
      "old_id": "47a902b161077a4b841c70d4c727f890f015b493",
      "old_mode": 33188,
      "old_path": "src/Lean/Compiler/LCNF/Simp/ConstantFold.lean",
      "new_id": "4dbe935ca5a9decdd879a5cc87eb0c5577924a60",
      "new_mode": 33188,
      "new_path": "src/Lean/Compiler/LCNF/Simp/ConstantFold.lean"
    },
    {
      "type": "modify",
      "old_id": "8a4553ccb6158850ca6d9e8653961e6cf94c0274",
      "old_mode": 33188,
      "old_path": "src/Lean/Compiler/LCNF/SimpleGroundExpr.lean",
      "new_id": "a95ccc629700919f0084e1ea194e3d7055ecea6a",
      "new_mode": 33188,
      "new_path": "src/Lean/Compiler/LCNF/SimpleGroundExpr.lean"
    },
    {
      "type": "modify",
      "old_id": "83589454bbd212c94013da577abee963e2604846",
      "old_mode": 33188,
      "old_path": "src/Lean/EnvExtension.lean",
      "new_id": "2be29e634ba290d10000319c1894ecf05daed264",
      "new_mode": 33188,
      "new_path": "src/Lean/EnvExtension.lean"
    },
    {
      "type": "modify",
      "old_id": "ee36b8e4fc921db8f1b3e4cfb5045f49fb008c07",
      "old_mode": 33188,
      "old_path": "src/Lean/Environment.lean",
      "new_id": "9cb291f1b63112c70b6dec23893cc1bd9f504b91",
      "new_mode": 33188,
      "new_path": "src/Lean/Environment.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "d7aa9998921e252b7091b50ccdd32e4eb86cecee",
      "new_mode": 33188,
      "new_path": "tests/elab_bench/realizations.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "771dfd9807452986caabd6147f49c81eb7e630ff",
      "new_mode": 33188,
      "new_path": "tests/elab_bench/realizations.lean.out.expected"
    }
  ]
}