Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use the directory of any file on the command line in the include path rather than "." #3690

Open
wants to merge 8 commits into
base: master
Choose a base branch
from
14 changes: 13 additions & 1 deletion src/basic/FStarC.Find.fst
Original file line number Diff line number Diff line change
Expand Up @@ -90,7 +90,18 @@ 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) |>
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
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
Expand All @@ -99,6 +110,7 @@ let do_find (paths : list string) (filename : string) : option string =
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 *)
Expand Down
29 changes: 23 additions & 6 deletions src/parser/FStarC.Parser.Dep.fst
Original file line number Diff line number Diff line change
Expand Up @@ -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))
)
)
Expand All @@ -491,12 +490,30 @@ 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
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)
Expand Down
Loading