)]}'
{
  "commit": "a8846d138ada08c1bc0d7a92ec2b05521a4aa671",
  "tree": "760e1ff547ea18cdb3a446b143e289bbf645c2d8",
  "parents": [
    "ba9237e196e4f6fa353c605230d81b7d9582d49f"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sat Oct 31 04:14:59 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sat Oct 31 04:14:59 2026 +0000"
  },
  "message": "perf: avoid instantiating `grind` proofs at every case split\n\nThis PR speeds up `grind` on goals with many nested case splits. Building the proof of a case split no longer traverses the proofs of the case splits below it.\n\n`grind`\u0027s own time compared to master:\n* `tests/elab_bench/lia_case_splits.lean`: 3.6 s → 1.6 s.\n* `lia` on a sum of 13 terms `if cᵢ then xᵢ else 0`: 8.9 s → 3.7 s.\n* `grind` on `x \u003d 0 ∨ … ∨ x \u003d 999` with `1010 ≤ x`: 180 s → 23 s.\n\nEach case split instantiated its proof, whose delayed assignments are not cached, so every enclosing case split traversed the whole subproof again. Now `getProofInfo` summarizes a proof without instantiating it: its free variables, whether it contains a synthetic `sorry`, and whether it contains an unassigned metavariable of `grind`\u0027s depth (e.g., an open subgoal after an interactive `cases_next`). Complete summaries are cached per metavariable. `getFalseProof?` and `mkHoistedDecls` use it instead of instantiating, and `mkHoistedDecls` abstracts the hoisted declarations with a delayed assignment, as `intro` does.\n\nNon-chronological backtracking now also applies when the goal contains metavariables created before `grind`, whose delayed assignments `instantiateMVars` does not resolve.\n\nCo-Authored-By: Claude Opus 5.5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "94153cdab4dcff9592710f7b7b73f1797a4bb0a2",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Split.lean",
      "new_id": "082cb0cdcd9009cb998a333518e9d2478fe671ca",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Split.lean"
    },
    {
      "type": "modify",
      "old_id": "6cd883cd4fc9c5e6bcbdb715d53b8bd0f75cba70",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Types.lean",
      "new_id": "65b65514bea9524f54e7081a57d67b23b0f7a9e5",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Types.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "27be0fe9a6f412061f9fc5f01745dbe3e7bfe9c8",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_split_proof_info.lean"
    }
  ]
}