Exponential blowup in compilation time

Stream: lean4

[Leni Aniva]

I have a series of function calls like this:

let (.some boo, a) <- function boo a | fail "incorrect"
checkEq boo ..
let (.some boo, a) <- function boo a | fail "incorrect"
checkEq boo ..
let (.some boo, a) <- function boo a | fail "incorrect"
checkEq boo ..
let (.some boo, a) <- function boo a | fail "incorrect"
checkEq boo ..

and with every pair of lines, the compilation time seems to exponentially increase. e.g. with just two pairs, it generated 78M of prof data, but with three pairs it generated 8G of data, and 4 pairs generated 80G of data.

I profiled the lean executable running on this particular file using perf, and these functions have the highest cycle count:
image.png

With the highest one being lean::replace_rec_fn::apply(lean::expr const&, unsigned int).

Is there a way pinpoint the root cause of the blowup?

[Cameron Zwarich]

Which version of Lean are you using, and what is the full stack trace of those replace_rec_fn calls?

[Leni Aniva]

Cameron Zwarich said:

Which version of Lean are you using, and what is the full stack trace of those replace_rec_fn calls?

4.21

The flamegraph looks like this

image.png

[Sebastian Ullrich]

Does trace.profiler give a better answer? It doesn't have any stack size limit at the very least

[Leni Aniva]

I found a fix, which involves changing

checkTrue "boo" $ boo matches .branch _ `Name

to

checkTrue "boo" $ boo matches .branch ..

and the compilation sped up by a couple hundred times

[Leni Aniva]

Sebastian Ullrich said:

Does trace.profiler give a better answer? It doesn't have any stack size limit at the very least

No it just outputs a bunch of elaborator messages

[Leni Aniva]

In the same compilation unit, adding more code causes it to compile faster.

This takes 5.71s

  checkTrue "[2] boo" $ boo matches .branch _ `Name

This takes 520ms

  let .branch _ n := boo | fail "Incorrect"
  checkEq "[2] boo" n `Name
  checkTrue "[2] boo" $ boo matches .branch _ `Name

[Justin Asher]

Do you know why this is so much faster?

[Leni Aniva]

Justin Asher said:

Do you know why this is so much faster?

no but it seems to be related to the exponential compile time problem

[Cameron Zwarich]

Leni Aniva said:

Cameron Zwarich said:

Which version of Lean are you using, and what is the full stack trace of those replace_rec_fn calls?

4.21

Is it possible for you to try this code with 4.22 rc3? I'm curious if it's fixed by the new compiler. If it's not, would it be possible for you to share this example with me?