Skip to content

Commit 04c562e

Browse files
Lef IoannidisCopilot
andcommitted
Parser.Dep: respect fstar.include in directory expansion
The all_fstar_files_in_dir function was unconditionally recursing into all subdirectories when --dep was given a directory argument. This changes it to use Find.expand_include_d, which only recurses into subdirectories listed in fstar.include files. Without fstar.include, only F* files in the immediate directory are found. With fstar.include, only the listed subdirectories are traversed (matching the existing behavior of the include path mechanism). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
1 parent 8c6f70d commit 04c562e

File tree

1 file changed

+14
-12
lines changed

1 file changed

+14
-12
lines changed

src/parser/FStarC.Parser.Dep.fst

Lines changed: 14 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1696,18 +1696,20 @@ let collect_deps_of_decl (deps:deps) (filename:string) (ds:list decl)
16961696
* to read the parsing data from checked files
16971697
*)
16981698
1699-
(** Recursively find all F* files in a directory *)
1700-
let rec all_fstar_files_in_dir (dir:string) : ML (list file_name) =
1701-
let files = safe_readdir_for_include dir in
1702-
List.collect (fun f ->
1703-
let full_path = Filepath.join_paths dir f in
1704-
if Filepath.is_directory full_path then
1705-
all_fstar_files_in_dir full_path
1706-
else if List.existsb (fun ext -> Util.ends_with f ext) (all_file_suffixes ()) then
1707-
[full_path]
1708-
else
1709-
[]
1710-
) files
1699+
(** Find all F* files in a directory, respecting fstar.include for subdirectory traversal.
1700+
Uses Find.expand_include_d to determine which subdirectories to visit. *)
1701+
let all_fstar_files_in_dir (dir:string) : ML (list file_name) =
1702+
let dirs = Find.expand_include_d dir in
1703+
List.collect (fun d ->
1704+
let files = safe_readdir_for_include d in
1705+
List.collect (fun f ->
1706+
let full_path = Filepath.join_paths d f in
1707+
if not (Filepath.is_directory full_path)
1708+
&& List.existsb (fun ext -> Util.ends_with f ext) (all_file_suffixes ())
1709+
then [full_path]
1710+
else []
1711+
) files
1712+
) dirs
17111713
17121714
(** Expand any directories in the command line file list to their contained F* files.
17131715
When a module has both .fst and .fsti, only include the .fsti to avoid

0 commit comments

Comments
 (0)