Nov 5, 2013

MXE: cross-compile windows binaries on ubuntu

This article introduces MXE (M cross environment) which helps set up a cross-compilation environment on *nix systems. Here, I use Lean theorem prover as a target program to illustrate the process.

Problem

I wanted to build a windows binary of Lean theorem prover while satisfying the following constraints:

  1. need C++11-compatible compilers: gcc (>=4.8) or clang (>= 3.3)
  2. need additional libraries — gmp, mpfr
  3. want to avoid CYGWIN, you know w-h-y
  4. prefer to build (cross-compile) on Linux/OS X to integrate with our automatic build system

Solution: MXE

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.

Setup

  • Check out MXE:
cd /tmp/
git clone -b stable https://github.com/mxe/mxe.git
  • Build gcc, gmp, mpfr, winpthreads and lua. MXE_TARGETS=x86_64-w64-mingw32 specifies that we only build for the x86_64 architecture. -j4 means upto four packages are built in parallel (inter-package) and JOBS=4 allows 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, gcc is configured with --enable-threads=win32 and it does not support C++11 <thread>, <mutex>, or <future> (for more information, read this). To support C++11, we need to configure gcc using posix threads. Modify the line 12 and 43 of src/gcc.mk:
...
 12: $(PKG)_DEPS     := binutils gcc-cloog gcc-gmp gcc-isl gcc-mpc \
                        gcc-mpfr winpthreads
...
 43:         --enable-threads=posix \
  • Make gcc again. Yes, you need to build gcc twice due to the circular dependency between winpthreads and 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

Precompiled Environment

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.

Known Issue

cmake-2.8.12 has a conflict with usr/x86_64-w64-mingw32/share/cmake/mxe-conf.cmake. In 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 2.8.11.2.