I wanted to build a windows binary of Lean theorem prover while satisfying the following constraints:
- need C++11-compatible compilers: gcc (>=4.8) or clang (>= 3.3)
- need additional libraries — gmp, mpfr
- want to avoid CYGWIN, you know w-h-y
- prefer to build (cross-compile) on Linux/OS X to integrate with our automatic build system
I found that MXE can satisfy all the constraints:
MXE (M cross environment) is a Makefile that compiles a cross compiler and cross compiles many free libraries…
- It uses mingw-w64.
- You can easily compile gcc and other libraries such as gmp and mpfr.
- It supports cmake, which makes my life easier.
- Check out
cd /tmp/ git clone -b stable https://github.com/mxe/mxe.git
MXE_TARGETS=x86_64-w64-mingw32specifies that we only build for the x86_64 architecture.
-j4means upto four packages are built in parallel (inter-package) and
JOBS=4allows four compiler processes to compile a package in parallel (intra-package).
make MXE_TARGETS='x86_64-w64-mingw32' gcc gmp mpfr winpthreads lua -j4 JOBS=4
- By default,
gccis configured with
--enable-threads=win32and it does not support C++11
<future>(for more information, read this). To support C++11, we need to configure
gccusing posix threads. Modify the line 12 and 43 of
... 12: $(PKG)_DEPS := binutils gcc-cloog gcc-gmp gcc-isl gcc-mpc \ gcc-mpfr winpthreads ... 43: --enable-threads=posix \
gccagain. Yes, you need to build
gcctwice due to the circular dependency between
gcc. (Please let me know if you know a better way)
make MXE_TARGETS='x86_64-w64-mingw32' winpthreads gcc -j4 JOBS=4
Cross-compile Lean with cmake
After setting up mxe, type the followings to cross-compile Lean:
cd <LEAN_DIR> mkdir build/release-cross cd build/release-cross cmake -DCMAKE_BUILD_TYPE=RELEASE ../../src -DTCMALLOC=OFF \ -DCMAKE_TOOLCHAIN_FILE=/tmp/mxe/usr/x86_64-w64-mingw32/share/cmake/mxe-conf.cmake make
I prepared a cross-compilation environment which can be used to compile Lean in Ubuntu systems. To use it, please follow the instructions:
cd /tmp mkdir mxe cd mxe wget http://dl.dropboxusercontent.com/u/203889738/gcc/mxe-gcc-4.8.2.tar.bz2 tar xvfj mxe-gcc-4.8.2.tar.bz2
How to use newer version of GCC
We found a problem while using the default gcc shipped with MXE — gcc-4.8.2. When thread_local is used in a program, gcc-4.8.2 generates a binary which crashes when executed.
To fix this, we use the latest version of gcc-4.8, gcc-4.8.3 (snapshot 20131205). To use this, you need to modify the top part of src/gcc.mk as follows:
# This file is part of MXE. # See index.html for further information. PKG := gcc $(PKG)_IGNORE := $(PKG)_VERSION := 4.8-20131205 $(PKG)_CHECKSUM := b5e77ad4395561ac3f13f3a635ed5d704bab3786 $(PKG)_SUBDIR := gcc-$($(PKG)_VERSION) $(PKG)_FILE := gcc-$($(PKG)_VERSION).tar.bz2 $(PKG)_URL := ftp://ftp.mirrorservice.org/sites/sourceware.org/pub/gcc/snapshots/4.8-20131205/$($(PKG)_FILE) $(PKG)_DEPS := mingwrt w32api mingw-w64 binutils gcc-gmp gcc-mpc gcc-mpfr
Basically, you can follow the same instructions to build a cross-compile environment using gcc-4.8.3 (20131205). We also prepared a pre-compiled one using gcc-4.8.3. You can download it at here.
cmake-2.8.12 has a conflict with
mxe-conf.cmake, it resets
CMAKE_FIND_ROOT_PATH and it affects
CMAKE_DETERMINE_COMPILER_ID function which is modified in version
2.8.12. For now, it is best to use version 22.214.171.124.