diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml index 17ac007a6e..8e3c9197f3 100644 --- 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 index b71356e39b..4d25d77427 100644 --- a/.github/workflows/Dockerfile +++ b/.github/workflows/Dockerfile @@ -1,8 +1,7 @@ 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 @@ -10,12 +9,7 @@ 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 @@ -23,8 +17,6 @@ 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 index 503eb2de48..b96cb9f354 100644 --- 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 index 2ea69188d8..9e12e7b154 100644 --- 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 index 76455a4245..e9ad3b53fe 100644 --- 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 index 03a3c9ed2f..64e173c1f6 100644 --- 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,7 +362,7 @@ 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) @@ -378,6 +370,7 @@ For more information about [The K Framework](https://kframework.org), refer to t - [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]: [Jello Paper]: [2017 Devcon3]: [K Reachability Logic Prover]: diff --git a/deps/k b/deps/k deleted file mode 160000 index cab7e1b2ff..0000000000 --- a/deps/k +++ /dev/null @@ -1 +0,0 @@ -Subproject commit cab7e1b2ffe6b0e8394d690a8d5b5d42f5d39b0a diff --git a/flake.nix b/flake.nix index 93434e9040..de68df5852 100644 --- 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 index 2c04428f73..3b09750379 100644 --- 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. ", diff --git a/package/debian/changelog b/package/debian/changelog index dcbb577350..fab23932e7 100644 --- 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 index 727467ddf0..5f6ecc9fa1 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.263 +1.0.264