diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile index cc1c14adef..ecc050bbe3 100644 --- a/.github/workflows/Dockerfile +++ b/.github/workflows/Dockerfile @@ -22,7 +22,6 @@ RUN apt-get update \ debhelper \ libboost-test-dev \ libcrypto++-dev \ - libprocps-dev \ libsecp256k1-dev \ libssl-dev \ libyaml-dev \ diff --git a/.github/workflows/update-version.yml b/.github/workflows/update-version.yml index e94383dd1b..45a90573b8 100644 --- a/.github/workflows/update-version.yml +++ b/.github/workflows/update-version.yml @@ -53,7 +53,7 @@ jobs: K_VERSION=v$(cat deps/k_release) BKP_VERSION=$(cat deps/blockchain-k-plugin_release) sed -i 's! k-framework.url = "github:runtimeverification/k/[v0-9\.]*"! k-framework.url = "github:runtimeverification/k/'"${K_VERSION}"'"!' flake.nix - sed -i 's! blockchain-k-plugin.url = "github:runtimeverification/blockchain-k-plugin/[0-9a-f]*"! blockchain-k-plugin.url = "github:runtimeverification/blockchain-k-plugin/'"${BKP_VERSION}"'"!' flake.nix + sed -i 's! "github:runtimeverification/blockchain-k-plugin/[0-9a-f]*"! "github:runtimeverification/blockchain-k-plugin/'"${BKP_VERSION}"'"!' flake.nix sed -i 's! pyk.url = "github:runtimeverification/k/[v0-9\.]*?dir=pyk"! pyk.url = "github:runtimeverification/k/'"${K_VERSION}"'?dir=pyk"!' flake.nix nix run .#update-from-submodules nix flake update diff --git a/README.md b/README.md index 0ab42a6360..2079436894 100644 --- a/README.md +++ b/README.md @@ -111,13 +111,13 @@ 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 -kup install k.openssl.procps --version v$(cat deps/k_release) +kup install k.openssl --version v$(cat deps/k_release) ``` You can also drop into a single development shell with the correct version of K on path by doing: ```sh -kup shell k.openssl.procps --version v$(cat deps/k_release) +kup shell k.openssl --version v$(cat deps/k_release) ``` ### Building diff --git a/flake.lock b/flake.lock index e39a33e2df..961cadb2bd 100644 --- a/flake.lock +++ b/flake.lock @@ -26,25 +26,36 @@ "k-framework", "flake-utils" ], + "k-framework": "k-framework", "libff": "libff", "nixpkgs": [ "k-framework", "nixpkgs" ], + "poetry2nix": [ + "blockchain-k-plugin", + "k-framework", + "poetry2nix" + ], + "rv-utils": [ + "blockchain-k-plugin", + "k-framework", + "rv-utils" + ], "xbyak": "xbyak" }, "locked": { - "lastModified": 1711321833, - "narHash": "sha256-p0HqLxjrYYYHx2BMODp0N/O2KQf0TAGenMFYmToLPrE=", + "lastModified": 1723480020, + "narHash": "sha256-OoJMpEw1zz37lo8CjD4rs2oN3OSUQqcKlTUIQdJSeLA=", "owner": "runtimeverification", "repo": "blockchain-k-plugin", - "rev": "5aa6993fab90675d971b8b98b3430d11f1ec2a2b", + "rev": "64bb64b6c908c15b3dfe67ace70936b7d3913672", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "blockchain-k-plugin", - "rev": "5aa6993fab90675d971b8b98b3430d11f1ec2a2b", + "rev": "64bb64b6c908c15b3dfe67ace70936b7d3913672", "type": "github" } }, @@ -98,6 +109,22 @@ "type": "github" } }, + "flake-compat_2": { + "flake": false, + "locked": { + "lastModified": 1696426674, + "narHash": "sha256-kvjfFW7WAETZlt09AgDn1MrtKzP7t90Vf7vypd3OL1U=", + "owner": "edolstra", + "repo": "flake-compat", + "rev": "0f9255e01c2351cc7d116c072cb317785dd33b33", + "type": "github" + }, + "original": { + "owner": "edolstra", + "repo": "flake-compat", + "type": "github" + } + }, "flake-utils": { "inputs": { "systems": "systems_2" @@ -118,7 +145,25 @@ }, "flake-utils_2": { "inputs": { - "systems": "systems_4" + "systems": "systems_5" + }, + "locked": { + "lastModified": 1694529238, + "narHash": "sha256-zsNZZGTGnMOf9YpHKJqMSsa0dXbfmxeoJ7xHlrt+xmY=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "ff7b65b44d01cf9ba6a71320833626af21126384", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "flake-utils_3": { + "inputs": { + "systems": "systems_7" }, "locked": { "lastModified": 1694529238, @@ -151,14 +196,33 @@ "type": "github" } }, + "fmt-src_2": { + "flake": false, + "locked": { + "lastModified": 1661615830, + "narHash": "sha256-rP6ymyRc7LnKxUXwPpzhHOQvpJkpnRFOt2ctvUNlYI0=", + "owner": "fmtlib", + "repo": "fmt", + "rev": "a33701196adfad74917046096bf5a2aa0ab0bb50", + "type": "github" + }, + "original": { + "owner": "fmtlib", + "ref": "9.1.0", + "repo": "fmt", + "type": "github" + } + }, "haskell-backend": { "inputs": { "nixpkgs": [ + "blockchain-k-plugin", "k-framework", "llvm-backend", "nixpkgs" ], "rv-utils": [ + "blockchain-k-plugin", "k-framework", "llvm-backend", "rv-utils" @@ -166,6 +230,36 @@ "stacklock2nix": "stacklock2nix", "z3": "z3" }, + "locked": { + "lastModified": 1722860063, + "narHash": "sha256-5K3BIIbwkMpN4idvAHRrw0JzHRL6Au4ui+7NqkX+c3w=", + "owner": "runtimeverification", + "repo": "haskell-backend", + "rev": "7047b0964349727e54425c2c81478caf3dad757c", + "type": "github" + }, + "original": { + "owner": "runtimeverification", + "ref": "v0.1.58", + "repo": "haskell-backend", + "type": "github" + } + }, + "haskell-backend_2": { + "inputs": { + "nixpkgs": [ + "k-framework", + "llvm-backend", + "nixpkgs" + ], + "rv-utils": [ + "k-framework", + "llvm-backend", + "rv-utils" + ], + "stacklock2nix": "stacklock2nix_2", + "z3": "z3_2" + }, "locked": { "lastModified": 1723630441, "narHash": "sha256-BbJwGKi2kwbSIegUZTuZvzOoA9g/NRn7mwsgOhKpFvg=", @@ -198,9 +292,27 @@ "type": "github" } }, + "immer-src_2": { + "flake": false, + "locked": { + "lastModified": 1708038459, + "narHash": "sha256-aV/mQFuPzioy1PxROc85ypeP7/d0nn+xcBPzy9taw2s=", + "owner": "runtimeverification", + "repo": "immer", + "rev": "4b0914f0b2acb33befe0ba4cd3a7954f2687e9bb", + "type": "github" + }, + "original": { + "owner": "runtimeverification", + "repo": "immer", + "rev": "4b0914f0b2acb33befe0ba4cd3a7954f2687e9bb", + "type": "github" + } + }, "k-framework": { "inputs": { "flake-utils": [ + "blockchain-k-plugin", "k-framework", "llvm-backend", "utils" @@ -208,11 +320,49 @@ "haskell-backend": "haskell-backend", "llvm-backend": "llvm-backend", "nixpkgs": [ + "blockchain-k-plugin", "k-framework", "llvm-backend", "nixpkgs" ], "poetry2nix": "poetry2nix", + "rv-utils": [ + "blockchain-k-plugin", + "k-framework", + "llvm-backend", + "rv-utils" + ] + }, + "locked": { + "lastModified": 1723222636, + "narHash": "sha256-V4rRuc7QN7rbtFS6d76kM0AZJJJp8vsXqXYz5nQebIk=", + "owner": "runtimeverification", + "repo": "k", + "rev": "0643095937a08f26e94d58cd8c2651ab1b0b4a07", + "type": "github" + }, + "original": { + "owner": "runtimeverification", + "ref": "v7.1.103", + "repo": "k", + "type": "github" + } + }, + "k-framework_2": { + "inputs": { + "flake-utils": [ + "k-framework", + "llvm-backend", + "utils" + ], + "haskell-backend": "haskell-backend_2", + "llvm-backend": "llvm-backend_2", + "nixpkgs": [ + "k-framework", + "llvm-backend", + "nixpkgs" + ], + "poetry2nix": "poetry2nix_2", "rv-utils": [ "k-framework", "llvm-backend", @@ -257,6 +407,7 @@ "fmt-src": "fmt-src", "immer-src": "immer-src", "nixpkgs": [ + "blockchain-k-plugin", "k-framework", "llvm-backend", "rv-utils", @@ -282,9 +433,41 @@ "type": "github" } }, + "llvm-backend_2": { + "inputs": { + "flake-compat": "flake-compat_2", + "fmt-src": "fmt-src_2", + "immer-src": "immer-src_2", + "nixpkgs": [ + "k-framework", + "llvm-backend", + "rv-utils", + "nixpkgs" + ], + "pybind11-src": "pybind11-src_2", + "rapidjson-src": "rapidjson-src_2", + "rv-utils": "rv-utils_2", + "utils": "utils_2" + }, + "locked": { + "lastModified": 1723094785, + "narHash": "sha256-JPe1rZkx4/q7wyEGIOitt3slEHpue5gSnT9x9tbnNMs=", + "owner": "runtimeverification", + "repo": "llvm-backend", + "rev": "e7266f7e0082b5a90ccf47ceed47ba1811bdc636", + "type": "github" + }, + "original": { + "owner": "runtimeverification", + "ref": "v0.1.77", + "repo": "llvm-backend", + "type": "github" + } + }, "nix-github-actions": { "inputs": { "nixpkgs": [ + "blockchain-k-plugin", "k-framework", "poetry2nix", "nixpkgs" @@ -305,6 +488,28 @@ } }, "nix-github-actions_2": { + "inputs": { + "nixpkgs": [ + "k-framework", + "poetry2nix", + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1693660503, + "narHash": "sha256-B/g2V4v6gjirFmy+I5mwB2bCYc0l3j5scVfwgl6WOl8=", + "owner": "nix-community", + "repo": "nix-github-actions", + "rev": "bd5bdbb52350e145c526108f4ef192eb8e554fa0", + "type": "github" + }, + "original": { + "owner": "nix-community", + "repo": "nix-github-actions", + "type": "github" + } + }, + "nix-github-actions_3": { "inputs": { "nixpkgs": [ "pyk", @@ -358,11 +563,28 @@ "type": "github" } }, + "nixpkgs_3": { + "locked": { + "lastModified": 1716457947, + "narHash": "sha256-Y+exebcqeprnhEpoPJrEUZmNeO60qeOxkVHhqG/OEwQ=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "69493a13eaea0dc4682fd07e8a084f17813dbeeb", + "type": "github" + }, + "original": { + "owner": "nixos", + "repo": "nixpkgs", + "rev": "69493a13eaea0dc4682fd07e8a084f17813dbeeb", + "type": "github" + } + }, "poetry2nix": { "inputs": { "flake-utils": "flake-utils", "nix-github-actions": "nix-github-actions", "nixpkgs": [ + "blockchain-k-plugin", "k-framework", "llvm-backend", "nixpkgs" @@ -390,10 +612,11 @@ "flake-utils": "flake-utils_2", "nix-github-actions": "nix-github-actions_2", "nixpkgs": [ - "pyk", + "k-framework", + "llvm-backend", "nixpkgs" ], - "systems": "systems_5", + "systems": "systems_6", "treefmt-nix": "treefmt-nix_2" }, "locked": { @@ -411,6 +634,32 @@ "type": "github" } }, + "poetry2nix_3": { + "inputs": { + "flake-utils": "flake-utils_3", + "nix-github-actions": "nix-github-actions_3", + "nixpkgs": [ + "pyk", + "nixpkgs" + ], + "systems": "systems_8", + "treefmt-nix": "treefmt-nix_3" + }, + "locked": { + "lastModified": 1698640399, + "narHash": "sha256-mXzyx79/iFLZ0UDuSkqgFfejYRcSJfsCnJ9WlMusaI0=", + "owner": "nix-community", + "repo": "poetry2nix", + "rev": "626111646fe236cb1ddc8191a48c75e072a82b7c", + "type": "github" + }, + "original": { + "owner": "nix-community", + "repo": "poetry2nix", + "rev": "626111646fe236cb1ddc8191a48c75e072a82b7c", + "type": "github" + } + }, "pybind11-src": { "flake": false, "locked": { @@ -428,6 +677,23 @@ "type": "github" } }, + "pybind11-src_2": { + "flake": false, + "locked": { + "lastModified": 1657936673, + "narHash": "sha256-/X8DZPFsNrKGbhjZ1GFOj17/NU6p4R+saCW3pLKVNeA=", + "owner": "pybind", + "repo": "pybind11", + "rev": "0ba639d6177659c5dc2955ac06ad7b5b0d22e05c", + "type": "github" + }, + "original": { + "owner": "pybind", + "repo": "pybind11", + "rev": "0ba639d6177659c5dc2955ac06ad7b5b0d22e05c", + "type": "github" + } + }, "pyk": { "inputs": { "flake-utils": [ @@ -440,8 +706,8 @@ "rv-utils", "nixpkgs" ], - "poetry2nix": "poetry2nix_2", - "rv-utils": "rv-utils_2" + "poetry2nix": "poetry2nix_3", + "rv-utils": "rv-utils_3" }, "locked": { "dir": "pyk", @@ -477,6 +743,23 @@ "type": "github" } }, + "rapidjson-src_2": { + "flake": false, + "locked": { + "lastModified": 1472111945, + "narHash": "sha256-SxUXSOQDZ0/3zlFI4R84J56/1fkw2jhge4mexNF6Pco=", + "owner": "Tencent", + "repo": "rapidjson", + "rev": "f54b0e47a08782a6131cc3d60f94d038fa6e0a51", + "type": "github" + }, + "original": { + "owner": "Tencent", + "repo": "rapidjson", + "rev": "f54b0e47a08782a6131cc3d60f94d038fa6e0a51", + "type": "github" + } + }, "root": { "inputs": { "blockchain-k-plugin": "blockchain-k-plugin", @@ -488,7 +771,7 @@ "k-framework", "haskell-backend" ], - "k-framework": "k-framework", + "k-framework": "k-framework_2", "nixpkgs": [ "k-framework", "nixpkgs" @@ -544,6 +827,24 @@ "type": "github" } }, + "rv-utils_3": { + "inputs": { + "nixpkgs": "nixpkgs_3" + }, + "locked": { + "lastModified": 1716459074, + "narHash": "sha256-IpahO+EkWdGl9QP7B2YXfJWpSfghjxgpz4ab47nRJY4=", + "owner": "runtimeverification", + "repo": "rv-nix-tools", + "rev": "a65058865cda201de504f5546271b8e997a0be9c", + "type": "github" + }, + "original": { + "owner": "runtimeverification", + "repo": "rv-nix-tools", + "type": "github" + } + }, "stacklock2nix": { "locked": { "lastModified": 1705051190, @@ -559,6 +860,21 @@ "type": "github" } }, + "stacklock2nix_2": { + "locked": { + "lastModified": 1705051190, + "narHash": "sha256-xgH0gaD3dNtOzZzX3A40hZTiHJP5cIGmifbmfcS2OGI=", + "owner": "cdepillabout", + "repo": "stacklock2nix", + "rev": "22676dfc45fa1c33899ba1da1a23665172a18ba7", + "type": "github" + }, + "original": { + "owner": "cdepillabout", + "repo": "stacklock2nix", + "type": "github" + } + }, "systems": { "locked": { "lastModified": 1681028828, @@ -619,6 +935,50 @@ } }, "systems_5": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + }, + "systems_6": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "id": "systems", + "type": "indirect" + } + }, + "systems_7": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + }, + "systems_8": { "locked": { "lastModified": 1681028828, "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", @@ -635,6 +995,7 @@ "treefmt-nix": { "inputs": { "nixpkgs": [ + "blockchain-k-plugin", "k-framework", "poetry2nix", "nixpkgs" @@ -655,6 +1016,28 @@ } }, "treefmt-nix_2": { + "inputs": { + "nixpkgs": [ + "k-framework", + "poetry2nix", + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1697388351, + "narHash": "sha256-63N2eBpKaziIy4R44vjpUu8Nz5fCJY7okKrkixvDQmY=", + "owner": "numtide", + "repo": "treefmt-nix", + "rev": "aae39f64f5ecbe89792d05eacea5cb241891292a", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "treefmt-nix", + "type": "github" + } + }, + "treefmt-nix_3": { "inputs": { "nixpkgs": [ "pyk", @@ -694,6 +1077,24 @@ "type": "github" } }, + "utils_2": { + "inputs": { + "systems": "systems_4" + }, + "locked": { + "lastModified": 1705309234, + "narHash": "sha256-uNRRNRKmJyCRC/8y1RqBkqWBLM034y4qN7EprSdmgyA=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "1ef2e671c3b0c19053962c07dbda38332dcebf26", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, "xbyak": { "flake": false, "locked": { @@ -712,6 +1113,23 @@ } }, "z3": { + "flake": false, + "locked": { + "lastModified": 1674011426, + "narHash": "sha256-7cuUf29TMpX62PwO1ab3ZuzmzlcrRjTKB1CyXnYgYus=", + "owner": "Z3Prover", + "repo": "z3", + "rev": "3012293c35eadbfd73e5b94adbe50b0cc44ffb83", + "type": "github" + }, + "original": { + "owner": "Z3Prover", + "ref": "z3-4.12.1", + "repo": "z3", + "type": "github" + } + }, + "z3_2": { "flake": false, "locked": { "lastModified": 1709835916, diff --git a/flake.nix b/flake.nix index 4418616802..0e5518326e 100644 --- a/flake.nix +++ b/flake.nix @@ -11,7 +11,7 @@ poetry2nix.follows = "pyk/poetry2nix"; blockchain-k-plugin = { url = - "github:runtimeverification/blockchain-k-plugin/5aa6993fab90675d971b8b98b3430d11f1ec2a2b"; + "github:runtimeverification/blockchain-k-plugin/64bb64b6c908c15b3dfe67ace70936b7d3913672"; inputs.flake-utils.follows = "k-framework/flake-utils"; inputs.nixpkgs.follows = "k-framework/nixpkgs"; }; @@ -22,7 +22,7 @@ let nixLibs = pkgs: with pkgs; - "-I${procps}/include -L${procps}/lib -I${openssl.dev}/include -L${openssl.out}/lib -I${secp256k1}/include -L${secp256k1}/lib"; + "-I${openssl.dev}/include -L${openssl.out}/lib -I${secp256k1}/include -L${secp256k1}/lib"; buildInputs = pkgs: with pkgs; [ @@ -38,9 +38,9 @@ mpfr openssl.dev pkg-config - procps python310-pyk time + secp256k1 ] ++ lib.optional (!stdenv.isDarwin) elfutils; overlay = final: prev: @@ -90,7 +90,7 @@ prev.lib.optionalString (prev.stdenv.isAarch64 && prev.stdenv.isDarwin) "APPLE_SILICON=true" - } kdist build -j4 + } kdist -v build -j4 ''; installPhase = '' diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index 2284c2062f..9880a67101 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -841,17 +841,17 @@ test = ["enum34", "ipaddress", "mock", "pywin32", "wmi"] [[package]] name = "pybind11" -version = "2.13.3" +version = "2.13.4" description = "Seamless operability between C++11 and Python" optional = false python-versions = ">=3.7" files = [ - {file = "pybind11-2.13.3-py3-none-any.whl", hash = "sha256:23f2e842ae2f37babec486d372f2545198a506df785a5fefccf6f0ad3f72a5fb"}, - {file = "pybind11-2.13.3.tar.gz", hash = "sha256:84b1314ca72397f79854161cf852466629dd374bb0efce0c6501d745699d9a43"}, + {file = "pybind11-2.13.4-py3-none-any.whl", hash = "sha256:5932d63d570b3a12ece2f6678adb3846cc1c229dc1f8518a46d5b540f240f959"}, + {file = "pybind11-2.13.4.tar.gz", hash = "sha256:75a9e1f967d3cd3fd59f981eb39406f9de05e33a4dd8f5f18b8e29cae023e1d5"}, ] [package.extras] -global = ["pybind11-global (==2.13.3)"] +global = ["pybind11-global (==2.13.4)"] [[package]] name = "pycodestyle" diff --git a/kevm-pyk/src/kevm_pyk/kdist/plugin.py b/kevm-pyk/src/kevm_pyk/kdist/plugin.py index 5f246eac43..c16d80bd05 100644 --- a/kevm-pyk/src/kevm_pyk/kdist/plugin.py +++ b/kevm-pyk/src/kevm_pyk/kdist/plugin.py @@ -1,10 +1,11 @@ from __future__ import annotations +import shutil import sys from distutils.dir_util import copy_tree from typing import TYPE_CHECKING -from pyk.kbuild.utils import k_version, sync_files +from pyk.kbuild.utils import k_version from pyk.kdist.api import Target from pyk.kllvm.compiler import compile_kllvm, compile_runtime from pyk.utils import run_process_2 @@ -51,23 +52,9 @@ def context(self) -> dict[str, str]: class PluginTarget(Target): def build(self, output_dir: Path, deps: dict[str, Any], args: dict[str, Any], verbose: bool) -> None: - sync_files( - source_dir=config.PLUGIN_DIR / 'plugin-c', - target_dir=output_dir / 'plugin-c', - file_names=[ - 'blake2.h', - 'crypto.cpp', - 'plugin_util.cpp', - 'plugin_util.h', - ], - ) - copy_tree(str(config.PLUGIN_DIR), '.') - run_process_2(['make', 'libcryptopp', 'libff', 'blake2', '-j8']) - - copy_tree('./build/libcryptopp', str(output_dir / 'libcryptopp')) - copy_tree('./build/libff', str(output_dir / 'libff')) - copy_tree('./build/blake2', str(output_dir / 'blake2')) + run_process_2(['make', '-j8']) + shutil.copy('./build/krypto/lib/krypto.a', str(output_dir)) def source(self) -> tuple[Path]: return (config.PLUGIN_DIR,) diff --git a/kevm-pyk/src/kevm_pyk/kompile.py b/kevm-pyk/src/kevm_pyk/kompile.py index 9c94686c4b..c2ef5ac42a 100644 --- a/kevm-pyk/src/kevm_pyk/kompile.py +++ b/kevm-pyk/src/kevm_pyk/kompile.py @@ -9,7 +9,6 @@ from pyk.kdist import kdist from pyk.ktool import TypeInferenceMode from pyk.ktool.kompile import HaskellKompile, KompileArgs, LLVMKompile, LLVMKompileType, MaudeKompile -from pyk.utils import run_process_2 from . import config @@ -225,8 +224,6 @@ def _kompile_haskell() -> None: def lib_ccopts(plugin_dir: Path, debug_build: bool = False) -> list[str]: - kernel = sys.platform - ccopts = ['-std=c++17'] if debug_build: @@ -234,42 +231,10 @@ def lib_ccopts(plugin_dir: Path, debug_build: bool = False) -> list[str]: ccopts += ['-lssl', '-lcrypto', '-lsecp256k1'] - libff_dir = plugin_dir / 'libff' - ccopts += [f'{libff_dir}/lib/libff.a', f'-I{libff_dir}/include'] - - libcryptopp_dir = plugin_dir / 'libcryptopp' - ccopts += [f'{libcryptopp_dir}/lib/libcryptopp.a', f'-I{libcryptopp_dir}/include'] - - blake2_dir = plugin_dir / 'blake2' - ccopts += [f'{blake2_dir}/lib/blake2.a'] - - plugin_include = plugin_dir / 'plugin-c' - ccopts += [ - f'{plugin_include}/plugin_util.cpp', - f'{plugin_include}/crypto.cpp', - ] - - if kernel == 'darwin': - if not config.NIX_LIBS: - brew_root = run_process_2(('brew', '--prefix'), logger=_LOGGER).stdout.strip() - ccopts += [ - f'-I{brew_root}/include', - f'-L{brew_root}/lib', - ] - - openssl_root = run_process_2(('brew', '--prefix', 'openssl'), logger=_LOGGER).stdout.strip() - ccopts += [ - f'-I{openssl_root}/include', - f'-L{openssl_root}/lib', - ] - else: - ccopts += config.NIX_LIBS.split(' ') - elif kernel == 'linux': - ccopts += ['-lprocps'] - if config.NIX_LIBS: - ccopts += config.NIX_LIBS.split(' ') - else: - raise AssertionError() + ccopts += [str(plugin_dir / 'krypto.a')] + + if config.NIX_LIBS: + ccopts += config.NIX_LIBS.split(' ') return ccopts