interested in lean 4

Stream: new members

[Diego Antonio Rosario Palomino]

Hello, i am a cs student interested in functional languages. Where can i find the most up to date lean 4 tutorial, list of packages and package manager; and information about the compiler. I am particularly interested about novel optimizations "counting inmutable beans" and the like that may make lean 4 faster than idris2

[Henrik Böving]

For theorem proving: https://leanprover.github.io/theorem_proving_in_lean4/
For programming (almost finished): https://leanprover.github.io/functional_programming_in_lean/
About the project itself: https://leanprover.github.io/lean4/doc/whatIsLean.html (although the ifnromation here is a bit sparse)

Our package manager is: github.com/leanprover/lake you can find documentation about both the standard as well as the mathematics library here: https://leanprover-community.github.io/mathlib4_docs/

If you want to know things about the compiler itself you'll have to resort to reading the papers, the compiler source code itself and asking people the specific questions you are interested in here. We do not have full comprehensive documentation on many parts of the system yet.

[Diego Antonio Rosario Palomino]

Thanks
-Does lake have a package database ?
-How would you expect lean 4 to perform against idris2? ( canonically compiles to chez scheme with dynamic type checks off ). Other than functional but in place, what other optimizations are you implementing?

[Henrik Böving]

• No you just refer to github repos right now
• I would generally speaking expect Lean to at least hold up again Idris2 (compiled Lean that is, the interpreter is not particularly hard optimized). We compile to C (or also experimentally directly LLVM) and besides FBIP we mosty do "regular" compiler optimizations like CSE, simplification of case statements like iin Haskell Core etc. To my knowledge we do not have optimizations for the compiler itself that are considered particularly novel (apart from FBIP). However the runtime has some nice optimizations such as real contigious in memory Arrays that you can mutate in place while the ref count is one for example

[Diego Antonio Rosario Palomino]

What would be the benefits of compiling to llvm? Functional constructs can be mapped to c with defunctionalization, de-recursion, etc
It would improve compile times but would that be important considering the cost of type checking and optimization?

[Henrik Böving]

To me it's been that we will in the future be able to generate LLVM code with very specific annotations based on knowledge that we have about the environment which would get lost if we were to translate first to C and then to LLVM with clang. But @Siddharth Bhat can most likely answer the question betterr.

[Siddharth Bhat]

@Diego Antonio Rosario Palomino Defunctionalization is usually a whole program optimisation. This might be prohibitive for something like Lean. I'd say in general, some information is only expressible in the C level via compiler specific annotations (eg. this call is a tail call), or inexpressible (eg. unwinding the stack, coroutines). Whether we take advantage of these exotics is a different question :smile: .

[Siddharth Bhat]

I am personally interested in LLVM because my background is high performance computing. Lean should allow us to control code generation to a degree where we are able to build the LLVM IR we expect to see programatically. This is feasible for numeric codes, and my hope is that it allows us to write numerical programs in Lean that hit the performance roofline.

[Diego Antonio Rosario Palomino]

Arbitrary recursion can be optimized away without the target language having tail call support. With cps ( or anf, i think ) optimizations
Those and defunctionalization are usually global operations, but there are parallel or local versions and alternatives

[Diego Antonio Rosario Palomino]

@Siddharth Bhat have you considered targeting this functional compiler https://github.com/grin-compiler?
Functional languages can target it ( now via STG, instead of GRIN ir directly ) to achieve the tecniques i mentioned

[Siddharth Bhat]

@Diego Antonio Rosario Palomino Yes, I have conversed with Csaba about GRIN. I find the ideas very interesting, and the project very ambitious. Last I checked in with GRIN, the key points-to analysis is still a whole program analysis. Also, it takes design decisions which adapt it very well to Haskell. It is unclear to me how much reuse we would get by trying to compile Lean's IR to it.

---

Would exploring whether we can easily adapt our backend to reuse GRIN be something you'd be interested to explore? I'd love to understand this space better, and would be interested to oversee this.

[Diego Antonio Rosario Palomino]

@Siddharth Bhat
-Key to points analysis being global is one of the reasons current GRIN IR is being supplemented by STG ( and possibly replaced by a new IR in the future )

-Andorp has already tried to use a language other than haskell: https://github.com/andorp/IdrisExtSTGCodegen
it seems to work well.

-I am very interested in state of the art language ( dependent and functional as far as i know ) optimization. Eg i toyed with an ml backend for idris2 ( for use with mlton )
So i would be interested to take over Andorp's work , implement a lean4 front end for Csbasas compiler, etc

[Diego Antonio Rosario Palomino]

And you seem to have your own optimization ideas, i would love to hear how they compare against other projects