Viewing IR?

Stream: lean4

[Zygimantas Straznickas]

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]

set_option trace.compiler.ir true

[Zygimantas Straznickas]

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]

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]

Thanks, got it to work

[Sebastian Ullrich]

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