From 7c0bb0a6dc940d7c74ae998a2ea59ee06827ca65 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 21 Aug 2022 11:09:51 -0700
Subject: [PATCH] feat: add `compiler.check` option

---
 src/Lean/Compiler/Main.lean | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Compiler/Main.lean b/src/Lean/Compiler/Main.lean
index 229485e39b..5a5fa871f3 100644
--- a/src/Lean/Compiler/Main.lean
+++ b/src/Lean/Compiler/Main.lean
@@ -33,6 +33,12 @@ where
     let info ← getConstInfo declName
     Meta.isProp info.type <||> Meta.isTypeFormerType info.type
 
+register_builtin_option compiler.check : Bool := {
+  defValue := true
+  group    := "compiler"
+  descr    := "type check code after each compiler step (this is useful for debugging purses)"
+}
+
 /--
 A checkpoint in code generation to print all declarations in between
 compiler passes in order to ease debugging.
@@ -44,7 +50,8 @@ def checkpoint (stepName : Name) (decls : Array Decl) (cfg : Check.Config := {})
       let clsName := `Compiler ++ stepName
       if (← Lean.isTracingEnabledFor clsName) then
         Lean.addTrace clsName m!"{decl.name} : {decl.type} :=\n{decl.value}"
-      decl.check cfg
+      if compiler.check.get (← getOptions) then
+        decl.check cfg
 
 @[export lean_compile_stage1]
 def compileStage1Impl (declNames : Array Name) : CoreM (Array Decl) := do