Building on Mac

Stream: lean4 dev

[Tom]

(Moving over not to pollute the Weak Symbol thread)

I have built Lean from source on Mac but some of the tests are failing. After looking into it, the vast majority of the problems are caused by the linker trying to link -lc++, which is clang's version of the C++ standard library.
I followed the instructions for Mac but this issue persists (fwiw, not all the install instructions seem to work anymore: brew install llvm --with-clang appears not to be supported anymore?)

Is this the intention or is my build misconfigured in some way? clang can also use gcc's libstdc++ and some people do. Before I try to figure this out, I want to make sure i'm chasing the right problem.

Thanks!

[Tom]

My experience so far:

• I still haven't been able to build natively on MacOS; the issue is still related to -lc++. It seems cause by the fact that leanc doesn't set -L to the llvm lib location. I've been reading through the CMakeLists.txt and tried using LEANC_OPT but that also didn't work

• I was able to finally build on MacOS using nix but then because I'm not familiar with it, I've not been able to find a version of binutils which contains gold

• My Ubuntu server was still on 18.0 LTS, so Lean also didn't build, seemingly because of an older version of glibc. I'm in the process of upgrading it to 22 LTS to see if that helps

If anybody has any suggestions regarding building on MacOS natively, I would welcome any feedback.

:sad:

[Sebastian Ullrich]

@Tom I believe CI is using the standard Xcode command line tools, whose c++ even seems to default to -lc++

[Tom]

Ok, I'll try installing xcode on my mac; It turns out one can use libc++ on the mac but when you install llvm via brew, it's installed into a non-standard location not to interfere with the "system" install of clang and I've not been able to convince cmake to respect the -L/-R for the linker. Seems the MacOS instructions are perhaps not current anymore? Some comments in the makefiles seems to indicate that this may have been done on purpose?

Just to make sure, I also tried installing the entire toolchain via conda and while I could build my own executables, ran into the same problems as above when building Lean.

I had to go through two upgrades of my Linux box which took a while but now I'm at least able to get a build on Linux, too.

[Sebastian Ullrich]

Oh yes, osx-10.9.md is as out of date as it sounds :)

[Tom]

Strange. I just went through, removed and reinstalled the xcode command line tools and still get the same errors in the tests.

[Sebastian Ullrich]

Actually I was wrong above, all our Mac CI jobs use our custom LLVM toolchain. So the standard setup might indeed be broken.

[Tom]

Ok, I'll see if I can figure out how the CI is setup and if I can replicate locally. Thanks.

[Sebastian Ullrich]

It would certainly be nice if it worked without any extra setup