slow compilation of logInfo

Stream: lean4

[Jovan Gerbscheid]

The following definition takes around 2 seconds to compile:

import Lean
open Lean Elab.Tactic
set_option profiler true
abbrev M := TacticM
def f : M Unit := logInfo ""

Why is this and can it be fixed?

[Kim Morrison]

set_option profiler.threshold 0

reveals that all the time is spent in compilation.

[Kim Morrison]

It seems to be a one-off cost: adding def g : M Unit := logInfo "" adds no time.

[Kim Morrison]

Could you open a bug report?

(Please say explicitly that without using the abbrev it is fine, to be clear.)

[Mario Carneiro]

Scott Morrison said:

It seems to be a one-off cost: adding def g : M Unit := logInfo "" adds no time.

It appears to be the cost of specializing Lean.log and Lean.logAt for a new monad

[Mario Carneiro]

the new compiler doesn't seem to have as much trouble, so I'm guessing this won't be fixed

[Jovan Gerbscheid]

What is the new compiler? Will it come with the next release of Lean?

[Mauricio Collares]

That's item 21 in https://lean-fro.org/about/roadmap/, corresponding to the "depends on new code generator" label in the Lean 4 issue tracker. The roadmap says work on it is "[re]starting on year 2", but I don't know if year 1 started when the FRO was founded (late July) or when the roadmap was published (late November, so basically year 1 = 2024).

[Sebastian Ullrich]

The former