Creusot IDE

A VS Code extension providing support for Creusot, a deductive verifier for Rust code.
This project is work in progress. An official release is upcoming.
Features
Creusot IDE helps you nagivate between your Rust sources and the verification artifacts generated by Creusot and Why3find.
- Run and inspect proofs from within the editor.
- Functions with proof obligations will have a button in the gutter to their left.
Click to run the prover (
why3find prove
).
Alt+click to start Why3 IDE (only if the prover fails).
- Diagnostics underline locations with failed proofs
- Syntax highlighting:
.rs
files: Creusot-specific attributes and Pearlite expressions,
.coma
files.
Install Creusot IDE
Creusot itself should be installed separately.
Creusot IDE consists of two parts:
The Creusot IDE extension, installed via VS Code: open VS Code > Extensions > Search "Creusot IDE".
The Creusot LSP language server, which must currently be installed separately:
First, install Creusot, Why3, and Why3find; see https://github.com/creusot-rs/creusot for instructions
git clone https://github.com/creusot-rs/creusot-ide
The installation location is the Creusot-local switch, which depends on your OS.
On Linux:
opam pin --switch=~/.local/share/creusot creusot-lsp creusot-ide/ -y
On MacOS:
opam pin --switch=~/.creusot creusot-lsp creusot-ide/ -y
At the moment, installing creusot-lsp
in another switch or without opam altogether is not supported.
Additional configuration / Known issues
Rust analyzer doesn't know how to parse Creusot specifications (attributes such as ensures
, etc.),
so they are underlined in red.
Add this option in settings.json
to run Creusot for checks instead:
"rust-analyzer.check.overrideCommand": [
"cargo",
"creusot",
"--",
"--message-format=json"
]
Rust analyzer overrides Creusot IDE's syntax highlighting by emitting semantic tokens inside
attributes and macros.
Disable semantic tokens: Settings (Ctrl+P
› Preferences: Open Settings (UI)) › Editor › Semantic Highlighting: Enabled › false
Commands
Available in the command palette (Ctrl+P
):
- Restart language server
- Stop language server
Settings
creusot.lspPath
: Path to the creusot-lsp
executable. Default: ""
, finding the executable in Creusot's Opam switch.
creusot.home
, creusot.dataHome
, creusot.configHome
: Override the environment variables HOME
, XDG_DATA_HOME
, and XDG_CONFIG_HOME
when invoking Creusot. This allows running Creusot from VS Code and other applications installed via Ubuntu Snap, which sets those variables to some custom directories, breaking Creusot. On Linux you probably want to set these paths:
creusot.home
: /home/$USER
(where $USER
is your user name)
creusot.dataHome
: /home/$USER/.local/share
(there should be a creusot
directory at this location)
creusot.configHome
: /home/$USER/.config
(there should be a creusot
directory at this location)
Developers' corner
To build and install the VS Code extension from source:
npx vsce package
Then, in VS Code: Command Palette > Install from VSIX. Select the creusot-ide-X.Y.Z.vsix
file created by the previous command.