fix generated lean project

src/bin/dune

@@ -241,6 +241,6 @@
   (%{workspace_root}/src/gen_lib/sail2_values.lem
    as
    src/gen_lib/sail2_values.lem)
-  (%{workspace_root}/src/sail_lean_backend/Sail/sail.lean
+  (%{workspace_root}/src/sail_lean_backend/Sail/Sail.lean
    as
-   src/sail_lean_backend/Sail/sail.lean)))
+   src/sail_lean_backend/Sail/Sail.lean)))

src/sail_lean_backend/pretty_print_lean.ml

@@ -260,17 +260,17 @@ let doc_typdef (TD_aux (td, tannot) as full_typdef) =
       let derivers = if List.length fields > 0 then [string "Inhabited"] else [] in
       let fields = List.map doc_id_ctor fields in
       let fields = List.map (fun i -> space ^^ pipe ^^ space ^^ i) fields in
-      let enums_doc = concat fields in
+      let fields_doc = concat fields in
       nest 2
         (flow (break 1) [string "inductive"; string id; string "where"]
-        ^^ enums_doc ^^ hardline ^^ string "deriving" ^^ space
+        ^^ fields_doc ^^ hardline ^^ string "deriving" ^^ space
         ^^ separate (comma ^^ space) derivers
         )
   | TD_record (Id_aux (Id id, _), TypQ_aux (tq, _), fields, _) ->
       let fields = List.map doc_typ_id fields in
-      let enums_doc = concat fields in
+      let fields_doc = concat fields in
       let rectyp = doc_typ_quant tq in
-      nest 2 (flow (break 1) [string "structure"; string id; rectyp; string "where"] ^^ hardline ^^ enums_doc)
+      nest 2 (flow (break 1) [string "structure"; string id; string "where"] ^^ hardline ^^ fields_doc)
   | _ -> failwith ("Type definition " ^ string_of_type_def_con full_typdef ^ " not translatable yet.")
 
 let doc_def (DEF_aux (aux, def_annot) as def) =
@@ -290,6 +290,5 @@ let rec remove_imports (defs : (Libsail.Type_check.tannot, Libsail.Type_check.en
 let pp_ast_lean ({ defs; _ } as ast : Libsail.Type_check.typed_ast) o =
   let defs = remove_imports defs 0 in
   let output : document = separate_map empty doc_def defs in
-  output_string o "import Sail.sail\n\n";
   print o output;
   ()

src/sail_lean_backend/sail_plugin_lean.ml

@@ -157,7 +157,7 @@ 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 (
+  if !opt_lean_force_output && Sys.file_exists project_dir && Sys.is_directory project_dir then (
     let _ = Unix.system ("rm -r " ^ project_dir ^ "/*") in
     ()
   )
@@ -174,13 +174,16 @@ let create_lake_project (out_name : string) default_sail_dir =
   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 = \"Sail\"\n\n[[lean_lib]]\nname = \"" ^ out_name_camel ^ "\""
+    ("name = \"" ^ out_name ^ "\"\ndefaultTargets = [\"" ^ out_name_camel ^ "\"]\n\n[[lean_lib]]\nname = \""
+   ^ out_name_camel ^ "\""
     );
   close_out lakefile;
+  let lean_src_dir = Filename.concat project_dir out_name_camel in
+  if not (Sys.file_exists lean_src_dir) then Unix.mkdir lean_src_dir 0o775;
   let sail_dir = Reporting.get_sail_dir default_sail_dir in
-  let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/sail_lean_backend/Sail " ^ project_dir) in
+  let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/sail_lean_backend/Sail " ^ lean_src_dir) in
   let project_main = open_out (Filename.concat project_dir (out_name_camel ^ ".lean")) in
+  output_string project_main ("import " ^ out_name_camel ^ ".Sail.Sail\n\n");
   project_main
 
 let output (out_name : string) ast default_sail_dir =

test/lean/struct.expected.lean

@@ -1,4 +1,4 @@
-import Sail.sail
+import My_Project.Sail.sail
 
 structure My_struct  where
   field1 : Int
@@ -10,4 +10,3 @@ def undefined_My_struct (lit : Unit) : My_struct :=
 
 def initialize_registers : Unit :=
   ()
-