mathlib test build fails (8 instead of 7 heartbeats)

Stream: lean4 dev

[Paul Reichert]

Hello, I have PRed two new builtin constructs for bootstrapping. The changes do not at all seem to be related to mathlib and the new constructs are used nowhere, so I was surprised to see some mathlib test fail:

✖ [6206/6245] Building MathlibTest.CountHeartbeats
trace: .> LEAN_PATH=[...]
info: ././././MathlibTest/CountHeartbeats.lean:17:0: Used 8 heartbeats, which is less than the minimum of 2000.
error: ././././MathlibTest/CountHeartbeats.lean:16:0: ❌️ Docstring on `#guard_msgs` does not match generated message:

info: Used 8 heartbeats, which is less than the minimum of 2000.
error: Lean exited with code 1

For context, this is the test:

/-- info: Used 7 heartbeats, which is less than the minimum of 2000. -/
#guard_msgs in
guard_min_heartbeats 2000 in
example (a : Nat) : a = a := rfl

According to the test, only 7 heartbeats are expected here and, as @Markus Himmel thankfully remembered, this was recently changed from 8 to 7 to fix this test.

Nevertheless, I can't explain this to myself. My small changes are built directly on top of nightly-2025-01-28 and if I revert them, the CountHeartbeats test becomes green again, locally as well as in CI.

Does anybody have an idea what the problem is? Do you consider it plausible that a change such as mine (adding two new files, simply defining new syntax, a builtin elaborator and a builtin attribute, all of them unused as of now) should affect the heartbeats of such a simple lemma?

[Kim Morrison]

We should remove these tests. This is just noise, and it is getting in the way of Lean development. We should never have tests that depend on an exact number of heartbeats.

I think @Damiano Testa added these tests?

[Damiano Testa]

Yes, I am responsible for this: there is a PR in progress by @Jon Eugster to fix bugs in the implementation and I will suggest to make a "test" version that does not report the actual numbers.

[Damiano Testa]

If it is urgent, I can prepare a PR to implement this change earlier (though likely not for several hours).

[Paul Reichert]

If there is already a fix planned, I could just change the tests back to 8 for now. This would unblock me, although it is possible that the next person that changes something will find themselves in the situation that the heartbeats have changed again. What do you think?

[Kim Morrison]

Yes, just change them freely to get unblocked, and it sounds like Damiano / Jon will make sure that the exact numbers disappear from tests later.

[Damiano Testa]

Ah, I forgot to reply here: I am coordinating with Jon whether to incorporate the changes in his PR or producing a separate one with this change.

[Damiano Testa]

I will probably produce an option to report a "round down to the nearest multiple of 1001000" for the heartbeats, so that the tests will be more robust, but might still make sure that the command is working as expected.

[Eric Wieser]

Kim Morrison said:

We should never have tests that depend on an exact number of heartbeats.

I'm on the fence on this; tests which record arbitrary limits are useful as canaries for detecting when the limit changes; but they should come with a comment saying that you should always just change the number to make it pass again.

[Damiano Testa]

I share your feeling Eric, but maybe it makes sense to have the test file for the linter not include the numbers and having a separate mechanism that tracks changes to heartbeats in a less intrusive way?

[Kim Morrison]

I'm happy with rounding to the nearest 1000.

[Paul Reichert]

Thanks for helping me out, everyone!

[Damiano Testa]

#21251 adds an Option to report approximate counts and uses it in the tests.

[Kim Morrison]

@Damiano Testa, this somehow seems to have relapsed on master. Could you investigate? Did someone revert #21251?

[Damiano Testa]

I'll look into this tomorrow: I'm not aware of a change, but have also been out of the loop for almost two weeks.

[Damiano Testa]

#21251 has not been reverted. The only change after that PR has been #22568, fixing a spelling mistake in a module doc.

[Damiano Testa]

There is one #count_heartbeats in that was still missing the approximately flag and there are two guard_min_heartbeats ... in that are possible also culprits.

[Damiano Testa]

I am going to add the approximately flag to the #count_heartbeats, but the others do not (yet?) have the approximately mechanism.

[Damiano Testa]

Could you say which tests are failing? Everything seems to work for me locally.

[Damiano Testa]

#23476 adds the missing approximately.

[Sebastian Ullrich]

All exact heartbeat messages regularly break on nightly-testing, they should all be avoided

[Damiano Testa]

I just updated the PR: now it also adds the approximately flag to guard_min_heartbeats and uses it in the tests.

[Damiano Testa]

The test file should now only contain heartbeat counts that are rounded down to the nearest 1k.