slow command elab

Stream: lean4

[James Gallicchio]

Fair warning: I'm generating these declarations automatically, so they're not super pretty, but why does this take a few seconds to compile?

EDIT: cleaned up version that shows the exponential slowdown

set_option profiler.threshold 2
set_option profiler true

def oops
  (x0 : Option String)
  (x1 : Option String)
  (x2 : Option String)
  (x3 : Option String)
  (x4 : Option String)
  (x5 : Option String)
  (x6 : Option String)
  (x7 : Option String)
  (x8 : Option String)
  (x9 : Option String)
  (y0 : Option String)
  (y1 : Option String)
  (y2 : Option String)
  :  List String
  :=
  let x0 := Option.map toString x0
  let x1 := Option.map toString x1
  let x2 := Option.map toString x2
  let x3 := Option.map toString x3
  let x4 := Option.map toString x4
  let x5 := Option.map toString x5
  let x6 := Option.map toString x6
  let x7 := Option.map toString x7
  let x8 := Option.map toString x8
  let x9 := Option.map toString x9
  let y0 := Option.map toString y0
  let y1 := Option.map toString y1
  let y2 := Option.map toString y2
  List.filterMap  (@id (Option String))
    [ x0.map (fun s => "x0" ++ s)
    , x1.map (fun s => "x1" ++ s)
    , x2.map (fun s => "x2" ++ s)
    , x3.map (fun s => "x3" ++ s)
    , x4.map (fun s => "x4" ++ s)
    , x5.map (fun s => "x5" ++ s)
    , x6.map (fun s => "x6" ++ s)
    , x7.map (fun s => "x7" ++ s)
    , x8.map (fun s => "x8" ++ s)
    , x9.map (fun s => "x9" ++ s)
  --, y0.map (fun s => "y0" ++ s)
  --, y1.map (fun s => "y1" ++ s)
  --, y2.map (fun s => "y2" ++ s)
    ]

This is simplified from what I'm auto-generating. The Option.map lines are idempotent, but if you remove them it speeds up. It also speeds up if you remove some elements from the list.

[James Gallicchio]

I'm guessing this is over-eager optimization passes? The compiler traces are generating some truly absurd terms that seem to be from inlining all the option operations.

[James Gallicchio]

with profiler on, threshold 5ms:

compilation new took 22.6ms
compilation of security-advisories/list-global-advisories took 1.99s
elaboration took 17.8ms

Does this mean it is entirely the old compiler?

[James Gallicchio]

Inlining the Option.map lines also makes it fast again. odd :) going to sleep now, I've reached the limits of my knowledge for how to poke at the compiler.

[James Gallicchio]

(edited MWE to show the exponential slowdown -- as you uncomment each line, it goes from a few seconds to not finishing in any reasonable time)