Use CCache to speed up build times in GitHub actions

[tautschnig]

We used to do this on Travis and CodeBuild, let's also port this to
GitHub actions.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a 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.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Merging #5609 (1042403) into develop (f2d735a) will not change coverage.
The diff coverage is n/a.

@@           Coverage Diff            @@
##           develop    #5609   +/-   ##
========================================
  Coverage    69.32%   69.32%           
========================================
  Files         1241     1241           
  Lines       100443   100443           
========================================
  Hits         69636    69636           
  Misses       30807    30807           

Flag	Coverage Δ
cproversmt2	43.08% <ø> (ø)
regression	66.22% <ø> (ø)
unit	32.27% <ø> (ø)

Flags with carried forward coverage won't be shown. Click here to find out 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 f2d735a...1042403. Read the comment docs.

[tautschnig]

FWIW, I am planning to do a separate PR to clean up the vs-2019-build-and-test configuration and, once done, also make it use clcache.

[NlightNFotis]

For me this looks good, but I'd be wary of merging something that's actively breaking CI, even if it promises to fix it later.

[NlightNFotis]

Also, this won't be able to be merged because the check-vs-2019-build-and-test check is marked as required. Can the two PRs not be one?

[hannes-steffenhagen-diffblue]

Have you checked if this has a measurable performance improvement in subsequent builds?

EDIT NVM apparently it’s in the commit messages

[hannes-steffenhagen-diffblue]

Looks like one java unit test is failing due to what looks like a pretty sketchy pretty function. Relies on a lot of platform specific behaviour which seems unnecessary.

[tautschnig]

@NlightNFotis

Also, this won't be able to be merged because the check-vs-2019-build-and-test check is marked as required. Can the two PRs not be one?

@hannes-steffenhagen-diffblue

Looks like one java unit test is failing due to what looks like a pretty sketchy pretty function. Relies on a lot of platform specific behaviour which seems unnecessary.

Argh, this was fixed in #5613. I should have rebased this earlier today, my apologies.

[thomasspriggs]

The issue with the test actually appears to be a long-standing issue with the floating_point_to_java_string function when compiled under Visual Studio. I would say that the issue is with the function rather than the test. This is because 1) Java is usually intended to be platform independent and 2) because the doxygen for this function mentions not printing unnecessary zeros, but it is returning more zeros when compiled under visual studio than on other platforms. Therefore I would prefer to see the function under test fixed, rather than in increasing number of exceptions for different compilers added to the unit test.

[tautschnig]

The issue with the test actually appears to be a long-standing issue with the floating_point_to_java_string function when compiled under Visual Studio. I would say that the issue is with the function rather than the test. This is because 1) Java is usually intended to be platform independent and 2) because the doxygen for this function mentions not printing unnecessary zeros, but it is returning more zeros when compiled under visual studio than on other platforms. Therefore I would prefer to see the function under test fixed, rather than in increasing number of exceptions for different compilers added to the unit test.

+100, but #5613 was the quick way to stop the bleeding.

[thomasspriggs]

It is worth noting that the total cache size for the whole repository is limited to 5GB. Source - https://github.com/actions/cache#cache-limits

[tautschnig]

It is worth noting that the total cache size for the whole repository is limited to 5GB. Source - https://github.com/actions/cache#cache-limits

Yes, that's why I limited each job to 500 MB, I should perhaps have noted that in the commit message. GitHub also compresses the tar ball, making it around 50 MB it seems, so we can have quite a lot of cache keys before old ones are expired.