fix: add missing initHeartbeats
#1037
Conversation
github-actions
bot
added
the
awaiting-review
|
Mathlib CI status (docs):
|
|
LGTM Could you explain, for documentation purposes, why this isn't something Lean core could do? |
fgdorais
added
awaiting-author
leanprover-community-mathlib4-bot
added
the
merge-conflict
|
Sorry, I missed that message. What are you expecting Lean core to do here? Because we are constructing a Perhaps @kmill should have a look at this and suggest if we can avoid this manual construction in the first place (and confirm whether the PR in its current state is still an improvement over the status quo). |
Batteries/Tactic/Lint/Frontend.lean
Outdated
| match ← withCurrHeartbeats (linter.test decl) | ||
| |>.run' mkMetaContext | ||
| |>.run' {options, fileName := "", fileMap := default} {env} | ||
| |>.run' {options, fileName := "", fileMap := default, initHeartbeats } {env} |
There was a problem hiding this comment.
It looks like the withCurrHeartbeats sets initHeartbeats from IO.getNumHeartbeats. What effect does initializing initHeartbeats here have? Can you come up with a test that validates this?
There was a problem hiding this comment.
I think you're right, this has no effect.
Batteries/Util/Cache.lean
Outdated
| let initHeartbeats ← IO.getNumHeartbeats | ||
| let res ← EIO.asTask <| | ||
| init {} |>.run' {} { options, fileName, fileMap } |>.run' { env } | ||
| init {} |>.run' {} { options, fileName, fileMap, initHeartbeats } |>.run' { env } |
There was a problem hiding this comment.
I see that Lean.Core.wrapAsync exists, and it does a bit more heartbeats arithmetic. Lean.Core.CoreM.toIO looks relevant.
There was a problem hiding this comment.
wrapAsync indeed looks like the right tool, as otherwise the hearbeat counts on one thread are meaninglessly transferred to another thread.
In only one case a `Core.Context` is created from within CoreM, and we inherit from the parent Context the `initHeartbeats`. Otherwise, we get the current heartbeats from IO. Co-authored-by: Laurent Sartran <[email protected]>
eric-wieser
force-pushed
the
eric-wieser/initHeartbeats
branch
from
c753fca to
9d7fca8
Compare
leanprover-community-mathlib4-bot
removed
the
merge-conflict
|
Have issues been fixed to everyone's satisfaction? |
|
I'm afraid I lost track of this one. What's the current status? |
|
I need to update the description to reflect the new version, but I think the approach now aligns with @kmill's suggestion. The mathlib failure suggests that either I have broken the heartbeat counting, or that we were previously erroneously resetting the heartbeat counter mid-linter. |
leanprover-community-mathlib4-bot
added
the
merge-conflict
In only one case a
Core.Contextis created from within CoreM, and we inherit from the parent Context theinitHeartbeats. Otherwise, we get the current heartbeats from IO.It's not entirely clear to me what the intended semantics of
lintCoreare; should they inherit the outer heartbeat count (as with this patch), or get a new heartbeat budget for each declaration (prior to it)?