count_heartbeats CPU usage

Stream: mathlib4

[Floris van Doorn]

@Sven Manthe reported the following to me:
The count_heartbeats command seems to increase Lean's CPU usage when editing the proof until you restart the file.

import Mathlib.Util.CountHeartbeats

count_heartbeats in
theorem test : True := by
  -- type some junk in the next line to increase Lean's CPU usage until you restart the file
  --
  trivial

[Matthew Ballard]

Does this have anything to do with incremental compilation being enabled?

[Floris van Doorn]

Maybe. Is there an option to turn it off?

[Sven Manthe]

Matthew Ballard said:

Does this have anything to do with incremental compilation being enabled?

Probably: I often realized this recently (in non-minimalized situations), but never before incremental proofs were introduced

[Matthew Ballard]

Floris van Doorn said:

Maybe. Is there an option to turn it off?

@Sebastian Ullrich

[Sebastian Ullrich]

It shouldn't directly be relevant, count_heartbeats does not opt into incrementality. But also I can't reproduce, CPU quickly subsides after typing on that line

[Floris van Doorn]

Matthew Ballard said:

Does this have anything to do with incremental compilation being enabled?

It seems not, this also blows up CPU usage for me:

import Mathlib.Util.CountHeartbeats

count_heartbeats in
def foo : Nat :=
  -- type some junk in the next line to increase Lean's CPU usage until you restart the file
  --
  0

[Floris van Doorn]

Sven, can you remind me: are you on Windows as well? Given that Sebastian cannot reproduce it, it would be good to see if it reproduces on all OSes, or whether it is a Windows-only issue.

[Sven Manthe]

Floris van Doorn said:

Sven, can you remind me: are you on Windows as well? Given that Sebastian cannot reproduce it, it would be good to see if it reproduces on all OSes, or whether it is a Windows-only issue.

No, I don't use Windows. More precisely, my VS Code "About" outputs:
Version: 1.74.3
Commit: 97dec172d3256f8ca4bfb2143f3f76b503ca0534
Date: 2023-01-13T15:24:47.250Z
Electron: 19.1.8
Chromium: 102.0.5005.167
Node.js: 16.14.2
V8: 10.2.154.15-electron.0
OS: Linux x64 5.15.0-118-generic
Sandboxed: No

[Michael Stoll]

Could this be related to the VSCode version?

I observed a while ago that in some cases threads were continuing to run using 100% of a core after editing in a file (e.g., in docstrings), and this was building up over time so that my laptop became sluggish (and hot). ("Restart file" helped in this situation.) This behavior began after a new version of VSCode was installed (Linux, in my case) and ended a couple of VSCode versions later.

[Sven Manthe]

Michael Stoll said:

This behavior began after a new version of VSCode was installed (Linux, in my case) and ended a couple of VSCode versions later.

What is your current version (then I could try whether updating fixes this for me)?

[Michael Stoll]

My VSCode version is 1.92.2; so this may be unrelated.

[Michael Stoll]

It could perhaps be some interaction between the VSCode version and the version of the language server.

[Sven Manthe]

I just installed a more recent version of VS Code (1.92.1) from another package manager (both of them seem to be inofficial; I didn't check details) and can't reproduce it with this one

[Sven Manthe]

Some new observations: I could reproduce the issue of increasing CPU usage while editing a proof in a file not containing count_heartbeats. A visible effect that sometimes occurs is that the yellow markers of incremental proofs reset to the beginning of the proof or file at the moment when the CPU usage increases. In contrast to the count_heartbeats problem, this also occurred in the recent version of VS Code. Creating a MWE would be much effort, but if anyone is interested, I can provide non-minimized code that reproduces the issue

[Sebastian Ullrich]

That would be great, I am definitely interested

[Sven Manthe]

Sebastian Ullrich said:

That would be great, I am definitely interested

I invited you to the corresponding gitlab repository and created a separate branch for this issue (the relevant file is mwe3.lean. This file reproduced this issue several times, although I cannot give a precise sequence of steps required for this. I put more details in a comment close to the end of the file)

[Sebastian Ullrich]

@Sven Manthe This doesn't look to be connected to incrementality. Note that when CPU usage spikes despite the orange bar being gone, the header of the info view turns yellow, meaning the time is spent in rendering (at least in this case) the goal, which seems to be very expensive between the conv and dsimp (the dsimp itself seems to be expensive too, just less so, which is probably connected). The odd thing is that this is happening in pretty printing code activated by pp.beta, but I don't see that option being set anywhere. If you could file an issue with public code, that would be great.

[Sven Manthe]

Thank you for having a look, and it's good to know that these problems are not related with the other one. The dsimp being slow can be fixed by adding generalize_proofs before and may be related to https://github.com/leanprover/lean4/issues/5108. (There are also other things happening that may be worth reporting in this project. E.g., linting a single theorem needs >20s.) If that helps, I could publish all the code together with some description of the issues (and I would definitely be happy if some of the performance issues in this project could be fixed on the language/library level), but currently I don't want to create MWEs for issues.

[Sebastian Ullrich]

Ah, I did not make the connection to that issue. Indeed both seems to be bottlenecked on proof term size. Does this description I added to the issue describe your example as well (I didn't look closely)?

filling in proof arguments of functions like help with expensive (big proof-producing) tactics like omega.

[Sven Manthe]

Yes. To avoid XY-problems, let me give an unnecessarily detailed description of my situation.
In this project, I did not follow the mathlib convention of using unbundled types and "junk" values. For example, I defined a type Strategy not as roughly List A -> A, but as (x : List A) -> P x -> {a : A | Q x a} for predicates P, Q. This leads to many propositional arguments to functions. Later in the project I used terms like by omega to fill these arguments, leading to the described performance issues. (Also, the simplifier struggles to work with these kinds of definitions, but this can mostly be fixed by adding manual congr-lemmas and no_index annotations.)
Naïvely, the following might be a quite general metaprogramming solution to all my performance issues and also to https://github.com/leanprover/lean4/issues/5108: Whenever a term of a Prop is generated with by "tactics" as a subterm of a term T, create a new opaque auxiliary definition of the required type and use this definition instead in T. It seems preferable to e.g. tweaking omega to not reuse these proof terms in the issue etc. (Of course, without knowledge of the system or metaprogramming, I don't know how feasible this would be to implement. In some sense it would implement your suggested solution not to use expensive tactics outside of opaque proofs, but would shift the burden from the end user to a metaprogram; at least in my project it becomes infeasible to extract all those proof terms by hand since the statements are much shorter than the proof terms but much longer than the tactic sequences.)

[Sebastian Ullrich]

Indeed, a tactic based on Lean.Meta.abstractNestedProofs may do the trick