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/compiler
fail with/usr/bin/ld: cannot find -lstdc++
. This is solvable by addinglibstdc++-9-dev
to theapt-get
invocation. leancomptest_foreign
still fails, for the unfortunate reason that it makes a hardcoded call toc++
, ignoring any settings ofCMAKE_CXX_COMPILER
orCXX
. Because we've only installedg++-10
, the invocation ofc++
fails. I'm not certain of the best fix for this. Should theleancomptest_foreign
Makefile check theCXX
environment variable? Or just add something to theapt-get
step 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: Dec 20 2023 at 11:08 UTC