Developing locally on Mac with Conda

Stream: lean4

[Saul Shanabrook]

Hey all! I am excited to have my local Lean4 setup working from source. I had a few issues getting it to compile, so wanted to share what I learned in case it would be helpful for others. Also let me know if this isn't the right place to post this sort of thing.

I am running macOS Catalina 10.15.7, and as I was trying to build, I would get two different errors: 'stdlib.h' file not found #include <stdlib.h> and ld: library not found for -lgmp.

I finally managed to successfully build, after creating a conda environment and setting some environmental variables. With an environment.yml set to:

name: lean4
channels:
- conda-forge
dependencies:
- clang
- clangxx
- cmake
- gmp
- ccache
- make

I then ran:

conda env create -f environment.yaml
conda activate lean4
mkdir -p build/release
cd build/release

env CXX=clang++ CC=clang  C_INCLUDE_PATH=$CONDA_PREFIX/include LIBRARY_PATH=$CONDA_PREFIX/lib  SDKROOT=(xcrun --sdk macosx --show-sdk-path)  cmake ../..
env CXX=clang++ CC=clang  C_INCLUDE_PATH=$CONDA_PREFIX/include LIBRARY_PATH=$CONDA_PREFIX/lib  SDKROOT=(xcrun --sdk macosx --show-sdk-path)  make

I always get confused by the compiler toolchain, so I am not recommending my method to others, but just wanted to share what worked for me!

Now that it's working, I am loving the dev experience in VS code, especially the ability to see the type for whatever is under the cursor. :party_ball:

[Julian Berman]

I (a regular ol' user) was personally aware of the gmp issue and needing to set SDKROOT manually. The rest I think might be conda-specific, which I assume you're using for some non-Python deps (but which obviously is good info to share with others)

[Julian Berman]

I sent a (bad) PR for fixing the need to manually tell it where gmp was but it was the wrong approach so I think @Sebastian Ullrich mentioned a better way to do it which may make this more seamless but I'm not sure PRs are welcome to implement it quite yet. But right now when I compile, I do something similar to what you showed and run rm -rf build/release && mkdir -p build/release && cd build/release && cmake -DCMAKE_INSTALL_PREFIX=/opt/lean4/nightly/ ../.. && make -j4 SDKROOT=$(xcrun --sdk macosx --show-sdk-path), with my libgmp coming from homebrew rather than conda

[Christian Pehle]

How did you solve the gmp issues? I installed gmp via homebrew, but it fails to link to it. I've looked through the CMakeLists.txt but found no obvious fix.

[Julian Berman]

@Christian Pehle something similar to the above should work where you set LIBRARY_PATH, e.g. cmake -DCMAKE_PREFIX_PATH=$(brew --prefix) -DCMAKE_INSTALL_PREFIX=/where/you/want/to/install -DCMAKE_LIBRARY_PATH=$(brew --prefix)/lib ../..

I forget off-hand what I tweaked to make it not even necessary to do so myself (it's not permanently setting LD_LIBRARY_PATH and friends in the environment, perhaps it's just that I have all the homebrew compilers first in PATH and they know to look in the Homebrew cellar for libraries) -- but if the above doesn't work and you're still seeing an issue, sharing the error we can probably help figure out what to set.

[Christian Pehle]

(deleted)