)]}'
{
  "commit": "286753d3c75f1e8d4eeedce09e1bcb0895f7f937",
  "tree": "893b62e5e0f35eacda818447b38d8fda3785550c",
  "parents": [
    "b4e5cf2007fba29f733eb11dd013e2eb29b946a6"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sat Oct 31 04:41:14 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sat Oct 31 04:41:14 2026 +0000"
  },
  "message": "perf: do not revisit shared subterms without matches in `kabstract`\n\nThis PR makes `rw` and other tactics based on `kabstract` faster on goals with shared subterms.\n\n`kabstract` traverses its input as a tree, so a shared subterm is visited, and its `isDefEq` candidates are tested, once per occurrence. It now remembers the subterms whose traversal found no match, and skips them when they occur again. The cache is cleared whenever a match is abstracted, since this is the only point where the metavariable context changes. Subterms containing matches that are not abstracted are not cached, so occurrence numbering for `occs` is unchanged.\n\nCo-Authored-By: Claude Opus 5.5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "2b6141d34ee76a85ac4a444d1d4a28d52e12d128",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/KAbstract.lean",
      "new_id": "237452df3b710641df38be9ba1256872af3cb280",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/KAbstract.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "afed03714a80117ec5432156a14c6ce99ad6d6c7",
      "new_mode": 33188,
      "new_path": "tests/elab/kabstractShared.lean"
    }
  ]
}