Emit an error if Kani executable was not found

[zhassan-aws]

Description of changes:

Check if which cargo-kani returned an error, abort execution, and set the test result as "errored". This is what gets shown in VSCode:

Resolved issues:

Resolves #72

Related RFC:

Optional #ISSUE-NUMBER.

Call-outs:

A cleaner approach would be to check on load if Kani is installed, and if not put the extension in an error state and prevent running any harnesses.

Testing:

• How is this change tested? Removed kani from path, launched extension, and ran one of the harnesses.

• Is this a refactor change?

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[jaisnan]

The changes look great! I do think the cleaner solution can be added easily as well on top of these changes. It should be simple to implement as we already do exactly the same, with cargo here - https://github.com/model-checking/kani-vscode-extension/blob/15c27c756b029833d126d12b4032b9c5aa1e6175/src/extension.ts#LL34C3-L34C3.

[jaisnan]

Could I ask if you could add a screenshot of what the end result looks like visually? And also what underlying environment conditions allowed you to trigger the issue (i.e what was the cargo-kani path in your case). Any information on how it was tested would be helpful to me.

Thanks!

[zhassan-aws]

Could I ask if you could add a screenshot of what the end result looks like visually? And also what underlying environment conditions allowed you to trigger the issue (i.e what was the cargo-kani path in your case). Any information on how it was tested would be helpful to me.

I added a script to the PR description as well as how I tested it. In my case, I removed kani from the PATH environment variable, which causes which cargo-kani to exit with an error status.

[jaisnan]

Could I ask if you could add a screenshot of what the end result looks like visually? And also what underlying environment conditions allowed you to trigger the issue (i.e what was the cargo-kani path in your case). Any information on how it was tested would be helpful to me.

I added a script to the PR description as well as how I tested it. In my case, I removed kani from the PATH environment variable, which causes which cargo-kani to exit with an error status.

Thanks for the description. The final change looks great too.

[zhassan-aws]

I do think the cleaner solution can be added easily as well on top of these changes. It should be simple to implement as we already do exactly the same, with cargo here

I couldn't get this approach to work. My approach is in this branch. With those changes, an error is popped-up as the extension was loading:

but the extension still activated and running any harness leads causes the wheel to keep spinning forever.

[jaisnan]

Thanks!