)]}'
{
  "commit": "4f75d3bdef2bc159eb90b80232514d56119aa422",
  "tree": "702089ec58b509c3c07c3ee7ca33b9a0c72208fd",
  "parents": [
    "31e25f0085d4529563572206003d9cdfcaa6d69e"
  ],
  "author": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Mon Mar 23 11:29:08 2026 +0000"
  },
  "committer": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Mon Mar 23 11:36:11 2026 +0000"
  },
  "message": "fix: use `declName?` pattern for `normalizeInstance` meta marking\n\nThe previous fix (#13043) used `isMetaSection` to determine whether\n`normalizeInstance` aux defs should be marked `meta`. This caused\n`deriving` in meta sections to fail: the deriving handler doesn\u0027t mark\nthe instance itself as meta, so the non-meta instance couldn\u0027t access\nits meta-marked aux defs.\n\nSwitch to the existing `declName?` pattern (already used by `unsafe`\nand `private_decl%`), which inherits meta status from the parent\ndeclaration rather than the scope. This correctly handles both cases:\n- `inferInstanceAs`: parent declaration is marked meta by\n  `processHeaders`, so aux defs are also marked meta\n- `deriving`: `declName?` reflects the actual meta status of the\n  declaration being elaborated, avoiding the mismatch\n\nCo-Authored-By: Claude Opus 4.6 (1M context) \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "5dbcd49d8bed74e19a0a6b1dbc248601a3ae888a",
      "old_mode": 33188,
      "old_path": "tests/elab/12897.lean",
      "new_id": "7a7718f9f822709e4c90f7c97b157534c6017753",
      "new_mode": 33188,
      "new_path": "tests/elab/12897.lean"
    }
  ]
}