diff --git a/ocaml/fstar-lib/generated/FStarC_Main.ml b/ocaml/fstar-lib/generated/FStarC_Main.ml index be4b9025da6..834232e780e 100644 --- a/ocaml/fstar-lib/generated/FStarC_Main.ml +++ b/ocaml/fstar-lib/generated/FStarC_Main.ml @@ -131,30 +131,68 @@ let (fstar_files : Prims.string Prims.list FStar_Pervasives_Native.option FStarC_Compiler_Effect.ref) = FStarC_Compiler_Util.mk_ref FStar_Pervasives_Native.None -let go : 'uuuuu . 'uuuuu -> unit = +let (go_ocamlenv : Prims.string Prims.list -> unit) = + fun rest_args -> + if FStarC_Platform.system = FStarC_Platform.Windows + then + (let uu___1 = + let uu___2 = + FStarC_Errors_Msg.text + "--ocamlenv is not supported on Windows (yet?)" in + [uu___2] in + FStarC_Errors.raise_error0 + FStarC_Errors_Codes.Fatal_OptionsNotCompatible () + (Obj.magic FStarC_Errors_Msg.is_error_message_list_doc) + (Obj.magic uu___1)) + else (); + (let shellescape s = + let uu___1 = + let uu___2 = FStarC_Compiler_String.list_of_string s in + FStarC_Compiler_List.map + (fun uu___3 -> + match uu___3 with + | 39 -> "'\"'\"'" + | c -> FStarC_Compiler_String.make Prims.int_one c) uu___2 in + FStarC_Compiler_String.concat "" uu___1 in + let ocamldir = FStarC_Find.locate_ocaml () in + let old_ocamlpath = + let uu___1 = + FStarC_Compiler_Util.expand_environment_variable "OCAMLPATH" in + FStarC_Compiler_Util.dflt "" uu___1 in + let new_ocamlpath = + Prims.strcat ocamldir (Prims.strcat ":" old_ocamlpath) in + match rest_args with + | [] -> + ((let uu___2 = shellescape new_ocamlpath in + FStarC_Compiler_Util.print1 "OCAMLPATH='%s'; export OCAMLPATH;\n" + uu___2); + FStarC_Compiler_Effect.exit Prims.int_zero) + | cmd::args -> + (FStarC_Compiler_Util.putenv "OCAMLPATH" new_ocamlpath; + FStarC_Compiler_Util.execvp cmd (cmd :: args))) +let (set_error_trap : unit -> unit) = + fun uu___ -> + let h = FStarC_Compiler_Util.get_sigint_handler () in + let h' s = + FStarC_Compiler_Debug.enable (); + FStarC_Options.set_option "error_contexts" (FStarC_Options.Bool true); + (let uu___4 = + let uu___5 = FStarC_Errors_Msg.text "GOT SIGINT! Exiting" in + [uu___5] in + FStarC_Errors.diag FStarC_Class_HasRange.hasRange_range + FStarC_Compiler_Range_Type.dummyRange () + (Obj.magic FStarC_Errors_Msg.is_error_message_list_doc) + (Obj.magic uu___4)); + FStarC_Compiler_Effect.exit Prims.int_one in + let uu___1 = FStarC_Compiler_Util.sigint_handler_f h' in + FStarC_Compiler_Util.set_sigint_handler uu___1 +let (go_normal : unit -> unit) = fun uu___ -> let uu___1 = process_args () in match uu___1 with | (res, filenames) -> ((let uu___3 = FStarC_Options.trace_error () in - if uu___3 - then - let h = FStarC_Compiler_Util.get_sigint_handler () in - let h' s = - FStarC_Compiler_Debug.enable (); - FStarC_Options.set_option "error_contexts" - (FStarC_Options.Bool true); - (let uu___7 = - let uu___8 = FStarC_Errors_Msg.text "GOT SIGINT! Exiting" in - [uu___8] in - FStarC_Errors.diag FStarC_Class_HasRange.hasRange_range - FStarC_Compiler_Range_Type.dummyRange () - (Obj.magic FStarC_Errors_Msg.is_error_message_list_doc) - (Obj.magic uu___7)); - FStarC_Compiler_Effect.exit Prims.int_one in - let uu___4 = FStarC_Compiler_Util.sigint_handler_f h' in - FStarC_Compiler_Util.set_sigint_handler uu___4 - else ()); + if uu___3 then set_error_trap () else ()); (match res with | FStarC_Getopt.Empty -> (FStarC_Options.display_usage (); @@ -165,12 +203,151 @@ let go : 'uuuuu . 'uuuuu -> unit = | FStarC_Getopt.Error msg -> (FStarC_Compiler_Util.print_error msg; FStarC_Compiler_Effect.exit Prims.int_one) - | uu___3 when FStarC_Options.print_cache_version () -> - ((let uu___5 = + | FStarC_Getopt.Success when FStarC_Options.print_cache_version () + -> + ((let uu___4 = FStarC_Compiler_Util.string_of_int FStarC_CheckedFiles.cache_version_number in FStarC_Compiler_Util.print1 "F* cache version number: %s\n" - uu___5); + uu___4); + FStarC_Compiler_Effect.exit Prims.int_zero) + | FStarC_Getopt.Success when + let uu___3 = FStarC_Options.dep () in + uu___3 <> FStar_Pervasives_Native.None -> + let uu___3 = + FStarC_Parser_Dep.collect filenames + FStarC_CheckedFiles.load_parsing_data_from_cache in + (match uu___3 with + | (uu___4, deps) -> + (FStarC_Parser_Dep.print deps; report_errors [])) + | FStarC_Getopt.Success when + (FStarC_Options.print ()) || (FStarC_Options.print_in_place ()) + -> + (if + Prims.op_Negation + FStarC_Platform.is_fstar_compiler_using_ocaml + then + failwith + "You seem to be using the F#-generated version of the compiler ; \\o\n reindenting is not known to work yet with this version" + else (); + (let printing_mode = + let uu___4 = FStarC_Options.print () in + if uu___4 + then FStarC_Prettyprint.FromTempToStdout + else FStarC_Prettyprint.FromTempToFile in + FStarC_Prettyprint.generate printing_mode filenames)) + | FStarC_Getopt.Success when + let uu___3 = FStarC_Options.read_checked_file () in + FStar_Pervasives_Native.uu___is_Some uu___3 -> + let path = + let uu___3 = FStarC_Options.read_checked_file () in + FStar_Pervasives_Native.__proj__Some__item__v uu___3 in + let env = + FStarC_Universal.init_env FStarC_Parser_Dep.empty_deps in + let res1 = FStarC_CheckedFiles.load_tc_result path in + (match res1 with + | FStar_Pervasives_Native.None -> + let uu___3 = + let uu___4 = + let uu___5 = + FStarC_Errors_Msg.text + "Could not read checked file:" in + let uu___6 = FStarC_Pprint.doc_of_string path in + FStarC_Pprint.op_Hat_Slash_Hat uu___5 uu___6 in + [uu___4] in + FStarC_Errors.raise_error0 + FStarC_Errors_Codes.Fatal_ModuleOrFileNotFound () + (Obj.magic FStarC_Errors_Msg.is_error_message_list_doc) + (Obj.magic uu___3) + | FStar_Pervasives_Native.Some (uu___3, tcr) -> + let uu___4 = + FStarC_Class_Show.show + FStarC_Syntax_Print.showable_modul + tcr.FStarC_CheckedFiles.checked_module in + FStarC_Compiler_Util.print1 "%s\n" uu___4) + | FStarC_Getopt.Success when + let uu___3 = FStarC_Options.read_krml_file () in + FStar_Pervasives_Native.uu___is_Some uu___3 -> + let path = + let uu___3 = FStarC_Options.read_krml_file () in + FStar_Pervasives_Native.__proj__Some__item__v uu___3 in + let uu___3 = FStarC_Compiler_Util.load_value_from_file path in + (match uu___3 with + | FStar_Pervasives_Native.None -> + let uu___4 = + let uu___5 = + let uu___6 = + FStarC_Errors_Msg.text "Could not read krml file:" in + let uu___7 = FStarC_Pprint.doc_of_string path in + FStarC_Pprint.op_Hat_Slash_Hat uu___6 uu___7 in + [uu___5] in + FStarC_Errors.raise_error0 + FStarC_Errors_Codes.Fatal_ModuleOrFileNotFound () + (Obj.magic FStarC_Errors_Msg.is_error_message_list_doc) + (Obj.magic uu___4) + | FStar_Pervasives_Native.Some (version, files) -> + ((let uu___5 = + FStarC_Class_Show.show + (FStarC_Class_Show.printableshow + FStar_Class_Printable.printable_int) version in + FStarC_Compiler_Util.print1 + "Karamel format version: %s\n" uu___5); + FStarC_Compiler_List.iter + (fun uu___5 -> + match uu___5 with + | (name, decls) -> + (FStarC_Compiler_Util.print1 "%s:\n" name; + FStarC_Compiler_List.iter + (fun d -> + let uu___7 = + FStarC_Class_Show.show + FStarC_Extraction_Krml.showable_decl d in + FStarC_Compiler_Util.print1 " %s\n" + uu___7) decls)) files)) + | FStarC_Getopt.Success when FStarC_Options.list_plugins () -> + let ps = FStarC_TypeChecker_Cfg.list_plugins () in + let ts = FStarC_Tactics_Interpreter.native_tactics_steps () in + ((let uu___4 = + let uu___5 = + FStarC_Compiler_List.map + (fun p -> + let uu___6 = + FStarC_Class_Show.show + FStarC_Ident.showable_lident + p.FStarC_TypeChecker_Primops_Base.name in + Prims.strcat " " uu___6) ps in + FStarC_Compiler_String.concat "\n" uu___5 in + FStarC_Compiler_Util.print1 "Registered plugins:\n%s\n" + uu___4); + (let uu___5 = + let uu___6 = + FStarC_Compiler_List.map + (fun p -> + let uu___7 = + FStarC_Class_Show.show + FStarC_Ident.showable_lident + p.FStarC_TypeChecker_Primops_Base.name in + Prims.strcat " " uu___7) ts in + FStarC_Compiler_String.concat "\n" uu___6 in + FStarC_Compiler_Util.print1 + "Registered tactic plugins:\n%s\n" uu___5)) + | FStarC_Getopt.Success when FStarC_Options.locate () -> + ((let uu___4 = FStarC_Find.locate () in + FStarC_Compiler_Util.print1 "%s\n" uu___4); + FStarC_Compiler_Effect.exit Prims.int_zero) + | FStarC_Getopt.Success when FStarC_Options.locate_lib () -> + let uu___3 = FStarC_Find.locate_lib () in + (match uu___3 with + | FStar_Pervasives_Native.None -> + (FStarC_Compiler_Util.print_error + "No library found (is --no_default_includes set?)\n"; + FStarC_Compiler_Effect.exit Prims.int_one) + | FStar_Pervasives_Native.Some s -> + (FStarC_Compiler_Util.print1 "%s\n" s; + FStarC_Compiler_Effect.exit Prims.int_zero)) + | FStarC_Getopt.Success when FStarC_Options.locate_ocaml () -> + ((let uu___4 = FStarC_Find.locate_ocaml () in + FStarC_Compiler_Util.print1 "%s\n" uu___4); FStarC_Compiler_Effect.exit Prims.int_zero) | FStarC_Getopt.Success -> (FStarC_Compiler_Effect.op_Colon_Equals fstar_files @@ -195,285 +372,81 @@ let go : 'uuuuu . 'uuuuu -> unit = uu___9); FStarC_Compiler_Util.print_string "\n") else ()); - load_native_tactics (); FStarC_Syntax_Unionfind.set_ro (); - (let uu___7 = - let uu___8 = FStarC_Options.dep () in - uu___8 <> FStar_Pervasives_Native.None in + load_native_tactics (); + (let uu___7 = FStarC_Options.lsp_server () in if uu___7 - then - let uu___8 = - FStarC_Parser_Dep.collect filenames - FStarC_CheckedFiles.load_parsing_data_from_cache in - match uu___8 with - | (uu___9, deps) -> - (FStarC_Parser_Dep.print deps; report_errors []) + then FStarC_Interactive_Lsp.start_server () else - (let uu___9 = - (FStarC_Options.print ()) || - (FStarC_Options.print_in_place ()) in + (let uu___9 = FStarC_Options.interactive () in if uu___9 then - (if FStarC_Platform.is_fstar_compiler_using_ocaml - then - let printing_mode = - let uu___10 = FStarC_Options.print () in - if uu___10 - then FStarC_Prettyprint.FromTempToStdout - else FStarC_Prettyprint.FromTempToFile in - FStarC_Prettyprint.generate printing_mode filenames - else - failwith - "You seem to be using the F#-generated version ofthe compiler ; \\o\n reindenting is not known to work yet with this version") - else - (let uu___11 = - let uu___12 = FStarC_Options.read_checked_file () in - FStar_Pervasives_Native.uu___is_Some uu___12 in - if uu___11 - then - let path = - let uu___12 = FStarC_Options.read_checked_file () in - FStar_Pervasives_Native.__proj__Some__item__v - uu___12 in - let env = - FStarC_Universal.init_env - FStarC_Parser_Dep.empty_deps in - let res1 = FStarC_CheckedFiles.load_tc_result path in - match res1 with - | FStar_Pervasives_Native.None -> - let uu___12 = - let uu___13 = - let uu___14 = - FStarC_Errors_Msg.text - "Could not read checked file:" in - let uu___15 = - FStarC_Pprint.doc_of_string path in - FStarC_Pprint.op_Hat_Slash_Hat uu___14 - uu___15 in - [uu___13] in - FStarC_Errors.raise_error0 - FStarC_Errors_Codes.Fatal_ModuleOrFileNotFound - () + (FStarC_Syntax_Unionfind.set_rw (); + (match filenames with + | [] -> + (FStarC_Errors.log_issue0 + FStarC_Errors_Codes.Error_MissingFileName () + (Obj.magic + FStarC_Errors_Msg.is_error_message_string) + (Obj.magic + "--ide: Name of current file missing in command line invocation\n"); + FStarC_Compiler_Effect.exit Prims.int_one) + | uu___11::uu___12::uu___13 -> + (FStarC_Errors.log_issue0 + FStarC_Errors_Codes.Error_TooManyFiles () + (Obj.magic + FStarC_Errors_Msg.is_error_message_string) (Obj.magic - FStarC_Errors_Msg.is_error_message_list_doc) - (Obj.magic uu___12) - | FStar_Pervasives_Native.Some (uu___12, tcr) -> - let uu___13 = - FStarC_Class_Show.show - FStarC_Syntax_Print.showable_modul - tcr.FStarC_CheckedFiles.checked_module in - FStarC_Compiler_Util.print1 "%s\n" uu___13 - else - (let uu___13 = FStarC_Options.list_plugins () in - if uu___13 - then - let ps = FStarC_TypeChecker_Cfg.list_plugins () in - let ts = - FStarC_Tactics_Interpreter.native_tactics_steps - () in - ((let uu___15 = - let uu___16 = - FStarC_Compiler_List.map - (fun p -> - let uu___17 = - FStarC_Class_Show.show - FStarC_Ident.showable_lident - p.FStarC_TypeChecker_Primops_Base.name in - Prims.strcat " " uu___17) ps in - FStarC_Compiler_String.concat "\n" uu___16 in - FStarC_Compiler_Util.print1 - "Registered plugins:\n%s\n" uu___15); - (let uu___16 = - let uu___17 = - FStarC_Compiler_List.map - (fun p -> - let uu___18 = - FStarC_Class_Show.show - FStarC_Ident.showable_lident - p.FStarC_TypeChecker_Primops_Base.name in - Prims.strcat " " uu___18) ts in - FStarC_Compiler_String.concat "\n" uu___17 in - FStarC_Compiler_Util.print1 - "Registered tactic plugins:\n%s\n" uu___16)) - else - (let uu___15 = FStarC_Options.locate () in - if uu___15 - then - ((let uu___17 = FStarC_Find.locate () in - FStarC_Compiler_Util.print1 "%s\n" uu___17); - FStarC_Compiler_Effect.exit Prims.int_zero) - else - (let uu___17 = FStarC_Options.locate_lib () in - if uu___17 - then - let uu___18 = FStarC_Find.locate_lib () in - match uu___18 with - | FStar_Pervasives_Native.None -> - (FStarC_Compiler_Util.print_error - "No library found (is --no_default_includes set?)\n"; - FStarC_Compiler_Effect.exit - Prims.int_one) - | FStar_Pervasives_Native.Some s -> - (FStarC_Compiler_Util.print1 "%s\n" s; - FStarC_Compiler_Effect.exit - Prims.int_zero) - else - (let uu___19 = - FStarC_Options.locate_ocaml () in - if uu___19 - then - ((let uu___21 = - FStarC_Find.locate_ocaml () in - FStarC_Compiler_Util.print1 "%s\n" - uu___21); - FStarC_Compiler_Effect.exit - Prims.int_zero) - else - (let uu___21 = - let uu___22 = - FStarC_Options.read_krml_file () in - FStar_Pervasives_Native.uu___is_Some - uu___22 in - if uu___21 - then - let path = - let uu___22 = - FStarC_Options.read_krml_file () in - FStar_Pervasives_Native.__proj__Some__item__v - uu___22 in - let uu___22 = - FStarC_Compiler_Util.load_value_from_file - path in - match uu___22 with - | FStar_Pervasives_Native.None -> - let uu___23 = - let uu___24 = - let uu___25 = - FStarC_Errors_Msg.text - "Could not read krml file:" in - let uu___26 = - FStarC_Pprint.doc_of_string - path in - FStarC_Pprint.op_Hat_Slash_Hat - uu___25 uu___26 in - [uu___24] in - FStarC_Errors.raise_error0 - FStarC_Errors_Codes.Fatal_ModuleOrFileNotFound - () - (Obj.magic - FStarC_Errors_Msg.is_error_message_list_doc) - (Obj.magic uu___23) - | FStar_Pervasives_Native.Some - (version, files) -> - ((let uu___24 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) - version in - FStarC_Compiler_Util.print1 - "Karamel format version: %s\n" - uu___24); - FStarC_Compiler_List.iter - (fun uu___24 -> - match uu___24 with - | (name, decls) -> - (FStarC_Compiler_Util.print1 - "%s:\n" name; - FStarC_Compiler_List.iter - (fun d -> - let uu___26 = - FStarC_Class_Show.show - FStarC_Extraction_Krml.showable_decl - d in - FStarC_Compiler_Util.print1 - " %s\n" uu___26) - decls)) files) - else - (let uu___23 = - FStarC_Options.lsp_server () in - if uu___23 - then - FStarC_Interactive_Lsp.start_server - () - else - (let uu___25 = - FStarC_Options.interactive () in - if uu___25 - then - (FStarC_Syntax_Unionfind.set_rw - (); - (match filenames with - | [] -> - (FStarC_Errors.log_issue0 - FStarC_Errors_Codes.Error_MissingFileName - () - (Obj.magic - FStarC_Errors_Msg.is_error_message_string) - (Obj.magic - "--ide: Name of current file missing in command line invocation\n"); - FStarC_Compiler_Effect.exit - Prims.int_one) - | uu___27::uu___28::uu___29 -> - (FStarC_Errors.log_issue0 - FStarC_Errors_Codes.Error_TooManyFiles - () - (Obj.magic - FStarC_Errors_Msg.is_error_message_string) - (Obj.magic - "--ide: Too many files in command line invocation\n"); - FStarC_Compiler_Effect.exit - Prims.int_one) - | filename::[] -> - let uu___27 = - FStarC_Options.legacy_interactive - () in - if uu___27 - then - FStarC_Interactive_Legacy.interactive_mode - filename - else - FStarC_Interactive_Ide.interactive_mode - filename)) - else - if - (FStarC_Compiler_List.length - filenames) - >= Prims.int_one - then - (let uu___27 = - FStarC_Dependencies.find_deps_if_needed - filenames - FStarC_CheckedFiles.load_parsing_data_from_cache in - match uu___27 with - | (filenames1, dep_graph) -> - let uu___28 = - FStarC_Universal.batch_mode_tc - filenames1 dep_graph in - (match uu___28 with - | (tcrs, env, cleanup1) - -> - ((let uu___30 = - cleanup1 env in - ()); - (let module_names = - FStarC_Compiler_List.map - (fun tcr -> - FStarC_Universal.module_or_interface_name - tcr.FStarC_CheckedFiles.checked_module) - tcrs in - report_errors - module_names; - finished_message - module_names - Prims.int_zero)))) - else - FStarC_Errors.raise_error0 - FStarC_Errors_Codes.Error_MissingFileName - () - (Obj.magic - FStarC_Errors_Msg.is_error_message_string) - (Obj.magic - "No file provided")))))))))))))) + "--ide: Too many files in command line invocation\n"); + FStarC_Compiler_Effect.exit Prims.int_one) + | filename::[] -> + let uu___11 = FStarC_Options.legacy_interactive () in + if uu___11 + then + FStarC_Interactive_Legacy.interactive_mode + filename + else + FStarC_Interactive_Ide.interactive_mode filename)) + else + if + (FStarC_Compiler_List.length filenames) >= + Prims.int_one + then + (if Prims.uu___is_Nil filenames + then + FStarC_Errors.raise_error0 + FStarC_Errors_Codes.Error_MissingFileName () + (Obj.magic + FStarC_Errors_Msg.is_error_message_string) + (Obj.magic "No file provided") + else (); + (let uu___12 = + FStarC_Dependencies.find_deps_if_needed filenames + FStarC_CheckedFiles.load_parsing_data_from_cache in + match uu___12 with + | (filenames1, dep_graph) -> + let uu___13 = + FStarC_Universal.batch_mode_tc filenames1 + dep_graph in + (match uu___13 with + | (tcrs, env, cleanup1) -> + ((let uu___15 = cleanup1 env in ()); + (let module_names = + FStarC_Compiler_List.map + (fun tcr -> + FStarC_Universal.module_or_interface_name + tcr.FStarC_CheckedFiles.checked_module) + tcrs in + report_errors module_names; + finished_message module_names + Prims.int_zero))))) + else ()))))) +let (go : unit -> unit) = + fun uu___ -> + let args = FStarC_Compiler_Util.get_cmd_args () in + match args with + | uu___1::"--ocamlenv"::rest -> go_ocamlenv rest + | uu___1 -> go_normal () let (lazy_chooser : FStarC_Syntax_Syntax.lazy_kind -> FStarC_Syntax_Syntax.lazyinfo -> FStarC_Syntax_Syntax.term) diff --git a/ocaml/fstar-lib/generated/FStarC_Options.ml b/ocaml/fstar-lib/generated/FStarC_Options.ml index a40aed6b8c3..2ee31ae438b 100644 --- a/ocaml/fstar-lib/generated/FStarC_Options.ml +++ b/ocaml/fstar-lib/generated/FStarC_Options.ml @@ -3523,7 +3523,32 @@ let rec (specs_with_types : (Bool true)), uu___278) in - [uu___277] in + let uu___278 + = + let uu___279 + = + let uu___280 + = + text + "With no arguments: print shell code to set up an environment with the OCaml libraries in scope (similar to 'opam env'). With arguments: run a command in that environment. NOTE: this must be the FIRST argument passed to F* and other options are NOT processed." in + (FStarC_Getopt.noshort, + "ocamlenv", + (WithSideEffect + ((fun + uu___281 + -> + FStarC_Compiler_Util.print_error + "--ocamlenv must be the first argument, see fstar.exe --help for details\n"; + FStarC_Compiler_Effect.exit + Prims.int_one), + (Const + (Bool + true)))), + uu___280) in + [uu___279] in + uu___277 + :: + uu___278 in uu___275 :: uu___276 in diff --git a/src/basic/FStarC.Options.fst b/src/basic/FStarC.Options.fst index 389c2e13d05..86a46785360 100644 --- a/src/basic/FStarC.Options.fst +++ b/src/basic/FStarC.Options.fst @@ -1631,6 +1631,13 @@ let rec specs_with_types warn_unsafe : list (char & string & opt_type & Pprint.d "locate_ocaml", Const (Bool true), text "Print the root of the built OCaml F* library and exit"); + ( noshort, + "ocamlenv", + WithSideEffect ((fun _ -> print_error "--ocamlenv must be the first argument, see fstar.exe --help for details\n"; exit 1), + (Const (Bool true))), + text "With no arguments: print shell code to set up an environment with the OCaml libraries in scope (similar to 'opam env'). \ + With arguments: run a command in that environment. \ + NOTE: this must be the FIRST argument passed to F* and other options are NOT processed."); ] and specs (warn_unsafe:bool) : list (FStarC.Getopt.opt & Pprint.document) = diff --git a/src/fstar/FStarC.Main.fst b/src/fstar/FStarC.Main.fst index b0245f4a8e8..e575fdcced8 100644 --- a/src/fstar/FStarC.Main.fst +++ b/src/fstar/FStarC.Main.fst @@ -30,7 +30,7 @@ module E = FStarC.Errors module UF = FStarC.Syntax.Unionfind module RE = FStarC.Reflection.V2.Embeddings -let _ = FStarC.Version.dummy () +let _ = Version.dummy () (* These modules only mentioned to put them in the dep graph and hence compile and link them in. They do not export anything, @@ -113,178 +113,212 @@ let load_native_tactics () = (* print_in_place options are passed *) let fstar_files: ref (option (list string)) = Util.mk_ref None -(****************************************************************************) -(* Main function *) -(****************************************************************************) -let go _ = - let res, filenames = process_args () in - if Options.trace_error () then begin - let h = get_sigint_handler () in - let h' s = - let open FStarC.Pprint in - let open FStarC.Errors.Msg in - Debug.enable (); (* make sure diag is printed *) - Options.set_option "error_contexts" (Options.Bool true); - (* ^ Print context. Stack trace will be added since we have trace_error. *) - Errors.diag Range.dummyRange [ - text "GOT SIGINT! Exiting"; - ]; - exit 1 - in - set_sigint_handler (sigint_handler_f h') - end; - match res with - | Empty -> - Options.display_usage(); exit 1 - - | Help -> - Options.display_usage(); exit 0 +(* ocamlenv mode: called whenever the *first* argument is exactly '--ocamlenv' *) +let go_ocamlenv rest_args = + if Platform.system = Platform.Windows then ( + Errors.raise_error0 Errors.Fatal_OptionsNotCompatible [ + Errors.text "--ocamlenv is not supported on Windows (yet?)" + ] + ); + let shellescape (s:string) : string = + String.list_of_string s |> + List.map (function + | '\'' -> "'\"'\"'" // to escape single quotes we need to put them inside a double quote + | c -> String.make 1 c + ) |> + String.concat "" + in + let ocamldir = Find.locate_ocaml () in + let old_ocamlpath = Util.dflt "" (Util.expand_environment_variable "OCAMLPATH") in + let new_ocamlpath = ocamldir ^ ":" ^ old_ocamlpath in + match rest_args with + | [] -> + Util.print1 "OCAMLPATH='%s'; export OCAMLPATH;\n" (shellescape new_ocamlpath); + exit 0 - | Error msg -> - Util.print_error msg; exit 1 + | cmd :: args -> + (* Update OCAMLPATH and run (exec) the command *) + Util.putenv "OCAMLPATH" new_ocamlpath; + Util.execvp cmd (cmd :: args) + +(* This is used to print a backtrace when F* is interrupted by SIGINT *) +let set_error_trap () = + let h = get_sigint_handler () in + let h' s = + let open FStarC.Pprint in + let open FStarC.Errors.Msg in + Debug.enable (); (* make sure diag is printed *) + Options.set_option "error_contexts" (Options.Bool true); + (* ^ Print context. Stack trace will be added since we have trace_error. *) + Errors.diag Range.dummyRange [ + text "GOT SIGINT! Exiting"; + ]; + exit 1 + in + set_sigint_handler (sigint_handler_f h') - | _ when Options.print_cache_version () -> - Util.print1 "F* cache version number: %s\n" - (string_of_int FStarC.CheckedFiles.cache_version_number); +(* Normal mode with some flags, files, etc *) +let go_normal () = + let res, filenames = process_args () in + if Options.trace_error () then set_error_trap (); + match res with + | Empty -> Options.display_usage(); exit 1 + | Help -> Options.display_usage(); exit 0 + | Error msg -> Util.print_error msg; exit 1 + + | Success when Options.print_cache_version () -> + Util.print1 "F* cache version number: %s\n" + (string_of_int FStarC.CheckedFiles.cache_version_number); + exit 0 + + (* --dep: Just compute and print the transitive dependency graph; + don't verify anything *) + | Success when Options.dep () <> None -> + let _, deps = Parser.Dep.collect filenames FStarC.CheckedFiles.load_parsing_data_from_cache in + Parser.Dep.print deps; + report_errors [] + + (* --print: Emit files in canonical source syntax *) + | Success when Options.print () || Options.print_in_place () -> + if not Platform.is_fstar_compiler_using_ocaml then + failwith "You seem to be using the F#-generated version of the compiler ; \o + reindenting is not known to work yet with this version"; + let printing_mode = + if Options.print () + then Prettyprint.FromTempToStdout + else Prettyprint.FromTempToFile + in + Prettyprint.generate printing_mode filenames + + (* --read_checked: read and print a checked file *) + | Success when Some? (Options.read_checked_file ()) -> ( + let path = Some?.v <| Options.read_checked_file () in + let env = Universal.init_env Parser.Dep.empty_deps in + let res = CheckedFiles.load_tc_result path in + match res with + | None -> + let open FStarC.Pprint in + Errors.raise_error0 Errors.Fatal_ModuleOrFileNotFound [ + Errors.Msg.text "Could not read checked file:" ^/^ doc_of_string path + ] + + | Some (_, tcr) -> + print1 "%s\n" (show tcr.checked_module) + ) + + (* --read_krml_file: read and print a krml file *) + | Success when Some? (Options.read_krml_file ()) -> ( + let path = Some?.v <| Options.read_krml_file () in + match load_value_from_file path <: option Extraction.Krml.binary_format with + | None -> + let open FStarC.Pprint in + Errors.raise_error0 Errors.Fatal_ModuleOrFileNotFound [ + Errors.Msg.text "Could not read krml file:" ^/^ doc_of_string path + ] + | Some (version, files) -> + print1 "Karamel format version: %s\n" (show version); + (* Just "show decls" would print it, we just format this a bit *) + files |> List.iter (fun (name, decls) -> + print1 "%s:\n" name; + decls |> List.iter (fun d -> print1 " %s\n" (show d)) + ) + ) + + (* --list_plugins: emit a list of plugins and exit *) + | Success when Options.list_plugins () -> + let ps = TypeChecker.Cfg.list_plugins () in + let ts = Tactics.Interpreter.native_tactics_steps () in + Util.print1 "Registered plugins:\n%s\n" (String.concat "\n" (List.map (fun p -> " " ^ show p.TypeChecker.Primops.Base.name) ps)); + Util.print1 "Registered tactic plugins:\n%s\n" (String.concat "\n" (List.map (fun p -> " " ^ show p.TypeChecker.Primops.Base.name) ts)); + () + + (* --locate, --locate_lib, --locate_ocaml *) + | Success when Options.locate () -> + Util.print1 "%s\n" (Find.locate ()); + exit 0 + | Success when Options.locate_lib () -> ( + match Find.locate_lib () with + | None -> + Util.print_error "No library found (is --no_default_includes set?)\n"; + exit 1 + | Some s -> + Util.print1 "%s\n" s; exit 0 + ) + | Success when Options.locate_ocaml () -> + Util.print1 "%s\n" (Find.locate_ocaml ()); + exit 0 + (* either batch or interactive mode *) | Success -> - fstar_files := Some filenames; - - if Debug.any () then ( - Util.print1 "- F* executable: %s\n" (Util.exec_name); - Util.print1 "- Library root: %s\n" ((Util.dflt "" (Find.lib_root ()))); - Util.print1 "- Full include path: %s\n" (show (Find.include_path ())); - Util.print_string "\n"; - () - ); - - load_native_tactics (); - - (* Set the unionfind graph to read-only mode. - * This will be unset by the typechecker and other pieces - * of code that intend to use it. It helps us catch errors. *) - (* TODO: also needed by the interactive mode below. *) - UF.set_ro (); - - (* --dep: Just compute and print the transitive dependency graph; - don't verify anything *) - if Options.dep() <> None - then let _, deps = Parser.Dep.collect filenames FStarC.CheckedFiles.load_parsing_data_from_cache in - Parser.Dep.print deps; - report_errors [] - - (* --print: Emit files in canonical source syntax *) - else if Options.print () || Options.print_in_place () then - if FStarC.Platform.is_fstar_compiler_using_ocaml - then let printing_mode = - if Options.print () - then FStarC.Prettyprint.FromTempToStdout - else FStarC.Prettyprint.FromTempToFile - in - FStarC.Prettyprint.generate printing_mode filenames - else failwith "You seem to be using the F#-generated version ofthe compiler ; \o - reindenting is not known to work yet with this version" - - (* --read_checked: read and print a checked file *) - else if Some? (Options.read_checked_file ()) then - let path = Some?.v <| Options.read_checked_file () in - let env = Universal.init_env Parser.Dep.empty_deps in - let res = FStarC.CheckedFiles.load_tc_result path in - match res with - | None -> - let open FStarC.Pprint in - Errors.raise_error0 Errors.Fatal_ModuleOrFileNotFound [ - Errors.Msg.text "Could not read checked file:" ^/^ doc_of_string path - ] - - | Some (_, tcr) -> - print1 "%s\n" (show tcr.checked_module) - - else if Options.list_plugins () then - let ps = FStarC.TypeChecker.Cfg.list_plugins () in - let ts = FStarC.Tactics.Interpreter.native_tactics_steps () in - Util.print1 "Registered plugins:\n%s\n" (String.concat "\n" (List.map (fun p -> " " ^ show p.FStarC.TypeChecker.Primops.Base.name) ps)); - Util.print1 "Registered tactic plugins:\n%s\n" (String.concat "\n" (List.map (fun p -> " " ^ show p.FStarC.TypeChecker.Primops.Base.name) ts)); - () - - else if Options.locate () then ( - Util.print1 "%s\n" (Find.locate ()); - exit 0 - - ) else if Options.locate_lib () then ( - match Find.locate_lib () with - | None -> - Util.print_error "No library found (is --no_default_includes set?)\n"; - exit 1 - | Some s -> - Util.print1 "%s\n" s; - exit 0 - - ) else if Options.locate_ocaml () then ( - Util.print1 "%s\n" (Find.locate_ocaml ()); - exit 0 - - ) else if Some? (Options.read_krml_file ()) then - let path = Some?.v <| Options.read_krml_file () in - match load_value_from_file path <: option FStarC.Extraction.Krml.binary_format with - | None -> - let open FStarC.Pprint in - Errors.raise_error0 Errors.Fatal_ModuleOrFileNotFound [ - Errors.Msg.text "Could not read krml file:" ^/^ doc_of_string path - ] - | Some (version, files) -> - print1 "Karamel format version: %s\n" (show version); - (* Just "show decls" would print it, we just format this a bit *) - files |> List.iter (fun (name, decls) -> - print1 "%s:\n" name; - decls |> List.iter (fun d -> print1 " %s\n" (show d)) - ) - - (* --lsp *) - else if Options.lsp_server () then - FStarC.Interactive.Lsp.start_server () - - (* For the following cases we might need native tactics, try to load *) - else begin - - (* --ide, --in: Interactive mode *) - if Options.interactive () then begin - UF.set_rw (); - match filenames with - | [] -> (* input validation: move to process args? *) - Errors.log_issue0 Errors.Error_MissingFileName - "--ide: Name of current file missing in command line invocation\n"; - exit 1 - | _ :: _ :: _ -> (* input validation: move to process args? *) - Errors.log_issue0 Errors.Error_TooManyFiles - "--ide: Too many files in command line invocation\n"; - exit 1 - | [filename] -> - if Options.legacy_interactive () then - FStarC.Interactive.Legacy.interactive_mode filename - else - FStarC.Interactive.Ide.interactive_mode filename - end - - (* Normal, batch mode compiler *) - else if List.length filenames >= 1 then begin //normal batch mode - let filenames, dep_graph = FStarC.Dependencies.find_deps_if_needed filenames FStarC.CheckedFiles.load_parsing_data_from_cache in - let tcrs, env, cleanup = Universal.batch_mode_tc filenames dep_graph in - ignore (cleanup env); - let module_names = - tcrs - |> List.map (fun tcr -> - Universal.module_or_interface_name tcr.checked_module) - in - report_errors module_names; - finished_message module_names 0 - end //end batch mode - - else - Errors.raise_error0 Errors.Error_MissingFileName "No file provided" + fstar_files := Some filenames; + + if Debug.any () then ( + Util.print1 "- F* executable: %s\n" (Util.exec_name); + Util.print1 "- Library root: %s\n" ((Util.dflt "" (Find.lib_root ()))); + Util.print1 "- Full include path: %s\n" (show (Find.include_path ())); + Util.print_string "\n"; + () + ); + + (* Set the unionfind graph to read-only mode. + * This will be unset by the typechecker and other pieces + * of code that intend to use it. It helps us catch errors. *) + UF.set_ro (); + + (* Try to load the plugins that are specified in the command line *) + load_native_tactics (); + + (* --lsp: interactive mode for Language Server Protocol *) + if Options.lsp_server () then + Interactive.Lsp.start_server () + (* --ide, --in: Interactive mode *) + else if Options.interactive () then begin + UF.set_rw (); + match filenames with + | [] -> (* input validation: move to process args? *) + Errors.log_issue0 Errors.Error_MissingFileName + "--ide: Name of current file missing in command line invocation\n"; + exit 1 + | _ :: _ :: _ -> (* input validation: move to process args? *) + Errors.log_issue0 Errors.Error_TooManyFiles + "--ide: Too many files in command line invocation\n"; + exit 1 + | [filename] -> + if Options.legacy_interactive () then + Interactive.Legacy.interactive_mode filename + else + Interactive.Ide.interactive_mode filename end + (* Normal, batch mode compiler *) + else if List.length filenames >= 1 then begin //normal batch mode + if Nil? filenames then + Errors.raise_error0 Errors.Error_MissingFileName "No file provided"; + + let filenames, dep_graph = Dependencies.find_deps_if_needed filenames CheckedFiles.load_parsing_data_from_cache in + let tcrs, env, cleanup = Universal.batch_mode_tc filenames dep_graph in + ignore (cleanup env); + let module_names = + tcrs + |> List.map (fun tcr -> + Universal.module_or_interface_name tcr.checked_module) + in + report_errors module_names; + finished_message module_names 0 + end //end batch mode + +(****************************************************************************) +(* Main function *) +(****************************************************************************) + +(* choose a main driver function and go *) +let go () = + let args = Util.get_cmd_args () in + match args with + | _ :: "--ocamlenv" :: rest -> go_ocamlenv rest + | _ -> go_normal () + (* This is pretty awful. Now that we have Lazy_embedding, we can get rid of this table. *) let lazy_chooser (k:Syntax.Syntax.lazy_kind) (i:Syntax.Syntax.lazyinfo) : Syntax.Syntax.term = match k with @@ -314,7 +348,7 @@ let lazy_chooser (k:Syntax.Syntax.lazy_kind) (i:Syntax.Syntax.lazyinfo) : Syntax | FStarC.Syntax.Syntax.Lazy_embedding (_, t) -> Thunk.force t | FStarC.Syntax.Syntax.Lazy_extension s -> FStarC.Syntax.Util.exp_string (format1 "((extension %s))" s) - + // This is called directly by the Javascript port (it doesn't call Main) let setup_hooks () = FStarC.Syntax.DsEnv.ugly_sigelt_to_string_hook := show; diff --git a/tests/Makefile b/tests/Makefile index 3d52c3bb60c..8fad46f21c1 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -19,6 +19,7 @@ ALL_TEST_DIRS += tactics ALL_TEST_DIRS += typeclasses ALL_TEST_DIRS += vale ALL_TEST_DIRS += hacl +ALL_TEST_DIRS += simple_hello HAS_OCAML := $(shell which ocamlfind 2>/dev/null) ifneq (,$(HAS_OCAML)) diff --git a/tests/simple_hello/Hello.fst b/tests/simple_hello/Hello.fst new file mode 100644 index 00000000000..d471870009e --- /dev/null +++ b/tests/simple_hello/Hello.fst @@ -0,0 +1,5 @@ +module Hello + +open FStar.IO + +let _ = print_string "Hello F*!\n" diff --git a/tests/simple_hello/Makefile b/tests/simple_hello/Makefile new file mode 100644 index 00000000000..0fae4812b8e --- /dev/null +++ b/tests/simple_hello/Makefile @@ -0,0 +1,13 @@ +# This is probably the simplest makefile to build an F* application, and can be adapted easily. +# We should not need to include any other internal makefiles. +# Dune also works fine under the --ocamlenv. + +FSTAR ?= ../../bin/fstar.exe + +all: Hello.exe + +%.ml: %.fst + $(FSTAR) --codegen OCaml $< --extract $* + +%.exe: %.ml + $(FSTAR) --ocamlenv ocamlfind ocamlopt -package fstar.lib -linkpkg $< -o $@