Cd/create debian package on release #5464

hannes-steffenhagen-diffblue · 2020-08-17T14:08:33Z

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.

hannes-steffenhagen-diffblue · 2020-08-17T15:23:38Z

The windows build here is broken not because of any of these changes, but because sourceforge links we were downloading packages from went stale.

NlightNFotis · 2020-08-17T15:45:10Z

This is a sick PR by the way - this has the potential to make all our packaging super easy if I understood correctly?

So it's possible now to build a package in all platforms just by doing a build package (or ninja package)?

Nicely done in any case 💯

martin-cs

This would be a good piece of functionality. I assume you have spoken to @tautschnig about this as he is the current maintainer for the Debian package : https://tracker.debian.org/pkg/cbmc

hannes-steffenhagen-diffblue · 2020-08-17T15:54:44Z

@NlightNFotis Not all our packaging, unfortunately. But we can produce debian binary packages, WiX installers, simple binary zips etc from this.

For an Ubuntu PPA we would need to produce debian source packages apparently and I am not completely sure what's involved with that yet.

@martin-cs I wasn't actually aware of that.

martin-cs · 2020-08-17T15:57:04Z

@hannes-steffenhagen-diffblue he has the power to get a package into Debian (and thus, I think, downstream, to Ubuntu) plus has all of the control.tar.gz meta-information you need to get through the Debian linter.

hannes-steffenhagen-diffblue · 2020-08-17T16:03:16Z

@martin-cs Our short term goal right now is actually to have an ‘unstable’ Ubuntu PPA so that people can keep their cbmc up-to-date through that. If I understand the process correctly – and I am not completely sure I do – this wouldn’t really work with the “normal” mainstream Debian or Ubuntu release process. Checking out your link it seems that @tautschnig has some scripts to keep debian-unstable up to date, but if I understood correctly using that would mean also pulling in a lot of other debian-unstable dependencies. We’re trying to get it working with stable Ubuntu dependencies, but rolling releases for cbmc (if that makes sense).

I think we should talk to Michael regardless because of course long term making sure cbmc stays up to date in Ubuntu/Debian mainline is also important.

martin-cs · 2020-08-17T16:15:26Z

@hannes-steffenhagen-diffblue having your own package repo and getting people to pull from there seems like a positive step and a good first target. Longer-term I believe it might be possible (with the assistance of @tautschnig or at least @tautschnig 's scripts) to have the unstable package up-to-date and (as long as it doesn't have any dependencies beyond the current stable) set the repository priority so that you get just that one and not accidentally upgrade everything to unstable.

codecov · 2020-08-17T16:49:52Z

Codecov Report

Merging #5464 into develop will not change coverage.
The diff coverage is n/a.

@@           Coverage Diff            @@
##           develop    #5464   +/-   ##
========================================
  Coverage    68.25%   68.25%           
========================================
  Files         1180     1180           
  Lines        97722    97722           
========================================
  Hits         66698    66698           
  Misses       31024    31024

Flag	Coverage Δ
#cproversmt2	`42.81% <ø> (ø)`
#regression	`65.42% <ø> (ø)`
#unit	`32.23% <ø> (ø)`

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 e58dad8...4e5ba60. Read the comment docs.

hannes-steffenhagen-diffblue · 2020-08-20T09:28:43Z

cmake/packaging.cmake

@@ -0,0 +1,34 @@
+set(CPACK_PACKAGE_NAME "cbmc") # XXX should this be cprover instead?
+set(CPACK_PACKAGE_VENDOR "Diffblue Ltd.")
+set(CPACK_PACKAGE_CONTACT "[email protected]") # XXX should this be a Diffblue email address instead?


Clarification on this point would be great, this is the address used in in src/cbmc/dist-linux, the current Ubuntu package lists “Ubuntu Developers” as the maintainer and @tautschnig as the ‘Original Maintainer’, so I’m genuinely unsure what to put here.

Can you put multiple contacts in? Might also be worth asking @peterschrammel for an opinion too.

If possible I'd put [email protected] to have a stable address.

chrisr-diffblue

Generally looks good - as you say, you need to clarify some details but I'm not sure I have answers for you there.

chrisr-diffblue · 2020-08-20T16:31:05Z

.github/workflows/pull-request-checks.yaml

+        run: |
+          cd build
+          ninja package
+          ls *.deb


What does the ls *.deb achieve, other than a nice output? Will it fail the build in someway? Or will it mask any failures from the ninja package because the exit code of the ls will be success?

My experience of debugging the run sections of github actions suggests that it will stop on the first line where an error code is returned. Similar to writing a bash script where set -e has been specified. Therefore this extra line should not mask any other failures.

@chrisr-diffblue ls returns a non-zero exit code if called on non-existent files... so this is just checking whether or not there is a file ending with .deb in the directory after ninja package. See here for a demonstration of how this works.

Failures propagate in github action scripts because I believe set -e is set by default.

chrisr-diffblue · 2020-08-20T16:32:45Z

cmake/packaging.cmake

@@ -0,0 +1,34 @@
+set(CPACK_PACKAGE_NAME "cbmc") # XXX should this be cprover instead?
+set(CPACK_PACKAGE_VENDOR "Diffblue Ltd.")
+set(CPACK_PACKAGE_CONTACT "[email protected]") # XXX should this be a Diffblue email address instead?


Can you put multiple contacts in? Might also be worth asking @peterschrammel for an opinion too.

thomasspriggs

LGTM.

It may be worth us investigating whether we can use cpack to make the .msi for the windows packaging as well. @markrtuttle added a handwritten xml file with the configuration to create it with WiX. But there is a WiX plugin for cpack which could potentially generate it for us and reduce the amount of packaging setup which would otherwise be duplicated.

thomasspriggs · 2020-08-20T18:14:28Z

.github/workflows/release-packages.yaml

+      - name: Build using Ninja
+        run: |
+          cd build
+          ninja


💡 This could be done as a single line -
run: ninja -C build

peterschrammel · 2020-08-20T18:53:39Z

cmake/packaging.cmake

@@ -0,0 +1,34 @@
+set(CPACK_PACKAGE_NAME "cbmc") # XXX should this be cprover instead?


I think cbmc is more well-known.

peterschrammel · 2020-08-20T18:57:55Z

cmake/packaging.cmake

@@ -0,0 +1,34 @@
+set(CPACK_PACKAGE_NAME "cbmc") # XXX should this be cprover instead?
+set(CPACK_PACKAGE_VENDOR "Diffblue Ltd.")
+set(CPACK_PACKAGE_CONTACT "[email protected]") # XXX should this be a Diffblue email address instead?


If possible I'd put [email protected] to have a stable address.

hannes-steffenhagen-diffblue · 2020-08-21T09:40:29Z

@thomasspriggs Yes, my plan was to try the WiX generation of CPack to reduce our maintenance burden on these things.

This only uploads it to the release page, updates via PPA are yet TBD

hannes-steffenhagen-diffblue force-pushed the CD/create-debian-package-on-release branch from afa4801 to e9ae5a3 Compare August 17, 2020 14:10

martin-cs approved these changes Aug 17, 2020

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the CD/create-debian-package-on-release branch from cae0fe9 to 3469760 Compare August 20, 2020 09:23

hannes-steffenhagen-diffblue marked this pull request as ready for review August 20, 2020 09:23

hannes-steffenhagen-diffblue requested review from chrisr-diffblue, kroening, peterschrammel, smowton and tautschnig as code owners August 20, 2020 09:23

hannes-steffenhagen-diffblue commented Aug 20, 2020

View reviewed changes

chrisr-diffblue approved these changes Aug 20, 2020

View reviewed changes

thomasspriggs approved these changes Aug 20, 2020

View reviewed changes

peterschrammel approved these changes Aug 20, 2020

View reviewed changes

hannes-steffenhagen-diffblue added 3 commits August 21, 2020 13:49

Add debian packaging for CMake

e900aa9

Add check to see if .deb package generation works

099dd48

Automatically build and upload debian package on release

4e5ba60

This only uploads it to the release page, updates via PPA are yet TBD

hannes-steffenhagen-diffblue force-pushed the CD/create-debian-package-on-release branch from 3469760 to 4e5ba60 Compare August 21, 2020 12:49

hannes-steffenhagen-diffblue merged commit b76314b into diffblue:develop Aug 21, 2020

		@@ -0,0 +1,34 @@
		set(CPACK_PACKAGE_NAME "cbmc") # XXX should this be cprover instead?

Cd/create debian package on release #5464

Cd/create debian package on release #5464

Uh oh!

Conversation

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

Uh oh!

Uh oh!

hannes-steffenhagen-diffblue commented Aug 17, 2020

Uh oh!

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

Uh oh!

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue commented Aug 17, 2020

Uh oh!

martin-cs commented Aug 17, 2020

Uh oh!

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

Uh oh!

Uh oh!

martin-cs commented Aug 17, 2020

Uh oh!

codecov bot commented Aug 17, 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!

Choose a reason for hiding this comment

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!

thomasspriggs Aug 20, 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!

hannes-steffenhagen-diffblue Aug 21, 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!

thomasspriggs 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!

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue commented Aug 21, 2020

Uh oh!

Uh oh!

hannes-steffenhagen-diffblue commented Aug 17, 2020 •

edited

Loading

NlightNFotis commented Aug 17, 2020 •

edited

Loading

hannes-steffenhagen-diffblue commented Aug 17, 2020 •

edited

Loading

codecov bot commented Aug 17, 2020 •

edited

Loading

thomasspriggs Aug 20, 2020 •

edited

Loading

hannes-steffenhagen-diffblue Aug 21, 2020 •

edited

Loading