Merge pull request #11 from GaloisInc/windows-yices

Re-enable Yices builds on Windows Closes #5 Closes #7
GaloisInc · Sep 17, 2021 · cc5ea80 · cc5ea80
2 parents 10eb358 + 75a48de
commit cc5ea80
Show file tree

Hide file tree

Showing 3 changed files with 178 additions and 63 deletions.
diff --git a/.github/ci.sh b/.github/ci.sh
@@ -23,13 +23,14 @@ build_abc() {
     sed -i.bak -e 's/-ldl//' Makefile
     sed -i.bak2 -e 's/-lrt//' Makefile
     echo "double Cudd_CountMinterm( DdManager * manager, DdNode * node, int nvars ) { return 0.0; }" >> src/base/abci/abc.c
-    make ABC_USE_NO_READLINE=1 ABC_USE_NO_PTHREADS=1 ABC_USE_NO_CUDD=1 CXXFLAGS="-fpermissive -DNT64" CFLAGS="-DNT64" -j4 abc
+    make ABC_USE_NO_READLINE=1 ABC_USE_NO_PTHREADS=1 ABC_USE_NO_CUDD=1 CXXFLAGS="-fpermissive -DNT64" CFLAGS="-DNT64" LDFLAGS="-static" -j4 abc
   else
     make -j4 abc
   fi
   cp abc$EXT $BIN
   (cd $BIN && deps abc$EXT && ./abc$EXT -S "%blast; &sweep -C 5000; &syn4; &cec -m -s" < $PROBLEM)
   popd
+  cleanup_bins
 }
 
 build_cvc4() {
@@ -38,6 +39,7 @@ build_cvc4() {
     echo "Downloading pre-built CVC4 binary for Windows"
     curl -o cvc4$EXT -sL "https://github.com/CVC4/CVC4/releases/download/1.8/cvc4-1.8-win64-opt.exe"
     cp cvc4$EXT $BIN
+    deps cvc4$EXT
   else
     ./contrib/get-antlr-3.4
     ./configure.sh --static --no-static-binary production
@@ -47,72 +49,95 @@ build_cvc4() {
     (cd $BIN && ./cvc4$EXT --version && deps cvc4$EXT && ./cvc4$EXT $PROBLEM)
   fi
   popd
+  cleanup_bins
 }
 
 build_yices() {
-  if "$IS_WIN"; then
-    echo "Downloading pre-built Yices binary for Windows"
-    curl -o yices.zip -sL "https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-mingw32-static-gmp.zip"
-    unzip yices.zip
-    cp yices-*/bin/* $BIN
-    mv $BIN/yices-sat.exe $BIN/yices_sat.exe
-    mv $BIN/yices-smt.exe $BIN/yices_smt.exe
-    mv $BIN/yices-smt2.exe $BIN/yices_smt2.exe
+  if $IS_WIN ; then
+    export CC=x86_64-w64-mingw32-gcc
+    export CXX=x86_64-w64-mingw32-g++
+  fi
+  export CFLAGS="-I$TOP/install-root/include -I$TOP/repos/libpoly/src -I$TOP/repos/libpoly/include"
+  export CXXFLAGS="-I$TOP/install-root/include -I$TOP/repos/libpoly/src -I$TOP/repos/libpoly/include"
+  export LDFLAGS="-L$TOP/install-root/lib"
+  if $IS_WIN ; then
+    export CONFIGURE_FLAGS="--build=x86_64-w64-mingw32 --prefix=$TOP/install-root"
   else
-    export CPPFLAGS="-I$TOP/install-root/include"
-    export LDFLAGS="-L$TOP/install-root/lib"
+    export CONFIGURE_FLAGS="--prefix=$TOP/install-root"
+  fi
 
-    mkdir install-root
-    mkdir install-root/include
-    mkdir install-root/lib
+  mkdir install-root
+  mkdir install-root/include
+  mkdir install-root/lib
 
-    # This is failing on Windows due to failing to find 'utils/open_memstream.h'
-    pushd repos/libpoly
-    cd build
-    if $IS_WIN; then
-      CPPFLAGS="$CPPFLAGS -I$TOP/repos/libpoly/src" cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_TOOLCHAIN_FILE=../cmake/x86_64-w64-mingw32.cmake -DLIBPOLY_BUILD_PYTHON_API=Off -DCMAKE_INSTALL_PREFIX=../install-root -DGMP_INCLUDE_DIR=/mingw64/include -DGMP_LIBRARY=/mingw64/lib/libgmp.a -DHAVE_OPEN_MEMSTREAM=0
-    else
-      cmake .. -DCMAKE_BUILD_TYPE=Release -DLIBPOLY_BUILD_PYTHON_API=Off -DCMAKE_INSTALL_PREFIX=$TOP/install-root
-    fi
-    make -j4
-    make install
-    popd
+  (cd repos && curl -o gmp.tar.lz -sL "https://gmplib.org/download/gmp/gmp-6.2.1.tar.lz" && tar xf gmp.tar.lz)
 
-    pushd repos/cudd
-    if [[ "$RUNNER_OS" == 'Linux' ]] ; then
-      autoreconf
-    fi
-    ./configure CFLAGS=-fPIC --prefix=$TOP/install-root
-    make -j4
-    make install
-    popd
+  pushd repos/gmp-6.2.1
+  ./configure $CONFIGURE_FLAGS
+  make -j4
+  make install
+  popd
+
+  pushd repos/cudd
+  case "$RUNNER_OS" in
+    Linux) autoreconf ;;
+    macOS) autoconf ;;
+    Windows) autoconf ;;
+  esac
+  ./configure CFLAGS=-fPIC $CONFIGURE_FLAGS
+  make -j4
+  make install
+  popd
 
-    pushd repos/yices2
-    autoconf
-    if $IS_WIN; then # Currently unreachable, but leaving in for when it's relevant again
-      ./configure --host=x86_64-w64-mingw32 --build=x86_64-w64-mingw32
-      cp configs/make.include.x86_64-w64-mingw32 configs/make.include.x86_64-pc-mingw64
-    else
-      ./configure --enable-mcsat
-    fi
-    make -j4 static-bin
-    cp build/*/static_bin/* $BIN
-    if [ -e $BIN/yices_smt2$EXT ] ; then cp $BIN/yices_smt2$EXT $BIN/yices-smt2$EXT ; else true ; fi
-    (cd $BIN && ./yices-smt2$EXT --version && deps yices-smt2$EXT && ./yices-smt2$EXT $PROBLEM)
-    popd
+  pushd repos/libpoly
+  cd build
+  if $IS_WIN; then
+    sed -i.bak -e 's/enable_testing()//' ../CMakeLists.txt
+    sed -i.bak -e 's/add_subdirectory(test\/polyxx)//' ../CMakeLists.txt
+    cmake .. -DCMAKE_TOOLCHAIN_FILE=$TOP/scripts/libpoly-x86_64-w64-mingw32.cmake -DCMAKE_INSTALL_PREFIX=$TOP/install-root -DGMP_INCLUDE_DIR=$TOP/install-root/include -DGMP_LIBRARY=$TOP/install-root/lib/libgmp.a -DLIBPOLY_BUILD_PYTHON_API=Off
+  else
+    cmake .. -DCMAKE_BUILD_TYPE=Release -DLIBPOLY_BUILD_PYTHON_API=Off -DCMAKE_INSTALL_PREFIX=$TOP/install-root
+  fi
+  make -j4 static_poly
+  cp ./src/libpoly.a $TOP/install-root/lib
+  mkdir -p $TOP/install-root/include/poly
+  cp -r ../include/*.h $TOP/install-root/include/poly
+  popd
+
+  pushd repos/yices2
+  autoconf
+  if $IS_WIN; then
+    ./configure --enable-mcsat $CONFIGURE_FLAGS
+    dos2unix src/frontend/smt2/smt2_tokens.txt
+    dos2unix src/frontend/smt2/smt2_keywords.txt
+    dos2unix src/frontend/smt2/smt2_symbols.txt
+    dos2unix src/frontend/smt1/smt_keywords.txt
+    dos2unix src/frontend/yices/yices_keywords.txt
+    cp configs/make.include.x86_64-w64-mingw32 configs/make.include.x86_64-pc-mingw64
+  else
+    ./configure --enable-mcsat $CONFIGURE_FLAGS
   fi
+  make -j4 static-bin
+  cp build/*/static_bin/* $BIN
+  if [ -e $BIN/yices_smt2$EXT ] ; then cp $BIN/yices_smt2$EXT $BIN/yices-smt2$EXT ; else true ; fi
+  (cd $BIN && ./yices-smt2$EXT --version && deps yices-smt2$EXT && ./yices-smt2$EXT $PROBLEM)
+  popd
+  cleanup_bins
 }
 
 build_z3() {
-  (cd repos/z3 && python scripts/mk_make.py && cd build && make -j4 && cp z3$EXT $BIN)
+  pushd repos/z3
+  if $IS_WIN ; then
+    sed -i.bak -e 's/STATIC_BIN=False/STATIC_BIN=True/' scripts/mk_util.py
+  fi
+  python scripts/mk_make.py
+  (cd build && make -j4 && cp z3$EXT $BIN)
+  popd
   (cd $BIN && ./z3$EXT --version && deps z3$EXT && ./z3$EXT $PROBLEM)
+  cleanup_bins
 }
 
-build_solvers() {
-  build_abc
-  build_yices
-  build_cvc4
-  build_z3
+cleanup_bins() {
   $IS_WIN || chmod +x $BIN/*
   strip $BIN/*
 }

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -10,12 +10,51 @@ env:
   CACHE_VERSION: 1
 
 jobs:
-  build:
+  build_simple:
     runs-on: ${{ matrix.os }}
     strategy:
       fail-fast: false
       matrix:
         os: [ubuntu-20.04, ubuntu-18.04, macos-10.15, windows-2019]
+        solver: [abc]
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          submodules: true
+          fetch-depth: 0
+
+      - name: Install dependencies (Windows)
+        uses: msys2/setup-msys2@v2
+        with:
+          update: true
+          msystem: MSYS
+          install: |
+            gcc
+            make
+        if: runner.os == 'Windows'
+
+      - name: build_solver (non-Windows)
+        shell: bash
+        run: .github/ci.sh build_${{ matrix.solver }}
+        if: runner.os != 'Windows'
+
+      - name: build_solver (Windows)
+        shell: msys2 {0}
+        run: .github/ci.sh build_${{ matrix.solver }}
+        if: runner.os == 'Windows'
+
+      - uses: actions/upload-artifact@v2
+        with:
+          path: bin
+          name: ${{ matrix.os }}-${{ matrix.solver }}-bin
+
+  build_complex:
+    runs-on: ${{ matrix.os }}
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [ubuntu-20.04, ubuntu-18.04, macos-10.15, windows-2019]
+        solver: [cvc4, yices, z3]
     steps:
       - uses: actions/checkout@v2
         with:
@@ -25,7 +64,7 @@ jobs:
       - name: Install dependencies (Ubuntu)
         run: |
           sudo apt-get update
-          sudo apt-get install gperf automake autoconf
+          sudo apt-get install gperf automake autoconf lzip
         if: runner.os == 'Linux'
 
       - name: Install dependencies (macOS)
@@ -38,16 +77,17 @@ jobs:
         uses: msys2/setup-msys2@v2
         with:
           update: true
-          msystem: MSYS
+          msystem: MINGW64
           install: |
             autoconf
+            automake
             cmake
-            gcc
+            dos2unix
             git
             gperf
+            lzip
             m4
             make
-            mingw-w64-x86_64-gmp
             mingw-w64-x86_64-gcc
             python
             unzip
@@ -62,16 +102,50 @@ jobs:
           packages: |
             toml
 
-      - name: build_solvers (non-Windows)
+      - name: build_solver (non-Windows)
         shell: bash
-        run: .github/ci.sh build_solvers
+        run: .github/ci.sh build_${{ matrix.solver }}
         if: runner.os != 'Windows'
 
-      - name: build_solvers (Windows)
+      - name: build_solver (Windows)
         shell: msys2 {0}
-        run: .github/ci.sh build_solvers
+        run: .github/ci.sh build_${{ matrix.solver }}
         if: runner.os == 'Windows'
 
+      - uses: actions/upload-artifact@v2
+        with:
+          path: bin
+          name: ${{ matrix.os }}-${{ matrix.solver }}-bin
+
+  package_solvers:
+    runs-on: ${{ matrix.os }}
+    needs: [build_simple, build_complex]
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [ubuntu-20.04, ubuntu-18.04, macos-10.15, windows-2019]
+    steps:
+
+      - uses: actions/download-artifact@v2
+        with:
+          name: "${{ matrix.os }}-abc-bin"
+          path: bin
+
+      - uses: actions/download-artifact@v2
+        with:
+          name: "${{ matrix.os }}-cvc4-bin"
+          path: bin
+
+      - uses: actions/download-artifact@v2
+        with:
+          name: "${{ matrix.os }}-yices-bin"
+          path: bin
+
+      - uses: actions/download-artifact@v2
+        with:
+          name: "${{ matrix.os }}-z3-bin"
+          path: bin
+
       - uses: actions/upload-artifact@v2
         with:
           path: bin
@@ -85,7 +159,6 @@ jobs:
   # - dependencies through `needs:` are validated, CI will fail if it's invalid
   mergify:
     runs-on: ubuntu-20.04
-    needs:
-      - build
+    needs: [build_simple, build_complex]
     steps:
       - run: "true"
diff --git a/scripts/libpoly-x86_64-w64-mingw32.cmake b/scripts/libpoly-x86_64-w64-mingw32.cmake
@@ -0,0 +1,17 @@
+# the name of the target operating system
+SET(CMAKE_SYSTEM_NAME Windows)
+
+SET(CMAKE_BUILD_TYPE Release)
+SET(HAVE_OPEN_MEMSTREAM 0)
+
+# which compilers to use for C and C++
+SET(CMAKE_C_COMPILER x86_64-w64-mingw32-gcc)
+SET(CMAKE_CXX_COMPILER x86_64-w64-mingw32-g++)
+SET(CMAKE_RC_COMPILER x86_64-w64-mingw32-windres)
+
+# adjust the default behaviour of the FIND_XXX() commands:
+# search headers and libraries in the target environment, search
+# programs in the host environment
+set(CMAKE_FIND_ROOT_PATH_MODE_PROGRAM NEVER)
+set(CMAKE_FIND_ROOT_PATH_MODE_LIBRARY ONLY)
+set(CMAKE_FIND_ROOT_PATH_MODE_INCLUDE ONLY)