## Stream: lean4

### Topic: Viewing IR?

#### Zygimantas Straznickas (Mar 23 2021 at 02:35):

What's the simplest way to see a function's compiler intermediate representation? I'm trying to figure out why my function isn't getting tail call optimized.

#### Daniel Selsam (Mar 23 2021 at 02:38):

set_option trace.compiler.ir true


#### Zygimantas Straznickas (Mar 23 2021 at 02:40):

Thanks! I found that trace class in the code and tried to turn it on but I can't see any obvious output. How should it appear? As stdout during compilation-to-c?

#### Daniel Selsam (Mar 23 2021 at 02:44):

It should appear as stdout when lean processes the commands, i.e.:

• fib.lean:
set_option trace.compiler.ir true in
def fib : Nat → Nat
| 0 => 1
| n+1 => (n+1) * fib n

• command line: lean fib.lean (produces detailed output)

#### Zygimantas Straznickas (Mar 23 2021 at 02:46):

Thanks, got it to work

#### Sebastian Ullrich (Mar 23 2021 at 07:51):

(This is because the trace is emitted in the part of the compiler still written in C++)

Last updated: May 18 2021 at 22:15 UTC