diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | compiler/Config.ml | 8 | ||||
| -rw-r--r-- | compiler/Driver.ml | 6 | ||||
| -rw-r--r-- | compiler/Translate.ml | 3 |
4 files changed, 16 insertions, 3 deletions
@@ -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 *) |