Update dependency: deps/pyk_release (#2202)

* deps/pyk_release: Set Version v0.1.524 * kevm-pyk/: sync poetry files pyk version v0.1.524 * flake.{nix,lock}: update Nix derivations * Set Version: 1.0.380 * Drop `kdist` --------- Co-authored-by: devops <[email protected]> Co-authored-by: Tamás Tóth <[email protected]>
runtimeverification · Dec 1, 2023 · 1a7517c · 1a7517c
1 parent d8fcaf8
commit 1a7517c
Show file tree

Hide file tree

Showing 23 changed files with 36 additions and 683 deletions.
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -108,7 +108,7 @@ jobs:
       - name: 'Build kevm-pyk'
         run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'make poetry'
       - name: 'Build targets'
-        run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` evm-semantics.llvm evm-semantics.haskell'
+        run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kdist --verbose build -j`nproc` evm-semantics.llvm evm-semantics.haskell'
       - name: 'Test integration'
         run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'make test-integration'
       - name: 'Test conformance'
@@ -150,7 +150,7 @@ jobs:
       - name: 'Build kevm-pyk'
         run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'make poetry'
       - name: 'Build distribution'
-        run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` evm-semantics.plugin evm-semantics.haskell'
+        run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kdist --verbose build -j`nproc` evm-semantics.plugin evm-semantics.haskell'
       - name: 'Prove Haskell'
         run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c "make ${{ matrix.test-suite }} PYTEST_ARGS='-vv ${{ matrix.test-args }}' PYTEST_PARALLEL=4"
       - name: 'Tear down Docker'

diff --git a/README.md b/README.md
@@ -184,42 +184,42 @@ You also need to get the blockchain plugin submodule and install it.
 
 ```sh
 git submodule update --init --recursive
-poetry -C kevm-pyk run kevm-dist --verbose build evm-semantics.plugin
+poetry -C kevm-pyk run kdist --verbose build evm-semantics.plugin
 ```
 
 To change the default compiler:
 
 ```sh
-CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build evm-semantics.plugin
+CXX=clang++-14 poetry -C kevm-pyk run kdist --verbose build evm-semantics.plugin
 ```
 
 On Apple silicon:
 
 ```sh
-APPLE_SILICON=true poetry -C kevm-pyk run kevm-dist --verbose build evm-semantics.plugin
+APPLE_SILICON=true poetry -C kevm-pyk run kdist --verbose build evm-semantics.plugin
 ```
 
 #### K Definitions
 
 Finally, you can build the semantics.
 
 ```sh
-poetry -C kevm-pyk run kevm-dist --verbose build -j4
+poetry -C kevm-pyk run kdist --verbose build -j4
 ```
 
 You can build specific targets using options `evm-semantics.{llvm,haskell,haskell-standalone,plugin}`, e.g.:
 
 ```sh
-poetry -C kevm-pyk run kevm-dist build -j2 evm-semantics.llvm evm-semantics.haskell
+poetry -C kevm-pyk run kdist build -j2 evm-semantics.llvm evm-semantics.haskell
 ```
 
 Targets can be cleaned with
 
 ```sh
-poetry -C kevm-pyk run kevm-dist clean
+poetry -C kevm-pyk run kdist clean
 ```
 
-For more information, refer to `kevm-dist --help` and the [dist.py](kevm-pyk/src/kevm_pyk/dist.py) module.
+For more information, refer to `kdist --help` and the [dist.py](kevm-pyk/src/kevm_pyk/dist.py) module.
 
 Running Tests
 -------------
@@ -275,7 +275,7 @@ poetry -C kevm-pyk run kevm-pyk run tests/ethereum-tests/LegacyTests/Constantino
 To enable the debug symbols for the llvm backend, build using this command:
 
 ```sh
-poetry -C kevm-pyk run kevm-dist build evm-semantics.llvm --arg enable-llvm-debug=true
+poetry -C kevm-pyk run kdist build evm-semantics.llvm --arg enable-llvm-debug=true
 ```
 
 To debug a conformance test, add the `--debugger` flag to the command:
@@ -291,8 +291,8 @@ Always have your build up-to-date.
 - If using the kup package manager, run `kup install kevm --version .` to install the local version.
 - If building from source:
     -   `make poetry` needs to be re-run if you touch any of the `kevm-pyk` code.
-    -   `poetry -C kevm-pyk run kevm-dist build <target> --force` needs to be re-run if you touch any of this repos files.
-    -   `poetry -C kevm-pyk run kevm-dist clean` is a safe way to remove the target directory
+    -   `poetry -C kevm-pyk run kdist build <target> --force` needs to be re-run if you touch any of this repos files.
+    -   `poetry -C kevm-pyk run kdist clean` is a safe way to remove the target directory
 
 ### Building with Nix
 

diff --git a/deps/pyk_release b/deps/pyk_release
@@ -1 +1 @@
-v0.1.523
+v0.1.524
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -6,7 +6,7 @@
     nixpkgs.follows = "k-framework/nixpkgs";
     flake-utils.follows = "k-framework/flake-utils";
     rv-utils.follows = "k-framework/rv-utils";
-    pyk.url = "github:runtimeverification/pyk/v0.1.523";
+    pyk.url = "github:runtimeverification/pyk/v0.1.524";
     nixpkgs-pyk.follows = "pyk/nixpkgs";
     poetry2nix.follows = "pyk/poetry2nix";
     blockchain-k-plugin = {
@@ -100,7 +100,7 @@
                 prev.lib.optionalString
                 (prev.stdenv.isAarch64 && prev.stdenv.isDarwin)
                 "APPLE_SILICON=true"
-              } kevm-dist build -j4
+              } kdist build -j4
             '';
 
             installPhase = ''
@@ -112,7 +112,7 @@
                   prev.which
                   k-framework.packages.${prev.system}.k
                 ]
-              } --set NIX_LIBS "${nixLibs prev}" --set KEVM_DIST_DIR $out
+              } --set NIX_LIBS "${nixLibs prev}" --set KDIST_DIR $out
             '';
           };
 

diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock
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.379"
+version = "1.0.380"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",
@@ -13,9 +13,8 @@ authors = [
 [tool.poetry.dependencies]
 python = "^3.10"
 pathos = "*"
-pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.523" }
+pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.524" }
 tomlkit = "^0.11.6"
-xdg-base-dirs = "^6.0.0"
 
 [tool.poetry.group.dev.dependencies]
 autoflake = "*"
@@ -39,7 +38,6 @@ pyupgrade = "*"
 [tool.poetry.scripts]
 kevm = "kevm_pyk.__main__:main"
 kevm-pyk = "kevm_pyk.__main__:main"
-kevm-dist = "kevm_pyk.kdist.__main__:main"
 gst-to-kore = "kevm_pyk.gst_to_kore:main"
 
 [tool.poetry.plugins.kdist]

diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py
@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.379'
+VERSION: Final = '1.0.380'
diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
@@ -19,6 +19,7 @@
 from pyk.cterm import CTerm
 from pyk.kast.outer import KApply, KRewrite, KSort, KToken
 from pyk.kcfg import KCFG
+from pyk.kdist import kdist
 from pyk.kore.tools import PrintOutput, kore_print
 from pyk.ktool.kompile import LLVMKompileType
 from pyk.ktool.krun import KRunOutput
@@ -31,7 +32,6 @@
 
 from . import VERSION, config
 from .cli import KEVMCLIArgs, node_id_like
-from .config import kdist
 from .gst_to_kore import SORT_ETHEREUM_SIMULATION, gst_to_kore, kore_pgm_to_kore
 from .kevm import KEVM, KEVMSemantics, kevm_node_printer
 from .kompile import KompileTarget, kevm_kompile

diff --git a/kevm-pyk/src/kevm_pyk/config.py b/kevm-pyk/src/kevm_pyk/config.py
@@ -6,8 +6,6 @@
 
 import kevm_pyk
 
-from .kdist import KDist
-
 if TYPE_CHECKING:
     from typing import Final
 
@@ -22,6 +20,3 @@
 
 
 NIX_LIBS: Final = os.getenv('NIX_LIBS')
-
-KEVM_DIST_DIR: Final = os.getenv('KEVM_DIST_DIR')  # Used by Nix flake to set the output
-kdist: Final = KDist(KEVM_DIST_DIR)
diff --git a/kevm-pyk/src/kevm_pyk/interpreter.py b/kevm-pyk/src/kevm_pyk/interpreter.py
@@ -2,10 +2,10 @@
 
 from typing import TYPE_CHECKING
 
+from pyk.kdist import kdist
 from pyk.kore.parser import KoreParser
 from pyk.utils import run_process
 
-from .config import kdist
 from .gst_to_kore import gst_to_kore
 
 if TYPE_CHECKING:

diff --git a/kevm-pyk/src/kevm_pyk/kdist/__init__.py b/kevm-pyk/src/kevm_pyk/kdist/__init__.py
@@ -1,2 +0,0 @@
-from ._cache import target_ids
-from ._kdist import KDist

diff --git a/kevm-pyk/src/kevm_pyk/kdist/__main__.py b/kevm-pyk/src/kevm_pyk/kdist/__main__.py