From 9e3bc9c4ff438fb84d893cdcbbaf938f07d472dc Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Wed, 8 Jan 2025 14:06:12 -0800
Subject: [PATCH] chore: have CoreM call lean_compile_decls itself

---
 src/Lean/CoreM.lean | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index f6d34ca8042a..d541bb1951f9 100644
--- 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