From 1c4d6f792335537f3e745f5d6a93a8e75c7b4d4e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 3 Dec 2024 15:11:12 +0000 Subject: [PATCH 1/2] Lean: Adding a lean_force_output option 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 | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/sail_lean_backend/sail_plugin_lean.ml b/src/sail_lean_backend/sail_plugin_lean.ml index 4880dbcc0..a60771452 100644 --- a/src/sail_lean_backend/sail_plugin_lean.ml +++ b/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), " 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"; From a49290f9630e94a4077a682bb1db3f530a92bb0d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9on=20Frenot?= Date: Tue, 3 Dec 2024 17:12:10 +0000 Subject: [PATCH 2/2] Missed space to properly print the help message --- src/sail_lean_backend/sail_plugin_lean.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sail_lean_backend/sail_plugin_lean.ml b/src/sail_lean_backend/sail_plugin_lean.ml index a60771452..007b999f5 100644 --- a/src/sail_lean_backend/sail_plugin_lean.ml +++ b/src/sail_lean_backend/sail_plugin_lean.ml @@ -83,7 +83,7 @@ let lean_options = ); ( "-lean_force_output", Arg.Unit (fun () -> opt_lean_force_output := true), - "removes the content of the output directory if it is non-empty" + " removes the content of the output directory if it is non-empty" ); ]