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.

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

Conversation

NlightNFotis
Copy link
Contributor

This is a draft (for now) PR that adds a windows * make Github Actions
job. This is using the already existing cmake one as a template.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@codecov
Copy link

codecov bot commented Feb 22, 2021

Codecov Report

Merging #5855 (fb36d81) into develop (4daa686) will increase coverage by 0.65%.
The diff coverage is 84.23%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #5855      +/-   ##
===========================================
+ Coverage    72.89%   73.55%   +0.65%     
===========================================
  Files         1423     1430       +7     
  Lines       154229   155222     +993     
===========================================
+ Hits        112426   114170    +1744     
+ Misses       41803    41052     -751     
Impacted Files Coverage Δ
src/analyses/goto_check.cpp 88.03% <ø> (-0.25%) ⬇️
.../goto-instrument/goto_instrument_parse_options.cpp 61.19% <ø> (+2.99%) ⬆️
...rc/goto-instrument/goto_instrument_parse_options.h 100.00% <ø> (ø)
src/goto-instrument/goto_program2code.cpp 67.88% <ø> (-0.22%) ⬇️
src/goto-programs/goto_convert_class.h 87.30% <ø> (ø)
src/goto-diff/goto_diff_parse_options.cpp 59.63% <31.25%> (+0.95%) ⬆️
src/goto-analyzer/goto_analyzer_parse_options.cpp 75.43% <50.00%> (+2.18%) ⬆️
src/goto-programs/goto_program.h 90.72% <66.66%> (+1.35%) ⬆️
src/util/format_expr.cpp 85.65% <86.20%> (-0.73%) ⬇️
src/util/std_code.h 94.02% <90.90%> (+0.01%) ⬆️
... and 219 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update a4c81ef...fb36d81. Read the comment docs.

@NlightNFotis NlightNFotis force-pushed the port-msbuild-make-job branch 4 times, most recently from ed9fc89 to 573a49c Compare February 23, 2021 22:50
@NlightNFotis NlightNFotis force-pushed the port-msbuild-make-job branch 4 times, most recently from 67fca92 to 98aa6ca Compare March 4, 2021 13:40
@NlightNFotis NlightNFotis force-pushed the port-msbuild-make-job branch 11 times, most recently from 5e7cee5 to f495bab Compare March 10, 2021 15:46
@NlightNFotis NlightNFotis force-pushed the port-msbuild-make-job branch from f495bab to b439bb3 Compare March 10, 2021 16:05
@NlightNFotis NlightNFotis force-pushed the port-msbuild-make-job branch from b439bb3 to 8494c5e Compare March 10, 2021 16:25
@NlightNFotis NlightNFotis changed the title [CI] Add a first iteration of a make windows github action job. [CI] Add a make + windows github action job. Mar 10, 2021
@NlightNFotis NlightNFotis force-pushed the port-msbuild-make-job branch from 8494c5e to fdb4df4 Compare March 10, 2021 18:14
Copy link
Contributor

@thomasspriggs thomasspriggs left a comment

Choose a reason for hiding this comment

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

One general nit pick here is that your commit messages titles should not end in a full stop and your commit message bodies should explain why you are making the change. See - Chis Beams full stop and Chris Beams why not how.

Nit picks aside, congratulations on finally getting this working.

@@ -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

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 :-)

When a user installs winflexbison on Windows, by default
the binaries are named win_flex and win_bison. This commit
aligns our configuration with the environment default.
@NlightNFotis NlightNFotis force-pushed the port-msbuild-make-job branch from fdb4df4 to 5ee53fa Compare March 11, 2021 10:35
Copy link
Contributor

@thomasspriggs thomasspriggs left a comment

Choose a reason for hiding this comment

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

LGTM.

Copy link
Contributor

@chrisr-diffblue chrisr-diffblue left a comment

Choose a reason for hiding this comment

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

It seems like the contentious part of the PR only affects VS builds, and not all windows builds - which perhaps was a bit of context missing from the original PR/commit history. Happy for this to go in.

.gitattributes Outdated
@@ -7,5 +7,5 @@
*.html text
*.css text
*.inc text
test.desc text
*.desc text eol=lf
Copy link
Collaborator

Choose a reason for hiding this comment

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

Can we fix test.pl instead? I've read rumours that Strawberry Perl isn't doing a good job adapting to the OS, so maybe we should just accept that there are perl implementations that don't play ball. I believe all that it takes is replacing chomp in line 79 of test.pl by some use of s/\R$//.

Copy link
Collaborator

Choose a reason for hiding this comment

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

More concretely: Replacing chomp @data; by s/\R$// for @data; should do the trick.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I'm happy with this if this works. I will wait for CI and if this is working, I am going to merge it.

Previously we had problems with test.pl choking on test.desc
file input on windows as a result of the test.pl files being
checkout out by git with CRLF instead of LF as line endings.
This includes tests under:
  * regression/cpp
  * regression/cbmc-cpp
  * regression/systemc
@NlightNFotis NlightNFotis force-pushed the port-msbuild-make-job branch from 5ee53fa to fb36d81 Compare March 11, 2021 14:33
@NlightNFotis NlightNFotis merged commit 1244577 into diffblue:develop Mar 11, 2021
@NlightNFotis NlightNFotis deleted the port-msbuild-make-job branch March 11, 2021 16:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

6 participants