Crazy unification quests

Stream: mathlib4

[Patrick Massot]

The following code snippet works as you expect

--import Mathlib
import Mathlib.Data.Complex.Exponential

open Real
--set_option trace.Meta.isDefEq true in
example (x y z w u : ℝ) (bound : x * exp y ≤ z + exp w) (h : w ≤ u) :  x * exp y ≤ z + exp u := by
  sorry

But uncommenting the import Mathlib makes elaborating the example very slow. Uncommenting also the tracing line makes Lean very slow because it tries to generate huge traces, full of completely crazy unification tasks like SlashInvariantFormClass ℝ ?m.138 ?m.139 =?= SlashInvariantFormClass ?m.153 ?m.154 ?m.155 .

[Patrick Massot]

This is related to the exponential function. Removing all exp kills the issue. So it seems that importing modular forms make Real.exp crazily slow.

[Patrick Massot]

@Chris Birkbeck

[Chris Birkbeck]

Oh thats really weird. When making the SlashInvariantFormClass I had basically copied what was done for Schwartz functions FunLike and ContinuousMapClass (if I remember correctly), so I dont know why this would cause problems and not that

[Chris Birkbeck]

The only place where Real.exp shows up in the Modular forms folder is in the JacobiTheta files, but I don't know why that would make it look for SlashInvariantFormClass instances (if thats what its doing)

[Eric Wieser]

As an aside, docs#SlashInvariantFormClass seems to have dropped all the arguments to FunLike on the floor:

image.png

[Jireh Loreaux]

Eric, I think that happens with everything. e.g., docs#CommRing (it says "extends Ring" not "extends Ring α")

[Scott Morrison]

We need more integration tests, i.e. files in test/ that import Mathlib and then do basic stuff, guarded by a timer.