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