Command-line Interface

List of commands

• cargo creusot
• cargo creusot doc
• cargo creusot clean
• cargo creusot why3 ide
• cargo creusot new
• cargo creusot init
• cargo creusot config
• cargo creusot version

Main commands

creusot

cargo creusot
  [-p <PACKAGE>] [--only=(coma|prove)]
  [--erasure-check]
  <PATTERN>* [-i|--ide-on-fail|--ide-always]
  [--replay] [--why3session] [--why3find-arg <ARG>] [--dry-run-why3find]
  [-- <CARGO_OPTIONS>]

Run Creusot: compile to Coma (into the verif/ directory) and run provers on verification conditions (using Why3find).

Creusot options

• -p <PACKAGE>: Only build <PACKAGE> (in multi-package workspaces). By default, all default members of a workspace are built, determined by one of the following configurations, in decreasing order of priority:

  • the default-members field of [workspace.metadata.creusot] in Cargo.toml

    [workspace.metadata.creusot]
    default-members = ["package1", "package2"]
    

  • the default-members field of [workspace] in Cargo.toml

    [workspace]
    default-members = ["package1", "package2"]
    

  • if neither of these fields exists, then the default members are—as defined by Cargo—either just the root package, if it exists, or all members of the workspace.

  Within a package, Creusot only compiles libraries and binaries. Tests, examples, and benches are currently unsupported. (Please reach out if you need this feature!)

• --erasure-check: Report #[erasure] check failures as errors; see Erasure check.

  • --erasure-check=no: Disable #[erasure] checks.
  • --erasure-check=warn (default): Report #[erasure] check failures as warnings.

• --only=coma: Only typecheck and compile to Coma, no provers.

• --only=prove: Only run provers without compiling to Coma (your Coma files may be out of date!).

Prover-specific options

• <PATTERN>: Select Coma files that match one of the patterns. If no patterns are provided, prove all files in selected packages (-p). Example patterns: name, name::*, m/*/f. Separators can be written as :: or /.
• -i, --ide-on-fail: Open the Why3 IDE on an unproved file to inspect its proof context.
• --ide-always: Open the Why3 IDE on a single Coma file regardless of whether the proof succeeded. The command fails if <PATTERN> does not match exactly one file.
• --replay: Don’t generate new proofs, only check if the existing proofs are valid.
• --why3session: Generate why3session.xml files (implied by -i and --ide-always).
• --why3find-arg <ARG>: pass <ARG> directly as an extra argument to why3find prove. Repeat this to pass multiple arguments.
• --dry-run-why3find: Print the why3find command without running it.

Cargo options

All options after -- are forwarded to cargo. Here is a selection of useful ones for Creusot users:

• -Zbuild-std: Recompile crates core, std, alloc, proc-macro. (Useful for --erasure-check.)

doc

cargo creusot doc

Build documentation.

This is a variant of cargo doc that also renders contracts (requires and ensures) and logic functions.

clean

cargo creusot clean [--force] [--dry-run]

Remove dangling proof files.

Removing (or renaming) Rust functions also removes (or renames) its compiled Coma file. However, the Creusot compiler can’t keep track of their associated proof files (proof.json, why3session.xml), which become dangling. cargo creusot will detect dangling files and print a warning to remind you to move those files if you want, otherwise you can remove them with cargo creusot clean.

Options

• --force: Don’t ask for confirmation before removing dangling files.
• --dry-run: Only print the list of files that would be removed by cargo creusot clean.

why3 ide

cargo creusot why3 ide <COMA_FILE|why3session.xml>

Run the Why3 IDE on a Coma file or a why3session.xml. This commands simply invokes why3 ide with the required options to load Coma files produced by Creusot.

This is a command for experts and for troubleshooting. In normal usage, prefer cargo creusot with -i or --ide-always, which ensures that the Coma artifacts are always up to date.

Create and maintain package

new

cargo creusot new <NAME> [--main] [--tests] [--no-std] [--creusot-path <PATH>]

Create or update package named <NAME>.

Create directory <NAME> if it doesn’t already exist, and run cargo creusot init inside it.

Options

• --main: Create main.rs for an executable crate. (By default, only a library crate lib.rs is created.)
• --creusot-path <PATH>: Path to local creusot repository, used to find dev versions of creusot-std, creusot-std-proc, and pearlite-syn.
  • This creates a symlink creusot pointing to <PATH> in the newly created project, and a file .cargo/config.toml that points to creusot/creusot-std, going through that symlink to find creusot-std (and thus the other crates as well).
  • This option has a default value so you shouldn’t need to set this normally.
    • For non-Nix installations, this defaults to a path hard-coded during the compilation of cargo-creusot, so it should work as long as you didn’t move it.
    • In a Nix shell, this option is set via the environment variable CREUSOT_PATH.
  • This option is ignored in released versions of Creusot.

init

cargo creusot init [<NAME>] [--main]

Create or update package in the current directory.

If Cargo.toml doesn’t exist, create a new package with starting configuration and source files.

If Cargo.toml exists, update an existing package for verification with Creusot:

• add or update creusot-std in the list of dependencies with the version matching your Creusot installation;

  For released versions of Creusot, this is equivalent to cargo add creusot-std@<VERSION> just with the right version.

  For a development version of Creusot (prerelease version -dev), this also creates .cargo/config.toml with these contents:

  [patch.crates-io]
  creusot-std = { path = "creusot/creusot-std" }
  

  and a creusot symlink to the Creusot repository.

  The [patch.crates-io] setting is documented in The Cargo Book: Overriding Dependencies.

• add why3find.json if it doesn’t exist.

Options

• <NAME>: Name of the package. (By default, it is the name of the directory.)
• --main: Create main.rs for an executable crate. (By default, only a library crate lib.rs is created.)
• --creusot-path <PATH>: Path to local creusot repository.

Configuration

config

cargo creusot config [--update]

For users of the dev version of Creusot (master branch): configure ~/.cargo/config.toml to point to the local version of creusot-std. Or if you are upgrading from a dev version to a released version (vX.Y.Z tag), undo that configuration, so that you can use creusot-std from crates.io.

Options

• --update: Update ~/.cargo/config.toml (default is to only check it).

version

cargo creusot version

Print version of Creusot and accompanying tools.