fix: run LCNF checks less often by default (leanprover#8764)

This PR changes the LCNF pass pipeline so checks are no longer run by
default after every pass, only after `init`, `saveBase`, `toMono` and
`saveMono`. This is a compile time improvement, and the utility of these
checks is decreased a bit after the decision to no longer attempt to
preserve types throughout compilation. They have not been a significant
way to discover issues during development of the new compiler.

Author: zwarich

src/Lean/Compiler/LCNF/Main.lean

@@ -54,16 +54,16 @@ A checkpoint in code generation to print all declarations in between
 compiler passes in order to ease debugging.
 The trace can be viewed with `set_option trace.Compiler.step true`.
 -/
-def checkpoint (stepName : Name) (decls : Array Decl) : CompilerM Unit := do
+def checkpoint (stepName : Name) (decls : Array Decl) (shouldCheck : Bool) : CompilerM Unit := do
   for decl in decls do
     trace[Compiler.stat] "{decl.name} : {decl.size}"
     withOptions (fun opts => opts.setBool `pp.motives.pi false) do
       let clsName := `Compiler ++ stepName
       if (← Lean.isTracingEnabledFor clsName) then
         Lean.addTrace clsName m!"size: {decl.size}\n{← ppDecl' decl}"
-      if compiler.check.get (← getOptions) then
+      if shouldCheck then
         decl.check
-  if compiler.check.get (← getOptions) then
+  if shouldCheck then
     checkDeadLocalDecls decls
 
 namespace PassManager
@@ -80,10 +80,11 @@ def run (declNames : Array Name) : CompilerM (Array IR.Decl) := withAtLeastMaxRe
   let mut decls ← declNames.mapM toDecl
   decls := markRecDecls decls
   let manager ← getPassManager
+  let isCheckEnabled := compiler.check.get (← getOptions)
   for pass in manager.passes do
     decls ← withTraceNode `Compiler (fun _ => return m!"new compiler phase: {pass.phase}, pass: {pass.name}") do
       withPhase pass.phase <| pass.run decls
-    withPhase pass.phaseOut <| checkpoint pass.name decls
+    withPhase pass.phaseOut <| checkpoint pass.name decls (isCheckEnabled || pass.shouldAlwaysRunCheck)
   if (← Lean.isTracingEnabledFor `Compiler.result) then
     for decl in decls do
       -- We display the declaration saved in the environment because the names have been normalized

src/Lean/Compiler/LCNF/PassManager.lean

@@ -49,6 +49,11 @@ structure Pass where
   phaseOut : Phase := phase
   phaseInv : phaseOut ≥ phase := by simp +arith +decide
   /--
+  Whether IR validation checks should always run after this pass, regardless
+  of configuration options.
+  -/
+  shouldAlwaysRunCheck : Bool := false
+  /--
   The name of the `Pass`
   -/
   name : Name

src/Lean/Compiler/LCNF/Passes.lean

@@ -31,18 +31,31 @@ def init : Pass where
     decls.forM (·.saveBase)
     return decls
   phase := .base
+  shouldAlwaysRunCheck := true
 
 -- Helper pass used for debugging purposes
 def trace (phase := Phase.base) : Pass where
   name  := `trace
   run   := pure
   phase := phase
 
-def saveBase : Pass :=
-  .mkPerDeclaration `saveBase (fun decl => do (← normalizeFVarIds decl).saveBase; return decl) .base
+def saveBase : Pass where
+  occurrence := 0
+  phase := .base
+  name := `saveBase
+  run decls := decls.mapM fun decl => do
+    (← normalizeFVarIds decl).saveBase
+    return decl
+  shouldAlwaysRunCheck := true
 
-def saveMono : Pass :=
-  .mkPerDeclaration `saveMono (fun decl => do (← normalizeFVarIds decl).saveMono; return decl) .mono
+def saveMono : Pass where
+  occurrence := 0
+  phase := .mono
+  name := `saveMono
+  run decls := decls.mapM fun decl => do
+    (← normalizeFVarIds decl).saveMono
+    return decl
+  shouldAlwaysRunCheck := true
 
 def builtinPassManager : PassManager := {
   passes := #[

src/Lean/Compiler/LCNF/ToMono.lean

@@ -340,6 +340,7 @@ def toMono : Pass where
   run      := (·.mapM (·.toMono))
   phase    := .base
   phaseOut := .mono
+  shouldAlwaysRunCheck := true
 
 builtin_initialize
   registerTraceClass `Compiler.toMono (inherited := true)

src/Lean/Compiler/Options.lean

@@ -10,7 +10,7 @@ import Lean.Data.Options
 namespace Lean.Compiler
 
 register_builtin_option compiler.check : Bool := {
-  defValue := true
+  defValue := false
   group    := "compiler"
   descr    := "type check code after each compiler step (this is useful for debugging purses)"
 }