cargo-kani setup fails due to python distutils error on Ubuntu 18.04.2

[JustusAdam]

I ran cargo-kani setup after successfully installing cargo +nightly install --locked kani-verifier and got the following error:

Installing collected packages: MarkupSafe, jinja2, setuptools, voluptuous, cbmc-viewer
Exception:
Traceback (most recent call last):
  File "/usr/lib/python3/dist-packages/pip/basecommand.py", line 215, in main
    status = self.run(options, args)
  File "/usr/lib/python3/dist-packages/pip/commands/install.py", line 356, in run
    requirement_set.install(
  File "/usr/lib/python3/dist-packages/pip/req/req_set.py", line 780, in install
    requirement.install(
  File "/usr/lib/python3/dist-packages/pip/req/req_install.py", line 851, in install
    self.move_wheel_files(self.source_dir, root=root, prefix=prefix)
  File "/usr/lib/python3/dist-packages/pip/req/req_install.py", line 1057, in move_wheel_files
    move_wheel_files(
  File "/usr/lib/python3/dist-packages/pip/wheel.py", line 245, in move_wheel_files
    scheme = distutils_scheme(
  File "/usr/lib/python3/dist-packages/pip/locations.py", line 153, in distutils_scheme
    i.finalize_options()
  File "/usr/lib/python3.8/distutils/command/install.py", line 274, in finalize_options
    raise DistutilsOptionError("can't combine user with prefix, "
distutils.errors.DistutilsOptionError: can't combine user with prefix, exec_prefix/home, or install_(plat)base

According to the interwebs this is because something is causing pip so perform a --user install, which does not combine with --target. I couldn't quite figure out if this (the user install) is an option that is set by Ubuntu and if I could disable it.

Apologies if you think this is not a kani issue.

Kani version: 0.1.0

[tedinski]

I'm going to guess it's a platform/os issue.

I notice /usr/lib/python3 and /usr/lib/python3.8. Could this be multiple versions of python conflicting? Maybe something related to how you got 3.8 installed on 18.04? (e.g. maybe that install package tries to force --user to avoid installing anything globally and conflicting with global python?)

[tedinski]

FWIW, the next release of Kani should use a newer version of viewer which relaxes python back to 3.6, and so it would work without needing a newer python package. If you can wait a week for that next release, it's probably the simplest fix!

(That said, if there's a way we can work around python packages forcing --user so we can use --prefix... we'd happily incorporate that too...)

[JustusAdam]

If you can wait a week for that next release, it's probably the simplest fix!

I'm currently trying the source install instead to deal with this. Btw during the source install it worked fine.

I'm not really sure how it could be because of the different pythons, but that said I did have to revert it for the source install so it might make sense to just wait it out for the next release and see if it fixes itself.

[zhassan-aws]

This seems to be a known issue on some OS: https://stackoverflow.com/questions/4495120/combine-user-with-prefix-error-with-setup-py-install
A suggested workaround is provided in the SO thread.

[zhassan-aws]

I reproduced the same error on a fresh 18.04 AWS instance with Kani version 0.2.