From c87256c814acb14dd5c2e6651c282bcfd3de51cf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 2 Sep 2024 16:37:25 -0700 Subject: [PATCH 1/3] ulib/Makefile: Remove unused include path setting Unused even before the fstar.include feature. --- ulib/Makefile.extract | 6 +++--- ulib/Makefile.extract.fsharp | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/ulib/Makefile.extract b/ulib/Makefile.extract index bd3836b55f5..a469d2611b6 100644 --- a/ulib/Makefile.extract +++ b/ulib/Makefile.extract @@ -37,10 +37,10 @@ $(DEPENDRSP): $(DEPEND): $(DEPENDRSP) $(call msg, "DEPEND") $(Q)mkdir -p .cache - $(Q)$(MY_FSTAR) --dep full $(EXTRACT_MODULES) $(addprefix --include , $(INCLUDE_PATHS)) @$(DEPENDRSP) --output_deps_to $@ + $(Q)$(MY_FSTAR) --dep full $(EXTRACT_MODULES) @$(DEPENDRSP) --output_deps_to $@ dep.graph: $(DEPENDRSP) - $(Q)$(MY_FSTAR) --dep graph $(EXTRACT_MODULES) $(addprefix --include , $(INCLUDE_PATHS)) @$(DEPENDRSP) --output_deps_to $@ + $(Q)$(MY_FSTAR) --dep graph $(EXTRACT_MODULES) @$(DEPENDRSP) --output_deps_to $@ depgraph.pdf: dep.graph $(Q)$(FSTAR_HOME)/.scripts/simpl_graph.py dep.graph > dep_simpl.graph @@ -49,7 +49,7 @@ depgraph.pdf: dep.graph # make depgraph-FStar.Tactics.fst.pdf to get a dep graph of FStar.Tactics.fst downwards depgraph-%.pdf: - $(Q)$(MY_FSTAR) --dep graph $(EXTRACT_MODULES) $(addprefix --include , $(INCLUDE_PATHS)) $* --output_deps_to $@.graph + $(Q)$(MY_FSTAR) --dep graph $(EXTRACT_MODULES) $* --output_deps_to $@.graph $(Q)$(FSTAR_HOME)/.scripts/simpl_graph.py $@.graph > $@.graph.simpl $(call msg, "DOT", $@) $(Q)dot -Tpdf -o $@ $@.graph.simpl diff --git a/ulib/Makefile.extract.fsharp b/ulib/Makefile.extract.fsharp index 9daa8d3cf5b..8aead6591e9 100644 --- a/ulib/Makefile.extract.fsharp +++ b/ulib/Makefile.extract.fsharp @@ -38,7 +38,7 @@ $(OUTPUT_DIRECTORY)/%.fs: .depend.extract.fsharp: $(call msg, "DEPEND") true $(shell rm -f .depend.extract.fsharp.rsp) $(foreach f,$(FSTAR_FILES),$(shell echo $(f) >> .depend.extract.fsharp.rsp)) - $(Q)$(MY_FSTAR) --extract 'FSharp:*;OCaml:None;krml:None' --dep full $(EXTRACT_MODULES) $(addprefix --include , $(INCLUDE_PATHS)) @.depend.extract.fsharp.rsp --output_deps_to .depend.extract.fsharp + $(Q)$(MY_FSTAR) --extract 'FSharp:*;OCaml:None;krml:None' --dep full $(EXTRACT_MODULES) @.depend.extract.fsharp.rsp --output_deps_to .depend.extract.fsharp depend.extract.fsharp: .depend.extract.fsharp From 01409f4df9790b7c0f405a9ab44cd462c48df5a1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 7 Jul 2024 00:31:39 -0700 Subject: [PATCH 2/3] Options: fstar.include --- src/basic/FStar.Options.fst | 48 +++++++++++++++++++++++++++---------- src/fstar/FStar.Main.fst | 3 +++ 2 files changed, 39 insertions(+), 12 deletions(-) diff --git a/src/basic/FStar.Options.fst b/src/basic/FStar.Options.fst index f6f3dc8ae56..79b45460c09 100644 --- a/src/basic/FStar.Options.fst +++ b/src/basic/FStar.Options.fst @@ -1724,24 +1724,48 @@ let should_print_message m = then m <> "Prims" else false +let read_fstar_include (fn : string) : option (list string) = + try + let s = file_get_contents fn in + let subdirs = String.split ['\n'] s |> List.filter (fun s -> s <> "" && not (String.get s 0 = '#')) in + Some subdirs + with + | _ -> + failwith ("Could not read " ^ fn); + None + +let rec expand_include_d (dirname : string) : list string = + let dot_inc_path = dirname ^ "/fstar.include" in + if Util.file_exists dot_inc_path then ( + let subdirs = Some?.v <| read_fstar_include dot_inc_path in + dirname :: List.collect (fun subd -> expand_include_d (dirname ^ "/" ^ subd)) subdirs + ) else + [dirname] + +let expand_include_ds (dirnames : list string) : list string = + List.collect expand_include_d dirnames + let include_path () = let cache_dir = match get_cache_dir() with | None -> [] | Some c -> [c] in - if get_no_default_includes() then - cache_dir @ get_include() - else - let lib_paths = - match Util.expand_environment_variable "FSTAR_LIB" with - | None -> - let fstar_home = fstar_bin_directory ^ "/.." in - let defs = universe_include_path_base_dirs in - defs |> List.map (fun x -> fstar_home ^ x) |> List.filter file_exists - | Some s -> [s] - in - cache_dir @ lib_paths @ get_include() @ [ "." ] + let lib_paths = + if get_no_default_includes() then + [] + else + match Util.expand_environment_variable "FSTAR_LIB" with + | None -> + let fstar_home = fstar_bin_directory ^ "/.." in + let defs = universe_include_path_base_dirs in + defs |> List.map (fun x -> fstar_home ^ x) |> List.filter file_exists |> expand_include_ds + | Some s -> [s] + in + let include_paths = + get_include () |> expand_include_ds + in + cache_dir @ lib_paths @ include_paths @ expand_include_d "." let find_file = let file_map = Util.smap_create 100 in diff --git a/src/fstar/FStar.Main.fst b/src/fstar/FStar.Main.fst index e25193a0dd3..4644f297d10 100644 --- a/src/fstar/FStar.Main.fst +++ b/src/fstar/FStar.Main.fst @@ -150,6 +150,9 @@ let go _ = | Success -> fstar_files := Some filenames; + if Debug.any () then + Util.print1 "Full include path = %s\n" (show (Options.include_path ())); + load_native_tactics (); (* Set the unionfind graph to read-only mode. From 89f9bbce9ee47d20d37750b0e0c539141c651d47 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 5 Sep 2024 01:27:28 -0700 Subject: [PATCH 3/3] snap --- ocaml/fstar-lib/generated/FStar_Main.ml | 144 +++++++++++---------- ocaml/fstar-lib/generated/FStar_Options.ml | 83 +++++++++--- 2 files changed, 142 insertions(+), 85 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_Main.ml b/ocaml/fstar-lib/generated/FStar_Main.ml index 2b50dc49c75..6df3385ef2e 100644 --- a/ocaml/fstar-lib/generated/FStar_Main.ml +++ b/ocaml/fstar-lib/generated/FStar_Main.ml @@ -170,30 +170,42 @@ let go : 'uuuuu . 'uuuuu -> unit = | FStar_Getopt.Success -> (FStar_Compiler_Effect.op_Colon_Equals fstar_files (FStar_Pervasives_Native.Some filenames); + (let uu___5 = FStar_Compiler_Debug.any () in + if uu___5 + then + let uu___6 = + let uu___7 = FStar_Options.include_path () in + FStar_Class_Show.show + (FStar_Class_Show.show_list + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_string)) uu___7 in + FStar_Compiler_Util.print1 "Full include path = %s\n" + uu___6 + else ()); load_native_tactics (); FStar_Syntax_Unionfind.set_ro (); - (let uu___6 = - let uu___7 = FStar_Options.dep () in - uu___7 <> FStar_Pervasives_Native.None in - if uu___6 + (let uu___7 = + let uu___8 = FStar_Options.dep () in + uu___8 <> FStar_Pervasives_Native.None in + if uu___7 then - let uu___7 = + let uu___8 = FStar_Parser_Dep.collect filenames FStar_CheckedFiles.load_parsing_data_from_cache in - match uu___7 with - | (uu___8, deps) -> + match uu___8 with + | (uu___9, deps) -> (FStar_Parser_Dep.print deps; report_errors []) else - (let uu___8 = + (let uu___9 = (FStar_Options.print ()) || (FStar_Options.print_in_place ()) in - if uu___8 + if uu___9 then (if FStar_Platform.is_fstar_compiler_using_ocaml then let printing_mode = - let uu___9 = FStar_Options.print () in - if uu___9 + let uu___10 = FStar_Options.print () in + if uu___10 then FStar_Prettyprint.FromTempToStdout else FStar_Prettyprint.FromTempToFile in FStar_Prettyprint.generate printing_mode filenames @@ -201,99 +213,99 @@ let go : 'uuuuu . 'uuuuu -> unit = FStar_Compiler_Effect.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___10 = - let uu___11 = FStar_Options.read_checked_file () in - FStar_Pervasives_Native.uu___is_Some uu___11 in - if uu___10 + (let uu___11 = + let uu___12 = FStar_Options.read_checked_file () in + FStar_Pervasives_Native.uu___is_Some uu___12 in + if uu___11 then let path = - let uu___11 = FStar_Options.read_checked_file () in + let uu___12 = FStar_Options.read_checked_file () in FStar_Pervasives_Native.__proj__Some__item__v - uu___11 in + uu___12 in let env = FStar_Universal.init_env FStar_Parser_Dep.empty_deps in let res1 = FStar_CheckedFiles.load_tc_result path in match res1 with | FStar_Pervasives_Native.None -> - let uu___11 = - let uu___12 = - let uu___13 = - let uu___14 = + let uu___12 = + let uu___13 = + let uu___14 = + let uu___15 = FStar_Errors_Msg.text "Could not read checked file:" in - let uu___15 = + let uu___16 = FStar_Pprint.doc_of_string path in - FStar_Pprint.op_Hat_Slash_Hat uu___14 - uu___15 in - [uu___13] in + FStar_Pprint.op_Hat_Slash_Hat uu___15 + uu___16 in + [uu___14] in (FStar_Errors_Codes.Fatal_ModuleOrFileNotFound, - uu___12) in - FStar_Errors.raise_err_doc uu___11 - | FStar_Pervasives_Native.Some (uu___11, tcr) -> - let uu___12 = + uu___13) in + FStar_Errors.raise_err_doc uu___12 + | FStar_Pervasives_Native.Some (uu___12, tcr) -> + let uu___13 = FStar_Class_Show.show FStar_Syntax_Print.showable_modul tcr.FStar_CheckedFiles.checked_module in - FStar_Compiler_Util.print1 "%s\n" uu___12 + FStar_Compiler_Util.print1 "%s\n" uu___13 else - (let uu___12 = - let uu___13 = FStar_Options.read_krml_file () in - FStar_Pervasives_Native.uu___is_Some uu___13 in - if uu___12 + (let uu___13 = + let uu___14 = FStar_Options.read_krml_file () in + FStar_Pervasives_Native.uu___is_Some uu___14 in + if uu___13 then let path = - let uu___13 = FStar_Options.read_krml_file () in + let uu___14 = FStar_Options.read_krml_file () in FStar_Pervasives_Native.__proj__Some__item__v - uu___13 in - let uu___13 = + uu___14 in + let uu___14 = FStar_Compiler_Util.load_value_from_file path in - match uu___13 with + match uu___14 with | FStar_Pervasives_Native.None -> - let uu___14 = - let uu___15 = - let uu___16 = - let uu___17 = + let uu___15 = + let uu___16 = + let uu___17 = + let uu___18 = FStar_Errors_Msg.text "Could not read krml file:" in - let uu___18 = + let uu___19 = FStar_Pprint.doc_of_string path in - FStar_Pprint.op_Hat_Slash_Hat uu___17 - uu___18 in - [uu___16] in + FStar_Pprint.op_Hat_Slash_Hat uu___18 + uu___19 in + [uu___17] in (FStar_Errors_Codes.Fatal_ModuleOrFileNotFound, - uu___15) in - FStar_Errors.raise_err_doc uu___14 + uu___16) in + FStar_Errors.raise_err_doc uu___15 | FStar_Pervasives_Native.Some (version, files) -> - ((let uu___15 = + ((let uu___16 = FStar_Class_Show.show (FStar_Class_Show.printableshow FStar_Class_Printable.printable_int) version in FStar_Compiler_Util.print1 - "Karamel format version: %s\n" uu___15); + "Karamel format version: %s\n" uu___16); FStar_Compiler_List.iter - (fun uu___15 -> - match uu___15 with + (fun uu___16 -> + match uu___16 with | (name, decls) -> (FStar_Compiler_Util.print1 "%s:\n" name; FStar_Compiler_List.iter (fun d -> - let uu___17 = + let uu___18 = FStar_Class_Show.show FStar_Extraction_Krml.showable_decl d in FStar_Compiler_Util.print1 - " %s\n" uu___17) decls)) + " %s\n" uu___18) decls)) files) else - (let uu___14 = FStar_Options.lsp_server () in - if uu___14 + (let uu___15 = FStar_Options.lsp_server () in + if uu___15 then FStar_Interactive_Lsp.start_server () else - (let uu___16 = FStar_Options.interactive () in - if uu___16 + (let uu___17 = FStar_Options.interactive () in + if uu___17 then (FStar_Syntax_Unionfind.set_rw (); (match filenames with @@ -304,7 +316,7 @@ let go : 'uuuuu . 'uuuuu -> unit = "--ide: Name of current file missing in command line invocation\n"); FStar_Compiler_Effect.exit Prims.int_one) - | uu___18::uu___19::uu___20 -> + | uu___19::uu___20::uu___21 -> (FStar_Errors.log_issue FStar_Compiler_Range_Type.dummyRange (FStar_Errors_Codes.Error_TooManyFiles, @@ -312,9 +324,9 @@ let go : 'uuuuu . 'uuuuu -> unit = FStar_Compiler_Effect.exit Prims.int_one) | filename::[] -> - let uu___18 = + let uu___19 = FStar_Options.legacy_interactive () in - if uu___18 + if uu___19 then FStar_Interactive_Legacy.interactive_mode filename @@ -326,18 +338,18 @@ let go : 'uuuuu . 'uuuuu -> unit = (FStar_Compiler_List.length filenames) >= Prims.int_one then - (let uu___18 = + (let uu___19 = FStar_Dependencies.find_deps_if_needed filenames FStar_CheckedFiles.load_parsing_data_from_cache in - match uu___18 with + match uu___19 with | (filenames1, dep_graph) -> - let uu___19 = + let uu___20 = FStar_Universal.batch_mode_tc filenames1 dep_graph in - (match uu___19 with + (match uu___20 with | (tcrs, env, cleanup1) -> - ((let uu___21 = cleanup1 env in + ((let uu___22 = cleanup1 env in ()); (let module_names = FStar_Compiler_List.map diff --git a/ocaml/fstar-lib/generated/FStar_Options.ml b/ocaml/fstar-lib/generated/FStar_Options.ml index 58364a35728..b7fbe6935cf 100644 --- a/ocaml/fstar-lib/generated/FStar_Options.ml +++ b/ocaml/fstar-lib/generated/FStar_Options.ml @@ -3842,6 +3842,49 @@ let (module_name_eq : Prims.string -> Prims.string -> Prims.bool) = let (should_print_message : Prims.string -> Prims.bool) = fun m -> let uu___ = should_verify m in if uu___ then m <> "Prims" else false +let (read_fstar_include : + Prims.string -> Prims.string Prims.list FStar_Pervasives_Native.option) = + fun fn -> + try + (fun uu___ -> + match () with + | () -> + let s = FStar_Compiler_Util.file_get_contents fn in + let subdirs = + FStar_Compiler_List.filter + (fun s1 -> + (s1 <> "") && + (let uu___1 = + let uu___2 = + FStar_Compiler_String.get s1 Prims.int_zero in + uu___2 = 35 in + Prims.op_Negation uu___1)) + (FStar_Compiler_String.split [10] s) in + FStar_Pervasives_Native.Some subdirs) () + with + | uu___ -> + ((let uu___2 = FStar_Compiler_String.op_Hat "Could not read " fn in + FStar_Compiler_Effect.failwith uu___2); + FStar_Pervasives_Native.None) +let rec (expand_include_d : Prims.string -> Prims.string Prims.list) = + fun dirname -> + let dot_inc_path = FStar_Compiler_String.op_Hat dirname "/fstar.include" in + if FStar_Compiler_Util.file_exists dot_inc_path + then + let subdirs = + let uu___ = read_fstar_include dot_inc_path in + FStar_Pervasives_Native.__proj__Some__item__v uu___ in + let uu___ = + FStar_Compiler_List.collect + (fun subd -> + let uu___1 = + let uu___2 = FStar_Compiler_String.op_Hat "/" subd in + FStar_Compiler_String.op_Hat dirname uu___2 in + expand_include_d uu___1) subdirs in + dirname :: uu___ + else [dirname] +let (expand_include_ds : Prims.string Prims.list -> Prims.string Prims.list) + = fun dirnames -> FStar_Compiler_List.collect expand_include_d dirnames let (include_path : unit -> Prims.string Prims.list) = fun uu___ -> let cache_dir = @@ -3849,14 +3892,12 @@ let (include_path : unit -> Prims.string Prims.list) = match uu___1 with | FStar_Pervasives_Native.None -> [] | FStar_Pervasives_Native.Some c -> [c] in - let uu___1 = get_no_default_includes () in - if uu___1 - then - let uu___2 = get_include () in - FStar_Compiler_List.op_At cache_dir uu___2 - else - (let lib_paths = - let uu___3 = + let lib_paths = + let uu___1 = get_no_default_includes () in + if uu___1 + then [] + else + (let uu___3 = FStar_Compiler_Util.expand_environment_variable "FSTAR_LIB" in match uu___3 with | FStar_Pervasives_Native.None -> @@ -3864,17 +3905,21 @@ let (include_path : unit -> Prims.string Prims.list) = FStar_Compiler_String.op_Hat fstar_bin_directory "/.." in let defs = universe_include_path_base_dirs in let uu___4 = - FStar_Compiler_List.map - (fun x -> FStar_Compiler_String.op_Hat fstar_home x) defs in - FStar_Compiler_List.filter FStar_Compiler_Util.file_exists - uu___4 - | FStar_Pervasives_Native.Some s -> [s] in - let uu___3 = - let uu___4 = - let uu___5 = get_include () in - FStar_Compiler_List.op_At uu___5 ["."] in - FStar_Compiler_List.op_At lib_paths uu___4 in - FStar_Compiler_List.op_At cache_dir uu___3) + let uu___5 = + FStar_Compiler_List.map + (fun x -> FStar_Compiler_String.op_Hat fstar_home x) defs in + FStar_Compiler_List.filter FStar_Compiler_Util.file_exists + uu___5 in + expand_include_ds uu___4 + | FStar_Pervasives_Native.Some s -> [s]) in + let include_paths = + let uu___1 = get_include () in expand_include_ds uu___1 in + let uu___1 = + let uu___2 = + let uu___3 = expand_include_d "." in + FStar_Compiler_List.op_At include_paths uu___3 in + FStar_Compiler_List.op_At lib_paths uu___2 in + FStar_Compiler_List.op_At cache_dir uu___1 let (find_file : Prims.string -> Prims.string FStar_Pervasives_Native.option) = let file_map = FStar_Compiler_Util.smap_create (Prims.of_int (100)) in