Lean: Make --lean calls create an empty lake project (#724)

* make --lean calls create an empty lake project

* coding style, avoid Sys.mkdir, avoid chdir

* use Filename.concat instead of adding '/'

* fix filepaths, .gitignore

* prune comments

src/lib/util.ml

@@ -592,3 +592,8 @@ let close_output_with_check (o, temp_file_name, opt_dir, file_name) =
   let do_replace = !always_replace_files || not (same_content_files temp_file_name file_name) in
   let _ = if not do_replace then Sys.remove temp_file_name else move_file temp_file_name file_name in
   ()
+
+let to_upper_camel_case s =
+  let ss = String.split_on_char '_' s |> List.map (String.split_on_char '-') |> List.concat in
+  let ss = List.map String.capitalize_ascii ss in
+  String.concat "" ss

src/lib/util.mli

@@ -335,3 +335,5 @@ val open_output_with_check :
 val open_output_with_check_unformatted : string option -> string -> out_channel * string * string option * string
 
 val close_output_with_check : out_channel * string * string option * string -> unit
+
+val to_upper_camel_case : string -> string

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 lean_version : string = "lean4:nightly-2024-09-25"
+
 let lean_options =
   [
     ( "-lean_output_dir",
@@ -145,10 +147,37 @@ let lean_rewrites =
     ("attach_effects", []);
   ]
 
-let output files = failwith "Lean backend not yet implemented"
+let create_lake_project (out_name : string) =
+  (* 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;
+  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";
+  close_out gitignore;
+  let lean_toolchain = open_out (Filename.concat project_dir "lean-toolchain") in
+  (* Set the Lean version *)
+  output_string lean_toolchain ("leanprover/" ^ lean_version);
+  close_out lean_toolchain;
+  (* Camel-case the output name *)
+  let out_name_camel = Libsail.Util.to_upper_camel_case out_name in
+  let lakefile = open_out (Filename.concat project_dir "lakefile.toml") in
+  output_string lakefile
+    ("name = \"" ^ out_name ^ "\"\ndefaultTargets = [\"" ^ out_name_camel ^ "\"]\n\n[[lean_lib]]\nname = \""
+   ^ out_name_camel ^ "\""
+    );
+  close_out lakefile;
+  let project_main = open_out (Filename.concat project_dir (out_name_camel ^ ".lean")) in
+  project_main
+
+let output (out_name : string) =
+  let project_main = create_lake_project out_name in
+  close_out project_main;
+  failwith "Empty Lean project created, the actual export is not yet implemented."
 
-let lean_target out_file { ctx; ast; effect_info; env; _ } =
-  let out_file = match out_file with Some f -> f | None -> "out" in
-  output [(out_file, ctx, effect_info, env, ast)]
+let lean_target out_name { ctx; ast; effect_info; env; _ } =
+  let out_name = match out_name with Some f -> f | None -> "out" in
+  output out_name
 
 let _ = Target.register ~name:"lean" ~options:lean_options ~rewrites:lean_rewrites ~asserts_termination:true lean_target