Cranelift and LLVM

Stream: lean4

[Huỳnh Trần Khanh]

well... we don't have LLVM support yet right? if we were to implement LLVM code generation then we should also implement Cranelift codegen as well. Cranelift is faster but generates less optimized code, so Cranelift is pretty decent for debug builds. i'm pretty sure that Cranelift generated code is much faster than interpreted code. note that i have no experience implementing compilers, so what i'm saying is based on hearsay knowledge from my smart friends :joy: please correct me if i'm saying nonsense as usual :heart:

[Mario Carneiro]

A new backend is a significant undertaking, and I don't think anyone has the cycles for this. You are free to try it yourself as an experiment but I don't think there is any need for it at the moment.