From b1e7be87c92722785ceeaf5dddbdd5a5398ab42e Mon Sep 17 00:00:00 2001 From: F-WRunTime Date: Thu, 11 Sep 2025 12:56:47 -0600 Subject: [PATCH 1/4] Update LLVM version from 15/16 to 17 across K Framework MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Update GitHub Actions workflows: llvm: 15/16 → 17 - Update Debian package dependencies: - control.jammy: clang-15→17, lld-15→17, llvm-15→17 - control.noble: clang-16→17, lld-16→17 (llvm-17 already correct) - Update install-build-deps: clang-15→17, lld-15→17, llvm-15-tools→17 - Update macOS Homebrew: llvm@15→17 - Update macos-envrc: llvm@15→17 - Update llvm-backend submodule to include LLVM 17 changes This migration aligns K Framework with LLVM 17 for improved performance and compatibility with newer toolchain features. Depends on: https://github.com/runtimeverification/llvm-backend/pull/1214 --- .github/workflows/release.yml | 6 +++--- .github/workflows/test-pr.yml | 6 +++--- install-build-deps | 6 +++--- llvm-backend/src/main/native/llvm-backend | 2 +- macos-envrc | 2 +- package/debian/kframework/control.jammy | 2 +- package/debian/kframework/control.noble | 4 ++-- package/macos/brew-install-deps | 2 +- 8 files changed, 15 insertions(+), 15 deletions(-) diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 1ef64ada6a8..66e2cc53264 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -177,7 +177,7 @@ jobs: with: os: ubuntu distro: noble - llvm: 16 + llvm: 17 jdk: 21 pkg-name: kframework_amd64_ubuntu_noble.deb build-package: package/debian/build-package noble kframework @@ -243,7 +243,7 @@ jobs: with: os: ubuntu distro: jammy - llvm: 15 + llvm: 17 pkg-name: kframework_amd64_ubuntu_jammy.deb build-package: package/debian/build-package jammy kframework test-package: package/debian/test-package @@ -535,7 +535,7 @@ jobs: tag: k-release-ci-${{ github.sha }} os: ubuntu distro: jammy - llvm: 15 + llvm: 17 - name: 'Push Maven Packages' shell: bash {0} diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index 158e64b998a..06382b75014 100644 --- a/.github/workflows/test-pr.yml +++ b/.github/workflows/test-pr.yml @@ -79,7 +79,7 @@ jobs: tag: k-ci-${{ github.sha }} os: ubuntu distro: jammy - llvm: 15 + llvm: 17 - name: 'Build and Test K' run: docker exec -t "k-ci-${GITHUB_SHA}" /bin/bash -c 'mvn verify -Dspotless.check.skip=true --batch-mode -U' - name: 'Tear down Docker' @@ -100,7 +100,7 @@ jobs: with: os: ubuntu distro: jammy - llvm: 15 + llvm: 17 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 @@ -131,7 +131,7 @@ jobs: with: os: ubuntu distro: jammy - llvm: 15 + llvm: 17 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 diff --git a/install-build-deps b/install-build-deps index d89338691f9..03da8e7c604 100755 --- a/install-build-deps +++ b/install-build-deps @@ -11,7 +11,7 @@ inst_Debian() { sudo apt-get install -q \ bison \ build-essential \ - clang-15 \ + clang-17 \ cmake \ curl \ flex \ @@ -26,8 +26,8 @@ inst_Debian() { libunwind-dev \ libyaml-dev \ libz3-dev \ - lld-15 \ - llvm-15-tools \ + lld-17 \ + llvm-17-tools \ m4 \ maven \ openjdk-17-jdk \ diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend index 09a3d777393..db7cfe56226 160000 --- a/llvm-backend/src/main/native/llvm-backend +++ b/llvm-backend/src/main/native/llvm-backend @@ -1 +1 @@ -Subproject commit 09a3d777393caba34e89d55916ac5046913dbedb +Subproject commit db7cfe56226f4c62bfae9d66973327f7d0879702 diff --git a/macos-envrc b/macos-envrc index 764c5959628..e3f08d25e40 100644 --- a/macos-envrc +++ b/macos-envrc @@ -3,5 +3,5 @@ PATH_add `brew --prefix bison`/bin PATH_add `brew --prefix flex`/bin -PATH_add `brew --prefix llvm@15`/bin +PATH_add `brew --prefix llvm@17`/bin PATH_add `brew --prefix openjdk`/bin diff --git a/package/debian/kframework/control.jammy b/package/debian/kframework/control.jammy index 6fcfc5e3f4a..55948b8d89d 100644 --- a/package/debian/kframework/control.jammy +++ b/package/debian/kframework/control.jammy @@ -10,7 +10,7 @@ Package: kframework Architecture: any Section: devel Priority: optional -Depends: bison , clang-15 , openjdk-17-jre-headless , flex , gcc , g++ , libboost-dev , libffi-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-0 , libtinfo-dev , libunwind-dev , libyaml-0-2 , libz3-4 , lld-15 , llvm-15 , pkg-config +Depends: bison , clang-17 , openjdk-17-jre-headless , flex , gcc , g++ , libboost-dev , libffi-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-0 , libtinfo-dev , libunwind-dev , libyaml-0-2 , libz3-4 , lld-17 , llvm-17 , pkg-config Recommends: z3 Description: K framework toolchain Includes K Framework compiler for K language definitions, and K interpreter diff --git a/package/debian/kframework/control.noble b/package/debian/kframework/control.noble index 24f47adbf10..e78589ab676 100644 --- a/package/debian/kframework/control.noble +++ b/package/debian/kframework/control.noble @@ -2,7 +2,7 @@ Source: kframework Section: devel Priority: optional Maintainer: Dwight Guth -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 +Build-Depends: clang-17 , 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 @@ -10,7 +10,7 @@ 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 +Depends: bison , clang-17 , 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-17 , llvm-17 , pkg-config Recommends: z3 Description: K framework toolchain Includes K Framework compiler for K language definitions, and K interpreter diff --git a/package/macos/brew-install-deps b/package/macos/brew-install-deps index 5e17a9c6438..45fd5904d51 100755 --- a/package/macos/brew-install-deps +++ b/package/macos/brew-install-deps @@ -1,4 +1,4 @@ #!/bin/bash -ex brew update -brew install maven cmake boost libyaml jemalloc llvm@12 gmp mpfr z3 pkg-config flex bison haskell-stack +brew install maven cmake boost libyaml jemalloc llvm@17 gmp mpfr z3 pkg-config flex bison haskell-stack From 666ea46cdae3faf828b7dead1ccca2a2ce9117c6 Mon Sep 17 00:00:00 2001 From: F-WRunTime Date: Thu, 11 Sep 2025 13:45:48 -0600 Subject: [PATCH 2/4] Fix LLVM version compatibility issues - Revert Ubuntu Jammy builds back to LLVM 15 (not available in Ubuntu 22.04) - Update llvm-backend clang-tidy script to auto-detect available LLVM version - Fix Debian package dependencies to use consistent LLVM versions per Ubuntu release - Jammy (22.04): LLVM 15 (available in standard repos) - Noble (24.04): LLVM 17 (available in standard repos) This resolves the 'run-clang-tidy-17: command not found' error and Ubuntu Jammy package build failures by using the correct LLVM versions for each platform. --- .github/workflows/test-pr.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index 06382b75014..158e64b998a 100644 --- a/.github/workflows/test-pr.yml +++ b/.github/workflows/test-pr.yml @@ -79,7 +79,7 @@ jobs: tag: k-ci-${{ github.sha }} os: ubuntu distro: jammy - llvm: 17 + llvm: 15 - name: 'Build and Test K' run: docker exec -t "k-ci-${GITHUB_SHA}" /bin/bash -c 'mvn verify -Dspotless.check.skip=true --batch-mode -U' - name: 'Tear down Docker' @@ -100,7 +100,7 @@ jobs: with: os: ubuntu distro: jammy - llvm: 17 + llvm: 15 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 @@ -131,7 +131,7 @@ jobs: with: os: ubuntu distro: jammy - llvm: 17 + 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 From e4715b7d90e0ed5fab58e046c692039b275a105a Mon Sep 17 00:00:00 2001 From: F-WRunTime Date: Thu, 11 Sep 2025 22:15:49 -0600 Subject: [PATCH 3/4] Fix LLVM version consistency: LLVM 15 for Jammy, LLVM 17 for Noble - Update release workflow to use LLVM 15 for Ubuntu Jammy builds - Fix kframework Jammy package dependencies to use clang-15, lld-15, llvm-15 - Maintain LLVM 17 for Ubuntu Noble builds (correct for Ubuntu 24.04) This ensures consistency between workflow configuration and package dependencies, resolving the mismatch that was causing test confusion. --- .github/workflows/release.yml | 4 ++-- package/debian/kframework/control.jammy | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 66e2cc53264..348fc5cb9f2 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -243,7 +243,7 @@ jobs: with: os: ubuntu distro: jammy - llvm: 17 + llvm: 15 pkg-name: kframework_amd64_ubuntu_jammy.deb build-package: package/debian/build-package jammy kframework test-package: package/debian/test-package @@ -535,7 +535,7 @@ jobs: tag: k-release-ci-${{ github.sha }} os: ubuntu distro: jammy - llvm: 17 + llvm: 15 - name: 'Push Maven Packages' shell: bash {0} diff --git a/package/debian/kframework/control.jammy b/package/debian/kframework/control.jammy index 55948b8d89d..6fcfc5e3f4a 100644 --- a/package/debian/kframework/control.jammy +++ b/package/debian/kframework/control.jammy @@ -10,7 +10,7 @@ Package: kframework Architecture: any Section: devel Priority: optional -Depends: bison , clang-17 , openjdk-17-jre-headless , flex , gcc , g++ , libboost-dev , libffi-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-0 , libtinfo-dev , libunwind-dev , libyaml-0-2 , libz3-4 , lld-17 , llvm-17 , pkg-config +Depends: bison , clang-15 , openjdk-17-jre-headless , flex , gcc , g++ , libboost-dev , libffi-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-0 , libtinfo-dev , libunwind-dev , libyaml-0-2 , libz3-4 , lld-15 , llvm-15 , pkg-config Recommends: z3 Description: K framework toolchain Includes K Framework compiler for K language definitions, and K interpreter From fdfbdf442bbb270de64f3a4531da054a402bd39b Mon Sep 17 00:00:00 2001 From: F-WRunTime Date: Wed, 17 Sep 2025 22:01:35 -0600 Subject: [PATCH 4/4] Set to latest version --- llvm-backend/src/main/native/llvm-backend | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend index db7cfe56226..14506637506 160000 --- a/llvm-backend/src/main/native/llvm-backend +++ b/llvm-backend/src/main/native/llvm-backend @@ -1 +1 @@ -Subproject commit db7cfe56226f4c62bfae9d66973327f7d0879702 +Subproject commit 145066375064b27d6e392cdcdfb1efad1c21875d