Optimizing compiler

Stream: general

[Diego Antonio Rosario Palomino]

Hello, i was checking Nora, a racket backend. It mentions that lean 4 also implements a backend using MLIR. Where can i find info about lean4s optimizying compiler? I had already heard about it was being worked on, but dont know any specifics

[Henrik Böving]

Lean 4 does not have a backend using MLIR. It has a C backend and a, usually disabled, LLVM backend. If you want information on them you'll have to ask more specific questions.

[Jason Rute]

Searching Zulip for “MLIR” brought up this: https://grosser.science/static/0b1eb3ff397733a16e3f3e0e2429cab5/bhat-2022-Lambda-the-Ultimate-SSA.pdf. Could that be what Nora was referencing?

[Henrik Böving]

The grosser group is working on things related to MLIR in Lean and they might end up working on an MLIR backend in the future yes

[Diego Antonio Rosario Palomino]

Jason Rute said:

Searching Zulip for “MLIR” brought up this: https://grosser.science/static/0b1eb3ff397733a16e3f3e0e2429cab5/bhat-2022-Lambda-the-Ultimate-SSA.pdf. Could that be what Nora was referencing?

Yes, i was talking about about that

[Andrés Goens]

cc @Siddharth Bhat

[Diego Antonio Rosario Palomino]

@Siddharth Bhat did you publish the code on that paper?

[Mauricio Collares]

The appendix links to https://dl.acm.org/do/10.5281/zenodo.5786074/full/, which should include the full code

[Siddharth Bhat]

@Diego Antonio Rosario Palomino our repository is public, at https://github.com/opencompl/lean-mlir. Feedback would be lovely!

[Diego Antonio Rosario Palomino]

Thanks for the link !

Sure . I am an idris2 programmar, but how different can one dependent language be from another ?
( sarcasm )