Merge branch 'master' into _update-deps/runtimeverification/evm-seman…

…tics
runtimeverification · Oct 27, 2023 · d5d73b4 · d5d73b4
2 parents 2d24c1b + 51a85d6
commit d5d73b4
Show file tree

Hide file tree

Showing 23 changed files with 1,698 additions and 42 deletions.
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -81,7 +81,7 @@ jobs:
       - name: 'Build KEVM'
         run: |
             docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} /bin/bash -c 'poetry install'
-            docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kevm-dist --verbose build -j`nproc` plugin foundry'
+            docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kevm-dist --verbose build -j`nproc` plugin foundryx'
       - name: 'Run profiling'
         run: |
           PROF_ARGS=--numprocesses=8
@@ -113,7 +113,7 @@ jobs:
       - name: 'Build KEVM'
         run: |
             docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'poetry install'
-            docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kevm-dist --verbose build -j`nproc` plugin haskell foundry'
+            docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kevm-dist --verbose build -j`nproc` plugin haskell foundryx'
       - name: 'Run integration tests'
         run: |
           TEST_ARGS=--numprocesses=8

diff --git a/flake.nix b/flake.nix
@@ -27,7 +27,7 @@
         "-I${procps}/include -L${procps}/lib -I${openssl.dev}/include -L${openssl.out}/lib";
       overlay = final: prev:
         let
-          kontrol = { solc_version ? null }:
+          kontrol-pyk = { solc_version ? null }:
             (prev.poetry2nix.mkPoetryApplication {
               python = prev.python310;
               projectDir = ./.;
@@ -54,26 +54,70 @@
               groups = [ ];
               # We remove `"dev"` from `checkGroups`, so that poetry2nix does not try to resolve dev dependencies.
               checkGroups = [ ];
+            });
+
+          kontrol = { solc_version ? null }:
+            prev.stdenv.mkDerivation {
+              pname = "kontrol";
+              version = self.rev or "dirty";
+              buildInputs = with prev; [
+                autoconf
+                automake
+                cmake
+                (kevm-pyk.overridePythonAttrs (old: {
+                  propagatedBuildInputs = (old.propagatedBuildInputs or [ ])
+                    ++ [ (kontrol-pyk { inherit solc_version; }) ];
+                }))
+                k-framework.packages.${prev.system}.k
+                libtool
+                openssl.dev
+                gmp
+              ];
+              nativeBuildInputs = [ prev.makeWrapper ];
+
+              src = ./.;
 
-              postInstall = ''
-                wrapProgram $out/bin/kontrol --prefix PATH : ${
-                  prev.lib.makeBinPath
-                  ([ prev.which k-framework.packages.${prev.system}.k ]
-                    ++ prev.lib.optionals (solc_version != null) [
-                      final.foundry-bin
-                      (solc.mkDefault final solc_version)
-                    ])
-                } --set NIX_LIBS "${nixLibs prev}" --set KEVM_DIST_DIR ${
-                  prev.kevm k-framework.packages.${prev.system}.k
-                }
+              dontUseCmakeConfigure = true;
+
+              enableParallelBuilding = true;
+
+              buildPhase = ''
+                XDG_CACHE_HOME=$(pwd) NIX_LIBS="${nixLibs prev}" ${
+                  prev.lib.optionalString
+                  (prev.stdenv.isAarch64 && prev.stdenv.isDarwin)
+                  "APPLE_SILICON=true"
+                } kevm-dist build -j4 foundryx
               '';
-            }).overrideAttrs (old: {
-              passthru = old.passthru // (if solc_version == null then {
+
+              installPhase =
+                let kevm = prev.kevm k-framework.packages.${prev.system}.k;
+                in ''
+                  mkdir -p $out
+                  cp -r ./kdist-*/* $out/
+                  ln -s ${kevm}/foundry $out/foundry
+                  ln -s ${kevm}/haskell $out/haskell
+                  ln -s ${kevm}/haskell-standalone $out/haskell-standalone
+                  ln -s ${kevm}/llvm $out/llvm
+                  ln -s ${kevm}/plugin $out/plugin
+                  mkdir -p $out/bin
+                  makeWrapper ${
+                    (kontrol-pyk { inherit solc_version; })
+                  }/bin/kontrol $out/bin/kontrol --prefix PATH : ${
+                    prev.lib.makeBinPath
+                    ([ prev.which k-framework.packages.${prev.system}.k ]
+                      ++ prev.lib.optionals (solc_version != null) [
+                        final.foundry-bin
+                        (solc.mkDefault final solc_version)
+                      ])
+                  } --set NIX_LIBS "${nixLibs prev}" --set KEVM_DIST_DIR $out
+                '';
+
+              passthru = if solc_version == null then {
                 # list all supported solc versions here
                 solc_0_8_13 = kontrol { solc_version = final.solc_0_8_13; };
               } else
-                { });
-            });
+                { };
+            };
         in { inherit kontrol; };
     in flake-utils.lib.eachSystem [
       "x86_64-linux"
@@ -96,9 +140,9 @@
           ];
         };
       in {
-        packages = rec {
+        packages = {
           kontrol = pkgs.kontrol { };
-          default = self.kontrol;
+          default = pkgs.kontrol { };
         };
       }) // {
         overlays.default = overlay;

diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.38
+0.1.40
diff --git a/pyproject.toml b/pyproject.toml
@@ -4,15 +4,12 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.38"
+version = "0.1.40"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
 ]
 
-[tool.poetry.scripts]
-kontrol = "kontrol.__main__:main"
-
 [tool.poetry.dependencies]
 python = "^3.10"
 kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.328", subdirectory = "kevm-pyk" }
@@ -34,6 +31,12 @@ pytest-mock = "*"
 pytest-xdist = "*"
 pyupgrade = "*"
 
+[tool.poetry.scripts]
+kontrol = "kontrol.__main__:main"
+
+[tool.poetry.plugins.kdist]
+kontrol = "kontrol.kdist.plugin"
+
 [tool.isort]
 profile = "black"
 line_length = 120

diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.38'
+VERSION: Final = '0.1.40'
diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
@@ -353,7 +353,7 @@ def help_info() -> list[str]:
             )
         res_lines.append('')
         res_lines.append(
-            'Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kevm-integration-for-foundry/'
+            'Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kontrol'
         )
         return res_lines
 

diff --git a/src/kontrol/kdist/__init__.py b/src/kontrol/kdist/__init__.py