This Visual Studio Code extension provides interactive IDE features for verifying Rusti programs with the Prusti verifier.
For advanced use cases, consider switching to the command-line version of Prusti.
In order to use this extension, please install the following components:
- Java JDK version 11 or later, 64 bit. We recommend OpenJDK 15.0.1.
- Rustup version 1.23.0 or later (on Windows this also requires the C++ build tools for Visual Studio 2013 or later).
- Install the requirements (listed above) and restart the IDE.
- This will ensure that programs like
rustup
are in the program path used by the IDE.
- This will ensure that programs like
- Install the "Prusti Assistant" extension.
- Open a Rust file to activate the extension.
- At its first activation, this extension will automatically download Prusti and install the required Rust toolchain.
- Click on the "Verify with Prusti" button in the status bar.
- Alternativelly, you can run the
Prusti: verify the current crate or file
command. - If the program is in a folder with a
Cargo.toml
file, Prusti will verify the crate in which the file is contained. - If no
Cargo.toml
file can be found in a parent folder of the workspace, Prusti will verify the file as a standalone Rust program. No Cargo dependencies are allowed in this mode.
- Alternativelly, you can run the
- Follow the progress from the status bar.
- You should see a "Verifying crate [folder name]" or "Verifying file [name]" message while Prusti is running.
- The result of the verification is reported in the status bar and in the "Problems" tab.
- You can open the "Problems" tab by clicking on Prusti's status bar.
- Be aware that the "Problems" tab is shared by all extensions. If you are not sure which extension generated which error, try disabling other extensions. (Related VS Code issue: #51103.)
To update Prusti, run the command Prusti: update verifier
in the command palette.
If something fails, check the "Troubleshooting" section below.
This extension provides the following commands:
Prusti: verify the current crate or file
to verify a Rust program;Prusti: update verifier
to update Prusti.Prusti: restart Prusti server
to restart the Prusti server used by this extension.
The main configuration options used by this extension are the following:
prusti-assistant.verifyOnSave
: Specifies if programs should be verified on save.prusti-assistant.verifyOnOpen
: Specifies if programs should be verified when opened.prusti-assistant.buildChannel
: Allows to choose between the latest Prusti release version (the default) and a slightly newer but potentially unstable Prusti development version.prusti-assistant.checkForUpdates
: Specifies if Prusti should check for updates at startup.
This extension automatically provides inline diagnostics for Prusti errors.
Basic code-completion snippets are provided for Prusti annotations.
If Prusti fails to run, you can inspect Prusti's log from VS Code (View -> Output -> Prusti Assistant ...) and see if one of the following solutions applies to you.
Problem | Solution |
---|---|
error[E0514]: found crate 'cfg_if' compiled by an incompatible version of rustc |
There is a conflict between Prusti and a previous Cargo compilation. Run cargo clean or manually delete the target folder. Then, rerun Prusti. |
error: the 'cargo' binary, normally provided by the 'cargo' component, is not applicable to the 'nightly-2021-09-20-x86_64-unknown-linux-gnu' toolchain or error[E0463]: can't find crate for std or error[E0463]: can't find crate for core |
The Rust toolchain installed by Rustup is probably corrupted (see issue rustup/#2417). Uninstall the nightly toolchain mentioned in the error (or all installed nightly toolchains). Then, rerun Prusti. |
Thanks to @Pointerbender for reporting issues and suggesting solutions!