Merge branch 'master' into noah/subproof-split

Author: nwatson22

package/version

@@ -1 +1 @@
-0.1.446
+0.1.447

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.446"
+version = "0.1.447"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/pyk/kbuild/kbuild.py

@@ -1,18 +1,21 @@
 from __future__ import annotations
 
 import re
+from contextlib import contextmanager
 from dataclasses import dataclass
 from functools import cached_property
 from pathlib import Path
+from tempfile import TemporaryDirectory
 from typing import TYPE_CHECKING, final
 
 from filelock import FileLock
 
 from ..ktool.kompile import kompile
-from ..utils import single
+from ..utils import check_dir_path, single
 from .utils import k_version, sync_files
 
 if TYPE_CHECKING:
+    from collections.abc import Iterator
     from re import Match
     from typing import Any
 
@@ -33,65 +36,19 @@ def k_version(self) -> str:
         return k_version().text
 
     def definition_dir(self, project: Project, target_name: str) -> Path:
-        return self.kdist_dir / project.name / 'target' / self.k_version / target_name
-
-    def resource_dir(self, project: Project, resource_name: str) -> Path:
-        return self.kdist_dir / project.name / 'resource' / resource_name
-
-    def resource_files(self, project: Project, resource_name: str) -> list[Path]:
-        return [
-            self.resource_dir(project, resource_name) / file_name
-            for file_name in project.resource_file_names[resource_name]
-        ]
-
-    def include_dir(self, project: Project) -> Path:
-        return self.kdist_dir / project.name / 'include'
-
-    def source_dir(self, project: Project) -> Path:
-        return self.include_dir(project) / project.name
-
-    def source_files(self, project: Project) -> list[Path]:
-        return [self.source_dir(project) / file_name for file_name in project.source_file_names]
-
-    def sync(self, project: Project) -> list[Path]:
-        res: list[Path] = []
-
-        # Sync sources
-        res += sync_files(
-            source_dir=project.source_dir,
-            target_dir=self.source_dir(project),
-            file_names=project.source_file_names,
-        )
-
-        # Sync resources
-        for resource_name in project.resources:
-            res += sync_files(
-                source_dir=project.resources[resource_name],
-                target_dir=self.resource_dir(project, resource_name),
-                file_names=project.resource_file_names[resource_name],
-            )
-
-        return res
+        return self.kdist_dir / self.k_version / target_name
 
     def kompile(self, project: Project, target_name: str) -> Path:
         self.kdist_dir.mkdir(parents=True, exist_ok=True)
-        with FileLock(self.kdist_dir / '.lock'):
-            for sub_project in project.sub_projects:
-                self.sync(sub_project)
 
+        with FileLock(self.kdist_dir / '.lock'):
             output_dir = self.definition_dir(project, target_name)
 
             if self.up_to_date(project, target_name):
                 return output_dir
 
-            target = project.get_target(target_name)
-            args = self.kompile_args(project, target)
-            kompile(
-                output_dir=output_dir,
-                include_dirs=[self.include_dir(sub_project) for sub_project in project.sub_projects],
-                cwd=self.kdist_dir,
-                **args,
-            )
+            with KBuildEnv.create_temp(project) as env:
+                env.kompile(target_name, output_dir)
 
             return output_dir
 
@@ -102,36 +59,92 @@ def up_to_date(self, project: Project, target_name: str) -> bool:
         if not timestamp.exists():
             return False
 
-        input_files: list[Path] = []
-        for sub_project in project.sub_projects:
-            input_files.append(sub_project.project_file)
-            input_files.extend(self.source_files(sub_project))
-            for resource_name in sub_project.resources:
-                input_files.extend(self.resource_files(sub_project, resource_name))
-
-        input_timestamps = (input_file.stat().st_mtime for input_file in input_files)
+        input_timestamps = (input_file.stat().st_mtime for input_file in project.all_files)
         target_timestamp = timestamp.stat().st_mtime
         return all(input_timestamp < target_timestamp for input_timestamp in input_timestamps)
 
-    def kompile_args(self, project: Project, target: Target) -> dict[str, Any]:
+
+@final
+@dataclass(frozen=True)
+class KBuildEnv:
+    project: Project
+    path: Path
+
+    def __init__(self, project: Project, path: str | Path):
+        path = Path(path).resolve()
+        check_dir_path(path)
+        object.__setattr__(self, 'project', project)
+        object.__setattr__(self, 'path', path)
+
+    @staticmethod
+    @contextmanager
+    def create_temp(project: Project) -> Iterator[KBuildEnv]:
+        with TemporaryDirectory(prefix=f'kbuild-{project.name}-') as path_str:
+            env = KBuildEnv(project, path_str)
+            env.sync()
+            yield env
+
+    def sync(self) -> None:
+        for sub_project in self.project.sub_projects:
+            self._sync_project(sub_project)
+
+    def kompile(self, target_name: str, output_dir: Path) -> None:
+        target = self.project.get_target(target_name)
+        kompile(
+            output_dir=output_dir,
+            include_dirs=self._include_dirs,
+            cwd=self.path,
+            **self._kompile_args(target),
+        )
+
+    @property
+    def _include_dirs(self) -> list[Path]:
+        return [self._include_dir(sub_project) for sub_project in self.project.sub_projects]
+
+    def _include_dir(self, project: Project) -> Path:
+        return self.path / project.name / 'include'
+
+    def _source_dir(self, project: Project) -> Path:
+        return self._include_dir(project) / project.name
+
+    def _resource_dir(self, project: Project, resource_name: str) -> Path:
+        return self.path / project.name / 'resource' / resource_name
+
+    def _sync_project(self, project: Project) -> None:
+        # Sync sources
+        sync_files(
+            source_dir=project.source_dir,
+            target_dir=self._source_dir(project),
+            file_names=project.source_file_names,
+        )
+
+        # Sync resources
+        for resource_name in project.resources:
+            sync_files(
+                source_dir=project.resources[resource_name],
+                target_dir=self._resource_dir(project, resource_name),
+                file_names=project.resource_file_names[resource_name],
+            )
+
+    def _kompile_args(self, target: Target) -> dict[str, Any]:
         args = target.dict
         args.pop('name')
-        args['main_file'] = self.source_dir(project) / args['main_file']
+        args['main_file'] = self._source_dir(self.project) / args['main_file']
 
         if 'ccopts' in args:
-            args['ccopts'] = [self.render_opt(project, opt) for opt in args['ccopts']]
+            args['ccopts'] = [self._render_opt(opt) for opt in args['ccopts']]
 
         return args
 
-    def render_opt(self, project: Project, opt: str) -> str:
+    def _render_opt(self, opt: str) -> str:
         def render(match: Match) -> str:
             project_name = match.group('project')
             resource_name = match.group('resource')
 
             sub_project = single(
-                sub_project for sub_project in project.sub_projects if sub_project.name == project_name
+                sub_project for sub_project in self.project.sub_projects if sub_project.name == project_name
             )
-            resource_path = self.resource_dir(sub_project, resource_name)
+            resource_path = self._resource_dir(sub_project, resource_name)
 
             if not resource_path.exists():
                 raise ValueError('Failed to resolve opt {opt}: resource path {resource_path} does not exist')

src/pyk/kbuild/project.py

@@ -1,9 +1,11 @@
 from __future__ import annotations
 
 import dataclasses
+from abc import ABC, abstractmethod
 from dataclasses import dataclass
 from functools import cached_property
-from pathlib import Path
+from importlib import resources
+from pathlib import Path, PosixPath
 from typing import TYPE_CHECKING, final
 
 import tomli
@@ -18,6 +20,41 @@
     from typing import Any
 
 
+class Source(ABC):
+    @staticmethod
+    def from_dict(dct: Mapping[str, Any]) -> Source:
+        if 'path' in dct:
+            return PathSource(Path(dct['path']))
+        if 'package' in dct:
+            return PackageSource(dct['package'])
+        raise ValueError(f'Cannot parse source: {dct}')
+
+    @abstractmethod
+    def resolve(self, project_path: Path) -> Path:
+        ...
+
+
+@final
+@dataclass(frozen=True)
+class PathSource(Source):
+    path: Path
+
+    def resolve(self, project_path: Path) -> Path:
+        return abs_or_rel_to(self.path, project_path)
+
+
+@final
+@dataclass(frozen=True)
+class PackageSource(Source):
+    package: str
+
+    def resolve(self, project_path: Path) -> Path:
+        traversable = resources.files(self.package)
+        if not isinstance(traversable, PosixPath):
+            raise ValueError(f'Package name {self.package!r} does not resolve to a directory')
+        return traversable.resolve(strict=True)
+
+
 @final
 @dataclass(frozen=True)
 class Target:
@@ -164,24 +201,28 @@ def __init__(
     def load(project_file: str | Path) -> Project:
         project_file = Path(project_file)
         check_file_path(project_file)
+        project_path = project_file.parent
 
-        with open(project_file, 'rb') as f:
-            dct = tomli.load(f)
-
-        def _load_dependency(name: str, path: str) -> Project:
-            dependency_path = abs_or_rel_to(Path(path), project_file.parent)
+        def _load_dependency(name: str, dct: Any) -> Project:
+            source = Source.from_dict(dct)
+            dependency_path = source.resolve(project_path)
             project = Project.load_from_dir(dependency_path)
             if project.name != name:
                 raise ValueError(f'Invalid dependency, expected name {name}, got: {project.name}')
             return project
 
+        with open(project_file, 'rb') as f:
+            dct = tomli.load(f)
+
         project = Project(
-            path=project_file.parent,
+            path=project_path,
             name=dct['project']['name'],
             version=dct['project']['version'],
             source_dir=dct['project']['source'],
             resources=dct['project'].get('resources'),
-            dependencies=tuple(_load_dependency(name, path) for name, path in dct.get('dependencies', {}).items()),
+            dependencies=tuple(
+                _load_dependency(name, source_dct) for name, source_dct in dct.get('dependencies', {}).items()
+            ),
             targets=tuple(Target.from_dict(name, target) for name, target in dct.get('targets', {}).items()),
         )
 
@@ -232,6 +273,16 @@ def resource_file_names(self) -> dict[str, list[str]]:
             for resource_name, resource_files in self.resource_files.items()
         }
 
+    @property
+    def all_files(self) -> list[Path]:
+        res: list[Path] = []
+        for sub_project in self.sub_projects:
+            res.append(sub_project.project_file)
+            res.extend(sub_project.source_files)
+            for resource_name in sub_project.resources:
+                res.extend(sub_project.resource_files[resource_name])
+        return res
+
     def get_target(self, target_name: str) -> Target:
         # TODO Should be enforced as a validation rule
         return single(target for target in self.targets if target.name == target_name)

src/tests/profiling/test-data/kbuild/a-semantics/kbuild.toml

@@ -4,8 +4,8 @@ version = "0.1.0"
 source = "."
 
 [dependencies]
-b-semantics = "../b-semantics"
-c-semantics = "../c-semantics"
+b-semantics = { path = "../b-semantics" }
+c-semantics = { path = "../c-semantics" }
 
 [targets.llvm]
 main-file = 'a.k'