chore: have CoreM call lean_compile_decls itself

leanprover · Jan 12, 2025 · 9e3bc9c · 9e3bc9c
1 parent 8acec05
commit 9e3bc9c
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
@@ -514,13 +514,16 @@ register_builtin_option compiler.enableNew : Bool := {
 @[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 KernelException Environment
+
 def compileDecl (decl : Declaration) : CoreM Unit := do
   let opts ← getOptions
   let decls := Compiler.getDeclNamesForCodeGen decl
   if compiler.enableNew.get opts then
     compileDeclsNew decls
   let res ← withTraceNode `compiler (fun _ => return m!"compiling old: {decls}") do
-    return (← getEnv).compileDecl opts decl
+    return compileDeclsOld (← getEnv) opts decls
   match res with
   | Except.ok env => setEnv env
   | Except.error (KernelException.other msg) =>
@@ -533,7 +536,7 @@ def compileDecls (decls : List Name) : CoreM Unit := do
   let opts ← getOptions
   if compiler.enableNew.get opts then
     compileDeclsNew decls
-  match (← getEnv).compileDecls opts decls with
+  match compileDeclsOld (← getEnv) opts decls with
   | Except.ok env   => setEnv env
   | Except.error (KernelException.other msg) =>
     throwError msg