Build debian package (#1036)

This PR sets up a Debian package build for the LLVM backend, such that we will be able to adapt the K CI testing process to download this released version rather than rebuilding the backend from scratch on every run. The package building step is tested in CI, and I have tested the part of the workflow that deals with _uploading_ the released package locally by creating and deleting releases on pushes to this branch. I'll make sure to babysit the release to ensure that the file is attached correctly when this PR is merged. The Debian packaging specifics in this PR have been largely adapted from the main K repo. --------- Co-authored-by: devops <[email protected]>
runtimeverification · Apr 30, 2024 · d7fb8af · d7fb8af
1 parent 6a6c288
commit d7fb8af
Show file tree

Hide file tree

Showing 15 changed files with 341 additions and 4 deletions.
diff --git a/.github/actions/test-package/action.yml b/.github/actions/test-package/action.yml
@@ -0,0 +1,109 @@
+name: 'Build Ubuntu Package'
+description: 'Build the package for a given distribution and test it.'
+
+inputs:
+  os: 
+    description: 'Release OS to build and test package for.'
+    required: true
+  distro:
+    description: 'Distribution to build and test package for.'
+    required: true
+  llvm:
+    description: 'LLVM version to use.'
+    required: true
+  dockerfile:
+    description: 'Hardcode the path of the dockerfile to use.'
+    required: false
+    default: .github/workflows/Dockerfile
+  build-package:
+    description: 'Script which builds the given package.'
+    required: true
+  test-package:
+    description: 'Script which tests the given package.'
+    required: true
+  pkg-name:
+    description: 'Where to move the package.'
+    required: false
+    default: package.pkg
+
+runs:
+  using: 'composite'
+
+  steps:
+
+  - name: 'Check out code'
+    uses: actions/checkout@v4
+    with:
+      path: k-${{ inputs.distro }}
+      submodules: recursive
+
+  - name: 'Set up Docker'
+    uses: ./.github/actions/with-docker
+    with:
+      tag: kllvm-package-build-${{ inputs.os }}-${{ inputs.distro }}-${{ github.sha }}
+      subdir: k-${{ inputs.distro }}/
+      os: ${{ inputs.os }}
+      distro: ${{ inputs.distro }}
+      llvm: ${{ inputs.llvm }}
+      dockerfile: ${{ inputs.dockerfile }}
+
+  - name: 'Build Package: ${{ inputs.distro }}'
+    shell: bash {0}
+    env:
+      BASE_DISTRO: ${{ inputs.distro }}
+      BASE_OS: ${{ inputs.os }}
+      BUILD_PACKAGE: ${{ inputs.build-package }}
+      PKG_NAME: ${{ inputs.pkg-name }}
+    run: |
+      set -euxo pipefail
+      docker exec -t kllvm-package-build-${BASE_OS}-${BASE_DISTRO}-${GITHUB_SHA} /bin/bash -c "${BUILD_PACKAGE} ${PKG_NAME}"
+
+  - name: 'Tear down Docker'
+    shell: bash {0}
+    env:
+      BASE_DISTRO: ${{ inputs.distro }}
+      BASE_OS: ${{ inputs.os }}
+    if: always()
+    run: |
+      docker stop --time=0 kllvm-package-build-${BASE_OS}-${BASE_DISTRO}-${GITHUB_SHA}
+      docker container rm --force kllvm-package-build-${BASE_OS}-${BASE_DISTRO}-${GITHUB_SHA} || true
+
+  - name: 'Set up Docker Test Image: ${{ inputs.os }}:${{ inputs.distro }}'
+    shell: bash {0}
+    env:
+      BASE_OS: ${{ inputs.os }}
+      BASE_DISTRO: ${{ inputs.distro }}
+    run: |
+      set -euxo pipefail
+      workspace=$(pwd)
+      cd k-${BASE_DISTRO}
+      docker run                                                      \
+        --name kllvm-package-test-${BASE_OS}-${BASE_DISTRO}-${GITHUB_SHA} \
+        --rm -it                                                      \
+        --detach                                                      \
+        --workdir /opt/workspace                                      \
+        -v "${workspace}:/opt/workspace"                              \
+        ${BASE_OS}:${BASE_DISTRO}
+
+  - name: 'Test Package: ${{ inputs.os }}:${{ inputs.distro }}'
+    shell: bash {0}
+    env:
+      BASE_OS: ${{ inputs.os }}
+      BASE_DISTRO: ${{ inputs.distro }}
+      TEST_PACKAGE: ${{ inputs.test-package }}
+      PKG_NAME: ${{ inputs.pkg-name }}
+      SUBDIR: k-${{ inputs.distro }}/
+    run: |
+      set -euxo pipefail
+      mv ${SUBDIR}${PKG_NAME} ${PKG_NAME}
+      docker exec -t kllvm-package-test-${BASE_OS}-${BASE_DISTRO}-${GITHUB_SHA} /bin/bash -c "${TEST_PACKAGE} ${PKG_NAME}"
+
+  - name: 'Tear down Docker Test'
+    shell: bash {0}
+    env:
+      BASE_OS: ${{ inputs.os }}
+      BASE_DISTRO: ${{ inputs.distro }}
+    if: always()
+    run: |
+      docker stop --time=0 k-package-test-${BASE_OS}-${BASE_DISTRO}-${GITHUB_SHA}
+      docker container rm --force k-package-test-${BASE_OS}-${BASE_DISTRO}-${GITHUB_SHA} || true
diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile
@@ -16,11 +16,13 @@ RUN     apt-get update                    \
           cmake                           \
           clang-${LLVM_VERSION}           \
           clang-tidy-${LLVM_VERSION}      \
+          debhelper                       \
           llvm-${LLVM_VERSION}-tools      \
           lld-${LLVM_VERSION}             \
           zlib1g-dev                      \
           flex                            \
           locales                         \
+          libboost-dev                    \
           libboost-test-dev               \
           libfmt-dev                      \
           libgmp-dev                      \

diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -5,21 +5,88 @@ on:
       - master
 
 jobs:
+  draft-release:
+    name: 'Draft Release'
+    runs-on: ubuntu-latest
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v4
+      - name: 'Make release'
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        run: |
+          set -x
+          VERSION=v$(cat package/version)
+          gh release create ${VERSION}              \
+            --repo runtimeverification/llvm-backend \
+            --draft                                 \
+            --title ${VERSION}                      \
+            --target ${{ github.sha }}
+
+
+  build-jammy-package:
+    name: 'Build Ubuntu Jammy Package'
+    runs-on: [self-hosted, linux, normal]
+    needs: draft-release
+
+    steps:
+      - uses: actions/checkout@v4
+      - name: 'Check out code'
+        uses: actions/checkout@v4
+        with:
+          path: k-llvm-jammy
+          submodules: recursive
+
+      - name: 'Build package in Docker'
+        uses: ./.github/actions/test-package
+        with:
+          os: ubuntu
+          distro: jammy
+          llvm: 15
+          build-package: package/debian/build-package jammy
+          test-package: package/debian/test-package
+          pkg-name: k-llvm-backend_amd64_ubuntu_jammy.deb
+
+      - name: 'Upload to release'
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        run: |
+          set -x
+          VERSION=v$(cat package/version)
+          cp k-llvm-backend_amd64_ubuntu_jammy.deb k-llvm-backend_${VERSION}_amd64_ubuntu_jammy.deb
+          gh release upload ${VERSION}                        \
+            --repo runtimeverification/llvm-backend           \
+            --clobber                                         \
+            k-llvm-backend_${VERSION}_amd64_ubuntu_jammy.deb
+
+      - name: 'On failure, delete drafted release'
+        if: failure()
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        run: |
+          set -x
+          VERSION=v$(cat package/version)
+          gh release delete ${VERSION}              \
+            --repo runtimeverification/llvm-backend \
+            --yes                                   \
+            --cleanup-tag
+            
 
   release:
     name: 'Publish Release'
     runs-on: ubuntu-latest
     environment: production
+    needs: build-jammy-package
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v4
-      - name: 'Make release'
+      - name: 'Finalise release'
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         run: |
           set -x
           VERSION=v$(cat package/version)
-          gh release create ${VERSION} --target ${{ github.sha }}
+          gh release edit ${VERSION} --draft=false
       - name: 'Update dependents'
         env:
           GITHUB_TOKEN: ${{ secrets.JENKINS_GITHUB_PAT }}

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
@@ -6,7 +6,6 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
-
   version-bump:
     name: 'Version Bump'
     runs-on: ubuntu-latest
@@ -108,3 +107,24 @@ jobs:
         run: |
           docker stop --time=0 llvm-backend-ci-${GITHUB_SHA}
           docker container rm --force llvm-backend-ci-${GITHUB_SHA} || true
+
+  build-jammy-package:
+    name: 'Build Ubuntu Jammy package'
+    runs-on: [self-hosted, linux, normal]
+
+    steps:
+      - uses: actions/checkout@v4
+      - name: 'Check out code'
+        uses: actions/checkout@v4
+        with:
+          path: k-llvm-jammy
+          submodules: recursive
+
+      - name: 'Build package in Docker'
+        uses: ./.github/actions/test-package
+        with:
+          os: ubuntu
+          distro: jammy
+          llvm: 15
+          build-package: package/debian/build-package jammy
+          test-package: package/debian/test-package
diff --git a/package/debian/build-package b/package/debian/build-package
@@ -0,0 +1,21 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+base_distro="$1" ; shift
+pkg_name="$1" ; shift
+
+mkdir debian
+
+mv package/debian/changelog debian/changelog
+mv package/debian/copyright debian/copyright
+mv package/debian/k-llvm-backend-docs.docs debian/k-llvm-backend-docs.docs
+mv package/debian/source debian/source
+
+mv package/debian/compat.${base_distro} debian/compat
+mv package/debian/control.${base_distro} debian/control
+mv package/debian/rules.${base_distro} debian/rules
+
+dpkg-buildpackage
+
+mv ../k-llvm-backend_$(cat package/version)_amd64.deb ${pkg_name}
diff --git a/package/debian/changelog b/package/debian/changelog
@@ -0,0 +1,5 @@
+k-llvm-backend (0.1.3) unstable; urgency=medium
+
+  * Initial release
+
+ -- Bruce Collie <[email protected]>  Fri, 26 Apr 2024 15:43:00 +0100
diff --git a/package/debian/compat.jammy b/package/debian/compat.jammy
@@ -0,0 +1 @@
+10
diff --git a/package/debian/control.jammy b/package/debian/control.jammy
@@ -0,0 +1,16 @@
+Source: k-llvm-backend
+Section: devel
+Priority: optional
+Maintainer: Bruce Collie <[email protected]>
+Build-Depends: clang-15 , cmake , debhelper (>=10) , flex , libboost-dev , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libyaml-dev , llvm-15-tools , pkg-config , python3 , python3-dev , xxd
+Standards-Version: 3.9.6
+Homepage: https://github.com/runtimeverification/llvm-backend
+
+Package: k-llvm-backend
+Architecture: any
+Section: devel
+Priority: optional
+Depends: clang-15 , flex , libboost-dev , libffi-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libyaml-0-2 , lld-15 , llvm-15 , pkg-config
+Description: K Framework LLVM backend
+ Fast concrete execution backend for programming language semantics implemented using the K Framework.
+Homepage: https://github.com/runtimeverification/llvm-backend
diff --git a/package/debian/copyright b/package/debian/copyright
@@ -0,0 +1,34 @@
+Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
+Upstream-Name: k-llvm-backend
+Upstream-Contact: Bruce Collie <[email protected]>
+Source: https://github.com/runtimeverification/llvm-backend
+
+Files: *
+Copyright: 2018-2024 K Team <[email protected]>
+License: BSD-3-Clause
+
+License: BSD-3-Clause
+ Redistribution and use in source and binary forms, with or without
+ modification, are permitted provided that the following conditions are met:
+
+ 1. Redistributions of source code must retain the above copyright notice, this
+    list of conditions and the following disclaimer.
+
+ 2. Redistributions in binary form must reproduce the above copyright notice,
+    this list of conditions and the following disclaimer in the documentation
+    and/or other materials provided with the distribution.
+
+ 3. Neither the name of the copyright holder nor the names of its
+    contributors may be used to endorse or promote products derived from
+    this software without specific prior written permission.
+
+ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+ DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+ FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+ SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+ CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+ OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/package/debian/k-llvm-backend-docs.docs b/package/debian/k-llvm-backend-docs.docs
diff --git a/package/debian/rules.jammy b/package/debian/rules.jammy
@@ -0,0 +1,48 @@
+#!/usr/bin/make -f
+# See debhelper(7) (uncomment to enable)
+# output every command that modifies files on the build system.
+#export DH_VERBOSE = 1
+
+
+# see FEATURE AREAS in dpkg-buildflags(1)
+
+# The LLVM backend is built using Clang, which is incompatible with LTO flags
+# added by default in newer versions of dpkg.
+# https://wiki.debian.org/ToolChain/LTO
+export DEB_BUILD_MAINT_OPTIONS=hardening=-stackprotector optimize=-lto
+
+# see ENVIRONMENT in dpkg-buildflags(1)
+# package maintainers to append CFLAGS
+#export DEB_CFLAGS_MAINT_APPEND  = -Wall -pedantic
+# package maintainers to append LDFLAGS
+#export DEB_LDFLAGS_MAINT_APPEND = -Wl,--as-needed
+
+DESTDIR=$(shell pwd)/debian/k-llvm-backend
+PREFIX=/usr
+PYTHON_VERSION=python3.10
+PYTHON_DEB_VERSION=python3
+export DESTDIR
+export PREFIX
+
+%:
+	dh $@
+
+override_dh_auto_build:
+	mkdir build
+	cmake  \
+		-S . \
+		-B build \
+		-DCMAKE_BUILD_TYPE=Release \
+		-DCMAKE_INSTALL_PREFIX=$(PREFIX)
+	cmake --build build
+
+override_dh_auto_install:
+	cmake --install build
+
+override_dh_strip:
+	dh_strip -Xliballoc.a -Xlibarithmetic.a -XlibAST.a -Xlibutil.a -XlibParser.a -Xlibcollect.a -Xlibcollections.a -Xlibjson.a -Xlibstrings.a -Xlibmeta.a -Xlibio.a
+
+# dh_make generated override targets
+# This is example for Cmake (See https://bugs.debian.org/641051 )
+#override_dh_auto_configure:
+#	dh_auto_configure -- #	-DCMAKE_LIBRARY_PATH=$(DEB_HOST_MULTIARCH)
diff --git a/package/debian/source/format b/package/debian/source/format
@@ -0,0 +1 @@
+3.0 (native)
diff --git a/package/debian/test-package b/package/debian/test-package
@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+pkg="$1" ; shift
+
+cp "${pkg}" k-llvm-backend.deb
+
+export DEBIAN_FRONTEND=noninteractive
+apt-get update
+apt-get upgrade --yes
+apt-get install --yes ./k-llvm-backend.deb
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.2
+0.1.3