)]}'
{
  "commit": "448bfbfc4e2400bd6f33e01c6e706165adcf7405",
  "tree": "051bc12fa62aa5dac04feaef48a6d3b2824b78ee",
  "parents": [
    "c029d915d12bd1a1199881cefcae07f00ec9f568"
  ],
  "author": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Wed Nov 04 03:31:17 2026 +0000"
  },
  "committer": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Wed Nov 04 03:31:17 2026 +0000"
  },
  "message": "fix: respect `debug.skipKernelTC` when replaying realized constants\n\n`realizeConst` runs `realize` with kernel checking disabled and then type checks the realized constants when it replays them into each calling branch\u0027s kernel environment. That replay ignored the caller\u0027s `debug.skipKernelTC`, so realizing, for example, the equation theorems of an imported definition ran the kernel in a background task even when the caller had disabled kernel checking. Pass the caller\u0027s `debug.skipKernelTC` to the replay.\n\nCo-Authored-By: Claude Opus 5.5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "297985fbec34c08a4f5536a0a0bddf3c65b026ef",
      "old_mode": 33188,
      "old_path": "src/Lean/Environment.lean",
      "new_id": "8b9459be741a97d7f6a015ab90490f5166474231",
      "new_mode": 33188,
      "new_path": "src/Lean/Environment.lean"
    },
    {
      "type": "modify",
      "old_id": "690e4d83ca43346b6bb36792284dd3f91c7981b0",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Basic.lean",
      "new_id": "00e6de4e3ff1991f7445d0815d4fdafc45ca8bc8",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Basic.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "b48ade4fbf401bf18d1b11b50f1680279668e23a",
      "new_mode": 33188,
      "new_path": "tests/elab/realizeConstSkipKernelTC.lean"
    }
  ]
}