Current state of LLVM backend?

Stream: lean4

[Jianqiu Zhao]

The bundled GLIBC is too old to link with system-wide dependencies. Maybe LLVM backend will fix this? Is it still being developed?

[Anthony Wang]

If you're getting linker errors due to Lean's old glibc version, you could try adding moreLinkArgs := #["-Wl,--unresolved-symbols=ignore-all"] to your lakefile, which is what sqlite-lean and lean-sdl3 do.