Lean Mac OS Ventura (Intel) CPU usage

Stream: lean4

[Shreyas Srinivas]

This is in #general because I am not sure where it belongs. Often when I am working on a proof in lean 4 (with mathlib), after all the setup is complete, if I make an error, lean's CPU usage goes up. On activity monitor, I have seen %CPU go as high as 1400. This number stays high even a few minutes after the bug has been fixed and the proof works. I am not using simp or library_search like tactics that would have to search all of mathlib. My question: Why does Lean's CPU usage remain high, well after all proofs are complete and lean has checked them?

[Shreyas Srinivas]

What often works is killing the lean process and restarting it from inside VSCode.

[Shreyas Srinivas]

For instance, right now, I just fixed an error in a file. No other lean files are open. And since the last error came up, lean has had 17 open threads and has been causing my system to heat up.

[Shreyas Srinivas]

I did not encounter this issue on a different linux machine.

[Alex J. Best]

These sorts of issues are really annoying but really hard to debug without a way to reproduce them reliably. Do you think you can produce a test case that shows this behavior every time? Ideally this would be a small self contained project with simple instructions to produce this spike in usage every time

[Shreyas Srinivas]

It is hard to produce a test case that might reliably reproduce this bug as you say. I encountered this issue when writing long propositions involving Finsets, powersets of Finsets, and quantifiers over subsets of Finsets.

[Shreyas Srinivas]

But the quantifier depth was \leq 2

[Shreyas Srinivas]

Shreyas Srinivas said:

What often works is killing the lean process and restarting it from inside VSCode.

The reason it is hard for me to reliable reproduce the issue is that while the CPU usage stays high for a long time after fixing proofs or expressions, as soon as I kill the lean process and restart it, for the exact same code, the CPU usage is suddenly low.

[Shreyas Srinivas]

So the issue might very well not be with the specific code, just that somewhere deep down some threads which were assigned some work, were never stopped long after the need for those threads passed.

[Shreyas Srinivas]

For example after restarting now, I still have 17 threads in the lean process, but CPU usage is 0%.

[Shreyas Srinivas]

Here's the file I am working on :

import Mathlib


namespace IndivisibleGoods

  def Agents (α : Type) := Finset α

  def Goods (β : Type) := Finset β


  structure Valuation (α β: Type) where
    values : Agents α → Set (Goods β) → NNReal
    empty_zero_val : ∀ i : Agents α, values i ∅ = 0

  structure Allocation (α β : Type) where
    alloc : Goods β → Agents α


  structure Alloc
    (α β : Type) where
      alloc : Goods β → Agents α
      valuation : Agents α → Set (Goods β) → NNReal
      empty_zero_val : ∀ i : Agents α, valuation i ∅ = 0

  def Monotonicity (v : Valuation α β) := ∀ (i : Agents α) (X Y : Set (Goods β)) (_ : X ⊆ Y),
    v.values i X ≤ v.values i Y

  def Submodularity (v : Valuation α β) := ∀ (i : Agents α) (X Y : Set (Goods β)),
      v.values i (X ∪ Y) ≤ v.values i X + v.values i Y - v.values i (X ∩ Y)


  def Additivity (v : Valuation α β) := ∀ (i : Agents α) (X Y : Set (Goods β)), v.values i (X ∪ Y) = v.values i X + v.values i Y - v.values i (X ∩ Y)


  theorem additive_alloc_monotone_alloc : ∀ (v : Valuation α β), Additivity v → Monotonicity v := by
    unfold Additivity Monotonicity
    intros valuation additivity agent
    intros X Y X_subseteq_Y
    have additivity' := additivity agent X (Y \ X)
    have X_union_Y_eq_Y : X ∪ Y = Y := by
      exact Set.union_eq_self_of_subset_left X_subseteq_Y
    have X_union_exists_Y : X ∪ (Y \ X) = Y := by
      exact Set.union_diff_cancel X_subseteq_Y
    have X_intersect_Y_minus_X : X ∩ (Y \ X) = ∅ := by
      exact Set.inter_diff_self X Y
    rw[X_intersect_Y_minus_X, X_union_exists_Y, valuation.empty_zero_val] at additivity'
    simp only [ge_iff_le, nonpos_iff_eq_zero, add_eq_zero_iff, tsub_zero] at additivity'
    apply le_iff_exists_add.mpr
    use Valuation.values valuation agent (Y \ X)
    exact additivity'



  def bundle (a : Allocation α β) (i : Agents α): Set (Goods β):=
    {x : Goods β | a.alloc x = i}

  -- EF = Envy Free

  def isEnvyRemovalSet {α β : Type} (v : Valuation α β) (a : Allocation α β) (i j : Agents α) (X : Set (Goods β)) : Prop := X ⊆ bundle a j ∧ v.values i (bundle a i) ≥ v.values i ((bundle a j) \ X)

  def isMinimalSet {α : Type} (X : Finset α) (P : Set α → Prop) : Prop := P X ∧ ∀ Y : Set α, Y ⊆ X → ¬ P Y

  def isMinimumSet {α : Type} (X : Finset α) (P : Set α → Prop) : Prop :=
  P X ∧ ∀ Y : Finset α, Y.card < X.card → ¬ P Y

  def isMinimalEnvyRemovalSet {α β : Type} (v : Valuation α β) (a : Allocation α β) (i j : Agents α) (X : Finset (Goods β)) : Prop := isMinimalSet X (isEnvyRemovalSet v a i j)



-- CPU Consumption goes up. There is a type error in this definition. The error is not shown. Instead VSCode marks every line from this point with a yellow bar on the left
  def isMinimumEnvyRemovalSet {α β : Type} (a : Alloc α β) (i j : Agents α) (X : Finset (Goods β)) : Prop := isMinimumSet X (isEnvyRemovalSet a i j)

  def EF_alloc (v : Valuation α β) (a : Allocation α β) : Prop :=
    ∀ (i j : Agents α) (_ : i ≠ j), (v.values i (bundle a i)) ≥ (v.values i (bundle a j))

  def EF1 (v : Valuation α β) (a : Allocation α β) : Prop :=
    ∀ (i j : Agents α) (_ : i ≠ j), ∃ g ∈ bundle a j, (v.values i (bundle a i)) ≥ (v.values i ((bundle a j) \ {g}))

  def EFX (v : Valuation α β) (a : Allocation α β) : Prop :=
    ∀ (i j : Agents α) (_ : i ≠ j), ∀ g ∈ bundle a j, (v.values i (bundle a i)) ≥ (v.values i ((bundle a j) \ {g}))

  theorem non_EF_allocs_exist: ∃ (a : Alloc α β), ¬ EF_alloc a := by sorry

end IndivisibleGoods

[Shreyas Srinivas]

This below is the fix:

-- CPU Consumption goes up. There is a type error in this definition. The error is not shown. Instead VSCode marks every line from this point with a yellow bar on the left
  def isMinimumEnvyRemovalSet {α β : Type} (v : Valuation α β) (a : Allocation α β) (i j : Agents α) (X : Finset (Goods β)) : Prop := isMinimumSet X (isEnvyRemovalSet v a i j)

[Shreyas Srinivas]

Here is the CPU usage after a minute of fixing the error. VScode still shows the lines below the comment in yellow:
telegram-cloud-photo-size-5-6091620157244945458-y.jpg

[Shreyas Srinivas]

Further, after letting this happen for a few minutes. All I did was kill this process , go to VSCode, and restart lean through the VSCode notification. It immediately started and accepted the corrected definition.

[Shreyas Srinivas]

No more yellow lines

[Shreyas Srinivas]

Now it is able to highlight the error in the last line without CPU usage climbing up

[Sebastian Ullrich]

It would be interesting to get stack traces from these stuck threads, but the issue most likely is that elaboration of a single command currently cannot be interrupted. So if you manage to temporarily produce very expensive input, threads can get stuck processing it. We need more interaction between the elaborator and language server to fix this.

[Notification Bot]

This topic was moved here from #general > Lean Mac OS Ventura (Intel) CPU usage by Sebastian Ullrich.

[Shreyas Srinivas]

Sebastian Ullrich said:

It would be interesting to get stack traces from these stuck threads, but the issue most likely is that elaboration of a single command currently cannot be interrupted. So if you manage to temporarily produce very expensive input, threads can get stuck processing it. We need more interaction between the elaborator and language server to fix this.

In general this happens whenever I am either writing Predicates or proofs where there is quantification over sets or finsets.

[Shreyas Srinivas]

I reconstructed the above example to illustrate the point with two errors, one with such quantification and another without. The server only got stuck on the one with such (higher order?) quantification

[Shreyas Srinivas]

As an aside, I wrote this file to demonstrate lean4 to a group of colleagues who work on fair division problems. So this issue kind of defeats the purpose, if I can't show them how lean catches mistakes or checks proofs

[Shreyas Srinivas]

@Sebastian Ullrich Additional information : I opened this in the lean4 web playground. It worked perfectly well. So this issue might be specific to macOS