Upcoming release -- Request for feedback and testers

[ivanperez-keera]

Hi everyone,

I've closed all the issues in this repo that I was planning to include in the next release of IKOS: https://github.com/NASA-SW-VnV/ikos/milestone/1.

There's an issue pending in that milestone atm, but that issue requires no changes to this repo. I'm planning to sort that too prior to the final release.

One thing that worries me a bit is that the installation method for python tools is still not working as well as it should. I'm randomly seeing errors like:

error: could not find ikos python module
error: see TROUBLESHOOTING.md

even after setting the PYTHONPATH correctly. This is somehow more likely to happen on MacOSX (see the Action to build for Mac), but randomly: sometimes a re-build is all it takes for it to build and execute correctly.

I'm also sometimes seeing this instead:

error: externally-managed-environment

× This environment is externally managed
╰─> To install Python packages system-wide, try apt install
    python3-xyz, where xyz is the package you are trying to
    install.

    If you wish to install a non-Debian-packaged Python package,
    create a virtual environment using python3 -m venv path/to/venv.
    Then use path/to/venv/bin/python and path/to/venv/bin/pip. Make
    sure you have python3-full installed.

    If you wish to install a non-Debian packaged Python application,
    it may be easiest to use pipx install xyz, which will manage a
    virtual environment for you. Make sure you have pipx installed.

    See /usr/share/doc/python3.11/README.venv for more information.

note: If you believe this is a mistake, please contact your Python installation or OS distribution provider. You can override this, at the risk of breaking your Python installation or OS, by passing --break-system-packages.
hint: See PEP 668 for the detailed specification.

It would help if people in the community tried the current master, and also people who know about python checked if installation should be happening in a different way. The following merged PR maybe relevant: #231.

Also helpful may be the following dockerfile (which should be updated to use setuptools): #203 (comment).

[arthaud]

I tried to build this from source and I'm getting issues with python, indeed.

First, I would get "no such file or directory" at the pip install . command. I think that's because we assume pip is available as a system binary, that's wrong. We should use python -m pip. It should be an easy fix:
In https://github.com/NASA-SW-VnV/ikos/blob/master/analyzer/CMakeLists.txt#L365

  set(PIP_INSTALL
    \"${PYTHON_EXECUTABLE}\"
    \"-m\"
    \"pip\"
    \"install\"
  )

Now, I'm getting the same error as you, "This environment is externally managed".
I think that's because DESTDIR is not set, so it tries to install the python library as a system package, that's wrong.
https://github.com/NASA-SW-VnV/ikos/blob/master/analyzer/CMakeLists.txt#L369
I tried using:

  if (DEFINED ENV{DESTDIR})
    list(APPEND PIP_INSTALL \"--target=\$ENV{DESTDIR}\")
  else()
    list(APPEND PIP_INSTALL \"--target=${CMAKE_INSTALL_PREFIX}\")
  endif()

Now it seems to produce:

$ ll install
total 0
drwx------ 13 arthaud staff 416 2023-12-09 13:33 bin
drwx------ 20 arthaud staff 640 2023-12-09 13:44 ikos
drwx------  9 arthaud staff 288 2023-12-09 13:44 ikos-3.1.dist-info
drwxr-xr-x  3 arthaud staff  96 2023-12-09 13:33 include
drwx------  5 arthaud staff 160 2023-12-09 13:44 lib
drwx------  3 arthaud staff  96 2023-12-09 13:33 share

I think instead it should install something under lib/pythonX.Y/ikos. I don't know what changed.

I might have more time to look into this tomorrow.

[ivanperez-keera]

I think instead it should install something under lib/pythonX.Y/ikos. I don't know what changed.

Could it be because we are using --target as opposed to --prefix?

[ivanperez-keera]

@arthaud I have created two issues to capture these: #242, #243

For now, I'll go ahead and fix #242 with the suggestion you made. We should still figure out #243.

I reached out to a couple other folks in the past few days and they recommended we switch to venvs.

[ivanperez-keera]

I have made the first change of using python -m pip instead of pip. That closes #242.

We need to decide what to do about #243.

The way that venv seems to work is that it'll put all dependencies inside the target directory, which is what we want. However, it also puts a wrapper for python itself that adjusts environment variables. If I'm not mistaken, then either we require users to adjust the PATH before using IKOS (not nice) or we adjust all python-based IKOS tools to pick "our" python executable as opposed to the standard python executable.

Currently the script templates refer to the python executable as @PYTHON_EXECUTABLE@, so we'd have to replace that with the python executable in the venv, and we'd have to figure out which one that is before those templates are expanded.

We need to be careful about this. If I'm not mistaken, at that point, in the CMakeLists.txt, there'll be two python executables being referred to: the one used during compilation/installation, and the one in the venv, used only after installation.

[arthaud]

Alright, the idea of installing under a virtualenv seems to work, I implemented it in #245.

We will need to update the homebrew formula once version 3.2 is out. I can handle that.

[ivanperez-keera]

Awesome! Let me try it.

[ivanperez-keera]

I took a look at the diff and left a few comments. I still have not run it on my side but the CI jobs did complete successfully. They run ikos --version at the end, showing that it's finding the python modules.

[ivanperez-keera]

Update for everyone: The issues with installation appear to be fixed, thanks to @arthaud 's last PR.

Please try it and report any problems you find.