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.:
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