From 1aa860af33e1aa30fb8aff6339816999e89f921b Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 1 Apr 2026 12:54:13 +0200 Subject: [PATCH] fix: avoid heartbeat timeout in `symbolFrequencyExt` export (#13202) This PR fixes a heartbeat timeout from an environment extension at the end of the file that cannot be avoided by raising the limit. Fixes #12989 --- src/Lean/LibrarySuggestions/SymbolFrequency.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Lean/LibrarySuggestions/SymbolFrequency.lean b/src/Lean/LibrarySuggestions/SymbolFrequency.lean index 37d92703cd..b4f097c6b2 100644 --- a/src/Lean/LibrarySuggestions/SymbolFrequency.lean +++ b/src/Lean/LibrarySuggestions/SymbolFrequency.lean @@ -66,7 +66,11 @@ Helper function for running `MetaM` code during module export, when there is not Panics on errors. -/ unsafe def _root_.Lean.Environment.unsafeRunMetaM [Inhabited α] (env : Environment) (x : MetaM α) : α := - match unsafeEIO ((((withoutExporting x).run' {} {}).run' { fileName := "symbolFrequency", fileMap := default } { env })) with + match unsafeEIO ((((withoutExporting x).run' {} {}).run' + { fileName := "symbolFrequency", fileMap := default + -- avoid triggering since limit cannot be raised here + maxHeartbeats := 0 } + { env })) with | Except.ok a => a | Except.error ex => panic! match unsafeIO ex.toMessageData.toString with | Except.ok s => s