fix: add checkSystem to LCNF compiler passes (#13231)

This PR adds checkSystem calls to the LCNF compiler to improve IDE
cancellation responsiveness during compilation of large declarations.

Two changes:
1. `Pass.mkPerDeclaration` now calls `checkSystem` before processing
each declaration, allowing interruption between declarations.
2. The LCNF `simp` pass calls `checkSystem` every 128 recursive visits,
allowing interruption within large single-declaration simplifications.

Note: LCNF simp has its own custom `withIncRecDepth` (in `SimpM.lean`)
that does **not** call `checkInterrupted`, unlike
`Core.withIncRecDepth`. So this `checkSystem` call is the only
cancellation check on this code path.

Performance: unconditional `checkSystem` added +0.44% instructions on
`big_do.lean` per CI benchmarks. Amortizing to every 128 visits brings
overhead to noise level while keeping the max simp gap under ~80M
instructions (~14ms at 6 Ginstr/s).

**Before** (measured with `LEAN_CHECK_SYSTEM_INTERVAL_INSN` on the
instrumentation branch):

| Test | Largest LCNF gap | Time at 6 Ginstr/s |
|------|------------------|-------------------|
| `big_do.lean` | 12,623M insn (simp) | 2.1s |
| `riscv-ast.lean` | 1,162M insn (simp) | 194ms |
| `riscv-ast.lean` | 37 gaps total | — |

**After:**

| Test | Largest LCNF gap | Time at 6 Ginstr/s |
|------|------------------|-------------------|
| `big_do.lean` | 869M insn (resetReuse) | 145ms |
| `riscv-ast.lean` | 232M insn (simp) | 39ms |
| `riscv-ast.lean` | reduced gap count | — |

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

src/Lean/Compiler/LCNF/PassManager.lean

@@ -121,7 +121,7 @@ def mkPerDeclaration (name : Name) (phase : Phase)
   occurrence := occurrence
   phase := phase
   name := name
-  run := fun xs => xs.mapM run
+  run := fun xs => xs.mapM fun decl => do checkSystem "LCNF compiler"; run decl
 
 end Pass
 

src/Lean/Compiler/LCNF/Simp/Main.lean

@@ -217,6 +217,8 @@ Simplify `code`
 -/
 partial def simp (code : Code .pure) : SimpM (Code .pure) := withIncRecDepth do
   incVisited
+  if (← get).visited % 128 == 0 then
+    checkSystem "LCNF simp"
   match code with
   | .let decl k =>
     let baseDecl := decl