)]}'
{
  "commit": "d15db3ad8e0418c5141030067ed2869176c168ea",
  "tree": "7a558dd991cb721675470f110c0f9b68eb9a1754",
  "parents": [
    "0e28043ec6749ab227d84b690fbb10375dcf714c"
  ],
  "author": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Tue Jan 27 03:17:16 2026 +0000"
  },
  "committer": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Tue Jan 27 03:38:49 2026 +0000"
  },
  "message": "fix: bump numInstances for delayed grind theorem instances\n\nThis PR fixes a bug where delayed E-match theorem instances could\ncause uniqueId collisions in the instance tracking map.\n\nThe `uniqueId` for theorem instances is generated using `numInstances`,\nbut this counter was only bumped for immediately activated instances\n(`.ready` case), not for delayed instances (`.next` case). This caused\nID collisions:\n\n1. Theorem A matches, becomes delayed, gets uniqueId \u003d N\n2. Counter isn\u0027t bumped (stays at N)\n3. Theorem B matches next, gets uniqueId \u003d N (same!)\n4. B\u0027s entry overwrites A\u0027s entry in instanceMap\n5. A\u0027s tracking is lost\n\nThis manifested as `grind?` and `finish?` producing `instantiate approx`\n(meaning \"we couldn\u0027t determine which theorems to use\") instead of\nproper `instantiate only [...]` with specific theorem lists.\n\nThe fix is to bump `numInstances` for delayed instances too, ensuring\neach theorem instance gets a truly unique ID.\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": "c05bbd78d2547acb0d82311426417b0a38117465",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Types.lean",
      "new_id": "0a8b1e9e4b6cca3e9f53c52e6cc577b7feae91dc",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Types.lean"
    },
    {
      "type": "modify",
      "old_id": "1aff08f26cb79f10a930bca88cf64200aca6b170",
      "old_mode": 33188,
      "old_path": "tests/lean/run/grind_indexmap_trace.lean",
      "new_id": "943a9271a1437bbc0fcd5c43700c25f127a2d862",
      "new_mode": 33188,
      "new_path": "tests/lean/run/grind_indexmap_trace.lean"
    }
  ]
}