Merge b7ab4a6 into a07b0aa

Author: tothtamas28

.github/workflows/test-pr.yml

@@ -58,12 +58,24 @@ jobs:
   profile:
     needs: code-quality-checks
     name: 'Profiling'
-    runs-on: ubuntu-latest
+    runs-on: [self-hosted, linux, normal-ephemeral]
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
+      - name: 'Install Python'
+        uses: actions/setup-python@v4
+        with:
+          python-version: '3.10'
       - name: 'Install Poetry'
         uses: Gr1N/setup-poetry@v8
+      - name: 'Install K'
+        run: |
+          K_VERSION=$(cat deps/k_release)
+          DEB_PACKAGE_NAME=kframework_${K_VERSION}_amd64_ubuntu_jammy.deb
+          wget https://github.com/runtimeverification/k/releases/download/v${K_VERSION}/${DEB_PACKAGE_NAME}
+          sudo apt-get update
+          sudo apt-get -y install ./${DEB_PACKAGE_NAME}
+          kompile --version
       - name: 'Run profiling'
         run: |
           make profile

src/tests/profiling/profile_kbuild.py

@@ -0,0 +1,33 @@
+from __future__ import annotations
+
+from typing import TYPE_CHECKING
+
+import pytest
+
+from pyk.kbuild import KBuild, Package
+
+from .utils import TEST_DATA_DIR
+
+if TYPE_CHECKING:
+    from pathlib import Path
+    from typing import Final
+
+    from pyk.testing import Profiler
+
+
+A_SEMANTICS_DIR: Final = TEST_DATA_DIR / 'kbuild/a-semantics'
+
+
+@pytest.fixture
+def kbuild(tmp_path: Path) -> KBuild:
+    return KBuild(tmp_path / 'kbuild')
+
+
+def test_kbuild(kbuild: KBuild, profile: Profiler) -> None:
+    with profile('kompile.txt', sort_keys=('cumtime', 'tottime'), limit=35):
+        package = Package.create(A_SEMANTICS_DIR / 'kbuild.toml')
+        kbuild.kompile(package, 'llvm')
+
+    with profile('rekompile.txt', sort_keys=('cumtime', 'tottime'), limit=35):
+        package = Package.create(A_SEMANTICS_DIR / 'kbuild.toml')
+        kbuild.kompile(package, 'llvm')

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

@@ -0,0 +1,10 @@
+requires "b-semantics/b.k"
+requires "c-semantics/c.k"
+
+module A-SYNTAX
+endmodule
+
+module A
+    imports B
+    imports C
+endmodule

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

@@ -0,0 +1,12 @@
+[project]
+name = "a-semantics"
+version = "0.1.0"
+source = "."
+
+[dependencies]
+b-semantics = { path = "../b-semantics" }
+c-semantics = { path = "../c-semantics" }
+
+[targets.llvm]
+main-file = 'a.k'
+backend='llvm'

src/tests/profiling/test-data/kbuild/b-semantics/b.k

@@ -0,0 +1,5 @@
+module B-SYNTAX
+endmodule
+
+module B
+endmodule

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

@@ -0,0 +1,4 @@
+[project]
+name = "b-semantics"
+version = "0.1.0"
+source = "."

src/tests/profiling/test-data/kbuild/c-semantics/c.k

@@ -0,0 +1,5 @@
+module C-SYNTAX
+endmodule
+
+module C
+endmodule

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

@@ -0,0 +1,4 @@
+[project]
+name = "c-semantics"
+version = "0.1.0"
+source = "."