Add command cargo creusot clean

cargo-creusot/src/main.rs

@@ -3,7 +3,8 @@ use creusot_args::{options::*, CREUSOT_RUSTC_ARGS};
 use creusot_setup as setup;
 use std::{
     env,
-    path::PathBuf,
+    io::Write,
+    path::{Display, PathBuf},
     process::{exit, Command},
 };
 use tempdir::TempDir;
@@ -62,6 +63,7 @@ fn main() -> Result<()> {
         }
         Some(New(args)) => new(args),
         Some(Init(args)) => init(args),
+        Some(Clean(args)) => clean(args),
     }
 }
 
@@ -100,6 +102,7 @@ fn creusot(
     };
 
     invoke_cargo(&creusot_args, creusot_rustc, cargo_flags);
+    warn_if_dangling()?;
 
     if let Some((mode, coma_src, args)) = launch_why3 {
         let mut coma_files = vec![coma_src];
@@ -230,6 +233,8 @@ pub enum CargoCreusotSubCommand {
     New(NewArgs),
     /// Create new project in current directory
     Init(InitArgs),
+    /// Clean dangling files in verif/
+    Clean(CleanArgs),
 }
 use CargoCreusotSubCommand::*;
 
@@ -263,3 +268,148 @@ fn default_provers_parallelism() -> usize {
         Err(_) => 1,
     }
 }
+
+/// Arguments for `cargo creusot clean`.
+#[derive(Debug, Parser)]
+pub struct CleanArgs {
+    /// Remove dangling files without asking for confirmation.
+    #[clap(long)]
+    force: bool,
+    /// Do not remove any files, only print what would be removed.
+    #[clap(long, conflicts_with = "force")]
+    dry_run: bool,
+}
+
+const OUTPUT_PREFIX: &str = "verif";
+
+/// Remove dangling files in `verif/`
+fn clean(options: CleanArgs) -> Result<()> {
+    let dangling = find_dangling(&PathBuf::from(OUTPUT_PREFIX))?;
+    if dangling.is_empty() {
+        eprintln!("No dangling files found");
+        return Ok(());
+    }
+    if !options.force {
+        // Ask for confirmation
+        eprintln!("The following files and directories will be removed:");
+        for path in &dangling {
+            eprintln!("  {}", path.display());
+        }
+        if options.dry_run {
+            return Ok(());
+        }
+        eprint!("Do you want to proceed? [y/N] ");
+        std::io::stderr().flush()?;
+        let mut input = String::new();
+        std::io::stdin().read_line(&mut input)?;
+        if !input.trim().eq_ignore_ascii_case("y") {
+            return Ok(());
+        }
+    }
+    for path in dangling {
+        path.remove()?;
+    }
+    Ok(())
+}
+
+/// Print a warning if there are dangling files in `verif/`
+fn warn_if_dangling() -> Result<()> {
+    let dangling = find_dangling(&PathBuf::from(OUTPUT_PREFIX))?;
+    if !dangling.is_empty() {
+        eprintln!("Warning: found dangling files and directories:");
+        for path in dangling {
+            eprintln!("  {}", path.display());
+        }
+        eprintln!("Run 'cargo creusot clean' to remove them");
+    }
+    Ok(())
+}
+
+enum FileOrDirectory {
+    File(PathBuf),
+    Directory(PathBuf),
+}
+
+use FileOrDirectory::*;
+
+impl FileOrDirectory {
+    fn display(&self) -> Display<'_> {
+        match self {
+            File(path) => path.display(),
+            Directory(path) => path.display(),
+        }
+    }
+
+    fn remove(&self) -> std::io::Result<()> {
+        match self {
+            File(path) => std::fs::remove_file(&path),
+            Directory(path) => std::fs::remove_dir_all(&path),
+        }
+    }
+}
+
+/// Find dangling files in directory `dir`: files named `why3session.xml`, `why3shapes.gz`, and `proof.json`
+/// that are not associated with a `.coma` file.
+fn find_dangling(dir: &PathBuf) -> Result<Vec<FileOrDirectory>> {
+    if !dir.is_dir() {
+        return Ok(Vec::new());
+    }
+    match find_dangling_rec(dir)? {
+        None => Ok(vec![Directory(dir.clone())]),
+        Some(dangling) => Ok(dangling),
+    }
+}
+
+/// Find dangling files in directory `dir`.
+/// Return `None` if the directory `dir` contains only dangling files,
+/// otherwise there must be some non-dangling files in `dir`, return `Some` of only the dangling files and subdirectories.
+/// Assumes `dir` exists and is a directory.
+fn find_dangling_rec(dir: &PathBuf) -> Result<Option<Vec<FileOrDirectory>>> {
+    let mut all_dangling = true;
+    let mut dangling = Vec::new();
+    let mut has_coma = None; // whether the file "{dir}.coma" exists; only check if needed.
+    for entry in std::fs::read_dir(dir)? {
+        let entry = entry?;
+        let file_type = entry.file_type()?;
+        let path = entry.path();
+        if file_type.is_dir() {
+            match find_dangling_rec(&path)? {
+                Some(more_dangling) => {
+                    dangling.extend(more_dangling);
+                    all_dangling = false;
+                }
+                None => dangling.push(Directory(path)),
+            }
+        } else if file_type.is_file() {
+            let file_name = entry.file_name();
+            if [
+                "proof.json",
+                "why3session.xml",
+                "why3shapes.gz",
+                "why3session.xml.bak",
+                "why3shapes.gz.bak",
+            ]
+            .contains(&file_name.to_str().unwrap())
+            {
+                if has_coma.is_none() {
+                    has_coma = Some(dir.with_extension("coma").exists());
+                }
+                if has_coma == Some(false) {
+                    dangling.push(File(path));
+                } else {
+                    all_dangling = false;
+                }
+            } else {
+                all_dangling = false;
+            }
+        } else {
+            // Don't touch symlinks (if they exist maybe there's a good reason)
+            all_dangling = false;
+        }
+    }
+    if all_dangling {
+        Ok(None)
+    } else {
+        Ok(Some(dangling))
+    }
+}

guide/src/SUMMARY.md

@@ -20,3 +20,4 @@
   - [Ghost structures](ghost/ghost-structures.md)
   - [`Int` in ghost](ghost/int-in-ghost.md)
 - [Type invariants](./type_invariants.md)
+- [Command-line interface](./command_line_interface.md)

guide/src/command_line_interface.md

@@ -0,0 +1,135 @@
+# Command-line Interface
+
+## List of commands
+
+- [`cargo creusot`](#creusot)
+- [`cargo creusot prove`](#prove)
+- [`cargo creusot doc`](#doc)
+- [`cargo creusot clean`](#clean)
+- [`cargo creusot new`](#new)
+- [`cargo creusot init`](#init)
+- [`cargo creusot config`](#config)
+- [`cargo creusot setup install`](#setup-install)
+- [`cargo creusot setup status`](#setup-status)
+
+## Main commands
+
+### `creusot`
+
+```
+cargo creusot [-- [-p <CRATE>]]
+```
+
+Run the Creusot compiler.
+
+Output Coma code in the `verif/` directory.
+
+#### Options
+
+- `-p <CRATE>`: Compile a specific crate `<CRATE>` in a multi-crate project.
+
+### `prove`
+
+```
+cargo creusot prove [-i] [<COMA_FILE>]
+```
+
+Verify contracts.
+
+This first runs `cargo creusot` to be sure that the compiled code is up-to-date.
+Then `why3find` verifies the compiled Coma code: it generates verification conditions
+and tries to prove them.
+
+#### Options
+
+- `-i`: Open the Why3 IDE on an unproved file to inspect its proof context.
+- `<COMA_FILE>`: Verify a specific file (corresponding to one Rust function).
+
+### `doc`
+
+```
+cargo creusot doc
+```
+
+Build documentation.
+
+This is a variant of `cargo doc` that also renders contracts (`requires` and `ensures`), logic functions, and predicates.
+
+
+### `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`.
+
+## Create package
+
+### `new`
+
+```
+cargo creusot new <NAME> [--main]
+```
+
+Create package named `<NAME>`.
+
+Create a directory `<NAME>` and initialize it with starting configuration and source files.
+
+#### Options
+
+- `--main`: Create `main.rs` for an executable crate. (By default, only a library crate `lib.rs` is created.)
+
+### `init`
+
+```
+cargo creusot init [<NAME>] [--main]
+```
+
+Create package in the current directory.
+
+#### 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.)
+
+### `config`
+
+```
+cargo creusot config
+```
+
+Generate `why3find` configuration.
+
+This is used to set up Creusot in an existing Rust package.
+You don't need to run this command if you used `cargo creusot new` or `cargo creusot init`.
+
+## Install Creusot
+
+### `setup install`
+
+```
+cargo creusot setup install
+```
+
+See the [README](https://github.com/creusot-rs/creusot) for installation instructions.
+
+### `setup status`
+
+```
+cargo creusot setup status
+```
+
+Show the status of the Creusot installation.
+
+Print tool locations and configuration paths.