You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
When K is installed via kup, care needs to be taken to make sure that we use a Nix-supplied version of Python to run Pyk applications via the Poetry environment. If this is not the case, we see errors like:
I have proposed a new feature in kup that will supply the correct Python interpreter path to use; we should also have Pyk print a friendlier error message when the following conditions are met on running llvm-kompile to build a runtime Python binding module:
llvm-kompile is somewhere under /nix/store/...
The --python argument (i.e. the current executing Python interpreter) is not under /nix/store/...
llvm-kompile fails to run successfully
If these conditions are met, we should add a message that suggests running something like:
$ poetry env use --no-cache $(k-which-python)
Note that these conditions are just a heuristic for a particular common bug with kup + K + Pyk, so we should still report the full error message from llvm-kompile, and allow it to run successfully if it somehow does work.
There's a second way that this can manifest, whereby an ImportError is thrown when running module_from_spec(spec). We should catch this and report the error similarly.
When K is installed via
kup
, care needs to be taken to make sure that we use a Nix-supplied version of Python to run Pyk applications via the Poetry environment. If this is not the case, we see errors like:kup
installs an incompatible version of K kup#82I have proposed a new feature in
kup
that will supply the correct Python interpreter path to use; we should also have Pyk print a friendlier error message when the following conditions are met on runningllvm-kompile
to build a runtime Python binding module:llvm-kompile
is somewhere under/nix/store/...
--python
argument (i.e. the current executing Python interpreter) is not under/nix/store/...
llvm-kompile
fails to run successfullyIf these conditions are met, we should add a message that suggests running something like:
$ poetry env use --no-cache $(k-which-python)
Note that these conditions are just a heuristic for a particular common bug with
kup
+ K + Pyk, so we should still report the full error message fromllvm-kompile
, and allow it to run successfully if it somehow does work.Blocked onkup
support in: runtimeverification/kup#92The text was updated successfully, but these errors were encountered: