Merge remote-tracking branch 'origin/develop'

runtimeverification · Sep 3, 2024 · 8a67157 · 8a67157
2 parents 240d9ff + b4f86f2
commit 8a67157
Show file tree

Hide file tree

Showing 11 changed files with 162 additions and 8 deletions.
diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile
@@ -63,7 +63,6 @@ RUN    apt-get update              \
         pkg-config                 \
         python3                    \
         python3-dev                \
-        python3-distutils          \
         python3-pip                \
         xxd                        \
         zlib1g-dev

diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -87,6 +87,67 @@ jobs:
             kup publish k-framework-binary .#k --keep-days 180
             kup publish k-framework-binary .#k.openssl.procps.secp256k1 --keep-days 180
 
+  ubuntu-noble:
+    name: 'K Ubuntu Noble Package'
+    runs-on: [self-hosted, linux, normal]
+    timeout-minutes: 90
+    steps:
+      - uses: actions/checkout@v4
+      - name: 'Build and Test Package'
+        uses: ./.github/actions/test-package
+        with:
+          os: ubuntu
+          distro: noble
+          llvm: 16
+          jdk: 21
+          pkg-name: kframework_amd64_ubuntu_noble.deb
+          build-package: package/debian/build-package noble kframework
+          test-package: package/debian/test-package
+      - name: 'Upload the package built to the Summary Page'
+        uses: actions/upload-artifact@v4
+        with:
+          name: kframework_amd64_ubuntu_noble.deb
+          path: kframework_amd64_ubuntu_noble.deb
+          if-no-files-found: error
+          retention-days: 1
+      - name: 'Upload Package to Release'
+        env:
+          GITHUB_TOKEN: ${{ secrets.JENKINS_GITHUB_PAT }}
+        run: |
+          set -x
+          version=$(cat package/version)
+          cp kframework_amd64_ubuntu_noble.deb "kframework_${version}_amd64_ubuntu_noble.deb"
+          gh release upload --repo runtimeverification/k --clobber "v${version}" "kframework_${version}_amd64_ubuntu_noble.deb"
+      - name: 'Build, Test, and Push Dockerhub Image'
+        shell: bash {0}
+        env:
+          DOCKERHUB_PASSWORD: ${{ secrets.DOCKERHUB_PASSWORD }}
+          DOCKERHUB_REPO: runtimeverificationinc/kframework-k
+        run: |
+          set -euxo pipefail
+          version=$(cat package/version)
+          version_tag=ubuntu-noble-${version}
+          docker login --username rvdockerhub --password "${DOCKERHUB_PASSWORD}"
+          docker image build . --file package/docker/Dockerfile.ubuntu-noble --tag "${DOCKERHUB_REPO}:${version_tag}"
+          docker run --name "k-package-docker-test-noble-${GITHUB_SHA}" --rm -it --detach "${DOCKERHUB_REPO}:${version_tag}"
+          docker exec -t "k-package-docker-test-noble-${GITHUB_SHA}" bash -c 'cd ~ && echo "module TEST imports BOOL endmodule" > test.k'
+          docker exec -t "k-package-docker-test-noble-${GITHUB_SHA}" bash -c 'cd ~ && kompile test.k --backend llvm'
+          docker exec -t "k-package-docker-test-noble-${GITHUB_SHA}" bash -c 'cd ~ && kompile test.k --backend haskell'
+          docker exec -t "k-package-docker-test-noble-${GITHUB_SHA}" bash -c 'cd ~ && pyk kompile test.k --backend llvm'
+          docker exec -t "k-package-docker-test-noble-${GITHUB_SHA}" bash -c 'cd ~ && pyk kompile test.k --backend haskell'
+          docker image push "${DOCKERHUB_REPO}:${version_tag}"
+      - name: 'Clean up Docker Container'
+        if: always()
+        run: |
+          docker stop --time=0 "k-package-docker-test-noble-${GITHUB_SHA}"
+      - 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
+
   ubuntu-jammy:
     name: 'K Ubuntu Jammy Package'
     runs-on: [self-hosted, linux, normal]
@@ -359,7 +420,7 @@ jobs:
     name: 'Publish Release'
     runs-on: [self-hosted, linux, normal]
     environment: production
-    needs: [cachix-release, macos-test, source-tarball, ubuntu-jammy, set-release-id]
+    needs: [cachix-release, macos-test, source-tarball, ubuntu-jammy, ubuntu-noble, set-release-id]
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v4

diff --git a/package/debian/kframework-frontend/control.jammy b/package/debian/kframework-frontend/control.jammy
@@ -2,7 +2,7 @@ Source: kframework-frontend
 Section: devel
 Priority: optional
 Maintainer: Tamas Toth <[email protected]>
-Build-Depends: debhelper (>=10) , flex , maven , openjdk-17-jdk , pkg-config , python3 , python3-dev , python3-distutils , python3-pip , zlib1g-dev
+Build-Depends: debhelper (>=10) , flex , maven , openjdk-17-jdk , pkg-config , python3 , python3-dev , python3-pip , zlib1g-dev
 Standards-Version: 3.9.6
 Homepage: https://github.com/runtimeverification/k
 

diff --git a/package/debian/kframework/compat.noble b/package/debian/kframework/compat.noble
@@ -0,0 +1 @@
+10
diff --git a/package/debian/kframework/control.jammy b/package/debian/kframework/control.jammy
@@ -2,7 +2,7 @@ Source: kframework
 Section: devel
 Priority: optional
 Maintainer: Dwight Guth <[email protected]>
-Build-Depends: clang-15 , cmake , debhelper (>=10) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-dev , libunwind-dev , libyaml-dev , maven , openjdk-17-jdk , pkg-config , python3 , python3-dev , python3-distutils , python3-pip , xxd , zlib1g-dev
+Build-Depends: clang-15 , cmake , debhelper (>=10) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-dev , libunwind-dev , libyaml-dev , maven , openjdk-17-jdk , pkg-config , python3 , python3-dev , python3-pip , xxd , zlib1g-dev
 Standards-Version: 3.9.6
 Homepage: https://github.com/runtimeverification/k
 

diff --git a/package/debian/kframework/control.noble b/package/debian/kframework/control.noble
@@ -0,0 +1,18 @@
+Source: kframework
+Section: devel
+Priority: optional
+Maintainer: Dwight Guth <[email protected]>
+Build-Depends: clang-16 , cmake , debhelper (>=10) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-dev , libunwind-dev , libyaml-dev , maven , openjdk-21-jdk , pkg-config , python3 , python3-dev , python3-pip , xxd , zlib1g-dev
+Standards-Version: 3.9.6
+Homepage: https://github.com/runtimeverification/k
+
+Package: kframework
+Architecture: any
+Section: devel
+Priority: optional
+Depends: bison , clang-16 , openjdk-21-jre-headless , flex , gcc , g++ , libboost-dev , libffi-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-1 , libtinfo-dev , libunwind-dev , libyaml-0-2 , libz3-4 , lld-16 , llvm-16 , pkg-config
+Recommends: z3
+Description: K framework toolchain
+ Includes K Framework compiler for K language definitions, and K interpreter
+ and prover for programs written in languages defined in K.
+Homepage: https://github.com/runtimeverification/k
diff --git a/package/debian/kframework/rules.noble b/package/debian/kframework/rules.noble
@@ -0,0 +1,43 @@
+#!/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/kframework
+PREFIX=/usr
+PYTHON_VERSION=python3.10
+PYTHON_DEB_VERSION=python3
+export DESTDIR
+export PREFIX
+
+%:
+	dh $@ 
+
+override_dh_auto_build:
+	mvn --batch-mode package -DskipTests -Dllvm.backend.prefix=$(PREFIX) -Dllvm.backend.destdir=$(DESTDIR)
+
+override_dh_auto_install:
+	package/package
+
+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/docker/Dockerfile.ubuntu-jammy b/package/docker/Dockerfile.ubuntu-jammy
@@ -9,15 +9,18 @@ RUN    apt-get update                   \
                         build-essential \
                         git             \
                         python3         \
-                        python3-pip
+                        python3-pip     \
+                        pipx
 
 COPY kframework_amd64_ubuntu_jammy.deb /kframework_amd64_ubuntu_jammy.deb
 RUN    apt-get update                                                                   \
     && apt-get upgrade --yes                                                            \
     && apt-get install --yes --no-install-recommends /kframework_amd64_ubuntu_jammy.deb
 
 COPY pyk /pyk
-RUN pip install poetry        \
+RUN pipx install poetry       \
+    && pipx ensurepath        \
+    && . /root/.profile       \
     && cd /pyk                \
     && make build             \
     && pip install dist/*.whl \

diff --git a/package/docker/Dockerfile.ubuntu-noble b/package/docker/Dockerfile.ubuntu-noble
@@ -0,0 +1,29 @@
+FROM runtimeverificationinc/z3:ubuntu-noble-4.13.0
+
+ENV TZ=America/Chicago
+RUN ln -snf /usr/share/zoneinfo/$TZ /etc/localtime && echo $TZ > /etc/timezone
+
+RUN    apt-get update                   \
+    && apt-get upgrade --yes            \
+    && apt-get install --yes            \
+                        build-essential \
+                        git             \
+                        python3         \
+                        python3-pip     \
+                        pipx
+
+COPY kframework_amd64_ubuntu_noble.deb /kframework_amd64_ubuntu_noble.deb
+RUN    apt-get update                                                                   \
+    && apt-get upgrade --yes                                                            \
+    && apt-get install --yes --no-install-recommends /kframework_amd64_ubuntu_noble.deb
+
+COPY pyk /pyk
+RUN pipx install poetry                               \
+    && pipx ensurepath                                \
+    && . /root/.profile                               \
+    && cd /pyk                                        \
+    && make build                                     \
+    && pip install dist/*.whl --break-system-packages \
+    && rm -rf /pyk
+
+RUN rm -rf /kframework_amd64_ubuntu_noble.deb
diff --git a/pyk/poetry.lock b/pyk/poetry.lock
diff --git a/pyk/pyproject.toml b/pyk/pyproject.toml
@@ -22,7 +22,7 @@ coloredlogs = "^15.0.1"
 filelock = "^3.9.0"
 graphviz = "^0.20.1"
 hypothesis = "^6.103.1"
-psutil = "5.9.5"
+psutil = "^5.9.5"
 pybind11 = "^2.10.3"
 pytest = "*"
 textual = "^0.27.0"