Adding `import Mathlib` makes Finsupp.support.max' timeout

Stream: general

[Aaron Hill]

The following code compiles almost instantly (0.03 seconds on lean web):

import Mathlib.Data.Finsupp.Defs
import Mathlib.Data.Finsupp.Notation

set_option trace.profiler true

example: True := by
  have hsupp: (((-fun₀ | (0 : ℕ) => (1 : ℤ)) + fun₀ | 1 => (1 : ℤ)) : (ℕ →₀ ℤ)).support.Nonempty := by
    sorry
  let a := (((-fun₀ | (0 : ℕ) => (1 : ℤ)) + fun₀ | 1 => (1 : ℤ)) : (ℕ →₀ ℤ)).support.max' hsupp
  trivial

However, adding an import Mathlib line below the existing imports makes the example hit "(deterministic) timeout at whnf, maximum number of heartbeats (200000) has been reached" :

import Mathlib.Data.Finsupp.Defs
import Mathlib.Data.Finsupp.Notation
import Mathlib

set_option trace.profiler true

example: True := by
  have hsupp: (((-fun₀ | (0 : ℕ) => (1 : ℤ)) + fun₀ | 1 => (1 : ℤ)) : (ℕ →₀ ℤ)).support.Nonempty := by
    sorry
  let a := (((-fun₀ | (0 : ℕ) => (1 : ℤ)) + fun₀ | 1 => (1 : ℤ)) : (ℕ →₀ ℤ)).support.max' hsupp
  trivial

Looking at the trace output, it seems to be spending almost all of the time inside [Meta.isDefEq] [12.020135] 💥️ (-?m.1031 + ?m.1034).support.Nonempty =?= ((-fun₀ | 0 => 1) + fun₀ | 1 => 1).support.Nonempty, and considers a large number of Finset-related definitions. However, I'm not familiar enough with lean/mathlib to determine exactly what's going on.

The example is quite sensitive to the way the proof is written - using sorry instead of hsupp, or removing the negative sign, dramatically speeds it up.

[Kevin Buzzard]

This is fast:

import Mathlib

set_option trace.profiler true

example: True := by
  let foo := (((-fun₀ | (0 : ℕ) => (1 : ℤ)) + fun₀ | 1 => (1 : ℤ)) : (ℕ →₀ ℤ))
  have hsupp: foo.support.Nonempty := by
    sorry
  let a := foo.support.max' hsupp
  trivial

if you're just looking for a workaround

[Aaron Hill]

Yeah, either that or just using an inline sorry is enough to unblock me. I'm still curious about the original problem, though

[Kevin Buzzard]

If you're curious enough to find the actual file which causes the explosion (i.e. importing the file makes it slow, importing all the imports of that file makes it quick) then that would be the next step.

[Aaron Hill]

Are there any tools to help do that, or should I just start manually importing files referenced in the trace messages?

[Kevin Buzzard]

For example it's still quick after import Mathlib.Tactic which imports a huge amount of mathlib, which is an indication that it's not just "the more you import, the slower you get". My guess is that there is one "bad" declaration somewhere which is causing you a lot of grief and isolating it would be great (esp for you).

As for tools, the way I usually do this is to put the contents of Mathlib.lean into the file (7000+ lines) and then just start deleting 1000-line chunks and play around like that.

[Aaron Hill]

I'll give that a try

[Kevin Buzzard]

import Mathlib.Data.DFinsupp.Notation

makes it slow

[Kevin Buzzard]

In fact that's the answer, because importing only the imports for that makes it quick

[Kevin Buzzard]

import Mathlib.Data.DFinsupp.Defs
import Mathlib.Data.Finsupp.Notation

-- Here are around 18 lines from Data.DFunsupp.Notation
namespace DFinsupp

open Lean Parser Term

-- either comment out this to fix the slowness
attribute [term_parser] Finsupp.stxSingle₀ Finsupp.stxUpdate₀

-- or comment out this to fix the slowness
/-- `DFinsupp` elaborator for `single₀`. -/
@[term_elab Finsupp.stxSingle₀]
def elabSingle₀ : Elab.Term.TermElab
  | `(term| single₀ $i $x) => fun ty? => do
    Elab.Term.tryPostponeIfNoneOrMVar ty?
    let .some ty := ty? | Elab.throwUnsupportedSyntax
    let_expr DFinsupp _ _ _ := ← Meta.withReducible (Meta.whnf ty) | Elab.throwUnsupportedSyntax
    Elab.Term.elabTerm (← `(DFinsupp.single $i $x)) ty?
  | _ => fun _ => Elab.throwUnsupportedSyntax

end DFinsupp

set_option trace.profiler true

example: True := by
  have hsupp: (((-fun₀ | (0 : ℕ) => (1 : ℤ)) + fun₀ | 1 => (1 : ℤ)) : (ℕ →₀ ℤ)).support.Nonempty := by
    sorry
  let a := (((-fun₀ | (0 : ℕ) => (1 : ℤ)) + fun₀ | 1 => (1 : ℤ)) : (ℕ →₀ ℤ)).support.max' hsupp
  trivial

@Eric Wieser any ideas on how to continue? The example times out as it stands (or with import Mathlib.Data.DFinsupp.Notation) but if you remove some random stuff from Mathlib.Data.DFinsupp.Notation then it's fine.

[Aaron Hill]

I wonder if this is related to the fact that DFinsupp and Finsupp both use the single₀ syntax internally

[Eric Wieser]

I think the HAdd heterogenous add is to blame here, and you need to annotate both operands

[Eric Wieser]

Indeed the shared notation is the other half of the puzzle

[Eric Wieser]

If we deleted Finsupp and used DFinsupp everywhere then this problem would go away :upside_down:

[Aaron Hill]

Naively, I would have expected the fun_0 expressions to behave 'the same way' in hsupp and a - that is, either both or neither would be slow to elaborate. Why does HAdd end up causing problems in that snippet, but not with hsupp alone or max' sorry alone?

[Eric Wieser]

I'm not too sure. For what it's worth, let a := (Finsupp.support _).max' hsupp is fast

[Eric Wieser]

As is let a := ((Finsupp.support (((-fun₀ | (0 : ℕ) => (1 : ℤ)) + fun₀ | 1 => (1 : ℤ)) : (ℕ →₀ ℤ))).max' :) hsupp