From 66fec84abb0356f76adb3b45008e45b099cf11f7 Mon Sep 17 00:00:00 2001 From: Raoul Date: Wed, 28 Oct 2026 12:47:15 +0000 Subject: [PATCH] Use a K frontend with faster claim loading (runtimeverification/k branch raoul/kprove-spec-steps) The K branch makes kprove apply the specification steps only to the spec's own modules, which shortens `kprove --dry-run --emit-json-spec` (claim loading in `kevm prove`). - flake.nix, flake.lock: k-framework at that K commit. - deps/k_frontend_rev: the K commit whose k-frontend jar the CI Docker image uses. The image is still based on the K release in deps/k_release; only the k-frontend jar is rebuilt from the commit and swapped in. Co-Authored-By: Claude Opus 5.5 --- .github/actions/with-docker/action.yml | 2 ++ .github/workflows/Dockerfile | 13 +++++++++++++ deps/k_frontend_rev | 1 + flake.lock | 8 ++++---- flake.nix | 2 +- 5 files changed, 21 insertions(+), 5 deletions(-) create mode 100644 deps/k_frontend_rev diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml index 8f71387f4c..e9e3fc5211 100644 --- a/.github/actions/with-docker/action.yml +++ b/.github/actions/with-docker/action.yml @@ -33,6 +33,7 @@ runs: IMAGE_GROUP=${IMAGE_USER} Z3_VERSION=$(cat deps/z3) K_VERSION=$(cat deps/k_release) + K_FRONTEND_REV=$(cat deps/k_frontend_rev) UV_VERSION=$(cat deps/uv_release) USER_ID=1000 GROUP_ID=${USER_ID} @@ -44,6 +45,7 @@ runs: --build-arg IMAGE_USER="${IMAGE_USER}" \ --build-arg IMAGE_GROUP="${IMAGE_GROUP}" \ --build-arg K_VERSION="${K_VERSION}" \ + --build-arg K_FRONTEND_REV="${K_FRONTEND_REV}" \ --build-arg Z3_VERSION="${Z3_VERSION}" \ --build-arg LLVM_VERSION="${LLVM_VERSION}" \ --build-arg UV_VERSION="${UV_VERSION}" diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile index aa08d880d5..74df1ffc5e 100644 --- a/.github/workflows/Dockerfile +++ b/.github/workflows/Dockerfile @@ -27,9 +27,22 @@ RUN apt-get update \ llvm-${LLVM_VERSION}-dev \ llvm-${LLVM_VERSION}-tools \ maven \ + openjdk-17-jdk-headless \ python3 \ python3-pip +# The K frontend (k-frontend jar) of the K commit in deps/k_frontend_rev replaces the one of the K +# release above. Only the Java frontend differs from the release; everything else is unchanged. +ARG K_FRONTEND_REV +RUN curl -fsSL "https://github.com/runtimeverification/k/archive/${K_FRONTEND_REV}.tar.gz" | tar -xz -C /tmp \ + && cd "/tmp/k-${K_FRONTEND_REV}" \ + && mvn --batch-mode --quiet -f k-frontend/pom.xml package -DskipTests \ + && jars=$(find / -xdev -path '*/kframework/java/k-frontend-1.0-SNAPSHOT.jar' -not -path '/tmp/*') \ + && test -n "${jars}" \ + && for jar in ${jars}; do cp -v k-frontend/target/k-frontend-1.0-SNAPSHOT.jar "${jar}"; done \ + && cd / \ + && rm -rf "/tmp/k-${K_FRONTEND_REV}" /root/.m2 + ARG IMAGE_USER=user ARG IMAGE_GROUP ARG USER_ID diff --git a/deps/k_frontend_rev b/deps/k_frontend_rev new file mode 100644 index 0000000000..6b02e83558 --- /dev/null +++ b/deps/k_frontend_rev @@ -0,0 +1 @@ +cbdcb3c1441b9a93b454a3cd1900ea8ecffd5570 diff --git a/flake.lock b/flake.lock index 2ad5462794..f3207c2db8 100644 --- a/flake.lock +++ b/flake.lock @@ -400,17 +400,17 @@ "uv2nix": "uv2nix" }, "locked": { - "lastModified": 1781787476, - "narHash": "sha256-qJF6n4J9gf6bSR/G5iH4905xGHUVHyqKHW1dkgGBdhY=", + "lastModified": 1793186465, + "narHash": "sha256-W2Jzbr9k0wK6IMOfvObXedK5DhCPRLoKFVuTaYpdDJg=", "owner": "runtimeverification", "repo": "k", - "rev": "4a46d1231473b599c699160132fd6e76a5c46406", + "rev": "cbdcb3c1441b9a93b454a3cd1900ea8ecffd5570", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v7.1.337", "repo": "k", + "rev": "cbdcb3c1441b9a93b454a3cd1900ea8ecffd5570", "type": "github" } }, diff --git a/flake.nix b/flake.nix index 88da89ea64..456246daeb 100644 --- a/flake.nix +++ b/flake.nix @@ -5,7 +5,7 @@ rv-nix-tools.url = "github:runtimeverification/rv-nix-tools/854d4f05ea78547d46e807b414faad64cea10ae4"; nixpkgs.follows = "rv-nix-tools/nixpkgs"; - k-framework.url = "github:runtimeverification/k/v7.1.337"; + k-framework.url = "github:runtimeverification/k/cbdcb3c1441b9a93b454a3cd1900ea8ecffd5570"; k-framework.inputs.nixpkgs.follows = "nixpkgs"; flake-utils.follows = "k-framework/flake-utils"; blockchain-k-plugin = {