121 lines
3.4 KiB
Markdown
121 lines
3.4 KiB
Markdown
|
Compiling Lean with Split Stacks
|
||
|
|
================================
|
||
|
|
|
||
|
|
[Split stacks](http://gcc.gnu.org/wiki/SplitStacks) is a relatively
|
||
|
|
new feature in gcc. It allows the stack to grown automatically as
|
||
|
|
needed. There is a small performance penalty since the program stack
|
||
|
|
is stored in the heap. However, we multiple threads, each starting
|
||
|
|
with a small stack, and have the stack grow and shrink as required by
|
||
|
|
the program.
|
||
|
|
|
||
|
|
In principle, it is possible to build a program that uses split-stacks
|
||
|
|
with libraries that do not. However, it did not work in our experiments.
|
||
|
|
To be able to compile Lean with split-stacks, we also have to compile
|
||
|
|
GMP, MPFR and Lua using split-stacks.
|
||
|
|
|
||
|
|
We also had to use the [gold linker](http://en.wikipedia.org/wiki/Gold_(linker)).
|
||
|
|
|
||
|
|
Gold linker
|
||
|
|
-----------
|
||
|
|
|
||
|
|
The gold linker is called `ld.gold` (in our test system). On Ubuntu, you
|
||
|
|
can install it by executing
|
||
|
|
|
||
|
|
sudo apt-get install binutils-gold
|
||
|
|
|
||
|
|
Before we compiled GMP, MPFR, Lua, and Lean, we created an alias
|
||
|
|
|
||
|
|
alias ld=ld.gold
|
||
|
|
|
||
|
|
If everything is working correctly, when we execute `ld --version`, we should
|
||
|
|
get an output like the following one:
|
||
|
|
|
||
|
|
GNU gold (GNU Binutils for Ubuntu 2.22) 1.11
|
||
|
|
Copyright 2011 Free Software Foundation, Inc.
|
||
|
|
...
|
||
|
|
|
||
|
|
Compiling GMP using split-stacks
|
||
|
|
--------------------------------
|
||
|
|
|
||
|
|
- Download GMP from [https://gmplib.org](https://gmplib.org/)
|
||
|
|
- Uncompress the gmp tar-ball at `$HOME/tools`
|
||
|
|
- Configure it using
|
||
|
|
|
||
|
|
./configure CFLAGS=-fsplit-stack --prefix=$HOME/tools/split-stack --enable-static
|
||
|
|
|
||
|
|
- Build
|
||
|
|
|
||
|
|
make
|
||
|
|
|
||
|
|
- Install
|
||
|
|
|
||
|
|
make install
|
||
|
|
|
||
|
|
We should have the file `libgmp.a` at `$HOME/tools/split-stack/lib`.
|
||
|
|
|
||
|
|
Compiling MPFR using split-stacks
|
||
|
|
----------------------------------
|
||
|
|
|
||
|
|
- Download MPFR from [http://www.mpfr.org/](http://www.mpfr.org/)
|
||
|
|
- Uncompress the mpfr tar-ball at `$HOME/tools`
|
||
|
|
- Configure it using
|
||
|
|
|
||
|
|
./configure CFLAGS=-fsplit-stack --prefix=$HOME/tools/split-stack --with-gmp-include=$HOME/tools/split-stack/include --with-gmp-lib=$HOME/tools/split-stack/lib --enable-static
|
||
|
|
|
||
|
|
Make sure MPFR does not produce any warning/error message
|
||
|
|
|
||
|
|
- Build
|
||
|
|
|
||
|
|
make
|
||
|
|
|
||
|
|
- Install
|
||
|
|
|
||
|
|
make install
|
||
|
|
|
||
|
|
We should have the file `libmpfr.a` at `$HOME/tools/split-stack/lib`.
|
||
|
|
|
||
|
|
Compiling Lua using split-stacks
|
||
|
|
--------------------------------
|
||
|
|
|
||
|
|
- Download Lua from [http://www.lua.org/](http://www.lua.org/)
|
||
|
|
- Uncompress the Lua tar-ball at `$HOME/tools`
|
||
|
|
- Modify the following line in the file `src/Makefile` in the Lua directory
|
||
|
|
|
||
|
|
CFLAGS= -O2 -Wall -DLUA_COMPAT_ALL $(SYSCFLAGS) $(MYCFLAGS)
|
||
|
|
|
||
|
|
We should include the option `-fsplit-stack`
|
||
|
|
|
||
|
|
CFLAGS= -O2 -fsplit-stack -Wall -DLUA_COMPAT_ALL $(SYSCFLAGS) $(MYCFLAGS)
|
||
|
|
|
||
|
|
- Build
|
||
|
|
|
||
|
|
make linux
|
||
|
|
|
||
|
|
- Install
|
||
|
|
|
||
|
|
make linux install INSTALL_TOP=$HOME/tools/split-stack
|
||
|
|
|
||
|
|
We should have the file `liblua.a` at `$HOME/tools/split-stack/lib`.
|
||
|
|
|
||
|
|
Compiling Lean using split-stacks
|
||
|
|
--------------------------------
|
||
|
|
|
||
|
|
- Go to the Lean directory
|
||
|
|
- Create the folder `build/release`
|
||
|
|
|
||
|
|
mkdir build/release
|
||
|
|
|
||
|
|
- Configure it using
|
||
|
|
|
||
|
|
cmake -D CMAKE_BUILD_TYPE=Release -D CMAKE_CXX_COMPILER=g++ -D TCMALLOC=OFF -D LUA_LIBRARIES=$HOME/tools/split-stack/lib/liblua.a -D LUA_INCLUDE_DIR=$HOME/tool/split-stack/include -D GMP_INCLUDE_DIR=$HOME/tools/split-stack/include -D GMP_LIBRARIES=$HOME/tools/split-stack/lib/libgmp.a -D MPFR_LIBRARIES=$HOME/tools/split-stack/lib/libmpfr.a ../../src
|
||
|
|
|
||
|
|
Remark: if you have ninja build tool installed in your system, you can also provide `-G Ninja`
|
||
|
|
|
||
|
|
- Build
|
||
|
|
|
||
|
|
make
|
||
|
|
|
||
|
|
- Test it
|
||
|
|
|
||
|
|
yes "C" | ctest
|