Add target mx-semantics.plugin (#243)

* Move the `plugin` submodule into the Python package * Copy `krypto.md` into `mx-semantics.source` * Add target `PluginTarget` * Set Version: 0.1.42 * Set Version: 0.1.43 --------- Co-authored-by: devops <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · Apr 26, 2024 · e05964e · e05964e
1 parent b2045bf
commit e05964e
Show file tree

Hide file tree

Showing 8 changed files with 62 additions and 42 deletions.
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -63,8 +63,6 @@ jobs:
           container-name: elrond-semantics-ci-${{ github.sha }}
       - name: 'Build kmultiversx'
         run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} make kmultiversx
-      - name: 'Build plugin submodule'
-        run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} make plugin-deps
       - name: 'Build K definitions'
         run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} make build-all
       - name: 'KMultiversX Tests'
@@ -103,8 +101,6 @@ jobs:
           container-name: elrond-semantics-ci-${{ github.sha }}
       - name: 'Build kmultiversx'
         run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} make kmultiversx
-      - name: 'Build plugin submodule'
-        run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} make plugin-deps
       - name: 'Build K definition'
         run: docker exec -t elrond-semantics-ci-${GITHUB_SHA} make build
       - name: 'Feature Test: Basic'

diff --git a/.gitmodules b/.gitmodules
@@ -1,5 +1,5 @@
 [submodule "deps/plugin"]
-	path = deps/plugin
+	path = kmultiversx/src/kmultiversx/kdist/plugin
 	url = https://github.com/runtimeverification/blockchain-k-plugin.git
 [submodule "deps/mx-sdk-rs"]
 	path = deps/mx-sdk-rs

diff --git a/Makefile b/Makefile
@@ -9,11 +9,7 @@
 # Settings
 # --------
 
-DEPS_DIR  := deps
-
-PLUGIN_SUBMODULE := $(abspath $(DEPS_DIR)/plugin)
-
-ELROND_SDK_SUBMODULE     := $(DEPS_DIR)/mx-sdk-rs
+ELROND_SDK_SUBMODULE     := deps/mx-sdk-rs
 ELROND_CONTRACT          := $(ELROND_SDK_SUBMODULE)/contracts
 ELROND_CONTRACT_EXAMPLES := $(ELROND_CONTRACT)/examples
 
@@ -28,11 +24,6 @@ K_OPTS     := -Xmx8G -Xss512m
 POETRY     := poetry -C kmultiversx
 POETRY_RUN := $(POETRY) run
 
-
-.PHONY: plugin-deps
-plugin-deps:
-	$(MAKE) -C $(PLUGIN_SUBMODULE) blake2 libcryptopp libff -j8
-
 .PHONY: kmultiversx
 kmultiversx:
 	$(POETRY) install --no-ansi
@@ -41,26 +32,24 @@ kmultiversx:
 build: build-mandos
 
 .PHONY: build-mandos
-build-mandos: kmultiversx plugin-deps
+build-mandos: kmultiversx
 	K_OPTS='$(K_OPTS)' $(POETRY) run kdist -v build mx-semantics.llvm-mandos
 
 .PHONY: build-kasmer
-build-kasmer: kmultiversx plugin-deps
+build-kasmer: kmultiversx
 	K_OPTS='$(K_OPTS)' $(POETRY) run kdist -v build mx-semantics.llvm-kasmer
 
 .PHONY: build-haskell
 build-haskell: kmultiversx
 	$(POETRY) run kdist -v build mx-semantics.haskell-\* -j2
 
 .PHONY: build-all
-build-all: kmultiversx plugin-deps
+build-all: kmultiversx
 	K_OPTS='$(K_OPTS)' $(POETRY) run kdist -v build mx-semantics.\* -j4
 
 .PHONY: clean
 clean: kmultiversx
 	$(POETRY) run kdist clean
-	$(MAKE) -C $(PLUGIN_SUBMODULE) clean
-
 
 
 # Testing

diff --git a/kmultiversx/.flake8 b/kmultiversx/.flake8
@@ -5,3 +5,5 @@ extend-ignore = B950,E,W1,W2,W3,W4,W5
 per-file-ignores =
     */__init__.py: F401
 type-checking-strict = true
+exclude =
+    src/kmultiversx/kdist/plugin
diff --git a/kmultiversx/pyproject.toml b/kmultiversx/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmultiversx"
-version = "0.1.42"
+version = "0.1.43"
 description = "Python tools for Elrond semantics"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",
@@ -44,6 +44,7 @@ pyupgrade = "*"
 [tool.isort]
 profile = "black"
 line_length = 120
+skip = [ "src/kmultiversx/kdist/plugin" ]
 
 [tool.autoflake]
 recursive = true
@@ -52,10 +53,13 @@ remove-all-unused-imports = true
 ignore-init-module-imports = true
 remove-duplicate-keys = true
 remove-unused-variables = true
+exclude = [ "src/kmultiversx/kdist/plugin" ]
 
 [tool.black]
 line-length = 120
 skip-string-normalization = true
+exclude = "src/kmultiversx/kdist/plugin"
 
 [tool.mypy]
 disallow_untyped_defs = true
+exclude = "src/kmultiversx/kdist/plugin/*"
diff --git a/deps/plugin → kmultiversx/src/kmultiversx/kdist/plugin b/deps/plugin → kmultiversx/src/kmultiversx/kdist/plugin
diff --git a/kmultiversx/src/kmultiversx/kdist/plugin.py b/kmultiversx/src/kmultiversx/kdist/plugin.py
@@ -1,27 +1,26 @@
 from __future__ import annotations
 
 import shutil
+from distutils.dir_util import copy_tree
 from pathlib import Path
 from typing import TYPE_CHECKING
 
-from pyk.kbuild.utils import k_version
+from pyk.kbuild.utils import k_version, sync_files
 from pyk.kdist.api import Target
 from pyk.ktool.kompile import KompileBackend, kompile
+from pyk.utils import run_process
 
 if TYPE_CHECKING:
     from collections.abc import Callable, Mapping
     from typing import Any, Final
 
 
-CURRENT_DIR: Final = Path(__file__).parent
-PLUGIN_DIR: Final = CURRENT_DIR.parents[3] / 'deps/plugin'  # TODO Distribute plugin files with Python
-
-
 class SourceTarget(Target):
     SRC_DIR: Final = Path(__file__).parent
 
     def build(self, output_dir: Path, deps: dict[str, Path], args: dict[str, Any], verbose: bool) -> None:
         shutil.copytree(deps['wasm-semantics.source'] / 'wasm-semantics', output_dir / 'wasm-semantics')
+        shutil.copytree(self.SRC_DIR / 'plugin/plugin', output_dir / 'plugin')
         shutil.copytree(self.SRC_DIR / 'mx-semantics', output_dir / 'mx-semantics')
 
     def source(self) -> tuple[Path, ...]:
@@ -31,6 +30,35 @@ def deps(self) -> tuple[str]:
         return ('wasm-semantics.source',)
 
 
+class PluginTarget(Target):
+    PLUGIN_DIR: Final = Path(__file__).parent / 'plugin'
+
+    def build(self, output_dir: Path, deps: dict[str, Any], args: dict[str, Any], verbose: bool) -> None:
+        sync_files(
+            source_dir=self.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(self.PLUGIN_DIR), '.')
+        run_process(
+            ['make', 'libcryptopp', 'libff', 'blake2', '-j8'],
+            pipe_stdout=not verbose,
+        )
+
+        copy_tree('./build/libcryptopp', str(output_dir / 'libcryptopp'))
+        copy_tree('./build/libff', str(output_dir / 'libff'))
+        copy_tree('./build/blake2', str(output_dir / 'blake2'))
+
+    def source(self) -> tuple[Path]:
+        return (self.PLUGIN_DIR,)
+
+
 class KompileTarget(Target):
     _kompile_args: Callable[[Path], Mapping[str, Any]]
 
@@ -39,24 +67,24 @@ def __init__(self, kompile_args: Callable[[Path], Mapping[str, Any]]):
 
     def build(self, output_dir: Path, deps: dict[str, Path], args: dict[str, Any], verbose: bool) -> None:
         # TODO Pass K_OPTS='-Xmx8G -Xss512m'
-        kompile_args = self._kompile_args(deps['mx-semantics.source'])
+        kompile_args = self._kompile_args(deps['mx-semantics.source'], deps['mx-semantics.plugin'])
         kompile(output_dir=output_dir, verbose=verbose, **kompile_args)
 
     def context(self) -> dict[str, str]:
         return {'k-version': k_version().text}
 
-    def deps(self) -> tuple[str]:
-        return ('mx-semantics.source',)
+    def deps(self) -> tuple[str, str]:
+        return ('mx-semantics.source', 'mx-semantics.plugin')
 
 
 def llvm_target(main_file_name: str, main_module: str, syntax_module: str) -> KompileTarget:
     return KompileTarget(
-        lambda src_dir: {
+        lambda src_dir, plugin_dir: {
             'backend': KompileBackend.LLVM,
             'main_file': src_dir / 'mx-semantics' / main_file_name,
             'main_module': main_module,
             'syntax_module': syntax_module,
-            'include_dirs': [src_dir, PLUGIN_DIR],
+            'include_dirs': [src_dir],
             'md_selector': 'k',
             'hook_namespaces': ['KRYPTO'],
             'opt_level': 2,
@@ -67,27 +95,27 @@ def llvm_target(main_file_name: str, main_module: str, syntax_module: str) -> Ko
                 '-lprocps',
                 '-lsecp256k1',
                 '-lssl',
-                f"{PLUGIN_DIR / 'build/blake2/lib/blake2.a'}",
-                f"-I{PLUGIN_DIR / 'build/blake2/include'}",
-                f"{PLUGIN_DIR / 'build/libcryptopp/lib/libcryptopp.a'}",
-                f"-I{PLUGIN_DIR / 'build/libcryptopp/include'}",
-                f"{PLUGIN_DIR / 'build/libff/lib/libff.a'}",
-                f"-I{PLUGIN_DIR / 'build/libff/include'}",
-                f"{PLUGIN_DIR / 'plugin-c/crypto.cpp'}",
-                f"{PLUGIN_DIR / 'plugin-c/plugin_util.cpp'}",
+                str(plugin_dir / 'blake2/lib/blake2.a'),
+                f"-I{plugin_dir / 'blake2/include'}",
+                str(plugin_dir / 'libcryptopp/lib/libcryptopp.a'),
+                f"-I{plugin_dir / 'libcryptopp/include'}",
+                str(plugin_dir / 'libff/lib/libff.a'),
+                f"-I{plugin_dir / 'libff/include'}",
+                str(plugin_dir / 'plugin-c/crypto.cpp'),
+                str(plugin_dir / 'plugin-c/plugin_util.cpp'),
             ],
         },
     )
 
 
 def haskell_target(main_file_name: str, main_module: str, syntax_module: str) -> KompileTarget:
     return KompileTarget(
-        lambda src_dir: {
+        lambda src_dir, plugin_dir: {
             'backend': KompileBackend.HASKELL,
             'main_file': src_dir / 'mx-semantics' / main_file_name,
             'main_module': main_module,
             'syntax_module': syntax_module,
-            'include_dirs': [src_dir, PLUGIN_DIR],
+            'include_dirs': [src_dir],
             'md_selector': 'k',
             'hook_namespaces': ['KRYPTO'],
             'warnings_to_errors': True,
@@ -97,6 +125,7 @@ def haskell_target(main_file_name: str, main_module: str, syntax_module: str) ->
 
 __TARGETS__: Final = {
     'source': SourceTarget(),
+    'plugin': PluginTarget(),
     'llvm-mandos': llvm_target('mandos.md', 'MANDOS', 'MANDOS-SYNTAX'),
     'llvm-kasmer': llvm_target('kasmer.md', 'KASMER', 'KASMER-SYNTAX'),
     'haskell-mandos': haskell_target('mandos.md', 'MANDOS', 'MANDOS-SYNTAX'),

diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.42
+0.1.43