)]}'
{
  "commit": "d6fc6e6b457e70c33844c104866746e12c0f1477",
  "tree": "39171d9e0dfbbef32110bd6c7e16dbd0d5ebc4c2",
  "parents": [
    "272f0f5db390b3c720fc47ffed94f578018e8337"
  ],
  "author": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Wed Nov 26 03:44:33 2025 +0100"
  },
  "committer": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Tue Dec 02 18:39:38 2025 +1100"
  },
  "message": "perf: parallelize `rw?` tactic\n\nUse `MetaM.parIterWithCancel` to try all candidate rewrites in parallel\nwhile preserving deterministic result ordering. When an rfl-closeable\nresult is found (and `stopAtRfl` is true), or the maximum number of\nresults is reached, remaining tasks are cancelled.\n\nThis removes the old sequential `takeListAux` implementation along with\nthe heartbeat-based early termination and `RewriteResultConfig` structure.\n\n🤖 Generated with [Claude Code](https://claude.com/claude-code)\n\nCo-Authored-By: Claude \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "27f10b38ecbae78f59606ea66a8f38889a8f004a",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Rewrites.lean",
      "new_id": "14d245f067c01ad4e60aacf90b4e9eba61c1e98a",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Rewrites.lean"
    }
  ]
}
