Disable inlining?

Stream: lean4

[Leo Stefanesco]

Hi! Is there an option to disable inlining in the compiler, to make it easier to read the IR of a function?

[Henrik Böving]

There isn't. This also feels a bit like a #xy question, inlining is of utmost importance for so much stuff that happens in the compiler so the resulting IR usually completely depends on inlining being done, for example:

• Is there potential for reuse with FBIP
• Where do we need to add reference counts?
• Can we do classic functional optimizations like cases-of-cases?

Do you have a reason to want to read version of the IR that will potentially behave completely different from the actually optimized one?

[Leo Stefanesco]

My goal is to try to see if I'm getting reuse with FBIP. I tried to use set_option trace.compiler.ir.rc but it prints huge functions because of inlining, and was hoping that without inlining it would be clear if my function doesn't touch the ref counters. Is there a better way to see if my objects are being reused?

[Henrik Böving]

Right, you definitely need to have inlining enabled for reuse to happen optimally so disabling it is not an option for this at all. And no there is currently no better way apart from reasoning about the IR. That being said experienced Lean programmers at least have an intuition about what kind of code patterns will and won't give you reuse.