From 73673dc7fae0fb4ff35a968556e612a9e2159cbb Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 16 Mar 2022 14:29:27 -0700 Subject: [PATCH] [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. --- .github/actions/add-to-release/action.yml | 6 ++- .../actions/install-dependencies/action.yml | 15 +++++++ .github/workflows/ci.yml | 20 +++++++-- CMakeLists.txt | 3 ++ src/base/output.h | 44 +++++++++---------- 5 files changed, 58 insertions(+), 30 deletions(-) diff --git a/.github/actions/add-to-release/action.yml b/.github/actions/add-to-release/action.yml index a5939e20c..0bad0769f 100644 --- 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 a27758c05..33a645490 100644 --- 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 f4a8b7242..7700bd50e 100644 --- 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 ac654957a..07ab9c214 100644 --- 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 9ae5ad8db..d51a13002 100644 --- a/src/base/output.h +++ b/src/base/output.h @@ -29,10 +29,6 @@ namespace cvc5 { -template -std::ostream& operator<<(std::ostream& out, - const std::pair& p) CVC5_EXPORT; - template std::ostream& operator<<(std::ostream& out, const std::pair& 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 - 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 -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 -- 2.30.2