Remove k submodule, rely on release tags for updates (#2023)

* .gitmodules, deps/k: remove K submodule * .github/update-version, flake.nix: update to not use submodule build * Makefile: remove recipes for building K in submodule * README: update instructions * README: correct documentation about installing K from kup * Set Version: 1.0.264 * Makefile: formatting * .github/{with-docker,Dockerfile}: remove K_COMMIT argument * .github/Dockerfile: correct argument passing * .github/{Dockerfile,with-docker}: remove use of stack deps dockerfile --------- Co-authored-by: devops <[email protected]>
runtimeverification · Aug 18, 2023 · 867bfea · 867bfea
1 parent 2be4f95
commit 867bfea
Show file tree

Hide file tree

Showing 11 changed files with 29 additions and 91 deletions.
diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml
@@ -54,31 +54,23 @@ runs:
       USER=github-user
       GROUP=${USER}
       Z3_VERSION=4.12.1
-      K_COMMIT=$(cat deps/k_release)
+      K_VERSION=$(cat deps/k_release)
       USER_ID=1000
       GROUP_ID=${USER_ID}
-      K_VERSION=$(cat deps/k/package/version)
 
       docker build .                           \
         --file .github/workflows/Dockerfile.z3 \
         --tag z3:${Z3_VERSION}                 \
 
-      docker build deps/k                                           \
-        --file deps/k/.github/workflows/Dockerfile.stack-deps       \
-        --tag stack:${BASE_DISTRO}-${K_VERSION}                     \
-        --build-arg BASE_OS=${BASE_OS}                              \
-        --build-arg BASE_DISTRO=${BASE_DISTRO}
-
-      docker build . --file ${DOCKERFILE} \
-        --tag runtimeverification/${TAG_NAME}            \
-        --build-arg USER_ID=${USER_ID}                   \
-        --build-arg GROUP_ID=${GROUP_ID}                 \
-        --build-arg USER=${USER}                         \
-        --build-arg GROUP=${GROUP}                       \
-        --build-arg BASE_DISTRO=${BASE_DISTRO}           \
-        --build-arg K_COMMIT=${K_COMMIT}                 \
-        --build-arg K_VERSION=${K_VERSION}               \
-        --build-arg Z3_VERSION=${Z3_VERSION}             \
+      docker build . --file ${DOCKERFILE}        \
+        --tag runtimeverification/${TAG_NAME}    \
+        --build-arg USER_ID=${USER_ID}           \
+        --build-arg GROUP_ID=${GROUP_ID}         \
+        --build-arg USER=${USER}                 \
+        --build-arg GROUP=${GROUP}               \
+        --build-arg BASE_DISTRO=${BASE_DISTRO}   \
+        --build-arg K_VERSION=${K_VERSION}       \
+        --build-arg Z3_VERSION=${Z3_VERSION}     \
         --build-arg LLVM_VERSION=${LLVM_VERSION}
 
       docker run                        \

diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile
@@ -1,30 +1,22 @@
 ARG Z3_VERSION
-ARG LLVM_VERSION
 ARG K_VERSION
-ARG K_COMMIT
 ARG BASE_DISTRO
+ARG LLVM_VERSION
 
 FROM ghcr.io/foundry-rs/foundry:nightly-ca67d15f4abd46394b324c50e21e66f306a1162d as FOUNDRY
 
 ARG Z3_VERSION
 FROM z3:${Z3_VERSION} as Z3
 
 ARG K_VERSION
-ARG BASE_DISTRO
-FROM stack:${BASE_DISTRO}-${K_VERSION} as STACK
-
-ARG K_COMMIT
-ARG LLVM_VERSION
-FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_COMMIT}
+FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_VERSION}
 
 COPY --from=FOUNDRY /usr/local/bin/forge /usr/local/bin/forge
 COPY --from=FOUNDRY /usr/local/bin/anvil /usr/local/bin/anvil
 COPY --from=FOUNDRY /usr/local/bin/cast /usr/local/bin/cast
 
 COPY --from=Z3 /usr/bin/z3 /usr/bin/z3
 
-COPY --from=STACK /usr/local/bin/stack /usr/local/bin/stack
-
 ARG LLVM_VERSION
 
 RUN    apt-get update                  \
@@ -67,5 +59,3 @@ RUN    curl -sSL https://install.python-poetry.org | python3 - \
 RUN    cargo install svm-rs --version 0.3.0 \
     && svm install 0.8.13                   \
     && solc --version
-
-COPY --from=STACK --chown=$USER:$GROUP /home/$USER/.stack /home/$USER/.stack
diff --git a/.github/workflows/update-version.yml b/.github/workflows/update-version.yml
@@ -38,12 +38,6 @@ jobs:
           K_VERSION=$(poetry -C kevm-pyk run python3 -c 'import pyk; print(pyk.K_VERSION)')
           echo ${K_VERSION} > deps/k_release
           git add deps/k_release && git commit -m "deps/k_release: sync release file version ${K_VERSION}" || true
-      - name: 'Update K submodule'
-        run: |
-          K_VERSION=$(cat deps/k_release)
-          git -C deps/k fetch --tags
-          git -C deps/k checkout "v${K_VERSION}"
-          git add deps/k && git commit -m "deps/k: sync K submodule version v${K_VERSION}" || true
       - name: 'Update plugin release file'
         run: |
           BKP_VERSION=$(git -C deps/plugin rev-parse HEAD)

diff --git a/.gitmodules b/.gitmodules
@@ -3,10 +3,6 @@
 	url = https://github.com/ethereum/tests.git
 	branch = develop
 	ignore = untracked
-[submodule "deps/k"]
-	path = deps/k
-	url = https://github.com/runtimeverification/k
-	ignore = untracked
 [submodule "deps/plugin"]
 	path = deps/plugin
 	url = https://github.com/runtimeverification/blockchain-k-plugin

diff --git a/Makefile b/Makefile
@@ -44,13 +44,13 @@ PLUGIN_FULL_PATH := $(abspath ${PLUGIN_SUBMODULE})
 export PLUGIN_FULL_PATH
 
 
-.PHONY: all clean distclean install uninstall                                                            	\
-        deps k-deps plugin-deps protobuf proto-tester                                                      	\
-        poetry-env poetry shell kevm-pyk                                                                 	\
-        build build-haskell build-haskell-standalone build-foundry build-llvm build-node build-kevm      	\
-        test test-integration test-conformance test-prove test-foundry-prove test-prove-smoke            	\
-        test-vm test-rest-vm test-bchain test-rest-bchain test-node test-interactive test-interactive-run	\
-        profile                                                                                             \
+.PHONY: all clean distclean install uninstall                                                             \
+        plugin-deps protobuf proto-tester                                                                 \
+        poetry-env poetry shell kevm-pyk                                                                  \
+        build build-haskell build-haskell-standalone build-foundry build-llvm build-node build-kevm       \
+        test test-integration test-conformance test-prove test-foundry-prove test-prove-smoke             \
+        test-vm test-rest-vm test-bchain test-rest-bchain test-node test-interactive test-interactive-run \
+        profile                                                                                           \
         media media-pdf metropolis-theme
 
 .SECONDARY:
@@ -77,31 +77,6 @@ $(protobuf_out): $(NODE_DIR)/proto/msg.proto
 # K Dependencies
 # --------------
 
-deps: k-deps
-
-K_MVN_ARGS :=
-ifneq ($(SKIP_LLVM),)
-    K_MVN_ARGS += -Dllvm.backend.skip
-endif
-ifneq ($(SKIP_HASKELL),)
-    K_MVN_ARGS += -Dhaskell.backend.skip
-endif
-
-ifneq ($(APPLE_SILICON),)
-    K_MVN_ARGS += -Dstack.extra-opts='--compiler ghc-8.10.7 --system-ghc'
-endif
-
-ifneq ($(RELEASE),)
-    K_BUILD_TYPE := FastBuild
-else
-    K_BUILD_TYPE := Debug
-endif
-
-k-deps:
-	cd $(K_SUBMODULE)                                                                                                                                                                            \
-	    && mvn --batch-mode package -DskipTests -Dllvm.backend.prefix=$(INSTALL_LIB)/kframework -Dllvm.backend.destdir=$(CURDIR)/$(BUILD_DIR) -Dproject.build.type=$(K_BUILD_TYPE) $(K_MVN_ARGS) \
-	    && DESTDIR=$(CURDIR)/$(BUILD_DIR) PREFIX=$(INSTALL_LIB)/kframework package/package
-
 plugin_k_include  := $(KEVM_INCLUDE)/kframework/plugin
 plugin_include    := $(KEVM_LIB)/blockchain-k-plugin/include
 plugin_k          := krypto.md

diff --git a/README.md b/README.md
@@ -159,25 +159,17 @@ export PATH=$HOME/.local/bin:$PATH
 
 #### K Framework
 
-The `Makefile` and `kevm` will work with either a (i) globally installed K or a (ii) K submodule included in this repository.
-For contributing to `kevm`, it is highly recommended to go with (ii) because some of the build scripts might not work otherwise.
-Follow these instructions to get and build the K submodule:
+You need to install the [K Framework] on your system, see the instructions there.
+The fastest way is via the [kup package manager], with which you can do to get the correct version of K:
 
 ```sh
-git submodule update --init --recursive -- deps/k
-make k-deps
+kup install k.openssl.procps --version v$(cat deps/k_release)
 ```
 
-If you don't need either the LLVM or Haskell backend, there are flags to skip them:
+You can also drop into a single development shell with the correct version of K on path by doing:
 
 ```sh
-make k-deps SKIP_LLVM=true SKIP_HASKELL=true
-```
-
-On an Apple Silicon machine, an additional flag to `make` is required to correctly build the Haskell backend:
-
-```sh
-make k-deps APPLE_SILICON=true
+kup shell k.openssl.procps --version v$(cat deps/k_release)
 ```
 
 #### Blockchain Plugin
@@ -370,14 +362,15 @@ Resources
 -   [EVM Opcode Interactive Reference](https://www.evm.codes/?fork=merge)
 -   [Solidity ABI Encoding](https://docs.soliditylang.org/en/v0.8.19/abi-spec.html)
 
-For more information about [The K Framework](https://kframework.org), refer to these sources:
+For more information about the [K Framework], refer to these sources:
 
 -   [The K Tutorial](https://github.com/runtimeverification/k/tree/master/k-distribution/k-tutorial)
 -   [Semantics-Based Program Verifiers for All Languages](https://fsl.cs.illinois.edu/publications/stefanescu-park-yuwen-li-rosu-2016-oopsla)
 -   [Reachability Logic Resources](http://fsl.cs.illinois.edu/index.php/Reachability_Logic_in_K)
 -   [Matching Logic Resources](http://www.matching-logic.org/)
 -   [Logical Frameworks](https://dl.acm.org/doi/10.5555/208683.208700): Discussion of logical frameworks.
 
+[K Framework]: <https://kframework.org>
 [Jello Paper]: <https://jellopaper.org>
 [2017 Devcon3]: <https://archive.devcon.org/archive/watch?edition=3&order=desc&sort=edition>
 [K Reachability Logic Prover]: <http://fsl.cs.illinois.edu/FSL/papers/2016/stefanescu-park-yuwen-li-rosu-2016-oopsla/stefanescu-park-yuwen-li-rosu-2016-oopsla-public.pdf>

diff --git a/deps/k b/deps/k
diff --git a/flake.nix b/flake.nix
@@ -241,7 +241,6 @@
 
           update-from-submodules =
             rv-utils.lib.update-from-submodules pkgs ./flake.lock {
-              k-framework.submodule = "deps/k";
               blockchain-k-plugin.submodule = "deps/plugin";
               ethereum-tests.submodule = "tests/ethereum-tests";
               ethereum-legacytests.submodule =

diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.263"
+version = "1.0.264"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/package/debian/changelog b/package/debian/changelog
@@ -1,4 +1,4 @@
-kevm (1.0.263) unstable; urgency=medium
+kevm (1.0.264) unstable; urgency=medium
 
   * Initial Release.
 

diff --git a/package/version b/package/version
@@ -1 +1 @@
-1.0.263
+1.0.264