Zulip Chat Archive
Stream: lean4
Topic: build requirements for Lean4
Scott Morrison (Oct 03 2021 at 02:20):
The Lean4 manual advises that the requirements for building Lean4 from source on Ubuntu are:
sudo apt-get install git libgmp-dev cmake ccache gcc-10 g++-10
However I've discovered this isn't quite enough if you're building on a bare Ubuntu machine (e.g. the Docker ubuntu image): while you can build Lean4 with these dependencies, the test suite will fail, for two reasons.
- Many tests in
tests/compilerfail with/usr/bin/ld: cannot find -lstdc++. This is solvable by addinglibstdc++-9-devto theapt-getinvocation. leancomptest_foreignstill fails, for the unfortunate reason that it makes a hardcoded call toc++, ignoring any settings ofCMAKE_CXX_COMPILERorCXX. Because we've only installedg++-10, the invocation ofc++fails. I'm not certain of the best fix for this. Should theleancomptest_foreignMakefile check theCXXenvironment variable? Or just add something to theapt-getstep that will makec++directly usable?
Scott Morrison (Oct 03 2021 at 02:21):
An easy option that fixes both problems is to add build-essential to the recommended apt-get list. This isn't the most lightweight solution, but possibly simplest.
Last updated: May 02 2025 at 03:31 UTC