From e39894e62d363322fa18af76e12e54799496e2c0 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sat, 15 Nov 2025 18:36:09 +0100
Subject: [PATCH] feat: realizeConst to set CoreM's maxHeartbeat (#11191)

This PR makes sure that inside a `realizeConst` the `maxHeartbeat`
option is effective.
---
 src/Lean/Meta/Basic.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 585bdc98af..ded9c1fbef 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -2657,7 +2657,10 @@ def realizeConst (forConst : Name) (constName : Name) (realize : MetaM Unit) :
 where
   -- similar to `wrapAsyncAsSnapshot` but not sufficiently so to share code
   realizeAndReport (coreCtx : Core.Context) env opts := do
-    let coreCtx := { coreCtx with options := opts }
+    let coreCtx := { coreCtx with
+      options := opts
+      maxHeartbeats := Core.getMaxHeartbeats opts
+    }
     let act :=
       IO.FS.withIsolatedStreams (isolateStderr := Core.stderrAsMessages.get opts) (do
         -- catch all exceptions