Error building Lean4

Stream: new members

[Aurélien Saue]

Hi, when trying to build Lean4 from source I always get the same error: /usr/bin/ld: cannot find -lleancpp
Do you know how to fix this?

[Julian Berman]

Can you share how you're compiling it and the full output

[Aurélien Saue]

Yes, here it is:

aurelien@pavilion15:~/Documents/VU/mathport/lean4/build/release$ make
[  6%] Performing build step for 'stage0'
[  0%] Built target initialize
[  5%] Built target runtime
[  9%] Built target util
[ 13%] Built target kernel
[ 17%] Built target library
[ 18%] Built target constructions
[ 23%] Built target compiler
[ 23%] Built target leancpp
[ 27%] Built target leanruntime
[ 80%] Built target Lean
[ 84%] Built target Std
[100%] Built target Init
[100%] Built target shell
[100%] Built target lean
[ 12%] No install step for 'stage0'
[ 18%] Completed 'stage0'
[ 50%] Built target stage0
[ 56%] Performing configure step for 'stage1'
-- No build type selected, default to Release
-- 64-bit machine detected
-- Using compressed object headers and only 32-bits for reference counter, this feature assume the OS only uses memory addresses < 2^48
CMake Warning at CMakeLists.txt:295 (message):
  Failed to find ccache, prepare for longer and redundant builds...


-- git commit sha1: 478dc9b05fd2d0c4a441bce552025cb0f70d15c5
-- Configuring done
-- Generating done
-- Build files have been written to: /home/aurelien/Documents/VU/mathport/lean4/build/release/stage1
[ 62%] Performing build step for 'stage1'
[    ] Linking /home/aurelien/Documents/VU/mathport/lean4/build/release/stage1/bin/leanpkg
/usr/bin/ld: cannot find -lleancpp
collect2: error: ld returned 1 exit status
make[7]: *** [/home/aurelien/Documents/VU/mathport/lean4/build/release/stage1/bin/../share/lean/lean.mk:82: /home/aurelien/Documents/VU/mathport/lean4/build/release/stage1/bin/leanpkg] Error 1
make[6]: *** [/home/aurelien/Documents/VU/mathport/lean4/build/release/stage1/stdlib.make:28: stdlib] Error 2
make[5]: *** [CMakeFiles/make_stdlib.dir/build.make:57: CMakeFiles/make_stdlib] Error 2
make[4]: *** [CMakeFiles/Makefile2:334: CMakeFiles/make_stdlib.dir/all] Error 2
make[3]: *** [Makefile:163: all] Error 2
make[2]: *** [CMakeFiles/stage1.dir/build.make:113: stage1-prefix/src/stage1-stamp/stage1-build] Error 2
make[1]: *** [CMakeFiles/Makefile2:218: CMakeFiles/stage1.dir/all] Error 2
make: *** [Makefile:130: all] Error 2

[Julian Berman]

I've had to re-figure-out how to compile lean4 a few times the past month or so (though I'm not a C ecosystem expert by any means). @Sebastian Ullrich may be the best person to chime in (and hopefully doesn't mind the ping). But I'm reasonably sure from your output that what's gone wrong there has already happened before that point -- so I think you should blow away that directory, run cmake again, and run make and show that full output if you can. I'm recompiling myself at the minute to see what I do, but it's some combination of just manually setting LIBRARY_PATH and friends, mostly to do with me being on macOS though.

[Julian Berman]

Yeah so my compilation just succeeded. For reference, what I had to do (which is probably nonidiomatic but at least works, and the other macOS trick for me is to ensure I'm in an arm64 terminal and not a rosetta'd one) is:

~/Development/lean4 is a git repository on master
⊙  trash build && mkdir -p build/release && cd build/release && cmake -DCMAKE_PREFIX_PATH=/opt/homebrew/ -DCMAKE_INSTALL_PREFIX=/opt/lean4/nightly/ -DCMAKE_LIBRARY_PATH=/opt/homebrew/lib ../.. && make LIBRARY_PATH=/opt/homebrew/lib:/Library/Developer/CommandLineTools/SDKs/MacOSX11.1.sdk/usr/lib C_INCLUDE_PATH=/opt/homebrew/include:/Library/Developer/CommandLineTools/usr/include/c++/v1:/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include CPP_INCLUDE_PATH=/opt/homebrew/include:/Library/Developer/CommandLineTools/usr/include/c++/v1:/Library/Developer/CommandLine -j4

If you share the full command and output from a fresh build directory it may help. Also just in case you're unaware there are nightly builds you can just use at https://github.com/leanprover/lean4-nightly/releases -- I also should have asked what OS and architecture you're on a long time ago :D

[Aurélien Saue]

Thank you for the help!
So I'm working with Ubuntu 20.04, on a x86_64 architecture if that is what you are asking for.
The nightly build works perfectly, but I am trying to use the mathport tool and I need to build Lean according to the instructions...

[Aurélien Saue]

I have tried building it from scratch again and get stuck with the same error :sad:
The output is too long to be included but here is what I think are the relevant parts of it:

[ 43%] No install step for 'stage0'
[ 50%] Completed 'stage0'
[ 50%] Built target stage0
Scanning dependencies of target stage1
[ 56%] Creating directories for 'stage1'
[ 62%] No download step for 'stage1'
[ 68%] No patch step for 'stage1'
[ 75%] No update step for 'stage1'
[ 81%] Performing configure step for 'stage1'
-- The CXX compiler identification is GNU 9.3.0
-- The C compiler identification is GNU 9.3.0
-- Check for working CXX compiler: /usr/bin/c++
-- Check for working CXX compiler: /usr/bin/c++ -- works
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Check for working C compiler: /usr/bin/cc
-- Check for working C compiler: /usr/bin/cc -- works
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Detecting C compile features
-- Detecting C compile features - done
-- No build type selected, default to Release
-- 64-bit machine detected
-- Using compressed object headers and only 32-bits for reference counter, this feature assume the OS only uses memory addresses < 2^48
-- Found GMP: /usr/include/x86_64-linux-gnu (Required is at least version "5.0.5")
CMake Warning at CMakeLists.txt:295 (message):
  Failed to find ccache, prepare for longer and redundant builds...


-- Found PythonInterp: /usr/bin/python3.8 (found version "3.8.5")
-- git commit sha1: 478dc9b05fd2d0c4a441bce552025cb0f70d15c5
-- Configuring done
-- Generating done
-- Build files have been written to: /home/aurelien/Documents/VU/mathport/lean4/build/release/stage1
[ 87%] Performing build step for 'stage1'
Scanning dependencies of target make_stdlib
[    ] Building Init/Prelude.lean
[    ] Building Init/Notation.lean
[    ] Building ../build/release/stage1/lib/temp/Init/Notation.c
[    ] Building Init/SizeOf.lean
[    ] Building Init/Core.lean


...


[    ] Building Leanpkg/Toml.lean
[    ] Building Leanpkg/Manifest.lean
[    ] Building ../build/release/stage1/lib/temp/Leanpkg/Manifest.c
[    ] Building Leanpkg/Proc.lean
[    ] Building ../build/release/stage1/lib/temp/Leanpkg/Proc.c
[    ] Building Leanpkg/Resolve.lean
[    ] Building ../build/release/stage1/lib/temp/Leanpkg/Resolve.c
[    ] Building ../build/release/stage1/lib/temp/Leanpkg/LeanVersion.c
[    ] Building ../build/release/stage1/lib/temp/Leanpkg/Toml.c
[    ] Building Leanpkg.lean
[    ] Building ../build/release/stage1/lib/temp/Leanpkg.c
[    ] Linking /home/aurelien/Documents/VU/mathport/lean4/build/release/stage1/bin/leanpkg
/usr/bin/ld: cannot find -lleancpp
collect2: error: ld returned 1 exit status
make[7]: *** [/home/aurelien/Documents/VU/mathport/lean4/build/release/stage1/bin/../share/lean/lean.mk:82: /home/aurelien/Documents/VU/mathport/lean4/build/release/stage1/bin/leanpkg] Error 1
make[6]: *** [/home/aurelien/Documents/VU/mathport/lean4/build/release/stage1/stdlib.make:28: stdlib] Error 2
make[5]: *** [CMakeFiles/make_stdlib.dir/build.make:57: CMakeFiles/make_stdlib] Error 2
make[4]: *** [CMakeFiles/Makefile2:334: CMakeFiles/make_stdlib.dir/all] Error 2
make[3]: *** [Makefile:163: all] Error 2
make[2]: *** [CMakeFiles/stage1.dir/build.make:113: stage1-prefix/src/stage1-stamp/stage1-build] Error 2
make[1]: *** [CMakeFiles/Makefile2:218: CMakeFiles/stage1.dir/all] Error 2
make: *** [Makefile:130: all] Error 2

[Julian Berman]

I think zulip elided that paste -- maybe a https://gist.github.com/

[Julian Berman]

And yeah ubuntu + x86_64 was what I was asking, thanks!

[Sebastian Ullrich]

I've seen this error before, but it has always been solved by removing the build directory. Not sure what could go wrong otherwise.

[Aurélien Saue]

https://gist.github.com/AurelienSaue/c73da70938ce0604f828f4815d362eef

[Sebastian Ullrich]

I think I found the mistake. It was probably hidden for other people when they use -j for building

[Sebastian Ullrich]

The fix is not trivial, so please use an appropriate -j or call make -C stage1 leancpp first

[Sebastian Ullrich]

Ok, I went with the trivial fix after all since the should be no downsides in practice https://github.com/leanprover/lean4/pull/373

[Julian Berman]

@Sebastian Ullrich How can/should I help on the mac+M1+homebrew side (lemme know if it's better to ask that elsewhere)? Presumably the ideal is that just running cmake+make should work on this setup same as others given it'll be the common one eventually, but I get a series of errors if I don't manually point things at the right places like in my example. Obviously understandable if it's not a priority at the minute

[Julian Berman]

In particular I think nightlys for darwin used to be universal somehow? But now they aren't, they're x86_64 only, and won't run on arm (because they expect an x86_64 libgmp present, which users with native-only homebrew installs won't have)

[Sebastian Ullrich]

I wouldn't know how to turn C++ code universal

[Sebastian Ullrich]

I also don't know what the correct way to automatically set up those paths is

[Julian Berman]

OK -- if I figure anything small out I presume a PR is welcome?

[Sebastian Ullrich]

sure!

[Aurélien Saue]

Just to let you know, it worked with the help of a -j. Thank you very much!