From 7f8ccd84259b975f2cbb6c293ca608696f2709fc Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Sat, 14 Jun 2025 07:41:27 -0700 Subject: [PATCH] feat: enable the new compiler --- src/Lean/CoreM.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 3943c5dfae..bb1d011680 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -667,9 +667,9 @@ private def checkUnsupported [Monad m] [MonadEnv m] [MonadError m] (decl : Decla | _ => pure () register_builtin_option compiler.enableNew : Bool := { - defValue := false + defValue := true group := "compiler" - descr := "(compiler) enable the new code generator, this should have no significant effect on your code but it does help to test the new code generator; unset to only use the old code generator instead" + descr := "(compiler) enable the new code generator, unset to use the old code generator instead" } /--