)]}'
{
  "commit": "1430e218f27a37aa453f6a3cc95c0d45434756a4",
  "tree": "f8e9e79800e36791898d6da8eb0db95462d5afe1",
  "parents": [
    "67b6e815b989a8c0aa328eedeca9216df44cbd12"
  ],
  "author": {
    "name": "Joachim Breitner",
    "email": "mail@joachim-breitner.de",
    "time": "Tue Mar 31 20:36:34 2026 +0000"
  },
  "committer": {
    "name": "Joachim Breitner",
    "email": "mail@joachim-breitner.de",
    "time": "Wed Apr 01 11:37:52 2026 +0000"
  },
  "message": "fix: add checkSystem calls to long-running elaboration paths\n\nThis PR adds `checkSystem` calls to several code paths that can run for\nextended periods without checking for cancellation, heartbeat limits, or\nstack overflow. This improves responsiveness of the cancellation mechanism\nin the language server.\n\nAffected paths:\n- `simp` rewrite candidate loops (`Rewrite.lean`)\n- `simpAppUsingCongr` argument traversal (`Types.lean`)\n- `synthesizeSyntheticMVarsStep` mvar loop (`SyntheticMVars.lean`)\n- `abstractNestedProofs` visitor (`AbstractNestedProofs.lean`)\n- `transform`/`transformWithCache` visitors (`Transform.lean`)\n- LCNF compiler pass runner loop (`Main.lean`)\n- LCNF checker recursive traversal (`Check.lean`)\n- LCNF simplifier recursive traversal (`Simp/Main.lean`)\n- `whnfCore` recursive reduction loop (`WHNF.lean`)\n\nWith these changes, at a 50ms monitoring threshold across the full test suite,\nthe only remaining Lean-side elaborator gaps are:\n- bv_decide pure computation wrapped in `IO.lazyPure` (architectural)\n- Single deep `whnf` reductions from the `constructorNameAsVariable` linter (~100-180ms)\n\nRemaining C++ gaps (type checker, interpreter module init) are tracked separately.\n\nFound using `LEAN_CHECK_SYSTEM_INTERVAL_MS` monitoring from #13218.\n\nCo-Authored-By: Claude Opus 4.6 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "98a391466c4a0f223b745be92dfda1c187ae45ec",
      "old_mode": 33188,
      "old_path": "src/Lean/Compiler/LCNF/Check.lean",
      "new_id": "594588f2c370fa9cf8787b036204ed01307740a5",
      "new_mode": 33188,
      "new_path": "src/Lean/Compiler/LCNF/Check.lean"
    },
    {
      "type": "modify",
      "old_id": "2f6189f17a5df691b1fc6620bd3cdfb0161e35d2",
      "old_mode": 33188,
      "old_path": "src/Lean/Compiler/LCNF/Main.lean",
      "new_id": "11023abb4d10d345fa71b0e17b8890c0b8df70d2",
      "new_mode": 33188,
      "new_path": "src/Lean/Compiler/LCNF/Main.lean"
    },
    {
      "type": "modify",
      "old_id": "3403cbfde65a41ea67336b83007ff4d4b5b8f3ca",
      "old_mode": 33188,
      "old_path": "src/Lean/CoreM.lean",
      "new_id": "ead24ad2a048a35e00659810faad6cb7182e091a",
      "new_mode": 33188,
      "new_path": "src/Lean/CoreM.lean"
    },
    {
      "type": "modify",
      "old_id": "310e9927b385ab77fb1cc61e5375b5cb76085a37",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/SyntheticMVars.lean",
      "new_id": "7b7f039bfa57aef97a3e44348d0f6194fa95fda9",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/SyntheticMVars.lean"
    },
    {
      "type": "modify",
      "old_id": "3b27b6f36bbb43ab8583b7fdef2609af78693249",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/AbstractNestedProofs.lean",
      "new_id": "b931c2cf0519ac38d0303e79d69e16f34e296c5c",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/AbstractNestedProofs.lean"
    },
    {
      "type": "modify",
      "old_id": "f8c2607a24cd93490265cd18cd5ea0c73539d628",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Simp/Main.lean",
      "new_id": "b648566cb9eb4c6aad421ead0e849092fcf4cffa",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Simp/Main.lean"
    },
    {
      "type": "modify",
      "old_id": "1ca46b5bb347aacc3c0e04b32bb17a678d0883d7",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Simp/Rewrite.lean",
      "new_id": "d30581f948b7fe6af9a5f87607de912280a97e4d",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Simp/Rewrite.lean"
    },
    {
      "type": "modify",
      "old_id": "6583ec6ae6dc102db81abb933ee28cb4d6d8c841",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Simp/Types.lean",
      "new_id": "c2d1d673f012145f18ef8c7f1837fac3600dd885",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Simp/Types.lean"
    },
    {
      "type": "modify",
      "old_id": "f75d4da31c0ea7924d73d51650348ba602bd308a",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Transform.lean",
      "new_id": "e526c71d75395cac41b2cf2e6bbaddf166cb5eb5",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Transform.lean"
    },
    {
      "type": "modify",
      "old_id": "74fcfef37f8449a9a6570af2ee3f68342690015b",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/WHNF.lean",
      "new_id": "0ce0dcac2261e27e5d1ba26f4904ca83e9503308",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/WHNF.lean"
    }
  ]
}