From c4a664eb5db2648780fa3c7a4be6d439e7233a72 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 6 Apr 2026 11:35:58 +0200 Subject: [PATCH] fix: add checkSystem to LCNF compiler passes (#13231) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --------- Co-authored-by: Claude Opus 4.6 --- src/Lean/Compiler/LCNF/PassManager.lean | 2 +- src/Lean/Compiler/LCNF/Simp/Main.lean | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/PassManager.lean b/src/Lean/Compiler/LCNF/PassManager.lean index 0390bbcfad..0e915b5798 100644 --- a/src/Lean/Compiler/LCNF/PassManager.lean +++ b/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 diff --git a/src/Lean/Compiler/LCNF/Simp/Main.lean b/src/Lean/Compiler/LCNF/Simp/Main.lean index 03507d87f3..52d358f5ab 100644 --- a/src/Lean/Compiler/LCNF/Simp/Main.lean +++ b/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