chore: default compiler.enableNew to false until development restar…

…ts (#3034)
leanprover · Dec 21, 2023 · bddb215 · bddb215
1 parent 8d04ac1
commit bddb215
Show file tree

Hide file tree

Showing 72 changed files with 45,366 additions and 38,598 deletions.
diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
@@ -315,7 +315,7 @@ private def checkUnsupported [Monad m] [MonadEnv m] [MonadError m] (decl : Decla
     | _ => pure ()
 
 register_builtin_option compiler.enableNew : Bool := {
-  defValue := true
+  defValue := false
   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"
 }

diff --git a/stage0/stdlib/Init/Conv.c b/stage0/stdlib/Init/Conv.c
diff --git a/stage0/stdlib/Init/NotationExtra.c b/stage0/stdlib/Init/NotationExtra.c
diff --git a/stage0/stdlib/Init/Tactics.c b/stage0/stdlib/Init/Tactics.c
diff --git a/stage0/stdlib/Lean/CoreM.c b/stage0/stdlib/Lean/CoreM.c