Zulip Chat Archive

Stream: lean4

Topic: building on macos

Scott Morrison (Oct 08 2021 at 00:50):

I'm having a terrible time building lean4 from source on macos. A week or two ago I could do this fine, but today I'm out of luck.

I'm running on Big Sur, with XCode installed, and the XCode command line tools installed. I've run brew install cmake gmp ccache per the macos build instructions.

Running

mkdir -p build/release
cd build/release
cmake ../..
make

gives me

[ 78%] Built target leancpp
[    ] Building ../stdlib//Init/Data.c
clang: error: invalid version number in '-mmacosx-version-min='

Adding export MACOSX_DEPLOYMENT_TARGET=10.14 resolves this issue (CI already does this; I'll make a PR for the manual), but then I get:

[    ] Building /Users/scott/projects/lean/lean4/build/release/stage0/bin/lean
ld: library not found for -lSystem
clang: error: linker command failed with exit code 1 (use -v to see invocation)

Does anyone know what to do to fix this? Has anyone successfully built lean4 on macos recently?

Julian Berman (Oct 08 2021 at 01:26):

Yes you need MACOSX_DEPLOYMENT_TARGET set

Julian Berman (Oct 08 2021 at 01:26):

This changed recently I think, not sure why, but also I put lean 4 in a tap

Julian Berman (Oct 08 2021 at 01:26):

So you can feel free to use that as well

Julian Berman (Oct 08 2021 at 01:27):

brew install --head julian/tap/lean

Julian Berman (Oct 08 2021 at 01:27):

Otherwise if you want to do it yourself you need https://github.com/Julian/homebrew-tap/blob/master/Formula/lean.rb#L20

Scott Morrison (Oct 08 2021 at 01:58):

Very frustrating. brew install --build-from-source --head julian/tap/lean does indeed work. Using the tap is not satisfactory: I would really prefer to just be able to do this with cmake and make, so that I can pass other compiler flags.

Scott Morrison (Oct 08 2021 at 02:01):

I've tried using the same arguments for cmake and make that brew install --build-from-source --verbose reports using:

cmake ../.. -DCMAKE_INSTALL_PREFIX=/usr/local/Cellar/lean/2 -DCMAKE_INSTALL_LIBDIR=lib -DCMAKE_BUILD_TYPE=Release -DCMAKE_FIND_FRAMEWORK=LAST -DCMAKE_VERBOSE_MAKEFILE=ON -Wno-dev -DBUILD_TESTING=OFF -DCMAKE_OSX_SYSROOT=/Library/Developer/CommandLineTools/SDKs/MacOSX11.sdk

make MACOSX_DEPLOYMENT_TARGET=11.00 -j36

but I still get the same ld: library not found for -lSystem error.

There is some difference between the environment brew install is providing and the terminal. :-(

Julian Berman (Oct 08 2021 at 02:04):

Fair enough. Perhaps which compiler you've got first on your path?

Julian Berman (Oct 08 2021 at 02:04):

Otherwise when I compile manually I do...

Julian Berman (Oct 08 2021 at 02:05):

rm -rf build/release && mkdir -p build/release && cd build/release && cmake -DCMAKE_INSTALL_PREFIX=/opt/lean4/nightly/ ../.. && make -j36 SDKROOT=$(xcrun --sdk macosx --show-sdk-path) MACOSX_DEPLOYMENT_TARGET=11.00

Julian Berman (Oct 08 2021 at 02:05):

Perhaps try that just in case?

Scott Morrison (Oct 08 2021 at 02:08):

Looks like the SDKROOT might be the trick.

Julian Berman (Oct 08 2021 at 02:08):

Great.

Sebastian Ullrich (Oct 08 2021 at 14:24):

This might be due to the following changed line: https://github.com/leanprover/lean4/blob/305d035f17d9b4d0297c0345bf67e5b9b360595b/src/CMakeLists.txt#L431
Could you post the output of grep LEANC_OPTS build/release/stage1/stdlib.make?

Julian Berman (Oct 08 2021 at 15:32):

Mine:

~/Development/lean4 is a git repository on master
⊙  grep LEANC_OPTS build/release/stage1/stdlib.make                                                                                                                                 julian@Airm
        LEANC_OPTS+=" -O3 -DNDEBUG -isysroot/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk -mmacosx-version-min=11.00"\
        +"/Users/julian/Development/lean4/build/release/stage1/bin/leanmake" lib PKG=Init $(LEANMAKE_OPTS) LEANC_OPTS+=-DLEAN_EXPORTING
        +"/Users/julian/Development/lean4/build/release/stage1/bin/leanmake" lib PKG=Std $(LEANMAKE_OPTS) LEANC_OPTS+=-DLEAN_EXPORTING
        +"/Users/julian/Development/lean4/build/release/stage1/bin/leanmake" lib PKG=Lean $(LEANMAKE_OPTS) LEANC_OPTS+=-DLEAN_EXPORTING

~/Development/lean4 is a git repository on master
⊙  xcrun --sdk macosx --show-sdk-path                                                                                                                                               julian@Airm
/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk

Sebastian Ullrich (Oct 08 2021 at 15:32):

Thanks. We're working on a fix.

Sebastian Ullrich (Oct 08 2021 at 16:34):

It should work without any extra flags again now

Julian Berman (Oct 08 2021 at 17:55):

Thanks! I can confirm I don't need MACOSX_DEPLOYMENT_TARGET (which for me was newly required). Though supplying SDKROOT still is necessary (but that was at least for me always necessary)

Mac (Oct 08 2021 at 19:30):

@Sebastian Ullrich fyi, you probably have already noticed this, but in case you missed it, that fix broke the Nix CI macOS build

Sebastian Ullrich (Oct 08 2021 at 19:52):

@Julian Berman CMake has some built-in logic for inferring the SDK, which seems to work on CI and on Leo's machine, but apparently not on yours for some reason

Julian Berman (Oct 08 2021 at 20:11):

Hrm. OK, not sure why -- though I guess let's see which bucket Scott falls into, probably not mine if he hasn't had to set it till now.

Scott Morrison (Oct 08 2021 at 21:24):

Unfortunately on master, without any flags, I am still failing with

[    ] Linking /Users/scott/projects/lean/lean4/build/release/stage1/bin/leanc
ld: library not found for -lSystem
clang: error: linker command failed with exit code 1 (use -v to see invocation)

Scott Morrison (Oct 08 2021 at 21:33):

And

make -j36 SDKROOT=$(xcrun --sdk macosx --show-sdk-path)

works.

Scott Morrison (Oct 08 2021 at 21:35):

For reference xcrun is reporting /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk, and in /Library/Developer/CommandLineTools/SDKs/ I have

% ls -al
total 0
drwxr-xr-x  6 root  wheel  192  8 Oct 12:39 .
drwxr-xr-x  5 root  admin  160  8 Oct 11:08 ..
lrwxr-xr-x  1 root  wheel   14  8 Oct 12:39 MacOSX.sdk -> MacOSX11.3.sdk
drwxr-xr-x  7 root  wheel  224 30 Nov  2020 MacOSX11.1.sdk
drwxr-xr-x  7 root  wheel  224  8 Oct 12:39 MacOSX11.3.sdk
lrwxr-xr-x  1 root  wheel   14  8 Oct 12:38 MacOSX11.sdk -> MacOSX11.3.sdk

Sebastian Ullrich (Oct 09 2021 at 08:08):

@Scott Morrison That's weird though, it must have succeeded for stage0/bin/lean this time? Could you try again with a clean build directory and make -j36 VERBOSE=1, and post the cmdlines after "Linking ..." if the error persists?

Scott Morrison (Oct 09 2021 at 08:16):

[    ] Linking /Users/scott/projects/lean/lean4/build/release/stage1/bin/leanc
/Users/scott/projects/lean/lean4/build/release/stage1/leanc.sh -o "/Users/scott/projects/lean/lean4/build/release/stage1/bin/leanc" /Users/scott/projects/lean/lean4/build/release/stage1/temp/Leanc.o -lleanshared  -Wl,-rpath,@executable_path/../lib -Wl,-rpath,@executable_path/../lib/lean
ld: library not found for -lSystem
clang: error: linker command failed with exit code 1 (use -v to see invocation)
make[7]: *** [/Users/scott/projects/lean/lean4/build/release/stage1/bin/leanc] Error 1
make[6]: *** [Leanc] Error 2
make[5]: *** [CMakeFiles/leanc] Error 2
make[4]: *** [CMakeFiles/leanc.dir/all] Error 2
make[4]: *** Waiting for unfinished jobs....
mv "../build/release/stage1/lib/temp/Leanpkg/Build.c.tmp" "../build/release/stage1/lib/temp/Leanpkg/Build.c"
mv "../build/release/stage1/lib/temp/Leanpkg/Manifest.c.tmp" "../build/release/stage1/lib/temp/Leanpkg/Manifest.c"
[    ] Building ../build/release/stage1/lib/temp/Leanpkg/Build.c
[    ] Building Leanpkg/Resolve.lean
/Users/scott/projects/lean/lean4/build/release/stage1/leanc.sh -c -o ../build/release/stage1/lib/temp/Leanpkg/Build.o ../build/release/stage1/lib/temp/Leanpkg/Build.c -O3 -DNDEBUG -isysroot/Library/Developer/CommandLineTools/SDKs/MacOSX11.3.sdk
/Users/scott/projects/lean/lean4/build/release/stage0/bin/lean -s40000 -o "../build/release/stage1/lib/lean/Leanpkg/Resolve.olean" --c="../build/release/stage1/lib/temp/Leanpkg/Resolve.c.tmp" Leanpkg/Resolve.lean
[    ] Building ../build/release/stage1/lib/temp/Leanpkg/Manifest.c
/Users/scott/projects/lean/lean4/build/release/stage1/leanc.sh -c -o ../build/release/stage1/lib/temp/Leanpkg/Manifest.o ../build/release/stage1/lib/temp/Leanpkg/Manifest.c -O3 -DNDEBUG -isysroot/Library/Developer/CommandLineTools/SDKs/MacOSX11.3.sdk
mv "../build/release/stage1/lib/temp/Leanpkg/Resolve.c.tmp" "../build/release/stage1/lib/temp/Leanpkg/Resolve.c"
[    ] Building Leanpkg.lean
/Users/scott/projects/lean/lean4/build/release/stage0/bin/lean -s40000 -o "../build/release/stage1/lib/lean/Leanpkg.olean" --c="../build/release/stage1/lib/temp/Leanpkg.c.tmp" Leanpkg.lean
[    ] Building ../build/release/stage1/lib/temp/Leanpkg/Resolve.c
/Users/scott/projects/lean/lean4/build/release/stage1/leanc.sh -c -o ../build/release/stage1/lib/temp/Leanpkg/Resolve.o ../build/release/stage1/lib/temp/Leanpkg/Resolve.c -O3 -DNDEBUG -isysroot/Library/Developer/CommandLineTools/SDKs/MacOSX11.3.sdk
mv "../build/release/stage1/lib/temp/Leanpkg.c.tmp" "../build/release/stage1/lib/temp/Leanpkg.c"
[    ] Building ../build/release/stage1/lib/temp/Leanpkg.c
/Users/scott/projects/lean/lean4/build/release/stage1/leanc.sh -c -o ../build/release/stage1/lib/temp/Leanpkg.o ../build/release/stage1/lib/temp/Leanpkg.c -O3 -DNDEBUG -isysroot/Library/Developer/CommandLineTools/SDKs/MacOSX11.3.sdk
[    ] Linking /Users/scott/projects/lean/lean4/build/release/stage1/bin/leanpkg
/Users/scott/projects/lean/lean4/build/release/stage1/leanc.sh -o "/Users/scott/projects/lean/lean4/build/release/stage1/bin/leanpkg" ../build/release/stage1/lib/temp/Leanpkg/LeanVersion.o ../build/release/stage1/lib/temp/Leanpkg/Proc.o ../build/release/stage1/lib/temp/Leanpkg/Manifest.o ../build/release/stage1/lib/temp/Leanpkg/Git.o ../build/release/stage1/lib/temp/Leanpkg/Build.o ../build/release/stage1/lib/temp/Leanpkg/Resolve.o ../build/release/stage1/lib/temp/Leanpkg/Toml.o ../build/release/stage1/lib/temp/Leanpkg.o -lleanshared  -Wl,-rpath,@executable_path/../lib -Wl,-rpath,@executable_path/../lib/lean
ld: library not found for -lSystem
clang: error: linker command failed with exit code 1 (use -v to see invocation)
make[7]: *** [/Users/scott/projects/lean/lean4/build/release/stage1/bin/leanpkg] Error 1
make[6]: *** [Leanpkg] Error 2
make[5]: *** [CMakeFiles/leanpkg] Error 2
make[4]: *** [CMakeFiles/leanpkg.dir/all] Error 2
make[3]: *** [all] Error 2
make[2]: *** [stage1-prefix/src/stage1-stamp/stage1-build] Error 2
make[1]: *** [CMakeFiles/stage1.dir/all] Error 2
make: *** [all] Error 2

Sebastian Ullrich (Oct 09 2021 at 08:18):

But make lean VERBOSE=1 works?

Scott Morrison (Oct 09 2021 at 08:19):

$ make lean VERBOSE=1
make: *** No rule to make target `lean'.  Stop.

Sebastian Ullrich (Oct 09 2021 at 08:20):

Ah, try again in stage1/

Scott Morrison (Oct 09 2021 at 08:21):

Yes, that works.

Scott Morrison (Oct 09 2021 at 08:21):

make[4]: Nothing to be done for `lean'.

Sebastian Ullrich (Oct 09 2021 at 08:21):

Ok, thanks. And after rm bin/lean?

Sebastian Ullrich (Oct 09 2021 at 08:22):

Wait, I can see the mistake

Sebastian Ullrich (Oct 09 2021 at 08:25):

This should fix it; will merge after CI is green https://github.com/Kha/lean4/commit/2ab8a38daa36650ad70f40f2290bf9c22ae0406e

Scott Morrison (Oct 09 2021 at 08:36):

That commit works beautifully for me. :-)

Julian Berman (Oct 09 2021 at 15:16):

Works here too now without any options. Thanks Sebastian.

Last updated: Dec 20 2023 at 11:08 UTC