maxHeartbeats

Stream: mathlib4

[Jeremy Tan]

Mauricio Collares said:

I can add the shameful maxHeartbeats bumps to !4#3457 myself :)

maxHeartbeats is never shameful. As long as it does the job it's OK

[Patrick Massot]

No, "As long as it does the job it's ok" is wrong.

[Patrick Massot]

It is the last thing to do when everything else failed.

[Eric Wieser]

Sometimes we've opted to set a highmaxHearbeats even when there was an alternative, because the alternative was just too ugly; with the hope that a future lean4 refactor will speed things up. That way we have no hack left to revert.

[Mauricio Collares]

Eric Wieser said:

Sometimes we've opted to set a highmaxHearbeats even when there was an alternative, because the alternative was just too ugly; with the hope that a future lean4 refactor will speed things up. That way we have no hack left to revert.

A particular case: when bumping maxHeartbeats is not needed in the reenableeta branch, hacky solutions should arguably be accepted less often.

[Matthew Ballard]

Yeah, bumping the heartbeats is not necessary on reenableeta.

[Scott Morrison]

I think also one should not add maxHeartbeats unless you've checked in mathlib3 how slow that declaration was, and noted in the porting comment whether this is a regression or just something that was already slow.

[Xavier Roblot]

Scott Morrison said:

I think also one should not add maxHeartbeats unless you've checked in mathlib3 how slow that declaration was, and noted in the porting comment whether this is a regression or just something that was already slow.

I had to add a bunch of maxHeartbeats to port !4#3777. Was I not supposed to do that? What are the other options?

Also, how do you test how slow a declaration is in mathlib3?

[Scott Morrison]

Also, how do you test how slow a declaration is in mathlib3?

set_option profiler true

(I guess you could also set_option timeout N for some N less than the default 100000.)

[Scott Morrison]

Or just eyeball how long the yellow bar takes. :-)

[Scott Morrison]

Usually when I encountered a maxHeartbeats problem, I:

set_option trace.profiler true in
set_option trace.Meta.synthInstance true in
set_option trace.Meta.isDefEq true in

and then look to see if I can see what is going wrong. Sometimes you can guess from the output if there is a bad instance. (e.g. I just noticed https://github.com/leanprover-community/mathlib/pull/18951 from looking at these trace outputs for the timeout that occurred on !4#3780.)

[Scott Morrison]

It's not a science, and if nothing is obvious then just putting the increased timelimits and noting them in the PR description is fine.

[Notification Bot]

12 messages were moved here from #mathlib4 > !4#3388 (revert porting of to_interval_mod) by Eric Wieser.

[Mauricio Collares]

In !4#3457, the expensive steps for the Ideal.Quotient.normedAlgebra instance seem to be AddCommMonoid.toAddMonoid =?= SubNegMonoid.toAddMonoid and SubNegMonoid.toAddMonoid =?= AddMonoidWithOne.toAddMonoid

[Kevin Buzzard]

@Sebastien Gouezel are you able to apply a small permutation to mathlib to make this issue far less prevalent? Is this the sort of question which a small permutation might solve?

[Sebastien Gouezel]

It's all a question of balance: maybe you can do it better here by a small perturbation, but it is likely that it will have some influence elsewhere, which could be positive or negative. The good news is that mathlib is now large enough that such tests are meaningful on the global scale. The bad news is that it takes time.

[Kevin Buzzard]

I'm very impressed that your permutation made so many of the files green in the bench. Was it precalculated or did it come from experimentation?

[Scott Morrison]

A fun data point: of the 31 set_option maxHeartbeats commands in current master, 29 are not needed in the reenableeta branch. !4#3845.

[Scott Morrison]

If anyone feels like fixing the 2 "genuine" ones, they are src4#CategoryTheory.Limits.pullbackDiagonalMapIso and src4#Matrix.det_mul. Apparently I wasn't actually at master, and one of those is already fixed.

[Heather Macbeth]

Is the reenableeta branch globally faster, on any benchmark?

[Scott Morrison]

Yes, considerably faster.