Use LLVM backend Python package

.github/workflows/test-flake.yml

@@ -30,4 +30,7 @@ jobs:
           signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}'
 
       - name: 'Build K Framework'
-        run: GC_DONT_GC=1 nix build .
+        run: GC_DONT_GC=1 nix build .
+
+      - name: 'Build pyk'
+        run: GC_DONT_GC=1 nix build .#pyk

CODEOWNERS

@@ -1,3 +1,3 @@
 /k-distribution/include/kframework/builtin/* @dwightguth @ehildenb
-/Jenkinsfile @runtimeverification/admin
-/.github/workflows/* @runtimeverification/admin
+/Jenkinsfile @runtimeverification/admin @F-WRunTime
+/.github/workflows/* @runtimeverification/admin @F-WRunTime

flake.nix

@@ -70,6 +70,8 @@
             pyk = prev.poetry2nix.mkPoetryApplication {
               python = prev.python39;
               projectDir = ./pyk;
+              overrides = prev.poetry2nix.overrides.withDefaults
+                (finalPython: prevPython: { kllvm = prev.kllvm; });
             };
           })
       ];

package/debian/rules

@@ -25,6 +25,8 @@ export PREFIX
 
 override_dh_auto_build:
 	mvn --batch-mode package -DskipTests -Dllvm.backend.prefix=$(PREFIX) -Dllvm.backend.destdir=$(DESTDIR)
+	package/fix-debian-kllvm-path
+	(cd pyk && rm poetry.lock && poetry update)
 
 override_dh_auto_install:
 	package/package

package/debian/rules.jammy

@@ -29,6 +29,8 @@ export PREFIX
 
 override_dh_auto_build:
 	mvn --batch-mode package -DskipTests -Dllvm.backend.prefix=$(PREFIX) -Dllvm.backend.destdir=$(DESTDIR)
+	package/fix-debian-kllvm-path
+	(cd pyk && rm poetry.lock && poetry update)
 
 override_dh_auto_install:
 	package/package

package/fix-debian-kllvm-path

@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+# This script is designed to be called _only_ during the K debian packaging
+# process. It will make a destructive change to the Pyk project file to point to
+# the debian root's installed path, rather than the default K build path. 
+
+ORIGINAL='kllvm = { path = "../k-distribution/target/release/k/lib/python" }'
+NEW="kllvm = { path = \"$DESTDIR$PREFIX/lib/python\" }"
+
+sed -i "s|$ORIGINAL|$NEW|g" pyk/pyproject.toml

pyk/Makefile

@@ -1,6 +1,12 @@
 K_ROOT := $(abspath ..)
 K_BIN  := $(K_ROOT)/k-distribution/target/release/k/bin
 
+ifeq ($(DESTDIR),)
+K_LIB  := $(K_ROOT)/k-distribution/target/release/k/lib
+else
+K_LIB  := $(DESTDIR)$(PREFIX)/lib
+endif
+
 export PATH := $(K_BIN):$(PATH)
 
 
@@ -23,7 +29,10 @@ build:
 	poetry build
 
 install: build
-	pip3 install ./dist/*.whl --root=$(DESTDIR) --prefix=$(PREFIX)
+	poetry export -f requirements.txt --without-hashes | \
+	pip3 install -r /dev/stdin --root=$(DESTDIR) --prefix=$(PREFIX)
+	pip3 install $(K_LIB)/python --root=$(DESTDIR) --prefix=$(PREFIX)
+	pip3 install ./dist/*.whl --no-dependencies --root=$(DESTDIR) --prefix=$(PREFIX)
 
 poetry-install:
 	poetry install

pyk/pyproject.toml

@@ -23,6 +23,7 @@ flake8-comprehensions = "*"
 isort = "*"
 mypy = "*"
 pep8-naming = "*"
+kllvm = { path = "../k-distribution/target/release/k/lib/python" }
 
 [tool.poetry.scripts]
 pyk = "pyk.__main__:main"
@@ -37,5 +38,5 @@ line-length = 120
 skip-string-normalization = true
 
 [[tool.mypy.overrides]]
-module = "graphviz"
+module = ["graphviz", "kllvm"]
 ignore_missing_imports = true

pyk/src/tests/test_kllvm.py

@@ -0,0 +1,9 @@
+from unittest import TestCase
+
+import kllvm
+
+
+class KLLVMTest(TestCase):
+    def test_basic(self):
+        sort_int = kllvm.ast.CompositeSort('SortInt')
+        self.assertEqual(str(sort_int), "SortInt{}")