From b2d682566119749ab77f077c00a17d8918bdcb8a 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] 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 | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/sail_lean_backend/sail_plugin_lean.ml b/src/sail_lean_backend/sail_plugin_lean.ml index 4880dbcc0..feb21a8dd 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,6 +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 + 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*)