Measure is overloaded

Stream: mathlib4

[Floris van Doorn]

The following example is bad:

import Mathlib.MeasureTheory.Measure.MeasureSpaceDef


open MeasureTheory
set_option profiler true
set_option trace.profiler true
set_option trace.Meta.synthInstance true

-- the following line takes 2+ seconds to compile
variable {α : Type _} [MeasurableSpace α] (μ μ₁ μ₂ μ₃ μ₄ μ₅ : Measure α)

variable (α) -- this also takes 2+ seconds to compile

-- every command in this file will take 2 extra seconds to compile

The problem is that docs4#MeasureTheory.Measure is overloaded with docs4#Measure, and for every variable it now attempts an (expensive and failing) type-class problem to find a coercion from Type ?u.2 (the type of α) to ?m.10 → ℕ (the type of the first argument of Measure). Note that variables are recompiled for every new variable/def/theorem/... so this file will probably get very slow

We hit this in !4#4929, but I expect this is a major slowdown in all files using measures.

What should we do to fix this? We should probably do multiple of the following list:
(1) As a temporary workaround, write MeasureTheory.Measure in a lot of places (especially variable commands) instead of Measure
(2) Move Measure to a namespace (Nat.Measure?)
(3) Cache type-class failures in this case
(4) Have a precached failure that Type _ will not coerce to any function (or anything else, probably).
(5) Have x : _root_.Measure α fail without doing any type-class inference: _root_.Measure _ will have type _ → _ → Prop which should never match with Sort _ (I'm very happy if we disallow coercions like this - assuming that we can keep the coercion Set _ >-> Type _)

[Oliver Nash]

Wow, great find. I definitely support 2, probably also 3--5, and maybe even 1. Who can action this?

[Floris van Doorn]

Continuing the example:

-- takes ~2.5s to compile (since it also parses variables)
example : 1 = 1 := rfl

-- takes ~10s to compile, apparently it parses all the variables 4 times?
notation:67 f " ⋆ " => id f

Is it intended that the notation command parses the variable list 4 separate times (at least, that's what seems to be happening)?

[Floris van Doorn]

!4#4929 takes 5m 46s to build using Measure and 1m 50s to build using MeasureTheory.Measure.

[Sebastian Ullrich]

Floris van Doorn said:

Is it intended that the notation command parses the variable list 4 separate times (at least, that's what seems to be happening)?

That's an "interesting" side effect of notation expanding into multiple primitive declarations

[Floris van Doorn]

Of course, the slowdown would be greatly mitigated by

(6) do not re-elaborate the variables for every command

but I don't know the reasons for the Lean 4 behavior of the variable command, so this option might be bad.

[Sebastian Ullrich]

I may be responsible for suggesting "variables should just be inserted syntactically, like macros!" in order to avoid all our problems with them in Lean 3. Now we have new problems...

[Floris van Doorn]

In !4#5100 I changed all occurences in variable lines. I think that will already have a big impact, and this PR can be used to measure how big. lean4#2275 implements option (2).