Start to integrate LLVM bindings into Pyk #2844
Conversation
|
It looks overall fine to me, but I suppose that the changes to the |
| 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{}") |
There was a problem hiding this comment.
Did you confirm that this test is being run on CI correctly (shows up in the output)?
There was a problem hiding this comment.
From the CI log:
test_basic (tests.test_kllvm.KLLVMTest) ... ok
| from . import kllvm | ||
| from .kllvm import ast |
There was a problem hiding this comment.
Is this the suggested way for wrapping native pybind11 modules? Whe I try to import the module from an interpreter, I get the following error.
In [1]: import kllvm
---------------------------------------------------------------------------
ImportError Traceback (most recent call last)
Input In [1], in <cell line: 1>()
----> 1 import kllvm
File ~/.local/lib/python3.8/site-packages/kllvm/__init__.py:1, in <module>
----> 1 from . import kllvm
2 from .kllvm import ast
ImportError: cannot import name 'kllvm' from partially initialized module 'kllvm' (most likely due to a circular import) (/home/ttoth/.local/lib/python3.8/site-packages/kllvm/__init__.py)
There was a problem hiding this comment.
Did you run make deps in the pyk directory beforehand?
There was a problem hiding this comment.
(i.e. is there a shared library kllvm.platform-os-etc.so beside src/kllvm/__init__.py?)
There was a problem hiding this comment.
There is, and the unit test passes accordingly.
But now I tried it with python, and it works, so the issue is only present with ipython.
There was a problem hiding this comment.
Currently, both of the following work:
from kllvm.kllvm import ast
from kllvm import astDid you consider putting this in __init__.py instead?
from .kllvm import *There was a problem hiding this comment.
If that doesn't solve the circular import problem of ipython, an other solution to consider is to rename the native module to _kllvm. (That also communicates to users that the module is not supposed to be imported directly.)
There was a problem hiding this comment.
The previous attempt aimed to build a wheel from the LLVM backend's build directory, then convince Poetry to track that wheel as a dependency locally. Unfortunately, this would require us to be able to build a wheel for every supported platform; this would be a lot of wrangling and cross-compilation.
I think that would be the right way to do it though. As I see it, the current solution just transfers the problem to pyk deployment.
What do you think about the following workaround?
Let's pull this module out from pyk to it's own package at the llvm-backend root. We then define a dev dependency in pyk to the corresponding path (we use the same hack downstreams). Once we have the capacity, we can set up the CI pipelines for proper deployment, and replace the dev dependency by a runtime dependency.
|
So to summarise - the LLVM backend should present a Python package that contains the shared library it compiled; this package can use a similar trick as above to re-export all the symbols from the shared library (module getting the imports / exports right - Pyk can then point its |
Yes, I think that would be the right approach for now. |
|
Great, thanks for the pointers! |
…untimeverification#2212) * haskell-backend/src/main/native/haskell-backend: d0bfb78f - Update regression tests (runtimeverification#2844) * haskell-backend/src/main/native/haskell-backend: 98e241ed - Update dependency: deps/k_release (runtimeverification#2843)
This PR is a revised attempt (following runtimeverification/llvm-backend#551, which wasn't what we were looking for) to integrate the new Python bindings for the LLVM backend into Pyk.
The previous attempt aimed to build a wheel from the LLVM backend's build directory, then convince Poetry to track that wheel as a dependency locally. Unfortunately, this would require us to be able to build a wheel for every supported platform; this would be a lot of wrangling and cross-compilation.
This PR works by symlinking the shared library built during the LLVM backend's build phase into the
src/kllvmpackage, which then transparently re-exports the symbols from that package. Poetry then packages this local package alongsidepykat build time.I've also added a trivial test case for the bindings to make sure that all of these changes actually work.
I've spent quite a bit of time fiddling with this, but I'm open to suggestions on how to improve it - it's by no means guaranteed to be the best solution, but it's the neatest one I've found as yet.
Per @goodlyrottenapple's request, this PR also adds a line to the github action spec to ensure we're testing Pyk via nix.