Skip to content

Installing Kani prints an ERROR even though it succeeds #2709

Description

@celinval

I tried running on Ubuntu 20.04:

cargo install --locked kani-verifier
kani setup

with Kani version: 0.35.0

I expected to see this happen: Setup should succeed and no error be printed

Instead, this happened: During installation, the following error message is printed:

ERROR: launchpadlib 1.10.13 requires testresources, which is not installed.

however, Kani is successfully installed

Full logs:

[0/5] Running Kani first-time setup...
[1/5] Ensuring the existence of: /home/ubuntu/.kani/kani-0.35.0
[2/5] Downloading Kani release bundle: kani-0.35.0-x86_64-unknown-linux-gnu.tar.gz
[3/5] Installing rust toolchain version: nightly-2023-08-19-x86_64-unknown-linux-gnu
info: syncing channel updates for 'nightly-2023-08-19-x86_64-unknown-linux-gnu'
info: latest update on 2023-08-19, rust version 1.73.0-nightly (d06ca0ffa 2023-08-18)
info: downloading component 'cargo'
info: downloading component 'clippy'
info: downloading component 'rust-docs'
info: downloading component 'rust-std'
info: downloading component 'rustc'
info: downloading component 'rustfmt'
info: installing component 'cargo'
info: installing component 'clippy'
info: installing component 'rust-docs'
 13.8 MiB /  13.8 MiB (100 %)   7.9 MiB/s in  1s ETA:  0s
info: installing component 'rust-std'
 24.2 MiB /  24.2 MiB (100 %)  12.1 MiB/s in  1s ETA:  0s
info: installing component 'rustc'
 61.5 MiB /  61.5 MiB (100 %)  14.2 MiB/s in  4s ETA:  0s
info: installing component 'rustfmt'

  nightly-2023-08-19-x86_64-unknown-linux-gnu installed - rustc 1.73.0-nightly (d06ca0ffa 2023-08-18)

info: checking for self-update
[4/5] Installing Kani python dependencies...
Collecting cbmc-viewer==3.8
  Using cached cbmc_viewer-3.8-py3-none-any.whl (71 kB)
Collecting setuptools
  Downloading setuptools-68.1.2-py3-none-any.whl (805 kB)
     |████████████████████████████████| 805 kB 5.4 MB/s 
Collecting jinja2
  Using cached Jinja2-3.1.2-py3-none-any.whl (133 kB)
Collecting voluptuous
  Using cached voluptuous-0.13.1-py3-none-any.whl (29 kB)
Collecting MarkupSafe>=2.0
  Using cached MarkupSafe-2.1.3-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (25 kB)
ERROR: launchpadlib 1.10.13 requires testresources, which is not installed.
Installing collected packages: setuptools, MarkupSafe, jinja2, voluptuous, cbmc-viewer
Successfully installed MarkupSafe-2.1.3 cbmc-viewer-3.8 jinja2-3.1.2 setuptools-68.1.2 voluptuous-0.13.1
[5/5] Successfully completed Kani first-time setup.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    [C] BugThis is a bug. Something isn't working.

    Type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions