[CI] Build and release Win64 binaries (#8321)

This commit adds a check that cross-compiles a Windows binary, fixes
some minor issues to make the Windows build work, and adds support for
publishing a Windows binary to a (micro-)release.

Note: Regressions are currently not run for Windows builds.

diff --git a/.github/actions/add-to-release/action.yml b/.github/actions/add-to-release/action.yml
index a5939e20cda6910d951bcc6518f9405887b2fada..0bad0769f8896c5ef811165da5a8f2641b496e1c 100644 (file)
--- a/.github/actions/add-to-release/action.yml
+++ b/.github/actions/add-to-release/action.yml
@@ -3,6 +3,8 @@ description: Add cvc5 binary to the current release
 inputs:
   binary:
     description: file name of binary
+  release-name:
+    description: name of binary in release
   github-token:
     description: token to upload binary
 runs:
@@ -11,10 +13,10 @@ runs:
     - name: Rename binaries for release
       shell: bash
       run: |
-        cp ${{ inputs.binary }} cvc5-${{ runner.os }}
+        cp ${{ inputs.binary }} ${{ inputs.release-name }}
 
     - name: Add binaries to release
       uses: softprops/action-gh-release@v1
       with:
         token: ${{ inputs.github-token }}
-        files: cvc5-*
+        files: ${{ inputs.release-name }}

diff --git a/.github/actions/install-dependencies/action.yml b/.github/actions/install-dependencies/action.yml
index a27758c055a211518b9736b2f14ba7f8d61f9c80..33a645490fa312d695dedc6b7723eaae3dceebd4 100644 (file)
--- a/.github/actions/install-dependencies/action.yml
+++ b/.github/actions/install-dependencies/action.yml
@@ -7,6 +7,9 @@ inputs:
     default: false
   with-python-packaging:
     default: false
+  windows-build:
+    default: false
+    type: boolean
 runs:
   using: composite
   steps:
@@ -44,6 +47,18 @@ runs:
         echo "/usr/lib/ccache" >> $GITHUB_PATH
         echo "::endgroup::"
 
+    - name: Install software for cross-compiling for Windows
+      # Boolean inputs are actually strings:
+      # https://github.com/actions/runner/issues/1483
+      if: inputs.windows-build == 'true'
+      shell: bash
+      run: |
+        echo "::group::Install software for cross-compiling for Windows"
+        sudo apt-get update
+        sudo apt-get install -y \
+          mingw-w64
+        echo "::endgroup::"
+
     # Note: macOS comes with a libedit; it does not need to brew-installed
     - name: Install macOS software
       if: runner.os == 'macOS'

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index f4a8b72424bd81d6df999ce10e42238b5193b010..7700bd50ec0cc373ce0414b1989d1742c65eecc3 100644 (file)
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -13,7 +13,7 @@ jobs:
             python-bindings: true
             build-documentation: true
             check-examples: true
-            store-to-release: true
+            store-to-release-name: cvc5-Linux
             exclude_regress: 3-4
             run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump
 
@@ -23,10 +23,18 @@ jobs:
             cache-key: production
             python-bindings: true
             check-examples: true
-            store-to-release: true
+            store-to-release-name: cvc5-macOS
             exclude_regress: 3-4
             run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump
 
+          - name: win64:production
+            os: ubuntu-latest
+            config: production --auto-download --win64
+            cache-key: productionwin64
+            windows-build: true
+            store-to-release-name: cvc5-Win64.exe
+            binary-ext: .exe
+
           - name: ubuntu:production-clang
             os: ubuntu-18.04
             env: CC=clang CXX=clang++
@@ -68,6 +76,7 @@ jobs:
       with:
         with-documentation: ${{ matrix.build-documentation }}
         with-python-bindings: ${{ matrix.python-bindings }}
+        windows-build: ${{ matrix.windows-build }}
 
     - name: Setup caches
       uses: ./.github/actions/setup-cache
@@ -87,6 +96,7 @@ jobs:
       run: ccache -s
 
     - name: Run tests
+      if: matrix.run_regression_args
       uses: ./.github/actions/run-tests
       with:
         build-dir: ${{ steps.configure-and-build.outputs.shared-build-dir }}
@@ -96,6 +106,7 @@ jobs:
         regressions-exclude: ${{ matrix.exclude_regress }}
   
     - name: Run tests
+      if: matrix.run_regression_args
       uses: ./.github/actions/run-tests
       with:
         build-dir: ${{ steps.configure-and-build.outputs.static-build-dir }}
@@ -112,10 +123,11 @@ jobs:
         build-dir: ${{ steps.configure-and-build.outputs.shared-build-dir }}
 
     - name: Add binary to release
-      if: matrix.store-to-release && startsWith(github.ref, 'refs/tags/')
+      if: matrix.store-to-release-binary && startsWith(github.ref, 'refs/tags/')
       uses: ./.github/actions/add-to-release
       with:
-        binary: ${{ steps.configure-and-build.outputs.static-build-dir }}/bin/cvc5
+        binary: ${{ steps.configure-and-build.outputs.static-build-dir }}/bin/cvc5${{ matrix.binary-ext }}
+        release-name: ${{ matrix.store-to-release-name }}
         github-token: ${{ secrets.GITHUB_TOKEN }}
 
 

diff --git a/CMakeLists.txt b/CMakeLists.txt
index ac654957ad86cdf83282e132cc98c54882f4a689..07ab9c214eb1f42f37db9e2526958947fd748e7f 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -198,6 +198,9 @@ add_check_cxx_supression_flag("-Wno-class-memaccess")
 
 if (WIN32)
   set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,--stack,100000000")
+
+  # ANTLR uses pragmas that certain versions of MinGW does not support
+  add_check_c_cxx_flag("-Wno-error=unknown-pragmas")
 endif ()
 
 #-----------------------------------------------------------------------------#

diff --git a/src/base/output.h b/src/base/output.h
index 9ae5ad8db9775fd984a452512c9f984cf10ed332..d51a130020ac4a53630b51424b8f1b47312d9916 100644 (file)
--- a/src/base/output.h
+++ b/src/base/output.h
@@ -29,10 +29,6 @@
 
 namespace cvc5 {
 
-template <class T, class U>
-std::ostream& operator<<(std::ostream& out,
-                         const std::pair<T, U>& p) CVC5_EXPORT;
-
 template <class T, class U>
 std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) {
   return out << "[" << p.first << "," << p.second << "]";
@@ -60,10 +56,10 @@ extern null_streambuf null_sb;
 /** A null output stream singleton */
 extern std::ostream null_os CVC5_EXPORT;
 
-class CVC5_EXPORT Cvc5ostream
+class Cvc5ostream
 {
-  static const std::string s_tab;
-  static const int s_indentIosIndex;
+  static const std::string s_tab CVC5_EXPORT;
+  static const int s_indentIosIndex CVC5_EXPORT;
 
   /** The underlying ostream */
   std::ostream* d_os;
@@ -111,7 +107,23 @@ class CVC5_EXPORT Cvc5ostream
   std::ostream* getStreamPointer() const { return d_os; }
 
   template <class T>
-  Cvc5ostream& operator<<(T const& t) CVC5_EXPORT;
+  Cvc5ostream& operator<<(T const& t)
+  {
+    if (d_os != nullptr)
+    {
+      if (d_firstColumn)
+      {
+        d_firstColumn = false;
+        long indent = d_os->iword(s_indentIosIndex);
+        for (long i = 0; i < indent; ++i)
+        {
+          d_os = &(*d_os << s_tab);
+        }
+      }
+      *d_os << t;
+    }
+    return *this;
+  }
 
   // support manipulators, endl, etc..
   Cvc5ostream& operator<<(std::ostream& (*pf)(std::ostream&))
@@ -157,22 +169,6 @@ inline Cvc5ostream& pop(Cvc5ostream& stream)
   return stream;
 }
 
-template <class T>
-Cvc5ostream& Cvc5ostream::operator<<(T const& t)
-{
-  if(d_os != NULL) {
-    if(d_firstColumn) {
-      d_firstColumn = false;
-      long indent = d_os->iword(s_indentIosIndex);
-      for(long i = 0; i < indent; ++i) {
-        d_os = &(*d_os << s_tab);
-      }
-    }
-    d_os = &(*d_os << t);
-  }
-  return *this;
-}
-
 /**
  * Does nothing; designed for compilation of non-debug/non-trace
  * builds.  None of these should ever be called in such builds, but we