Code lense on slow declarations

[Kha]

Just testing the waters here: would a code lense showing the processing time for declarations that took more time than profiler.threshold be more valuable to mathlib maintainers and authors than #975 (so that it should be turned on by default)? It should make users more mindful about expensive declarations without spamming into the message log. Because right now I'm in a file with many, sometimes surprisingly expensive declarations.

[digama0]

Oh, that's an interesting idea. It will need tweaking to calibrate how annoying it is; users might not be in the mood to think about performance depending on what they are doing, so I would be inclined to set the threshold fairly high, to signal "this isn't normal", rather than putting it on everything except for trivialities (which I think is what profiler.threshold will give you). The threshold is also somewhat domain specific; what is reasonable for a tactic definition or other simple program might be way too low for a mathlib tactic proof.

[gebner]

I agree with Mario that showing this as a code lens is only useful for extreme cases. And then it shouldn't be based on wall-clock measurements, but on heartbeats. (How to set these thresholds is another question. We want one threshold to fail CI and another to show a code lens.)

An alternative option would be to show some profiling information (heartbeats, seconds) when hovering over the command keyword.

Note that we already have a rough way to identify slow proofs, namely by looking at the orange progress bars.

[gebner]

Incidentally, I have disabled all code lenses in all languages because I think they're extremely annoying and only take up precious vertical space, except for one: the version lens extension which augments package.json files and shows the latest released version in a code lens. The code lens is also clickable so that you can upgrade to the latest version with a single click.