How much does the compiler optimise?

Stream: lean4

[Bhavik Mehta]

When writing Haskell scripts, I usually leave optimisations off while I'm testing, and then compile with -O2 when I want to run a big computation. Is there an equivalent in Lean 4? ie, a way to control the compile-time / optimisation balance.

(Context: I'm writing a program which uses LazyList for efficiency, and I'm curious if the compiler can do the clever fusion optimisations that Haskell does)

[Henrik Böving]

The compiler currently always does everything it can and there is no easily useable way to turn optimizations off. There is a way to tune down the optimizations that the C compiler performs with some lakefile stuff but the Lean compiler that produces the C is always full blast ahead.

It does not have specific optimizations for fusion, that said you can of course write programs in the style of rust's iterator API and might get similar effects due to lots of specialization/inlining/c compiler optimization.

[Max Nowak 🐉]

Will we be blazing fast once we have the LLVM backend?

[Henrik Böving]

The LLVM backend already exists and is fully operational for...a couple of months at least. And no it does not currently make anything faster, it just generates IR that's on a level with the LLVM that the C ends up generating really. Though there are a couple of tricks that we can pull to maybe get more out of it

[Diego Antonio Rosario Palomino]

@Henrik Böving
Where can i read about the backends, IRs, optimizations and the runtime representation of values?

[Daniel Weber]

I think https://lean-lang.org/lean4/doc/dev/ffi.html talks about runtime representation of values

[Henrik Böving]

Diego Antonio Rosario Palomino said:

Henrik Böving
Where can i read about the backends, IRs, optimizations and the runtime representation of values?

There is also a paper called "immutable beans counting" about one of the novel passes. Apart from that no documentation has been created about it sooo the answer for most of the compiler is "in the source code"

[Diego Antonio Rosario Palomino]

thanks