Add an option to not override Hashmap.lean

4 files changed, 16 insertions, 3 deletions

diff --git a/Makefile b/Makefile
index c94544be..a0111b37 100644
--- a/Makefile
+++ b/Makefile
@@ -147,7 +147,7 @@ trans-hashmap: SUBDIR := hashmap
 tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses
 tcoq-hashmap: OPTIONS += -use-fuel
 tlean-hashmap: SUBDIR :=
-tlean-hashmap: OPTIONS +=
+tlean-hashmap: OPTIONS += -no-gen-lib-entry # We add a custom import in the Hashmap.lean file: we do not want to overwrite it
 thol4-hashmap: OPTIONS +=
 
 trans-hashmap_main: OPTIONS += -test-trans-units
diff --git a/compiler/Config.ml b/compiler/Config.ml
index 0475899c..bd80769f 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -162,6 +162,14 @@ let backward_no_state_update = ref false
  *)
 let split_files = ref true
 
+(** Generate the library entry point, if the crate is split between different files.
+
+    Sometimes we want to skip this: the library entry points just includes all the
+    files in the project, and the user may want to write their own entry point, to
+    add custom includes (to include the files containing the proofs, for instance).
+ *)
+let generate_lib_entry_point = ref true
+
 (** For Lean, controls whether we generate a lakefile or not.
 
  *)
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index 166ef11b..d819768b 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -107,6 +107,10 @@ let () =
         Arg.Clear check_invariants,
         " Deactivate the invariant sanity checks performed at every evaluation \
          step. Dramatically increases speed." );
+      ( "-no-gen-lib-entry",
+        Arg.Clear generate_lib_entry_point,
+        " Do not generate the entry point file for the generated library (only \
+         valid if the crate is split between different files)" );
       ( "-lean-default-lakefile",
         Arg.Clear lean_gen_lakefile,
         " Generate a default lakefile.lean (Lean only)" );
@@ -133,6 +137,8 @@ let () =
     (not !use_fuel)
     || (not !extract_decreases_clauses)
        && not !extract_template_decreases_clauses);
+  (* We have: not generate_lib_entry_point ==> split_files *)
+  assert (!split_files || !generate_lib_entry_point);
   if !lean_gen_lakefile && not (!backend = Lean) then
     log#error
       "The -lean-default-lakefile option is valid only for the Lean backend";
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index dfc97246..6c6435c5 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -1334,7 +1334,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
          custom_includes = [];
        }
      in
-     (* Add the extension for F* *)
      extract_file gen_config gen_ctx file_info);
 
   (* Generate the build file *)
@@ -1352,7 +1351,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
        * Generate the library entry point, if the crate is split between
        * different files.
        *)
-      if !Config.split_files then (
+      if !Config.split_files && !Config.generate_lib_entry_point then (
         let filename = Filename.concat dest_dir (crate_name ^ ".lean") in
         let out = open_out filename in
         (* Write *)