From 38dd19e9375e9ee8eb746eb0735914d6d5349f95 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Sun, 19 Jan 2025 12:49:00 -0800 Subject: [PATCH 1/8] Use the directory of any file on the command line in the include path rather than . --- src/basic/FStarC.Find.fst | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/basic/FStarC.Find.fst b/src/basic/FStarC.Find.fst index 2cc3dcfbbc1..a4a97963272 100644 --- a/src/basic/FStarC.Find.fst +++ b/src/basic/FStarC.Find.fst @@ -90,15 +90,13 @@ let include_path () = let include_paths = Options.include_ () |> expand_include_ds in - cache_dir @ lib_paths () @ include_paths @ expand_include_d "." + let cmd_line_file_dirs = + Options.file_list() |> List.map (fun f -> BU.normalize_file_path <| BU.dirname f) + in + cache_dir @ lib_paths () @ include_paths @ cmd_line_file_dirs let do_find (paths : list string) (filename : string) : option string = - if BU.is_path_absolute filename then - if BU.file_exists filename then - Some filename - else - None - else + let filename = BU.basename filename in try (* In reverse, because the last directory has the highest precedence. *) (* FIXME: We should fail if we find two files with the same name *) From e181cc9af03cf51ea517e7ec5f0b003b235b7457 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Sun, 19 Jan 2025 21:03:51 -0800 Subject: [PATCH 2/8] remove special handling in the dependence analysis for files in the current directory --- src/basic/FStarC.Find.fst | 6 ++++++ src/parser/FStarC.Parser.Dep.fst | 3 +-- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/src/basic/FStarC.Find.fst b/src/basic/FStarC.Find.fst index a4a97963272..98b85727099 100644 --- a/src/basic/FStarC.Find.fst +++ b/src/basic/FStarC.Find.fst @@ -96,6 +96,12 @@ let include_path () = cache_dir @ lib_paths () @ include_paths @ cmd_line_file_dirs let do_find (paths : list string) (filename : string) : option string = + if BU.is_path_absolute filename then + if BU.file_exists filename then + Some filename + else + None + else let filename = BU.basename filename in try (* In reverse, because the last directory has the highest precedence. *) diff --git a/src/parser/FStarC.Parser.Dep.fst b/src/parser/FStarC.Parser.Dep.fst index 0765704fda9..2149141e3d9 100644 --- a/src/parser/FStarC.Parser.Dep.fst +++ b/src/parser/FStarC.Parser.Dep.fst @@ -471,14 +471,13 @@ let build_inclusion_candidates_list (): list (string & string) = (* Note that [BatList.unique] keeps the last occurrence, that way one can * always override the precedence order. *) let include_directories = List.unique include_directories in - let cwd = normalize_file_path (getcwd ()) in include_directories |> List.concatMap (fun d -> let files = safe_readdir_for_include d in files |> List.filter_map (fun f -> let f = basename f in check_and_strip_suffix f |> Util.map_option (fun longname -> - let full_path = if d = cwd then f else join_paths d f in + let full_path = join_paths d f in (longname, full_path)) ) ) From 00bf851e42dc660913cff99f1ff2e1938a1f0b7e Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Mon, 20 Jan 2025 09:01:33 -0800 Subject: [PATCH 3/8] other projects, notably karamel, rely on . being in the include path; try to retain it at a lower precedence --- src/basic/FStarC.Find.fst | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/basic/FStarC.Find.fst b/src/basic/FStarC.Find.fst index 98b85727099..b6510c6f926 100644 --- a/src/basic/FStarC.Find.fst +++ b/src/basic/FStarC.Find.fst @@ -93,7 +93,8 @@ let include_path () = let cmd_line_file_dirs = Options.file_list() |> List.map (fun f -> BU.normalize_file_path <| BU.dirname f) in - cache_dir @ lib_paths () @ include_paths @ cmd_line_file_dirs + let cwd = expand_include_d "." |> List.map BU.normalize_file_path in + cache_dir @ lib_paths () @ include_paths @ cwd @ cmd_line_file_dirs let do_find (paths : list string) (filename : string) : option string = if BU.is_path_absolute filename then From 4b634084db4ae30d8ff5418481fb0859dedb63f6 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Mon, 20 Jan 2025 09:07:59 -0800 Subject: [PATCH 4/8] expand include for all include paths; normalize file paths --- src/basic/FStarC.Find.fst | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/basic/FStarC.Find.fst b/src/basic/FStarC.Find.fst index b6510c6f926..92e3d6537c2 100644 --- a/src/basic/FStarC.Find.fst +++ b/src/basic/FStarC.Find.fst @@ -91,10 +91,17 @@ let include_path () = Options.include_ () |> expand_include_ds in let cmd_line_file_dirs = - Options.file_list() |> List.map (fun f -> BU.normalize_file_path <| BU.dirname f) + Options.file_list() |> + List.map (fun f -> BU.normalize_file_path <| BU.dirname f) |> + expand_include_ds + in + let cwd = + if BU.for_some (fun f -> BU.basename f = f) (Options.file_list ()) + then [] // we already have . in the path + else expand_include_d "." in - let cwd = expand_include_d "." |> List.map BU.normalize_file_path in cache_dir @ lib_paths () @ include_paths @ cwd @ cmd_line_file_dirs + |> List.map BU.normalize_file_path let do_find (paths : list string) (filename : string) : option string = if BU.is_path_absolute filename then From 405e63789f73b26021da440b6ced381721503f71 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Thu, 23 Jan 2025 04:47:23 +0000 Subject: [PATCH 5/8] resolve qualified paths as is, rather than in include path --- src/basic/FStarC.Find.fst | 42 ++++++++++++++++++++++++--------------- 1 file changed, 26 insertions(+), 16 deletions(-) diff --git a/src/basic/FStarC.Find.fst b/src/basic/FStarC.Find.fst index 92e3d6537c2..58ab46d7ecc 100644 --- a/src/basic/FStarC.Find.fst +++ b/src/basic/FStarC.Find.fst @@ -109,22 +109,32 @@ let do_find (paths : list string) (filename : string) : option string = Some filename else None - else - let filename = BU.basename filename in - try - (* In reverse, because the last directory has the highest precedence. *) - (* FIXME: We should fail if we find two files with the same name *) - BU.find_map (List.rev paths) (fun p -> - let path = - if p = "." then filename - else BU.join_paths p filename in - if BU.file_exists path then - Some path - else - None) - with - | _ -> None - // ^ to deal with issues like passing bogus strings as paths like " input" + else if BU.basename filename <> filename + then + // we have a qualified name like + // fstar.exe src/fstar/FStar.Main.fst + // it as is, without trying to find it in the include path + // We don't want to resolve to FStar.Main.fst found + // in some other directory + let abs_path = BU.normalize_file_path filename in + if BU.file_exists abs_path + then Some abs_path + else None + else //unqualified file name: resolve in include path + try + (* In reverse, because the last directory has the highest precedence. *) + (* FIXME: We should fail if we find two files with the same name *) + BU.find_map (List.rev paths) (fun p -> + let path = + if p = "." then filename + else BU.join_paths p filename in + if BU.file_exists path then + Some path + else + None) + with + | _ -> None + // ^ to deal with issues like passing bogus strings as paths like " input" let find_file = let cache = BU.smap_create 100 in From ae62dcbc1752f3a33d405b70e1b83c0ba37a6414 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Thu, 23 Jan 2025 05:29:43 +0000 Subject: [PATCH 6/8] Revert "resolve qualified paths as is, rather than in include path" This reverts commit 405e63789f73b26021da440b6ced381721503f71. --- src/basic/FStarC.Find.fst | 42 +++++++++++++++------------------------ 1 file changed, 16 insertions(+), 26 deletions(-) diff --git a/src/basic/FStarC.Find.fst b/src/basic/FStarC.Find.fst index 58ab46d7ecc..92e3d6537c2 100644 --- a/src/basic/FStarC.Find.fst +++ b/src/basic/FStarC.Find.fst @@ -109,32 +109,22 @@ let do_find (paths : list string) (filename : string) : option string = Some filename else None - else if BU.basename filename <> filename - then - // we have a qualified name like - // fstar.exe src/fstar/FStar.Main.fst - // it as is, without trying to find it in the include path - // We don't want to resolve to FStar.Main.fst found - // in some other directory - let abs_path = BU.normalize_file_path filename in - if BU.file_exists abs_path - then Some abs_path - else None - else //unqualified file name: resolve in include path - try - (* In reverse, because the last directory has the highest precedence. *) - (* FIXME: We should fail if we find two files with the same name *) - BU.find_map (List.rev paths) (fun p -> - let path = - if p = "." then filename - else BU.join_paths p filename in - if BU.file_exists path then - Some path - else - None) - with - | _ -> None - // ^ to deal with issues like passing bogus strings as paths like " input" + else + let filename = BU.basename filename in + try + (* In reverse, because the last directory has the highest precedence. *) + (* FIXME: We should fail if we find two files with the same name *) + BU.find_map (List.rev paths) (fun p -> + let path = + if p = "." then filename + else BU.join_paths p filename in + if BU.file_exists path then + Some path + else + None) + with + | _ -> None + // ^ to deal with issues like passing bogus strings as paths like " input" let find_file = let cache = BU.smap_create 100 in From ebea9470efc6559035799888b1c467a5fec1857b Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Thu, 23 Jan 2025 05:47:47 +0000 Subject: [PATCH 7/8] complain if multiple files for the same module/interface are found in the include path --- src/parser/FStarC.Parser.Dep.fst | 25 +++++++++++++++++++++---- 1 file changed, 21 insertions(+), 4 deletions(-) diff --git a/src/parser/FStarC.Parser.Dep.fst b/src/parser/FStarC.Parser.Dep.fst index 2149141e3d9..28eecec0d23 100644 --- a/src/parser/FStarC.Parser.Dep.fst +++ b/src/parser/FStarC.Parser.Dep.fst @@ -492,10 +492,27 @@ let build_map (filenames: list string): files_for_module_name = let add_entry key full_path = match smap_try_find map key with | Some (intf, impl) -> - if is_interface full_path then - smap_add map key (Some full_path, impl) - else - smap_add map key (intf, Some full_path) + if is_interface full_path then begin + match intf with + | Some other when other <> full_path -> + //duplicate interface file found + raise_error0 + Errors.Fatal_ModuleOrFileNotFound + (Util.format2 "Interface files %s and %s are both in the include path\n" + full_path other) + | _ -> + smap_add map key (Some full_path, impl) + end + else begin + match impl with + | Some other when other <> full_path -> + //duplicate implementation file found + raise_error0 + Errors.Fatal_ModuleOrFileNotFound + (Util.format2 "Files %s and %s are both in the include path\n" + full_path other) + | _ -> smap_add map key (intf, Some full_path) + end | None -> if is_interface full_path then smap_add map key (Some full_path, None) From 9db3e174b74dc743681925784ec41a50f6d4d0b7 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Thu, 23 Jan 2025 15:04:13 +0000 Subject: [PATCH 8/8] normalize file path in duplicate file check --- src/parser/FStarC.Parser.Dep.fst | 1 + 1 file changed, 1 insertion(+) diff --git a/src/parser/FStarC.Parser.Dep.fst b/src/parser/FStarC.Parser.Dep.fst index 28eecec0d23..42307b5d634 100644 --- a/src/parser/FStarC.Parser.Dep.fst +++ b/src/parser/FStarC.Parser.Dep.fst @@ -490,6 +490,7 @@ let build_inclusion_candidates_list (): list (string & string) = let build_map (filenames: list string): files_for_module_name = let map = smap_create 41 in let add_entry key full_path = + let full_path = BU.normalize_file_path full_path in match smap_try_find map key with | Some (intf, impl) -> if is_interface full_path then begin