From f681c4ea294afebc7be01f1ca9521cf61f371de2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 8 Sep 2024 13:04:17 -0700 Subject: [PATCH] snap --- .../fstar-lib/generated/FStar_Errors_Codes.ml | 2 +- ocaml/fstar-lib/generated/FStar_Options.ml | 97 ++++++++++--------- ocaml/fstar-lib/generated/FStar_Parser_Dep.ml | 19 ++-- 3 files changed, 65 insertions(+), 53 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_Errors_Codes.ml b/ocaml/fstar-lib/generated/FStar_Errors_Codes.ml index 1207154e5e6..5ecd0f64e4b 100644 --- a/ocaml/fstar-lib/generated/FStar_Errors_Codes.ml +++ b/ocaml/fstar-lib/generated/FStar_Errors_Codes.ml @@ -2085,7 +2085,7 @@ let (default_settings : error_setting Prims.list) = (Fatal_NotSupported, CFatal, (Prims.of_int (149))); (Fatal_NotTopLevelModule, CFatal, (Prims.of_int (150))); (Fatal_NotValidFStarFile, CFatal, (Prims.of_int (151))); - (Fatal_NotValidIncludeDirectory, CFatal, (Prims.of_int (152))); + (Fatal_NotValidIncludeDirectory, CWarning, (Prims.of_int (152))); (Fatal_OneModulePerFile, CFatal, (Prims.of_int (153))); (Fatal_OpenGoalsInSynthesis, CFatal, (Prims.of_int (154))); (Fatal_OptionsNotCompatible, CFatal, (Prims.of_int (155))); diff --git a/ocaml/fstar-lib/generated/FStar_Options.ml b/ocaml/fstar-lib/generated/FStar_Options.ml index f82b8900cb3..86e097be36a 100644 --- a/ocaml/fstar-lib/generated/FStar_Options.ml +++ b/ocaml/fstar-lib/generated/FStar_Options.ml @@ -4597,53 +4597,58 @@ let (should_extract : Prims.string -> codegen_t -> Prims.bool) = fun m -> fun tgt -> let m1 = FStar_Compiler_String.lowercase m in - let uu___ = extract_settings () in - match uu___ with - | FStar_Pervasives_Native.Some pes -> - ((let uu___2 = - let uu___3 = get_no_extract () in - let uu___4 = get_extract_namespace () in - let uu___5 = get_extract_module () in (uu___3, uu___4, uu___5) in - match uu___2 with - | ([], [], []) -> () - | uu___3 -> - FStar_Compiler_Effect.failwith - "Incompatible options: --extract cannot be used with --no_extract, --extract_namespace or --extract_module"); - (let tsetting = - let uu___2 = - find_setting_for_target tgt pes.target_specific_settings in - match uu___2 with - | FStar_Pervasives_Native.Some s -> s - | FStar_Pervasives_Native.None -> - (match pes.default_settings with - | FStar_Pervasives_Native.Some s -> s - | FStar_Pervasives_Native.None -> "*") in - module_matches_namespace_filter m1 [tsetting])) - | FStar_Pervasives_Native.None -> - let should_extract_namespace m2 = - let uu___1 = get_extract_namespace () in - match uu___1 with - | [] -> false - | ns -> - FStar_Compiler_Util.for_some - (fun n -> - FStar_Compiler_Util.starts_with m2 - (FStar_Compiler_String.lowercase n)) ns in - let should_extract_module m2 = - let uu___1 = get_extract_module () in - match uu___1 with - | [] -> false - | l -> - FStar_Compiler_Util.for_some - (fun n -> (FStar_Compiler_String.lowercase n) = m2) l in - (let uu___1 = no_extract m1 in Prims.op_Negation uu___1) && - (let uu___1 = + if m1 = "prims" + then false + else + (let uu___1 = extract_settings () in + match uu___1 with + | FStar_Pervasives_Native.Some pes -> + ((let uu___3 = + let uu___4 = get_no_extract () in + let uu___5 = get_extract_namespace () in + let uu___6 = get_extract_module () in + (uu___4, uu___5, uu___6) in + match uu___3 with + | ([], [], []) -> () + | uu___4 -> + FStar_Compiler_Effect.failwith + "Incompatible options: --extract cannot be used with --no_extract, --extract_namespace or --extract_module"); + (let tsetting = + let uu___3 = + find_setting_for_target tgt pes.target_specific_settings in + match uu___3 with + | FStar_Pervasives_Native.Some s -> s + | FStar_Pervasives_Native.None -> + (match pes.default_settings with + | FStar_Pervasives_Native.Some s -> s + | FStar_Pervasives_Native.None -> "*") in + module_matches_namespace_filter m1 [tsetting])) + | FStar_Pervasives_Native.None -> + let should_extract_namespace m2 = let uu___2 = get_extract_namespace () in - let uu___3 = get_extract_module () in (uu___2, uu___3) in - (match uu___1 with - | ([], []) -> true - | uu___2 -> - (should_extract_namespace m1) || (should_extract_module m1))) + match uu___2 with + | [] -> false + | ns -> + FStar_Compiler_Util.for_some + (fun n -> + FStar_Compiler_Util.starts_with m2 + (FStar_Compiler_String.lowercase n)) ns in + let should_extract_module m2 = + let uu___2 = get_extract_module () in + match uu___2 with + | [] -> false + | l -> + FStar_Compiler_Util.for_some + (fun n -> (FStar_Compiler_String.lowercase n) = m2) l in + (let uu___2 = no_extract m1 in Prims.op_Negation uu___2) && + (let uu___2 = + let uu___3 = get_extract_namespace () in + let uu___4 = get_extract_module () in (uu___3, uu___4) in + (match uu___2 with + | ([], []) -> true + | uu___3 -> + (should_extract_namespace m1) || + (should_extract_module m1)))) let (should_be_already_cached : Prims.string -> Prims.bool) = fun m -> let uu___ = get_already_cached () in diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml index 2173426cff3..84e68357671 100644 --- a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml +++ b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml @@ -821,12 +821,19 @@ let (build_inclusion_candidates_list : else FStar_Compiler_Util.join_paths d f1 in (longname, full_path)) uu___1) files else - (let uu___2 = - let uu___3 = - FStar_Compiler_Util.format1 - "not a valid include directory: %s\n" d in - (FStar_Errors_Codes.Fatal_NotValidIncludeDirectory, uu___3) in - FStar_Errors.raise_err uu___2)) include_directories2 + ((let uu___3 = + let uu___4 = + let uu___5 = + let uu___6 = + FStar_Errors_Msg.text "Not a valid include directory:" in + let uu___7 = FStar_Pprint.doc_of_string d in + FStar_Pprint.prefix (Prims.of_int (2)) Prims.int_one + uu___6 uu___7 in + [uu___5] in + (FStar_Errors_Codes.Fatal_NotValidIncludeDirectory, uu___4) in + FStar_Errors.log_issue_doc FStar_Compiler_Range_Type.dummyRange + uu___3); + [])) include_directories2 let (build_map : Prims.string Prims.list -> files_for_module_name) = fun filenames -> let map = FStar_Compiler_Util.smap_create (Prims.of_int (41)) in