Update Release Process script and add Installation Instructions to the Release Page #5517

NlightNFotis · 2020-10-06T16:17:56Z

This PR adds Linux installation instructions to the top-level README.md file, and adds some installation instructions to the release page when a new release is happening.

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.

thomasspriggs

LGTM.

codecov · 2020-10-06T18:22:06Z

Codecov Report

Merging #5517 into develop will increase coverage by 0.83%.
The diff coverage is n/a.

@@             Coverage Diff             @@
##           develop    #5517      +/-   ##
===========================================
+ Coverage    67.56%   68.40%   +0.83%     
===========================================
  Files         1187     1187              
  Lines        98090    98090              
===========================================
+ Hits         66279    67102     +823     
+ Misses       31811    30988     -823

Flag	Coverage Δ
#cproversmt2	`42.96% <ø> (?)`
#regression	`65.55% <ø> (ø)`
#unit	`32.25% <ø> (ø)`

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files	Coverage Δ
src/util/simplify_expr_int.cpp	`80.08% <0.00%> (+0.27%)`	⬆️
src/solvers/lowering/byte_operators.cpp	`83.84% <0.00%> (+0.38%)`	⬆️
src/cbmc/cbmc_parse_options.cpp	`77.01% <0.00%> (+0.45%)`	⬆️
src/util/mp_arith.cpp	`40.14% <0.00%> (+0.70%)`	⬆️
src/solvers/flattening/boolbv.cpp	`69.09% <0.00%> (+0.90%)`	⬆️
src/util/std_expr.h	`89.48% <0.00%> (+1.10%)`	⬆️
src/util/std_types.h	`94.39% <0.00%> (+1.17%)`	⬆️
src/solvers/smt2/smt2_solver.cpp	`83.01% <0.00%> (+1.25%)`	⬆️
src/util/pointer_offset_size.cpp	`94.85% <0.00%> (+1.28%)`	⬆️
src/util/simplify_expr_array.cpp	`94.20% <0.00%> (+1.44%)`	⬆️
... and 10 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 b49f31f...b86bf12. Read the comment docs.

piotr-grabalski · 2020-10-07T13:18:45Z

.github/workflows/regular-release.yaml

+              * For Linux, install the `.deb` package with 
+                `sudo apt install $CBMC_TAG-Linux.deb` on Debian-like systems
+              * For macOS, install with `brew install cbmc` or upgrade with
+                `brew upgrade cbmc`


Would it be useful to have a link to readme installation part in here? Something like:

For additional installation instructions please visit: https://github.com/diffblue/cbmc/blob/develop/README.md#installing

@piotr-grabalski these instructions should be self contained. If they need to make reference to our README that is a defect.

piotr-grabalski

looks OK!

hannes-steffenhagen-diffblue

Some changes required, some questions

hannes-steffenhagen-diffblue · 2020-10-07T13:52:02Z

.github/workflows/regular-release.yaml

+              * For Linux, install the `.deb` package with 
+                `sudo apt install $CBMC_TAG-Linux.deb` on Debian-like systems
+              * For macOS, install with `brew install cbmc` or upgrade with
+                `brew upgrade cbmc`


👎 Please be a bit more elaborate here. In particular, this needs the note on Windows requiring the Visual Studio redistributable (see readme) and different names for the ubuntu 18 and ubuntu 20 packages. This would read better if it was presented with section headers instead of a bulleted list.

Again, I’d ask you to refer to https://github.com/markrtuttle/cbmc/releases/tag/cbmc-5.15.0-github-actions for this.

(Except the note about depending on gcc, as we do in fact declare this dependency in our debian files)

What you're seeing is not the final version of it, and the final version more accurately conforms to the presentation in the link given - this version is from yesterday.

hannes-steffenhagen-diffblue · 2020-10-07T13:54:00Z

README.md

+   with `root` privileges, with `x.y` being substituted for the version
+   you are attempting to install.
+   *NOTE*: This is only available on distributions that are using debian's
+   packaging tools.


👎 The debian packages are distro specific (due to link constraints against libc/libc++ and package dependency names), this needs to be noted here. We have two separate packages for Ubuntu 18.04 and Ubuntu 20.04, they shouldn’t be used anywhere else.

Okay... I was unaware of any link constraints we have, can you expand on this? At least libc ABI should be stable, and I would go on a limb and say that libc++ should be stable enough for our needs as well - why is it not?

But noted in any case, I'll update the documentation.

@NlightNFotis libc/libc++ ABI is stable, but not backwards compatible. You can link binaries linked against libc against newer versions of libc, but not older ones.

hannes-steffenhagen-diffblue · 2020-10-07T13:54:24Z

.github/workflows/regular-release.yaml

      - name: Create release
        uses: actions/create-release@v1
        env:
          GITHUB_TOKEN: ${{ secrets.DB_CI_CPROVER_ACCESS_TOKEN }}
+          CBMC_TAG: ${{ github.ref }}


Earlier one we had this problem that this is a 3 part slash separated thing. Is that not a concern anymore?

This doesn't reflect the changed code yet.

hannes-steffenhagen-diffblue · 2020-10-07T13:58:17Z

Also this adds a new expected release process that replaces the previous one. This needs to be documented somewhere.

martin-cs

Yes once @hannes-steffenhagen-diffblue 's comments have been addressed.

NlightNFotis · 2020-10-07T15:52:13Z

@martin-cs All of Hannes' comments have been worked on, and where on my todo before - it's just that you can't see the progress, because I'm playing around with another branch on my fork to make it easier to test the release process. I'm working on fixing one last thing, then I will clean this up and it should be good to go.

chrisr-diffblue

Mostly looks good, just a couple of minor things to tweak if possible.

README.md

.github/workflows/regular-release.yaml

Remove scheduling from regular release script (because any update to the files requires a signoff by a code owner, which is infeasible) and add installation instructions to release body.

chrisr-diffblue

LGTM - Thanks for documenting both the process, and the decision making behind it really well!

hannes-steffenhagen-diffblue · 2020-10-08T15:15:48Z

README.md

+   package maintenance policy of the distribution is, or
+2. Install CBMC through the `.deb` package built by each release, available
+   on the [releases](https://github.com/diffblue/cbmc/releases) page. To
+   do that, download the `.deb` package and run `apt install cbmc-x.y.deb`


Nit: more stable version of this is dpkg -i, but if apt install also works I guess it works.

I think apt is always preferable, as it's a higher level tool and can do dependency management better than dpkg.

hannes-steffenhagen-diffblue

Thanks for keeping up with my nagging, I think this is pretty good now!

NlightNFotis requested review from chrisr-diffblue, kroening, peterschrammel, smowton and tautschnig as code owners October 6, 2020 16:17

NlightNFotis self-assigned this Oct 6, 2020

thomasspriggs approved these changes Oct 6, 2020

View reviewed changes

piotr-grabalski reviewed Oct 7, 2020

View reviewed changes

piotr-grabalski approved these changes Oct 7, 2020

View reviewed changes

hannes-steffenhagen-diffblue reviewed Oct 7, 2020

View reviewed changes

martin-cs approved these changes Oct 7, 2020

View reviewed changes

NlightNFotis force-pushed the ada-637-release-page-instructions branch from 1ce2de7 to 4401b34 Compare October 8, 2020 11:37

chrisr-diffblue reviewed Oct 8, 2020

View reviewed changes

README.md Outdated Show resolved Hide resolved

README.md Outdated Show resolved Hide resolved

.github/workflows/regular-release.yaml Show resolved Hide resolved

Fotis Koutoulakis added 3 commits October 8, 2020 15:16

Add installation instructions for Linux to README.md

e32553d

Change regular release script to perform release on tag upload.

44dd3b5

Remove scheduling from regular release script (because any update to the files requires a signoff by a code owner, which is infeasible) and add installation instructions to release body.

Add an ADR describing our release process.

b86bf12

NlightNFotis force-pushed the ada-637-release-page-instructions branch from 4401b34 to b86bf12 Compare October 8, 2020 14:16

NlightNFotis changed the title ~~Add Installation Instructions to Readme and Release page~~ Update Release Process script and add Installation Instructions to the Release Page Oct 8, 2020

chrisr-diffblue approved these changes Oct 8, 2020

View reviewed changes

hannes-steffenhagen-diffblue reviewed Oct 8, 2020

View reviewed changes

hannes-steffenhagen-diffblue approved these changes Oct 8, 2020

View reviewed changes

NlightNFotis merged commit f10e6c7 into diffblue:develop Oct 8, 2020

NlightNFotis deleted the ada-637-release-page-instructions branch October 20, 2020 15:12

Update Release Process script and add Installation Instructions to the Release Page #5517

Update Release Process script and add Installation Instructions to the Release Page #5517

Uh oh!

Conversation

NlightNFotis commented Oct 6, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

thomasspriggs left a comment

Choose a reason for hiding this comment

Uh oh!

codecov bot commented Oct 6, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

piotr-grabalski left a comment

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Oct 7, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue commented Oct 7, 2020

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

NlightNFotis commented Oct 7, 2020

Uh oh!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

NlightNFotis commented Oct 6, 2020 •

edited

Loading

codecov bot commented Oct 6, 2020 •

edited

Loading

hannes-steffenhagen-diffblue left a comment •

edited

Loading

hannes-steffenhagen-diffblue Oct 7, 2020 •

edited

Loading