Interrupted first-time setup procedure cannot resume

[waynexia]

I tried these commands:

Install kani with cargo install kani-verifier and run kani --help

$ kani --help                 
[0/6] Running Kani first-time setup...
[1/6] Ensuring the existence of: /home/wayne/.kani/kani-0.8.0
[2/6] Downloading Kani release bundle: kani-0.8.0-x86_64-unknown-linux-gnu.tar.gz
^C

then kill it with Ctrl C. And re-run kani --help got:

$ kani --help
Error: Failed to invoke kani-driver

Caused by:
    No such file or directory (os error 2)

The content in ~/.kani:

$ ll ~/.kani/
total 1004K
drwxr-xr-x 1 wayne wayne     0 Aug 18 22:59 kani-0.8.0
-rw-r--r-- 1 wayne wayne 1004K Aug 18 23:00 kani-0.8.0-x86_64-unknown-linux-gnu.tar.gz

After removing the content in ~/.kani it goes normal

$ rm -r ~/.kani/*

$ kani --help                 
[0/6] Running Kani first-time setup...
[1/6] Ensuring the existence of: /home/wayne/.kani/kani-0.8.0
[2/6] Downloading Kani release bundle: kani-0.8.0-x86_64-unknown-linux-gnu.tar.gz

with Kani version: v0.8.0

I expected to see this happen: kani can recognize the setup procedure is not finished and keep on setting things up.

Logs with backtrace:

$ RUST_BACKTRACE=1 kani --help
Error: Failed to invoke kani-driver

Caused by:
    No such file or directory (os error 2)

Stack backtrace:
   0: kani_verifier::proxy
   1: std::sys_common::backtrace::__rust_begin_short_backtrace
   2: std::rt::lang_start::{{closure}}
   3: std::rt::lang_start_internal
   4: main
   5: <unknown>
   6: __libc_start_main
   7: _start

I guess this is because the tarball's download hasn't finished. Maybe verifying the checksum or downloading it to a temporary filename before finishing can solve this?

[tedinski]

Thanks for the bug report. I cut a corner in this setup procedure, but also don't think I created a tracking issue for it, so this is now it. :)

It's assuming if the directory exists, setup was completed successfully. Which, of course, isn't true.

Workaround: Just running cargo kani setup explicitly again should also work. Or as you discovered, removing the directory and trying again will work.

We should fix the "are things already setup?" check. Possibly as simple as creating a "success" marker file as the last step of setup, though I'm very open to other ideas. It happens every time kani or cargo-kani are invoked, so it's got to be a cheap check.

[danielsn]

Perhaps the "success" file should be tagged to the installed version/os/etc?

[waynexia]

Workaround: Just running cargo kani setup explicitly again should also work. Or as you discovered, removing the directory and trying again will work.

Thanks for this!

Possibly as simple as creating a "success" marker file as the last step of setup

How about doing all the jobs in other dir, and mv that dir to the actual one in the end. Like cargo will download tarball into a tmp dir like ~/.rustup/tmp/. I see all the setup operations are using kani_dir from

kani/src/setup.rs

Line 36 in cf76024

let kani_dir = kani_dir();

And this doesn't need extra checks on invoking :D

Perhaps the "success" file should be tagged to the installed version/os/etc?

The dir contains version number (e.g kani-0.8.0), maybe this is enough I think?

[tedinski]

How about doing all the jobs in other dir, and mv that dir to the actual one in the end.

I like this idea, though I'm maybe slightly worried about how rustc might embed (absolute) paths into the kani libraries we build. There might be another solution to this problem though.

It'd also have the advantage of perhaps unifying the two code paths we have there for unpacking the tarball: one for testing and one "for real." The less these diverge the better.

[waynexia]

though I'm maybe slightly worried about how rustc might embed (absolute) paths

Library like tempfile perhaps helps, or we can operate under ~/.kani/temp to avoid hardcoding outer paths into kani.

unifying the two code paths we have there for unpacking the tarball

Do you mean this --use-local-bundle option?