Zulip Chat Archive

Stream: lean4

Topic: Viewing IR?


view this post on Zulip 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.

view this post on Zulip Daniel Selsam (Mar 23 2021 at 02:38):

set_option trace.compiler.ir true

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Zygimantas Straznickas (Mar 23 2021 at 02:46):

Thanks, got it to work

view this post on Zulip 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