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
This commit is contained in:
Sebastian Ullrich 2026-04-01 12:54:13 +02:00 committed by GitHub
parent cdd982a030
commit 1aa860af33
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -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