From dfdc2851a71a789252f2b951ce87ecf0d276009d Mon Sep 17 00:00:00 2001
From: Li-yao Xia <lysxia@gmail.com>
Date: Wed, 11 Dec 2024 15:07:52 +0100
Subject: [PATCH] Clean verif/ directory before writing to it

---
 creusot/src/translation.rs | 25 ++++++++++++++++++++++++-
 1 file changed, 24 insertions(+), 1 deletion(-)

diff --git a/creusot/src/translation.rs b/creusot/src/translation.rs
index 147bca8266..51323bda63 100644
--- a/creusot/src/translation.rs
+++ b/creusot/src/translation.rs
@@ -191,13 +191,36 @@ fn monolithic_output<T: Write>(modl: &FileModule, out: &mut T) -> std::io::Resul
     Ok(())
 }
 
+// Remove coma files in the `verif/` directory to avoid obsolete files left after
+// (re)moving functions in source code.
+// We don't want to just `remove_dir_all()` because it may contain
+// `proof.json`, `why3session.xml`, and `why3shapes.xml` files that users want to preserve.
+fn remove_coma_files(dir: &PathBuf) -> std::io::Result<()> {
+    if dir.exists() {
+        for entry in std::fs::read_dir(dir)? {
+            let entry = entry?;
+            let path = entry.path();
+            if path.is_dir() {
+                remove_coma_files(&path)?;
+                let _ = std::fs::remove_dir(path); // remove the directory if it's empty, do nothing otherwise
+            } else if path.extension().map_or(false, |ext| ext == "coma") {
+                std::fs::remove_file(&path)?;
+            }
+        }
+    }
+    Ok(())
+}
+
 fn print_crate<I: Iterator<Item = FileModule>>(
     output_target: Output,
     prefix: Vec<why3::Ident>,
     modules: I,
 ) -> std::io::Result<Option<PathBuf>> {
     let (root, mut output) = match output_target {
-        Output::Directory(dir) => (Some(dir.clone()), OutputHandle::Directory(dir, prefix)),
+        Output::Directory(dir) => {
+            remove_coma_files(&dir)?;
+            (Some(dir.clone()), OutputHandle::Directory(dir, prefix))
+        }
         Output::File(ref f) => {
             std::fs::create_dir_all(f.parent().unwrap()).unwrap();
             (