compilation performance issue

Stream: lean4

[Thomas Murrills]

I noticed that the following very small example takes several seconds to compile:

import Lean

set_option profiler true

open Lean Meta Elab Tactic in
example : TacticM Unit := do -- compilation of _example took 4.71s
  for _ in [:5] do
    logInfo ""

Interestingly, simply lowering the monad to TermElabM fixes the issue. (I checked the synthInstance and isDefEq traces and couldn't find much, but there are a lot of traces, so maybe it adds up. Though I'm not sure whether that's counted in compilation time or not in the first place.)

(On web, it seems to take only about 2 seconds.)

This is present on 4.7.0-nightly-2024-02-26.

[Thomas Murrills]

Also, adding pure () at the end of the for loop seems to fix it:

example : TacticM Unit := do -- no trace
  for _ in [:5] do
    logInfo ""
    pure ()

[Henrik Böving]

That doesn't look like too much IR in the trace so this is probably the old compiler being overeager at attempting to do things :tm:. While annoying this will probably only ever get fixed with the new compiler next year-ish.