From e6954b78376cdc2c071df529f8b89b590fce6810 Mon Sep 17 00:00:00 2001
From: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Date: Wed, 2 Jul 2025 05:42:00 +0200
Subject: [PATCH] fix: revert state on compilation failure (new compiler)
 (#8691)

This PR ensures that the state is reverted when compilation using the
new compiler fails. This is especially important for noncomputable
sections where the compiler might generate half-compiled functions which
may then be erroneously used while compiling other functions.
---
 src/Lean/CoreM.lean | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 506e8b5a08..78d5f274bd 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -718,9 +718,14 @@ where doCompile := do
     return
   let opts ← getOptions
   if compiler.enableNew.get opts then
-    withoutExporting
-      try compileDeclsNew decls catch e =>
-        if logErrors then throw e else return ()
+    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