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.

  1. Many tests in tests/compiler fail with /usr/bin/ld: cannot find -lstdc++. This is solvable by adding libstdc++-9-dev to the apt-get invocation.
  2. leancomptest_foreign still fails, for the unfortunate reason that it makes a hardcoded call to c++, ignoring any settings of CMAKE_CXX_COMPILER or CXX. Because we've only installed g++-10, the invocation of c++ fails. I'm not certain of the best fix for this. Should the leancomptest_foreign Makefile check the CXX environment variable? Or just add something to the apt-get step that will make c++ 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