Skip to content

Latest commit

 

History

History
217 lines (130 loc) · 7.43 KB

COMPILING_WINDOWS.md

File metadata and controls

217 lines (130 loc) · 7.43 KB
Raw

Boolector installation steps on Windows

Important preamble

These steps document what is necessary to build a 64-bit version of pyboolector.pyd on 64-bit Windows. They also do not guarantee the correctness of other parts of Boolector (e.g., the main boolector.exe).

To ensure the portability of pyboolector.pyd, every effort is made in this guide to avoid building Boolector with Cygwin (e.g., we wish to avoid a dependency on cygwin1.dll, which could affect the portability of pyboolector.pyd). Given this, the guide is written to use the MinGW-W64 "cross-compiler".

These notes are purposefully very detailed to allow for someone to go from a completely fresh Windows 10 installation to a working version of Boolector.

Finally, some of Boolector's dependencies have been heavily modified to allow them to build on Windows. This means that functionality such as timeouts might be completely inoperable on Windows.

Dependencies

MinGW

Install MinGW-W64 from here:

You should select the "MinGW-W64 Online Installer" (MinGW-W64-install.exe).

The following options are recommended and have been tested when writing this guide:

  • Version: 8.1.0
  • Architecture: x86_64
  • Threads: win32
  • Exception: seh (default)
  • Build revision: 0 (default)

When selecting the threading model, only the win32 threading model has been validated -- the POSIX model has not been tested at all. On Windows, Boolector's make system has been modified to statically link, expecting the win32 model.

MSYS

Install MSYS from here:

It is important to select the 64-bit installation option (msys2-x86_64-<DATE>.exe). There are no further choices to be made when installing MSYS.

Once MSYS is installed, start an MSYS shell, and run pacman -Syuu. Once this is complete, it will ask you to close the shell. Close MSYS, re-open it and re-run pacman -Syuu again. Once it is complete the second time, close and re-open MSYS. This process needs to be performed twice to allow for MSYS to first update itself, and then update its packages.

Now install the following:

  • pacman -S --needed make git vim wget patch tar

Python 3.8

Install the most recent 64-bit Python 3.8 from here:

You should download the "Windows x86-64 executable installer". If you wish to avoid Python being installed into your AppData folder, you should choose to customise the installation, and select "Install for all users" (recommended for the purposes of following these instructions).

Update your %PATH% variable to include both the path to python.exe and to the Scripts sub-directory of the Python installation. These paths will look something like:

  • C:\Program Files\Python38
  • C:\Program Files\Python38\Scripts

If you installed Python for only the current user, the paths will look something like:

  • C:\Users\%USERNAME%\AppData\Local\Programs\Python\Python38
  • C:\Users\%USERNAME%\AppData\Local\Programs\Python\Python38\scripts

You need to ensure that these paths appear before %USERPROFILE%\AppData\Local\Microsoft\WindowsApps, otherwise Window's "wrapper" to install Python will get invoked.

Once your %PATH% is set correctly, start cmd and run the following:

  • python -m pip install --upgrade pip
  • python -m pip install --upgrade cython

If you installed Python system-wide (e.g., in to the default path of C:\Program Files\Python38), you should ensure that the above commands are run inside of an administrative cmd, such that the packages get installed into the global Python installation.

CMake

The version of CMake that comes with MSYS does not correctly support MSYS Makefiles (strangely). You should download the most recent version of CMake from here:

Downloading "Windows win64-x64 ZIP" (cmake-<VERSION>-win64-x64.zip) is sufficient. You do not need the installer.

When this is downloaded, extract the zip, but remember the path you extracted it to! You will need it later to the set the variable CMAKE_DIR. The rest of this guide assumes you have extracted CMake to the root of your C: drive.

Building Boolector

Configuring Boolector's build environment

Now that you have installed all of the necessary dependencies for Boolector, we need to configure our build environment. Start an MSYS shell, enter the directory you wish to build Boolector in, and create a file called vars.sh. The file should have the following content:

#!/bin/bash

set -eu

# **Important**
#
# If you installed Python for only the current user, pay particular attention
# to the value of `PYTHON_DIR`. Before calling `cygpath -u`, call `cygpath -d`
# to remove the space.
#
export PYTHON_DIR=$(cygpath -u $(cygpath -d "C:\Program Files\Python38"))

export CMAKE_DIR=$(cygpath -u "C:\cmake-3.17.3-win64-x64")
export MINGW_DIR=$(cygpath -u "C:\Program Files\mingw-w64\x86_64-8.1.0-win32-seh-rt_v6-rev0\mingw64")

export PATH=${PYTHON_DIR}:${PATH}
export PATH=${PYTHON_DIR}/Scripts:${PATH}
export PATH=${CMAKE_DIR}/bin:${PATH}
export PATH=${MINGW_DIR}/bin:${PATH}

export DEBUG_FLAG=""
export COMPARCH=64

export EXTRA_FLAGS="-static-libstdc++ -static-libgcc"

# -DMS_WIN64 is required so the Python headers properly detect a 64-bit build
export COMPFLAGS="${EXTRA_FLAGS} -I${PYTHON_DIR}/include -m${COMPARCH} -DMS_WIN64"

if [ -z "$DEBUG_FLAG" ]; then
    COMPFLAGS="-O3 -DNDEBUG ${COMPFLAGS}"
fi

export CFLAGS="${COMPFLAGS} -std=gnu11"
export CXXFLAGS="${COMPFLAGS} -std=gnu++11"
export PYTHON_INCLUDE="${COMPFLAGS}"
export LDFLAGS="${EXTRA_FLAGS} -L${PYTHON_DIR}/lib"

export CC="gcc"
export CXX="g++"

set +eu

# EOF

Once you have created this file, you should run source vars.sh. You should now check the following:

  • which gcc
  • which python
  • which cmake
  • which cython

If any of these do not appear to look right, or return incorrect values, you need to check your contents of vars.sh -- pay special attention to CMAKE_DIR and MINGW_DIR!

Obtaining Boolector

Now that you have configured your environment, you should obtain a copy of Boolector:

  • git clone https://github.com/Boolector/boolector

Building Boolector

The following steps will allow you to build Boolector from the above clone:

#!/bin/bash

set -eu

cd boolector

#
# Download, patch and build Boolector's dependencies
#

./contrib/setup-picosat.sh
./contrib/setup-lingeling.sh
./contrib/setup-cadical.sh
./contrib/setup-btor2tools.sh

#
# Modify pyboolector.pyx to be "more Windows compatible"
#
./contrib/fix_cython_windows.sh

#
# Build Boolector
#
mkdir build
cd build
cmake .. -DPYTHON=ON -DIS_WINDOWS_BUILD=1 -G "MSYS Makefiles"
make -j12
cd ..

# EOF

Notes:

  • On Windows, the above setup scripts automatically patch the version of Boolector's dependencies to enable them to compile with Windows -- as per the start of this guide, these changes may dramatically change Boolector's behaviour.
  • The use of -G "MSYS Makefiles" is highly essential to allow you to build Boolector on Windows.

Testing Boolector

Now that you have built pyboolector.pyd, you can test it:

#!/bin/bash

# this script presumes it is run from the root of the Boolector clone

export PYTHONPATH=$(cygpath -d $(readlink -f build/lib))
python examples/api/python/api_usage_examples.py

# EOF

If you get uncaught exceptions on splice, then you probably did not run ./contrib/fix_cython_windows.sh before building.