Lean: Adding a lean_force_output option (#805)

If this option is used, and the project directory already exists,
the project directory is emptied before creating the project files

Otherwise, mkdir is used to create the project directory (and will fail if the directory already exists, and the option is not used.)

src/sail_lean_backend/sail_plugin_lean.ml

@@ -71,6 +71,8 @@ open Interactive.State
 
 let opt_lean_output_dir : string option ref = ref None
 
+let opt_lean_force_output : bool ref = ref false
+
 let lean_version : string = "lean4:nightly-2024-09-25"
 
 let lean_options =
@@ -79,6 +81,10 @@ let lean_options =
       Arg.String (fun dir -> opt_lean_output_dir := Some dir),
       "<directory> set a custom directory to output generated Lean"
     );
+    ( "-lean_force_output",
+      Arg.Unit (fun () -> opt_lean_force_output := true),
+      " removes the content of the output directory if it is non-empty"
+    );
   ]
 
 (* TODO[javra]: Currently these are the same as the Coq rewrites, we might want to change them. *)
@@ -151,7 +157,11 @@ let create_lake_project (out_name : string) default_sail_dir =
   (* Change the base directory if the option '--lean-output-dir' is set *)
   let base_dir = match !opt_lean_output_dir with Some dir -> dir | None -> "." in
   let project_dir = Filename.concat base_dir out_name in
-  Unix.mkdir project_dir 0o775;
+  if !opt_lean_force_output && Sys.is_directory project_dir then (
+    let _ = Unix.system ("rm -r " ^ project_dir ^ "/*") in
+    ()
+  )
+  else Unix.mkdir project_dir 0o775;
   let gitignore = open_out (Filename.concat project_dir ".gitignore") in
   (* Ignore the `z3_problems` file generated by Sail and the `.lake` directory generated by lake*)
   output_string gitignore "/.lake";