Merge remote-tracking branch 'origin/develop' into _update-deps/runti…

…meverification/haskell-backend

.github/workflows/Dockerfile

@@ -63,7 +63,6 @@ RUN    apt-get update              \
         pkg-config                 \
         python3                    \
         python3-dev                \
-        python3-distutils          \
         python3-pip                \
         xxd                        \
         zlib1g-dev

.github/workflows/develop.yml

@@ -37,59 +37,3 @@ jobs:
           if git add --update && git commit --no-edit --allow-empty --message "Set Version: $(cat package/version)"; then
             git push origin master
           fi
-
-  post-performance-tests:
-    name: 'Performance Tests'
-    runs-on: [self-hosted, linux, normal]
-    continue-on-error: true
-    steps:
-      - uses: actions/checkout@v4
-      - 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
-          BENCHER_ADAPTER: json
-        run: |
-          set -euxo pipefail
-          workspace=$(pwd)
-          docker run --name "k-posting-profiling-tests-${GITHUB_SHA}" \
-            --rm -it --detach                                         \
-            -e BENCHER_API_TOKEN="$BENCHER_API_TOKEN"                 \
-            -e BENCHER_PROJECT="$BENCHER_PROJECT"                     \
-            -e BENCHER_ADAPTER="$BENCHER_ADAPTER"                     \
-            -e GITHUB_HEAD_REF="$GITHUB_HEAD_REF"                     \
-            -e GITHUB_BASE_REF="$GITHUB_BASE_REF"                     \
-            -e GITHUB_TOKEN="$GITHUB_TOKEN"                           \
-            -e GITHUB_ACTIONS=true                                    \
-            -e GITHUB_EVENT_NAME="$GITHUB_EVENT_NAME"                 \
-            -e GITHUB_EVENT_PATH="$GITHUB_EVENT_PATH"                 \
-            -e GITHUB_REPOSITORY="$GITHUB_REPOSITORY"                 \
-            -e GITHUB_REF="$GITHUB_REF"                               \
-            -e GITHUB_SHA="$GITHUB_SHA"                               \
-            --workdir /opt/workspace                                  \
-            -v "${workspace}:/opt/workspace"                          \
-            -v "${GITHUB_EVENT_PATH}:${GITHUB_EVENT_PATH}"            \
-            "${BASE_OS}:${BASE_DISTRO}"
-      - name: 'Setting up dependencies'
-        run: |
-          set -euxo pipefail
-          docker exec -t "k-posting-profiling-tests-${GITHUB_SHA}" /bin/bash -c './k-distribution/tests/profiling/setup_profiling.sh SKIP_K_BUILD'
-      - name: 'Getting Performance Tests Results'
-        run: |
-          set -euxo pipefail
-          docker exec -t "k-posting-profiling-tests-${GITHUB_SHA}" /bin/bash -c './k-distribution/tests/profiling/post_results_to_develop.py "${GITHUB_SHA}"'
-      - name: 'Posting Performance Tests Results'
-        run: |
-          set -euxo pipefail
-          docker exec -t "k-posting-profiling-tests-${GITHUB_SHA}" /bin/bash -c 'bencher run            \
-            --if-branch "develop" --else-if-branch "master"                    \
-            --file .profiling-results.json --err --ci-only-on-alert            \
-            --github-actions "${GITHUB_TOKEN}" "echo Exporting report"'
-      - name: 'Tear down Docker'
-        if: always()
-        run: |
-          docker stop --time=0 "k-posting-profiling-tests-${GITHUB_SHA}"
-          docker container rm --force "k-posting-profiling-tests-${GITHUB_SHA}" || true

.github/workflows/release.yml

@@ -76,16 +76,77 @@ jobs:
           name: k-framework-binary
 
       - name: 'Publish K to k-framework-binary cache'
-        uses: workflow/[email protected].0
+        uses: workflow/[email protected].2
         env:
           CACHIX_AUTH_TOKEN: '${{ secrets.CACHIX_PRIVATE_KFB_TOKEN }}'
           GC_DONT_GC: '1'
         with:
           packages: jq
           script: |
             export PATH="$(nix build github:runtimeverification/kup --no-link --json | jq -r '.[].outputs | to_entries[].value')/bin:$PATH"
-            kup publish k-framework-binary .#k --keep-days 180
-            kup publish k-framework-binary .#k.openssl.procps.secp256k1 --keep-days 180
+            kup publish --verbose k-framework-binary .#k --keep-days 180
+            kup publish --verbose 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'
@@ -301,6 +362,8 @@ jobs:
           # test suite, so the PL-tutorial is disabled for now.
           #   - https://github.com/runtimeverification/k/issues/3705
           cd homebrew-k-old
+          # brew tap expects a git repository, so we initialise the current folder as a dummy repo
+          git init
           brew tap runtimeverification/k "file:///$(pwd)"
           brew install ${{ needs.macos-build.outputs.bottle_path }} -v
           # cp -R /usr/local/share/kframework/pl-tutorial ~
@@ -357,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

flake.nix

@@ -9,8 +9,7 @@
     };
 
     poetry2nix = {
-      url =
-        "github:nix-community/poetry2nix/626111646fe236cb1ddc8191a48c75e072a82b7c";
+      url = "github:nix-community/poetry2nix/2024.9.219347";
       inputs.nixpkgs.follows = "llvm-backend/nixpkgs";
     };
 
@@ -94,9 +93,8 @@
                   "org.checkerframework:checker-qual:3.33.0"
                   "com.google.errorprone:error_prone_annotations:2.18.0"
                 ];
-                manualMvnSourceArtifacts = [
-                  "org.scala-sbt:compiler-bridge_2.13:1.8.0"
-                ];
+                manualMvnSourceArtifacts =
+                  [ "org.scala-sbt:compiler-bridge_2.13:1.8.0" ];
                 inherit (final) maven;
                 inherit (prev) llvm-backend;
                 clang = prev."clang_${toString final.llvm-version}";
@@ -210,13 +208,18 @@
             };
         };
         defaultPackage = packages.k;
-        devShells.kore-integration-tests = pkgs.kore-tests (pkgs.mk-k-framework {
-          inherit (pkgs) haskell-backend-bins;
-          llvm-kompile-libs = { };
-        });
+        devShells.kore-integration-tests = pkgs.kore-tests
+          (pkgs.mk-k-framework {
+            inherit (pkgs) haskell-backend-bins;
+            llvm-kompile-libs = { };
+          });
       }) // {
         overlays.llvm-backend = llvm-backend.overlays.default;
         overlays.z3 = haskell-backend.overlays.z3;
+        overlays.pyk = (import ./nix/pyk-overlay.nix {
+          inherit poetry2nix;
+          projectDir = ./pyk;
+        });
 
         overlay = nixpkgs.lib.composeManyExtensions allOverlays;
       };

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
 

package/debian/kframework/compat.noble

@@ -0,0 +1 @@
+10

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
 

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

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)
+

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 \

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

package/version.sh

@@ -27,7 +27,6 @@ version_sub() {
     sed --in-place 's/^version = ".*"$/version = "'${version}'"/'                                                     pyk/pyproject.toml
     sed --in-place "s/^version = '.*'$/version = '${version}'/"                                                       pyk/docs/conf.py
     sed --in-place "s/^release = '.*'$/release = '${version}'/"                                                       pyk/docs/conf.py
-    sed --in-place "s/^__version__: Final = '.*'/__version__: Final = '${version}'/"                                  pyk/src/pyk/__init__.py
 }
 
 version_command="$1" ; shift