Reorganise CI to use pre-packaged LLVM backend release (#4308)

This PR refactors the way that we build Docker images with K installed to run later CI stages (i.e. the Pyk integration tests). Rather than building the entire K distribution from scratch, we instead download and install a pre-packaged release of the LLVM backend. A subsequent (much smaller) change will do the same for the Haskell backend, now that the supporting infrastructure is in place. I don't expect that CI times will actually decrease meaningfully with this PR; the LLVM backend is pretty quick to build. Doing the same for the haskell backend will be a much bigger impact, and should bring CI times down to ~20 minutes. The existing CI job that produces a "whole of K" distribution is still run, and we still release that package on new K versions.
runtimeverification · Jun 13, 2024 · 5c19b92 · 5c19b92
1 parent 4e8b76c
commit 5c19b92
Show file tree

Hide file tree

Showing 23 changed files with 240 additions and 46 deletions.
diff --git a/.github/actions/with-k-docker/Dockerfile b/.github/actions/with-k-docker/Dockerfile
@@ -1,19 +1,25 @@
-FROM ubuntu:jammy
+ARG BASE_DISTRO
+
+FROM ubuntu:${BASE_DISTRO}
 
 ARG K_DEB_PATH
+ARG LLVM_BACKEND_DEB_PATH
 
 COPY ${K_DEB_PATH} /kframework.deb
+COPY ${LLVM_BACKEND_DEB_PATH} /llvm-backend.deb
 
-RUN    apt-get -y update  \
-    && apt-get -y install \
-         curl             \
-         graphviz         \
-         make             \
-         python3.10-dev   \
-         python3.10-venv  \
-         /kframework.deb  \
+RUN    apt-get -y update    \
+    && apt-get -y install   \
+         curl               \
+         graphviz           \
+         make               \
+         python3.10-dev     \
+         python3.10-venv    \
+         /llvm-backend.deb  \
+         /kframework.deb    \
     && apt-get -y clean
 
+RUN rm /llvm-backend.deb
 RUN rm /kframework.deb
 
 ARG USER_ID=9876

diff --git a/.github/actions/with-k-docker/action.yml b/.github/actions/with-k-docker/action.yml
@@ -10,23 +10,54 @@ inputs:
     required: true
     type: string
     default: kframework.deb
+  distro:
+    description: 'Distribution to setup Docker for.'
+    required: true
+    type: string
+    default: jammy
+  run-container:
+    description: 'Run the K container automatically with default settings.'
+    required: true
+    type: boolean
+    default: true
 runs:
   using: 'composite'
   steps:
   - name: 'Set up Docker'
     shell: bash {0}
+    env:
+      BASE_DISTRO: ${{ inputs.distro }}
+      GH_TOKEN: ${{ github.token }}
     run: |
       set -euxo pipefail
 
+      gh release download                           \
+        --repo runtimeverification/llvm-backend     \
+        --pattern "*ubuntu_${BASE_DISTRO}.deb"  \
+        --output llvm-backend.deb                   \
+        v$(cat deps/llvm-backend_release)
+
       CONTAINER_NAME=${{ inputs.container-name }}
       TAG=runtimeverificationinc/${CONTAINER_NAME}
       DOCKERFILE=${{ github.action_path }}/Dockerfile
       K_DEB_PATH=${{ inputs.k-deb-path }}
+      LLVM_BACKEND_DEB_PATH=llvm-backend.deb
 
       docker build . \
-        --file ${DOCKERFILE}             \
-        --tag ${TAG}                     \
-        --build-arg K_DEB_PATH=${K_DEB_PATH}
+        --file ${DOCKERFILE}                                        \
+        --tag ${TAG}                                                \
+        --build-arg BASE_DISTRO=${BASE_DISTRO}                      \
+        --build-arg K_DEB_PATH=${K_DEB_PATH}                        \
+        --build-arg LLVM_BACKEND_DEB_PATH=${LLVM_BACKEND_DEB_PATH}
+
+  - name: 'Run Docker container'
+    shell: bash {0}
+    if: ${{ inputs.run-container == 'true' }}
+    run: |
+      set -euxo pipefail
+
+      CONTAINER_NAME=${{ inputs.container-name }}
+      TAG=runtimeverificationinc/${CONTAINER_NAME}
 
       docker run                 \
         --name ${CONTAINER_NAME} \

diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -99,7 +99,7 @@ jobs:
           distro: jammy
           llvm: 15
           pkg-name: kframework_amd64_ubuntu_jammy.deb
-          build-package: package/debian/build-package jammy
+          build-package: package/debian/build-package jammy kframework
           test-package: package/debian/test-package
       - name: 'Upload the package built to the Summary Page'
         uses: actions/upload-artifact@v4

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -101,7 +101,7 @@ jobs:
           os: ubuntu
           distro: jammy
           llvm: 15
-          build-package: package/debian/build-package jammy
+          build-package: package/debian/build-package jammy kframework
           test-package: package/debian/test-package
       - name: On Failure, Upload the kore-exec.tar.gz file to the Summary Page
         if: failure()
@@ -120,6 +120,37 @@ jobs:
           retention-days: 1
 
 
+  test-frontend-package-ubuntu-jammy:
+    name: 'K: Ubuntu Jammy Frontend Package'
+    runs-on: [self-hosted, linux, normal]
+    needs: code-quality
+    steps:
+      - uses: actions/checkout@v4
+      - name: 'Build and Test'
+        uses: ./.github/actions/test-package
+        with:
+          os: ubuntu
+          distro: jammy
+          llvm: 15
+          build-package: package/debian/build-package jammy kframework-frontend
+          test-package: package/debian/test-frontend-package
+      - name: On Failure, Upload the kore-exec.tar.gz file to the Summary Page
+        if: failure()
+        uses: actions/upload-artifact@v4
+        with:
+          name: kore-exec.tar.gz
+          path: |
+            **/kore-exec.tar.gz
+      - name: 'On Success, Upload the package built to the Summary Page'
+        if: success()
+        uses: actions/upload-artifact@v4
+        with:
+          name: kframework-frontend.deb
+          path: kframework-frontend.deb
+          if-no-files-found: error
+          retention-days: 1
+
+
   pyk-build-on-nix:
     needs: code-quality
     name: 'Pyk: Nix Build'
@@ -206,20 +237,20 @@ jobs:
 
   pyk-build-docs:
     name: 'Pyk: Documentation'
-    needs: test-package-ubuntu-jammy
+    needs: test-frontend-package-ubuntu-jammy
     runs-on: [self-hosted, linux, normal]
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v4
       - name: 'Download K package from the Summary Page'
         uses: actions/download-artifact@v4
         with:
-          name: kframework.deb
+          name: kframework-frontend.deb
       - name: 'Set up Docker'
         uses: ./.github/actions/with-k-docker
         with:
           container-name: k-pyk-docs-${{ github.sha }}
-          k-deb-path: kframework.deb
+          k-deb-path: kframework-frontend.deb
       - name: 'Build documentation'
         run: docker exec -u user k-pyk-docs-${{ github.sha }} make docs
       - name: 'Tear down Docker'
@@ -228,7 +259,7 @@ jobs:
 
 
   pyk-profile:
-    needs: test-package-ubuntu-jammy
+    needs: test-frontend-package-ubuntu-jammy
     name: 'Pyk: Profiling'
     runs-on: [self-hosted, linux, normal]
     timeout-minutes: 10
@@ -238,12 +269,13 @@ jobs:
       - name: 'Download K package from the Summary Page'
         uses: actions/download-artifact@v4
         with:
-          name: kframework.deb
+          name: kframework-frontend.deb
       - name: 'Set up Docker'
         uses: ./.github/actions/with-k-docker
         with:
           container-name: k-pyk-profile-${{ github.sha }}
-          k-deb-path: kframework.deb
+          k-deb-path: kframework-frontend.deb
+          distro: jammy
       - name: 'Run profiling'
         run: |
           docker exec -u user k-pyk-profile-${{ github.sha }} make profile PROF_ARGS=-n4
@@ -255,7 +287,7 @@ jobs:
 
 
   pyk-integration-tests:
-    needs: test-package-ubuntu-jammy
+    needs: test-frontend-package-ubuntu-jammy
     name: 'Pyk: Integration Tests'
     runs-on: [self-hosted, linux, normal]
     timeout-minutes: 30
@@ -265,12 +297,13 @@ jobs:
       - name: 'Download K package from the Summary Page'
         uses: actions/download-artifact@v4
         with:
-          name: kframework.deb
+          name: kframework-frontend.deb
       - name: 'Set up Docker'
         uses: ./.github/actions/with-k-docker
         with:
           container-name: k-pyk-integration-${{ github.sha }}
-          k-deb-path: kframework.deb
+          k-deb-path: kframework-frontend.deb
+          distro: jammy
       - name: 'Run integration tests'
         run: |
           docker exec -u user k-pyk-integration-${{ github.sha }} make test-integration TEST_ARGS='-n4 --maxfail=0 --timeout=300'
@@ -281,7 +314,7 @@ jobs:
 
 
   pyk-regression-tests:
-    needs: test-package-ubuntu-jammy
+    needs: test-frontend-package-ubuntu-jammy
     name: 'Pyk: Regression Tests'
     runs-on: ubuntu-latest
     timeout-minutes: 30
@@ -291,12 +324,13 @@ jobs:
       - name: 'Download K package from the Summary Page'
         uses: actions/download-artifact@v4
         with:
-          name: kframework.deb
+          name: kframework-frontend.deb
       - name: 'Set up Docker'
         uses: ./.github/actions/with-k-docker
         with:
           container-name: k-pyk-regression-${{ github.sha }}
-          k-deb-path: kframework.deb
+          k-deb-path: kframework-frontend.deb
+          distro: jammy
       - name: 'Run K regression tests'
         run: |
           docker exec -u user k-pyk-regression-${{ github.sha }} make test-regression-new -j4
@@ -309,17 +343,22 @@ jobs:
   performance-tests:
     name: 'K: Profiling'
     runs-on: [self-hosted, linux, performance]
-    needs: test-package-ubuntu-jammy
+    needs: test-frontend-package-ubuntu-jammy
     steps:
       - uses: actions/checkout@v4
       - name: 'Download K package from the Summary Page'
         uses: actions/download-artifact@v4
         with:
-          name: kframework.deb
+          name: kframework-frontend.deb
+      - name: 'Set up Docker'
+        uses: ./.github/actions/with-k-docker
+        with:
+          container-name: k-profiling-tests-${{ github.sha }}
+          k-deb-path: kframework-frontend.deb
+          distro: jammy
+          run-container: false
       - name: 'Set up Docker Test Image'
         env:
-          BASE_OS: ubuntu
-          BASE_DISTRO: jammy
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
           BENCHER_API_TOKEN: ${{ secrets.BENCHER_API_TOKEN }}
           BENCHER_PROJECT: k-framework
@@ -328,7 +367,7 @@ jobs:
           set -euxo pipefail
           workspace=$(pwd)
           docker run --name k-profiling-tests-${GITHUB_SHA}                    \
-            --rm -it --detach                                                  \
+            --rm -it --detach --user root                                      \
             -e BENCHER_API_TOKEN=$BENCHER_API_TOKEN                            \
             -e BENCHER_PROJECT=$BENCHER_PROJECT                                \
             -e BENCHER_ADAPTER=$BENCHER_ADAPTER                                \
@@ -343,7 +382,7 @@ jobs:
             --workdir /opt/workspace                                           \
             -v "${workspace}:/opt/workspace"                                   \
             -v "${GITHUB_EVENT_PATH}:${GITHUB_EVENT_PATH}"                     \
-            ${BASE_OS}:${BASE_DISTRO}
+            runtimeverificationinc/k-profiling-tests-${GITHUB_SHA}
       - name: 'Install K from Package'
         run: |
           set -euxo pipefail

diff --git a/k-distribution/tests/profiling/setup_profiling.sh b/k-distribution/tests/profiling/setup_profiling.sh
@@ -7,10 +7,6 @@ export BENCHER_VERSION="0.3.23"
 apt-get update
 apt-get upgrade --yes
 apt-get install --yes python3 python3-pip git curl make time sudo wget
-# Build K if no flag was given and don't execute if flag was given
-if [ $# -eq 0 ]; then
-    apt-get install --yes ./kframework.deb
-fi
 python3 -m pip install python-slugify
 
 wget https://github.com/bencherdev/bencher/releases/download/v"${BENCHER_VERSION}"/bencher_"${BENCHER_VERSION}"_amd64.deb

diff --git a/package/debian/build-package b/package/debian/build-package
@@ -3,19 +3,20 @@
 set -euxo pipefail
 
 base_distro="$1" ; shift
+subdir="$1" ; shift
 pkg_name="$1" ; shift
 
 mkdir debian
 
-mv package/debian/changelog debian/changelog
-mv package/debian/copyright debian/copyright
-mv package/debian/kframework-docs.docs debian/kframework-docs.docs
-mv package/debian/source debian/source
+mv package/debian/${subdir}/changelog               debian/changelog
+mv package/debian/${subdir}/copyright               debian/copyright
+mv package/debian/${subdir}/${subdir}-docs.docs     debian/${subdir}-docs.docs
+mv package/debian/${subdir}/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
+mv package/debian/${subdir}/compat.${base_distro}   debian/compat
+mv package/debian/${subdir}/control.${base_distro}  debian/control
+mv package/debian/${subdir}/rules.${base_distro}    debian/rules
 
 dpkg-buildpackage
 
-mv ../kframework_$(cat package/version)_amd64.deb ${pkg_name}
+mv ../${subdir}_$(cat package/version)_amd64.deb ${pkg_name}
diff --git a/package/debian/kframework-frontend/changelog b/package/debian/kframework-frontend/changelog
@@ -0,0 +1,5 @@
+kframework-frontend (7.1.0) unstable; urgency=medium
+
+  * Initial Release.
+
+ -- Bruce Collie <[email protected]>  Thu, 2 May 2024 10:52:06 +0100
diff --git a/package/debian/compat.jammy → ...e/debian/kframework-frontend/compat.jammy b/package/debian/compat.jammy → ...e/debian/kframework-frontend/compat.jammy
diff --git a/package/debian/kframework-frontend/control.jammy b/package/debian/kframework-frontend/control.jammy
@@ -0,0 +1,18 @@
+Source: kframework-frontend
+Section: devel
+Priority: optional
+Maintainer: Bruce Collie <[email protected]>
+Build-Depends: debhelper (>=10) , flex , maven , openjdk-17-jdk , pkg-config , python3 , python3-dev , python3-distutils , python3-pip , zlib1g-dev
+Standards-Version: 3.9.6
+Homepage: https://github.com/runtimeverification/k
+
+Package: kframework-frontend
+Architecture: any
+Section: devel
+Priority: optional
+Depends: bison , openjdk-17-jre-headless , flex , gcc , g++ , libsecp256k1-0 , libtinfo-dev , libz3-4 , pkg-config
+Recommends: z3
+Suggests: k-llvm-backend
+Description: K framework frontend
+ Includes K Framework compiler frontend for K language definitions.
+Homepage: https://github.com/runtimeverification/k
diff --git a/package/debian/kframework-frontend/copyright b/package/debian/kframework-frontend/copyright
@@ -0,0 +1,33 @@
+Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
+Upstream-Name: kframework-frontend
+Upstream-Contact: Bruce Collie <[email protected]>
+Source: https://github.com/runtimeverification/k
+
+Files: *
+Copyright: 2010-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 University 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 HOLDERS 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/kframework-docs.docs → ...rk-frontend/kframework-frontend-docs.docs b/package/debian/kframework-docs.docs → ...rk-frontend/kframework-frontend-docs.docs