Skip to content

[CI] Add a make + windows github action job. #5855

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Mar 11, 2021
Merged

[CI] Add a make + windows github action job. #5855

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
d436d86
Add a make + windows CI configuration for github actions.
NlightNFotis Feb 22, 2021
c60fc86
Change make commons to invoke win_flex and win_bison.
NlightNFotis Feb 23, 2021
211f198
Make test.pl capable of handling CRLF.
NlightNFotis Mar 11, 2021
fb36d81
Ignore regression tests marked winbug on windows make builds.
NlightNFotis Mar 9, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
53 changes: 53 additions & 0 deletions .github/workflows/pull-request-checks.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -277,6 +277,59 @@ jobs:
Set-Location build
ctest -V -L CORE -C Release . -j2

check-vs-2019-make-build-and-test:
runs-on: windows-2019
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
steps:
- uses: actions/checkout@v2
with:
submodules: recursive
- name: Fetch dependencies
run: |
choco install winflexbison3 strawberryperl
nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0
echo "c:\tools\clcache\clcache-4.1.0" >> $env:GITHUB_PATH
echo "c:\ProgramData\chocolatey\bin" >> $env:GITHUB_PATH
echo "c:\Strawberry\" >> $env:GITHUB_PATH
- name: Setup MSBuild
uses: microsoft/[email protected]
- name: Initialise Developer Command Line
uses: ilammy/msvc-dev-cmd@v1
- name: Prepare ccache
uses: actions/cache@v2
with:
path: .ccache
key: ${{ runner.os }}-msbuild-make-${{ github.ref }}-${{ github.sha }}-PR
restore-keys: |
${{ runner.os }}-msbuild-make-${{ github.ref }}
${{ runner.os }}-msbuild-make
- name: ccache environment
run: |
echo "CLCACHE_BASEDIR=$((Get-Item -Path '.\').FullName)" >> $env:GITHUB_ENV
echo "CLCACHE_DIR=$pwd\.ccache" >> $env:GITHUB_ENV
- name: Download minisat with make
run: make -C src minisat2-download
- name: Build CBMC with make
run: make CXX=clcache BUILD_ENV=MSVC -j2 -C src
- name: Build unit tests with make
run: make CXX=clcache BUILD_ENV=MSVC -j2 -C unit all
- name: Build jbmc with make
run: |
make CXX=clcache -j2 -C jbmc/src setup-submodules
make CXX=clcache BUILD_ENV=MSVC -j2 -C jbmc/src
- name: Build JBMC unit tests
run: make CXX=clcache BUILD_ENV=MSVC -j2 -C jbmc/unit all
- name: Print ccache stats
run: clcache -s
- name: Run CBMC and JBMC unit tests
run: |
make CXX=clcache BUILD_ENV=MSVC -C unit test
make CXX=clcache BUILD_ENV=MSVC -C jbmc/unit test
- name: Run CBMC regression tests
run: make CXX=clcache BUILD_ENV=MSVC -C regression test


check-clang-format:
runs-on: ubuntu-20.04
steps:
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ include ../../src/config.inc
include ../../src/common

ifeq ($(BUILD_ENV_),MSVC)
excluded_tests = -X gcc-only
excluded_tests = -X gcc-only -X winbug
else
# In MacOS, a change in the assert.h header file
# is causing template errors when exercising the
Expand Down
2 changes: 1 addition & 1 deletion regression/cpp/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ else
endif

ifeq ($(BUILD_ENV_),MSVC)
excluded_tests = -X gcc-only
excluded_tests = -X gcc-only -X winbug
else
# In MacOS, a change in the assert.h header file
# is causing template errors when exercising the
Expand Down
15 changes: 14 additions & 1 deletion regression/systemc/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,17 @@
ifneq ($(BUILD_ENV_),MSVC)
default: tests.log

include ../../src/config.inc
include ../../src/common

ifeq ($(BUILD_ENV_),MSVC)
exe = ../../../src/goto-cc/goto-cl
else
exe = ../../../src/goto-cc/goto-cc
endif

ifeq ($(BUILD_ENV_),MSVC)
excluded_tests = -X gcc-only -X winbug
else
# In MacOS, a change in the assert.h header file
# is causing template errors when exercising the
# C++ front end (because of a transitive include
Expand Down
2 changes: 1 addition & 1 deletion regression/test.pl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ ($$)
my @data = grep { !/^\/\// } <FILE>;
close FILE;

chomp @data;
s/\R$// for @data;
if($exit_signal_checks) {
grep { /^\^EXIT=[\(\|\d]*\d+\)?\$$/ } @data or die "$fname: Missing EXIT test\n";
grep { /^\^SIGNAL=\d+\$$/ } @data or die "$fname: Missing SIGNAL test\n";
Expand Down
4 changes: 2 additions & 2 deletions src/common
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -146,11 +146,11 @@ ifeq ($(origin CXX),default)
CXX = cl
endif
ifeq ($(origin YACC),default)
YACC = bison -y
YACC = win_bison -y
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⛏️ I am guessing this is required due to the names used by the versions of flex/bison we are using in the new job. But can you add the rationale to the commit message body so A) I don't have to guess B) Anyone who starts seeing local failures due to using different versions, knows there was a reason for doing this. Not just to ruin their day ;)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

May I suggest to simply override this variable when calling make. This way, local builds won't be broken.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's worth noting here that when someone installs winflexbison (https://github.com/lexxmark/winflexbison) the default binaries are called win_flex and win_bison. It takes an extra manual step to rename these to flex or bison

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this the only place that people could possibly source flex/bison for Windows from? Putting it differently, I don't recall hearing from anyone that they were unhappy with our Makefiles for Windows, which either means that no one is using them or existing users have a working set-up. So I'm with @kroening: set YACC='win_bison -y' and LEX=win_flex on the command-line.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There are many ways to get Flex / Bison on Windows. If a user has a build environment based on Cygwin or MSYS2 for example then the packages for those environments may still be using the original names. I'd need to check to know for sure, but I don't have a Windows machine on hand.

Copy link
Contributor Author

@NlightNFotis NlightNFotis Mar 11, 2021 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@tautschnig Are we sure we want to do that? Just for clarification, there are 3 potential configurations for building on windows (that I can see in src/common), and they are Cygwin, MSVC and MinGW based. For them:

  1. The MinGW configuration is inheriting flex and bison binary names from the default configuration,
  2. The Cygwin configuration also sets them explicitly to flex and bison, and
  3. The MSVC configuration is the one I changed to address win_flex and win_bison, which are the default binaries a user should end up with if he installs winflexbison (which is the default way a programmer would acquire these to use them with Visual Studio today, to my understanding).

So, I guess my question is: Does this really break anything? Alternative build environments on Windows should not be affected in any capacity (if a user is using Cygwin or MinGW) and the MSVC one I can argue that was misconfigured (or at least stale by current standards).

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have now taken another look at the rest of this file. I have now seen that there are other sets of configuration in this file for cygwin and mingw. Therefore I am less concerned about explicitly changing this for Visual Studio only. I am happy for this change to be merged as is.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So, I guess my question is: Does this really break anything? [...] and the MSVC one I can argue that was misconfigured [...]

I simply did not know whether winflexbison was the (single?) most common approach. If you're confident that's the case, then, sure, let's go with it. My concern was breaking existing user's set-ups, but if it seems unlikely that anyone was (successfully) using this configuration, then there shouldn't be a problem. Well, if there is, people will tell us and we can revert :-)

endif
YFLAGS ?= -v
ifeq ($(origin LEX),default)
LEX = flex
LEX = win_flex
endif


Expand Down