notation3 takes an age

Stream: mathlib4

[Kevin Buzzard]

import Mathlib.NumberTheory.Cyclotomic.PID

local notation3 "K" => CyclotomicField 3 ℚ

count_heartbeats in -- Used 958 heartbeats, which is less than the current maximum of 200000.
#check (IsCyclotomicExtension.zeta_spec 3 ℚ K).toInteger - 1

count_heartbeats in -- Used 131863 heartbeats, which is less than the current maximum of 200000.
local notation3 "t" => (IsCyclotomicExtension.zeta_spec 3 ℚ K).toInteger - 1

This innocuous (to me) use of notation3 to define t is taking 5 seconds to compile on someone's laptop. Whatever is going on?

[Kyle Miller]

If you do set_option pp.all true for the #check, you can see that (IsCyclotomicExtension.zeta_spec 3 ℚ K).toInteger is a much larger term than you might expect.

I suspect notation3 is spending a lot of time making a matcher for that term for the delaborator. You can see the matcher it constructs if you set set_option trace.notation3 true.

[Arend Mellendijk]

Two observations:

import Mathlib.NumberTheory.Cyclotomic.PID

local notation3 "K" => CyclotomicField 3 ℚ
#check (IsCyclotomicExtension.zeta_spec 3 ℚ K).toInteger - 1

set_option trace.profiler true in
local notation3 "t" => (IsCyclotomicExtension.zeta_spec 3 ℚ K).toInteger - 1

The profiler starts with this and then goes on for another 8000 or so lines displaying the definition of the pretty printer

[Elab.command] [5.711137s] local notation3"t" => (IsCyclotomicExtension.zeta_spec 3 ℚ K).toInteger - 1 ▼
  [] [0.038343s] macro_rules
        | `(t) => `((IsCyclotomicExtension.zeta_spec 3 ℚ K).toInteger - 1) ▶
  [step] [0.076106s] expected type: <not-available>, term
      (IsCyclotomicExtension.zeta_spec 3 ℚ K).toInteger - 1 ▶
  [] [5.538922s] /-- Pretty printer defined by `notation3` command. -/
      def termT.delab✝ : Delab✝ :=
        whenPPOption✝ getPPNotation✝ <|
          getExpr✝ >>= fun e✝ =>
            (matchApp✝
                    (matchApp✝
                      (matchApp✝ (...)

Moreover disabling the pretty printer for the second notation makes it fast:

import Mathlib.NumberTheory.Cyclotomic.PID

local notation3 "K" => CyclotomicField 3 ℚ

count_heartbeats in -- Used 958 heartbeats, which is less than the current maximum of 200000.
#check (IsCyclotomicExtension.zeta_spec 3 ℚ K).toInteger - 1

count_heartbeats in -- Used 461 heartbeats, which is less than the current maximum of 200000.
local notation3 (prettyPrint := false) "t" => (IsCyclotomicExtension.zeta_spec 3 ℚ K).toInteger - 1

[Kyle Miller]

Thanks for profiling.

Do I understand correctly from the profiler that it's the elaboration of the def termT.delab... function that's taking the bulk of the time? That means it's not the generation of the matcher per se, but the elaboration of it after it generates the syntax.

[Kyle Miller]

I hope to make a more efficient delaboration generator one day and upstream it into the notation command.

There are some questions about what it means to match. The notation3 command is conservative about what it accepts, and sometimes too conservative. With this example, it's aiming to make sure that it will only pretty print CyclotomicField 3 ℚ as K if the term is exactly what CyclotomicField 3 ℚ would elaborate to. That's why it's really going deep into the instances and creating this massive matcher. Probably it's an OK approximation to not match instances, because we should assume that instances are the canonical ones.

[Kevin Buzzard]

In what world does $\frac{\sqrt{-3}-3}{2}$ take 1800 lines of code to display? Has someone done something wrong here?

[Kyle Miller]

I expect it's the instances involved. There's a lot of algebraic structure to state this.

[Kevin Buzzard]

It's here if anyone wants to marvel at it.

[Kyle Miller]

Once #11700 builds, could you test out your notation on that branch @Kevin Buzzard?

[Kyle Miller]

I just tested it myself. The t notation now takes 5% of the number of heartbeats as before. I spot checked how various notation3s pretty print in mathlib, and while that's not a perfect test, I didn't notice anything broken.