new build system for lean

Stream: lean4

[Locria Cyber]

The current build system is Makefile + CMake. It's too complicated for me to understand.

[Locria Cyber]

Is there a plan for a simpler build system?

[Locria Cyber]

libleanrt.a is built with LLVM, but it has dependency on GLIBC. I want to change that, but don't know where to start.

[Henrik Böving]

Every Lean project apart from the compiler itself will use the Lean build system Lake. Changing the build system of the compiler is not on the list right now since it affects basically nobody apart from the compiler development team.

[Locria Cyber]

I do want to use musl libc with lean. Is there anything I can do to make it compile with musl libc?

[Sebastian Ullrich]

Do you use a compiler wrapper for that? Then it should be sufficient to set CMAKE_C_COMPILER and CMAKE_CXX_COMPILER to it.

[Gabriel Ebner]

We have some bugs with musl IIRC, since the IO functions return different error codes than glibc.

[Chris Lovett]

I too would love to see a pure cmake build system for lean that doesn't include bash shell scripts so that you can use the full power of cmake to build lean with many different C++ toolchains (including MSVC). I suspect if we did that and built a pure native win32 binary for lean it would be much faster than the current MSYS2 windows lean binaries which are 47% slower than the Linux versions on the same machine. For example lake build of mathlib4 takes 23 seconds in WSL and 34 seconds in windows on the same box.

[Sebastian Ullrich]

@Chris Lovett This sounds like a pretty dubious assumption to me without presenting any evidence from profiling. I find it far more likely that the difference in file systems is the culprit compared to the specific API calls used to interface with them, where MinGW doesn't really have a different choice from "pure" Windows programs anyway. And even if we can identify a problematic API bridge, we can simply replace that specific one with native Windows calls.