count_heartbeats for all declarations in a file?

Stream: mathlib4

[Michael Stoll]

Is there a way to obtain a heartbeats count for every declaration in a file without having to add count_heartbeats in before every single one?
A bare count_heartbeats at the beginning of the file gives an error "unexpected end of input; expected 'in'". It would be nice if that could be made to work.

[Damiano Testa]

I also wanted this for some time: #20421.

[Damiano Testa]

Jon reviewed the PR (thank you very much!) and raised a question of naming: should the "persistent" form of count_heartbeats in be called count_heartbeats or set_option linter.countHeartbeats true?

If the command had started as a linter in the first place, I would have definitely not introduced the shorter spelling. However, for discoverability and "historical reasons", I am slightly more in favor of having the count_heartbeats abbreviation.

I'll set up a poll!

[Damiano Testa]

/poll What should the persistent form of count_heartbeats in be called?
count_heartbeats
set_option linter.countHeartbeats

[Damiano Testa]

Once the poll results are in, I will in any case add pointers to all names in all relevant doc-strings.

[Damiano Testa]

(Notice that I missed a true in the poll alternative set_option linter.countHeartbeats *true*!)

[Kim Morrison]

It should be #count_heartbeats, shouldn't it?

[Damiano Testa]

An initial version of the PR had the #, but then it was pointed out that count_heartbeats in does not have the #, so I removed it.

[Damiano Testa]

Maybe I should add the hash to both commands...

[Kim Morrison]

Damiano Testa said:

Maybe I should add the hash to both commands...

Yes please.

[Damiano Testa]

Ok, I aligned the two commands: they now all use #count_heartbeats ....

[Damiano Testa]

#20421 has been merged. If you write #count_heartbeats in most Mathlib files, each following declaration will emit a count of the heartbeats that Lean takes to process it. This should help with figuring out speed ups/downs over whole files.

[Kevin Buzzard]

I have the following use case: I'd like to get some kind of a measure for how much it costs to compile a file, without bothering the speedcenter and without using a command line time. Is this possible?

I tried to count the total number of heartbeats used in everyone's favourite file RingTheory/Kaehler/JacobiZariski.lean, so I stuck #countheartbeats at the top expecting to get a number, but in practice I get 31 messages, most of which are claims that something either took exactly 344 heartbeats, exactly 347 heartbeats or exactly 560 heartbeats. Is this tool working correctly? This is the slowest file in mathlib, I would have expected some of these numbers to be much bigger especially given that some declarations take many seconds to compile. For example

'CotangentSpace.compEquiv' used 347 heartbeats, which is less than the current maximum of 200000.

but the profiler says that this declaration takes 2.8 seconds.

[Jon Eugster]

that clearly does not look right. I think this line picks out the wrong message

elabCommand (← `(command| #count_heartbeats in $(⟨stx⟩)))
msgs := (← get).messages.unreported.toArray.filter (·.severity != .error)

but I don't understand yet what's happening. I believe it's displaying the number from the first declaration of a given section/namespace over and over again.

[Christian Merten]

Kevin Buzzard said:

I have the following use case: I'd like to get some kind of a measure for how much it costs to compile a file, without bothering the speedcenter and without using a command line time. Is this possible?

I tried to count the total number of heartbeats used in everyone's favourite file RingTheory/Kaehler/JacobiZariski.lean, so I stuck #countheartbeats at the top expecting to get a number, but in practice I get 31 messages, most of which are claims that something either took exactly 344 heartbeats, exactly 347 heartbeats or exactly 560 heartbeats. Is this tool working correctly? This is the slowest file in mathlib, I would have expected some of these numbers to be much bigger especially given that some declarations take many seconds to compile. For example

'CotangentSpace.compEquiv' used 347 heartbeats, which is less than the current maximum of 200000.

but the profiler says that this declaration takes 2.8 seconds.

Does Sebastian's suggestion, i.e.lake env perf stat lean Mathlib/RingTheory/Kaehler/JacobiZariski.lean not work for you? That gives you numbers of instructions.

[Kevin Buzzard]

(a) no not out of the box: after struggling to install perf I got

Error:
Access to performance monitoring and observability operations is limited.
Consider adjusting /proc/sys/kernel/perf_event_paranoid setting to open
access to performance monitoring and observability operations for processes
without CAP_PERFMON, CAP_SYS_PTRACE or CAP_SYS_ADMIN Linux capability.
More information can be found at 'Perf events and tool security' document:
https://www.kernel.org/doc/html/latest/admin-guide/perf-security.html
perf_event_paranoid setting is 4:
  -1: Allow use of (almost) all events by all users
      Ignore mlock limit after perf_event_mlock_kb without CAP_IPC_LOCK
>= 0: Disallow raw and ftrace function tracepoint access
>= 1: Disallow CPU event access
>= 2: Disallow kernel profiling
To make the adjusted perf_event_paranoid setting permanent preserve it
in /etc/sysctl.conf (e.g. kernel.perf_event_paranoid = <setting>)

(which is unfortunately too intimidating for me) and (b) in this particular case, Sebastian's suggestion was made after I'd opened the PR to mathlib to run the benchmark bot anyway :-)

[Kevin Buzzard]

More importantly, after Jon's observation I can confirm that #count_heartbeats at the top of the file gives me (amongst other things)

'CotangentSpace.compEquiv' used 347 heartbeats, which is less than the current maximum of 200000.

but #count_heartbeats in directly before the CotangentSpace.compEquiv declaration gives

Used 58933 heartbeats, which is less than the current maximum of 200000.

so there's definitely something up with the global option.

[Jon Eugster]

Ah I think it is trying to re-elaborate an existing theorem and the 343 heartbeats are how long it takes lean to conclude

error: 'Algebra.Generators.kerCompPreimage' has already been declared

[Damiano Testa]

Jon Eugster said:

Ah I think it is trying to re-elaborate an existing theorem and the 343 heartbeats are how long it takes lean to conclude

error: 'Algebra.Generators.kerCompPreimage' has already been declared

I thought that I had taken care of this, since I distinctly remember seeing that it still elaborated the declaration and only when it was adding it to the environment it checked that it was already present.

[Damiano Testa]

I may have picked the wrong heartbeat count, though.

[Damiano Testa]

(And it might also be that this is another situation where Elab.async is giving me a headache!)

[Jon Eugster]

Damiano Testa said:

distinctly remember seeing that it still elaborated the declaration and only when it was adding it to the environment it checked that it was already present.

That's interesting, did that maybe change recently? I also don't see any interactive goal states in the infoview, suggesting that the proof is not elaborated:

theorem A : True := by
  skip
  skip
  exact True.intro
  done

theorem A : True := by. -- error: 'A' has already been declared
  skip
  skip     -- no goal state here
  exact True.intro
  done

I've created #21182 which just puts the declaration inside a namespace before re-elaboration, which seems to work. I'll test it on Kevin's favourite file once CI is done.

[Damiano Testa]

I have used the namespace trick, it works most of the times, but interacts weirdly with autonamespacing, self-referentiality and a couple of other edge cases.

Anyway, better than failing always!

[Jon Eugster]

You're right, maybe that's not good enough. Do you have a better approach usually?

Also, i noticed that the linter does not go into open ... in or variable ... in either yet.

[Damiano Testa]

I do not have a better approach, though I have a combination of approaches that covers most(?) cases! Anyway, I also stopped worrying about such issues since there should be at some point there is the hope that lean4#6076 will magically give access to quite a bit more of information, and possibly the ability to elaborate its code before the command being elaborated is actually elaborated.

[Damiano Testa]

Should that happen, you would simply elab the heartbeats inside a withoutModifyingEnvironment and then continue with the rest.

[Damiano Testa]

The conclusion is that all the workarounds that I know fail in some way or another, so I would not worry too much about making this perfect.

[Damiano Testa]

If it warns about the cases where there was an error, it is still better to add manually a #count_heartbeats in before the offending declarations anyway.

[Damiano Testa]

(In case you are curious, in some branch, I also have a Syntax --> Syntax transformation that converts declarations to examples, to avoid messing with the environment... needless to say, that is also fallible!)

[Damiano Testa]

However, recursive calls, dot-notation, previously opened namespaces and the declaration that was just added to the environment all conspire against any of these solutions really working robustly.

[Sebastian Ullrich]

If the goal is to find slow definitions, have you considered using the trace profiler? No need to reelaborate anything, or to think in heartbeats

[Jon Eugster]

(to be explicit, that's set_option trace.profiler true at the top of the file which gives you time in seconds for individual declarations)

[Kevin Buzzard]

Christian Merten said:

Does Sebastian's suggestion, i.e.lake env perf stat lean Mathlib/RingTheory/Kaehler/JacobiZariski.lean not work for you? That gives you numbers of instructions.

I bravely opened a file as root and changed a number to a random smaller number and now it seems to be working...

[Christian Merten]

Kevin Buzzard said:

Christian Merten said:

Does Sebastian's suggestion, i.e.lake env perf stat lean Mathlib/RingTheory/Kaehler/JacobiZariski.lean not work for you? That gives you numbers of instructions.

I bravely opened a file as root and changed a number to a random smaller number and now it seems to be working...

I have this line

kernel.perf_event_paranoid = -1

in my /etc/sysctl.conf which enables perf for non-root users. I don't know the security implications of this though. After that you need to do sysctl --system to reload the sysctl variables.

[Kevin Buzzard]

#23905 tracks the broken linter.countHeartbeats issue.

Sebastian Ullrich said:

If the goal is to find slow definitions, have you considered using the trace profiler? No need to reelaborate anything, or to think in heartbeats

The trace profiler is not a good solution to the problem I'm currently trying to analyse. The question is: did a certain commit make a file quite a bit faster because the speedcenter is reporting this and it's unexpected; if it's true I'd like to understand more. Manually checking heartbeats on many declarations it seems that most of them are unchanged, but a few did get 10% quicker. The profiler will however report different timings for every declaration due to noise.

A precise question: did Mathlib.Algebra.Order.Field.Basic actually just get 9.7% faster (see here) and if so, why?

lake env perf stat lean Mathlib/Algebra/Order/Field/Basic.lean only gives me per-file stats, getting a per-declaration heartbeat count really seems like the way to analyse such questions, especially because most declarations did not change (and because of course I don't have any understanding of the output of lake env perf stat, I am looking for changes in typeclass inference behaviour and not something low-level)

[Sebastian Ullrich]

If by "actually ... faster" you mean wall-clock time (i.e. the only time metric we're interested in the end as humans), I'm not sure heartbeats will be helpful either. You might want to start by measuring the time lake lean takes on the file in both commits, repeatedly, e.g. using hyperfine

[Sebastian Ullrich]

Do note that the trace profiler can measure heartbeats as well if wall time is too noisy. Measuring instructions would be an interesting extension that should be feasible at least on Linux.

[Kevin Buzzard]

I want to measure an approximation of how long Lean takes on each declaration so I can see precisely which declarations got quicker. The profiler is too noisy. Most of the time the heartbeats won't change, or will change by a very small percentage, but occasionally there will be a big jump. I suspect that what I want is a resolution of #23905 .

[Sebastian Ullrich]

And that's not covered by trace.profiler.useHeartbeats?

[Sebastian Ullrich]

There is one papercut here: You'll likely want to adjust trace.profiler.threshold as well when enabling that option as otherwise the profiling overhead might be too large. "10" is a reasonable threshold in ms but not in heartbeats!

[Kevin Buzzard]

Sebastian Ullrich said:

And that's not covered by trace.profiler.useHeartbeats?

Good to see Lean reporting integers to 6 decimal places here!

[Sebastian Ullrich]

Can never rule out heart palpitations

[Kevin Buzzard]

Right now putting

set_option trace.profiler true
set_option trace.profiler.useHeartbeats true

at the top of Mathlib/Algebra/Order/Field/Basic.lean gives squiggly blue line output for the first 300 or so lines of this 900 line file, and then it stops

[Sebastian Ullrich]

It's just the squigglies that give up, the trace is still there for me
image.png

[Aaron Liu]

Maybe you reached the squiggle limit for that file

[Aaron Liu]

It looks like the limit is 500 squiggles / file