Skip to content

Commit

Permalink
Add kdist setup
Browse files Browse the repository at this point in the history
  • Loading branch information
tothtamas28 committed May 10, 2024
1 parent c0c9fb2 commit 0925a78
Show file tree
Hide file tree
Showing 5 changed files with 74 additions and 0 deletions.
9 changes: 9 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,15 @@ poetry-install:
$(POETRY) install


# Semantics

kdist-build: poetry-install
$(POETRY) run kdist -v build soroban-semantics.llvm

kdist-clean: poetry-install
$(POETRY) run kdist clean


# Tests

TEST_ARGS :=
Expand Down
3 changes: 3 additions & 0 deletions pyproject.toml
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,9 @@ authors = [
"Runtime Verification, Inc. <[email protected]>",
]

[tool.poetry.plugins.kdist]
soroban-semantics = "ksoroban.kdist.plugin"

[tool.poetry.dependencies]
python = "^3.10"
pykwasm = { git = "https://github.com/runtimeverification/wasm-semantics.git", tag = "v0.1.48", subdirectory = "pykwasm" }
Expand Down
Empty file added src/ksoroban/kdist/__init__.py
Empty file.
58 changes: 58 additions & 0 deletions src/ksoroban/kdist/plugin.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
from __future__ import annotations

import shutil
from pathlib import Path
from typing import TYPE_CHECKING

from pyk.kbuild.utils import k_version
from pyk.kdist.api import Target
from pyk.ktool.kompile import kompile

if TYPE_CHECKING:
from collections.abc import Callable, Mapping
from typing import Any, Final


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 / 'soroban-semantics', output_dir / 'soroban-semantics')

def source(self) -> tuple[Path, ...]:
return (self.SRC_DIR,)

def deps(self) -> tuple[str]:
return ('wasm-semantics.source',)


class KompileTarget(Target):
_kompile_args: Callable[[Path], Mapping[str, Any]]

def __init__(self, kompile_args: Callable[[Path], Mapping[str, Any]]):
self._kompile_args = kompile_args

def build(self, output_dir: Path, deps: dict[str, Path], args: dict[str, Any], verbose: bool) -> None:
kompile_args = self._kompile_args(deps['soroban-semantics.source'])
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 ('soroban-semantics.source',)


__TARGETS__: Final = {
'source': SourceTarget(),
'llvm': KompileTarget(
lambda src_dir: {
'main_file': src_dir / 'soroban-semantics/soroban.md',
'syntax_module': 'SOROBAN',
'include_dirs': [src_dir],
'md_selector': 'k',
'warnings_to_errors': True,
},
),
}
4 changes: 4 additions & 0 deletions src/ksoroban/kdist/soroban-semantics/soroban.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
```k
module SOROBAN
endmodule
```

0 comments on commit 0925a78

Please sign in to comment.