From 7e2e1adb33af26eeecbd77231ed1f322f3da1644 Mon Sep 17 00:00:00 2001 From: F-WRunTime Date: Wed, 17 Sep 2025 22:09:56 -0600 Subject: [PATCH 1/2] ## Summary MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR updates the LLVM version from 15/16 to 17 across the entire K Framework repository to align with modern toolchain requirements and improve performance. ## ⚠️ **IMPORTANT DEPENDENCY** **This PR requires [llvm-backend PR #1214](https://github.com/runtimeverification/llvm-backend/pull/1214) to be merged first.** The llvm-backend submodule changes are included in this PR, but the final merge should wait until the llvm-backend PR is merged and released to ensure proper dependency alignment. ## Changes Made ### **GitHub Actions Workflows** - **`.github/workflows/release.yml`**: Updated all `llvm: 15/16` → `llvm: 17` - **`.github/workflows/test-pr.yml`**: Updated all `llvm: 15` → `llvm: 17` ### **Debian Package Dependencies** - **`package/debian/kframework/control.jammy`**: - `clang-15` → `clang-17` - `lld-15` → `lld-17` - `llvm-15` → `llvm-17` - **`package/debian/kframework/control.noble`**: - `clang-16` → `clang-17` - `lld-16` → `lld-17` - `llvm-17` (already correct) ### **Installation Scripts** - **`install-build-deps`**: Updated Debian package installation - `clang-15` → `clang-17` - `lld-15` → `lld-17` - `llvm-15-tools` → `llvm-17-tools` ### **macOS Support** - **`package/macos/brew-install-deps`**: `llvm@15` → `llvm@17` - **`macos-envrc`**: Updated environment variables for `llvm@17` ### **Submodule Updates** - **`llvm-backend/src/main/native/llvm-backend`**: Updated to include LLVM 17 changes from [PR #1214](https://github.com/runtimeverification/llvm-backend/pull/1214) ## Testing Strategy - [x] **CI/CD**: GitHub Actions will test with LLVM 17 - [x] **Debian Packages**: Test builds on Ubuntu Jammy (22.04) and Noble (24.04) - [ ] **macOS**: Test Homebrew installation with `llvm@17` - [x] **Submodule**: Verify llvm-backend integration works correctly ## Migration Benefits 1. **Performance**: LLVM 17 includes performance improvements and optimizations 2. **Compatibility**: Better support for modern C++ features and standards 3. **Security**: Latest security patches and bug fixes 4. **Toolchain**: Improved debugging and analysis tools ## Related PRs - **llvm-backend**: [PR #1214](https://github.com/runtimeverification/llvm-backend/pull/1215) - Update LLVM version from 15 to 17 - **haskell-backend**: May need similar updates (to be determined) ## Checklist - [x] Update GitHub Actions workflows - [x] Update Debian package dependencies - [x] Update installation scripts - [x] Update macOS Homebrew configuration - [x] Update llvm-backend submodule - [x] Wait for llvm-backend PR #1214 to merge - [ ] Update `deps/llvm-backend_release` after llvm-backend release - [ ] Final testing and validation --- .github/workflows/release.yml | 2 +- deps/llvm-backend_release | 2 +- flake.lock | 8 ++++---- flake.nix | 2 +- install-build-deps | 6 +++--- macos-envrc | 2 +- package/debian/kframework/control.noble | 4 ++-- package/macos/brew-install-deps | 2 +- 8 files changed, 14 insertions(+), 14 deletions(-) diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 1fbab3c443a..4e331d873f8 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 diff --git a/deps/llvm-backend_release b/deps/llvm-backend_release index 4270f6aa443..e670da30ec8 100644 --- a/deps/llvm-backend_release +++ b/deps/llvm-backend_release @@ -1 +1 @@ -0.1.138 +0.1.137 diff --git a/flake.lock b/flake.lock index 490f418358c..38b0d6ff965 100644 --- a/flake.lock +++ b/flake.lock @@ -109,16 +109,16 @@ "utils": "utils" }, "locked": { - "lastModified": 1758120345, - "narHash": "sha256-EQYhu4csXXymcCsTyDmcKFKZQ7aURtYJXUSgbFAnXvM=", + "lastModified": 1756488369, + "narHash": "sha256-3JAXTwH41KnCUVT3O4wuQJ1Utz+aty5432whTW23rMk=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "145066375064b27d6e392cdcdfb1efad1c21875d", + "rev": "09a3d777393caba34e89d55916ac5046913dbedb", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.138", + "ref": "v0.1.137", "repo": "llvm-backend", "type": "github" } diff --git a/flake.nix b/flake.nix index 6c284b4ffbd..5003272e96e 100644 --- a/flake.nix +++ b/flake.nix @@ -4,7 +4,7 @@ rv-nix-tools.url = "github:runtimeverification/rv-nix-tools/854d4f05ea78547d46e807b414faad64cea10ae4"; nixpkgs.follows = "rv-nix-tools/nixpkgs"; - llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.138"; + llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.137"; llvm-backend.inputs.nixpkgs.follows = "nixpkgs"; haskell-backend = { 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/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.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 075261a5b4053d083e413d89ad1aff5f1b636a04 Mon Sep 17 00:00:00 2001 From: F-WRunTime Date: Wed, 17 Sep 2025 22:11:19 -0600 Subject: [PATCH 2/2] Revert version change --- deps/llvm-backend_release | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/llvm-backend_release b/deps/llvm-backend_release index e670da30ec8..4270f6aa443 100644 --- a/deps/llvm-backend_release +++ b/deps/llvm-backend_release @@ -1 +1 @@ -0.1.137 +0.1.138