)]}'
{
  "commit": "4713811392c30b91d83558c28f41501658239fd7",
  "tree": "cf9c8406c0b2f3aa66f570edb715a95aab640b23",
  "parents": [
    "272f0f5db390b3c720fc47ffed94f578018e8337"
  ],
  "author": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Wed Nov 26 03:38:14 2025 +0100"
  },
  "committer": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Tue Dec 02 18:37:07 2025 +1100"
  },
  "message": "perf: parallelize `exact?` and `apply?` tactics\n\nUse `MetaM.parIterWithCancel` to try all candidate lemmas in parallel\nwhile preserving deterministic result ordering. When a complete solution\nis found, remaining tasks are cancelled and the result is returned\nimmediately.\n\nThis removes the old sequential `tryOnEach` implementation along with\nthe heartbeat-based abortion mechanism (`abortSpeculation`,\n`mkHeartbeatCheck`).\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": "1de486930139a33d81b12a9177b4706ff1f1a558",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/LibrarySearch.lean",
      "new_id": "f4582cff2bf56d6a7b1012174e56dad29bd25280",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/LibrarySearch.lean"
    },
    {
      "type": "modify",
      "old_id": "58edf8d81d30696a6b57d0a69f59191997817d20",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/LibrarySearch.lean",
      "new_id": "42ffd39db07f1a918d76748ed4711cdc8c63388e",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/LibrarySearch.lean"
    }
  ]
}