Commit 2023-06-07 23:57 28f3fa38

View on Github →

fix: library_search doesn't get tired (#4828) I had badly misunderstood how to keep track of remaining heartbeats in a given computation, and library_search was using a thread-local heartbeat count, rather than a declaration-local heartbeat count, so would "get tired" after working in the same file for a while.

Estimated changes

Modified Mathlib/Data/ListM/Heartbeats.lean

Modified Mathlib/Lean/CoreM.lean

added def getInitHeartbeats

modified def getMaxHeartbeats

modified def getRemainingHeartbeats

modified def heartbeatsPercent

modified def reportOutOfHeartbeats

Modified Mathlib/Tactic/LibrarySearch.lean