diff --git a/src/Lean/Compiler/LCNF/Main.lean b/src/Lean/Compiler/LCNF/Main.lean index 94e56ccf55..ddbe5d5a4e 100644 --- a/src/Lean/Compiler/LCNF/Main.lean +++ b/src/Lean/Compiler/LCNF/Main.lean @@ -111,8 +111,6 @@ def run (declNames : Array Name) : CompilerM (Array IR.Decl) := withAtLeastMaxRe let opts ← getOptions -- If the new compiler is disabled, then all of the saved IR was built with the old compiler, -- which causes IR type mismatches with IR generated by the new compiler. - if !(compiler.enableNew.get opts) then - return #[] let irDecls ← IR.toIR decls let env ← getEnv let ⟨log, res⟩ := IR.compile env opts irDecls diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 78d5f274bd..147849d79c 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -666,12 +666,6 @@ private def checkUnsupported [Monad m] [MonadEnv m] [MonadError m] (decl : Decla | some (Expr.const declName ..) => throwError "code generator does not support recursor '{declName}' yet, consider using 'match ... with' and/or structural recursion" | _ => pure () -register_builtin_option compiler.enableNew : Bool := { - defValue := true - group := "compiler" - descr := "(compiler) enable the new code generator, unset to use the old code generator instead" -} - /-- If `t` has not finished yet, waits for it under an `Elab.block` trace node. Returns `t`'s result. -/ @@ -686,11 +680,8 @@ def traceBlock (tag : String) (t : Task α) : CoreM α := do @[extern "lean_lcnf_compile_decls"] opaque compileDeclsNew (declNames : List Name) : CoreM Unit -@[extern "lean_compile_decls"] -opaque compileDeclsOld (env : Environment) (opt : @& Options) (decls : @& List Name) : Except Kernel.Exception Environment - -- `ref?` is used for error reporting if available -partial def compileDecls (decls : List Name) (ref? : Option Declaration := none) +partial def compileDecls (decls : List Name) (_ : Option Declaration := none) (logErrors := true) : CoreM Unit := do -- When inside `realizeConst`, do compilation synchronously so that `_cstage*` constants are found -- by the replay code @@ -716,29 +707,14 @@ where doCompile := do -- is made async as well if !decls.all (← getEnv).constants.contains then return - let opts ← getOptions - if compiler.enableNew.get opts then - withoutExporting do - let state ← Core.saveState - try - compileDeclsNew decls - catch e => - state.restore - if logErrors then - throw e - else - let res ← withTraceNode `compiler (fun _ => return m!"compiling old: {decls}") do - return compileDeclsOld (← getEnv) opts decls - match res with - | Except.ok env => setEnv env - | Except.error (.other msg) => + withoutExporting do + let state ← Core.saveState + try + compileDeclsNew decls + catch e => + state.restore if logErrors then - if let some decl := ref? then - checkUnsupported decl -- Generate nicer error message for unsupported recursors and axioms - throwError msg - | Except.error ex => - if logErrors then - throwKernelException ex + throw e def compileDecl (decl : Declaration) (logErrors := true) : CoreM Unit := do compileDecls (Compiler.getDeclNamesForCodeGen decl) decl logErrors