From 04c562ecbbe056f52aa87f329287340df8041821 Mon Sep 17 00:00:00 2001 From: Lef Ioannidis Date: Tue, 31 Mar 2026 22:51:24 +0000 Subject: [PATCH 1/2] 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> --- src/parser/FStarC.Parser.Dep.fst | 26 ++++++++++++++------------ 1 file changed, 14 insertions(+), 12 deletions(-) diff --git a/src/parser/FStarC.Parser.Dep.fst b/src/parser/FStarC.Parser.Dep.fst index a25e8477d64..6242b54214a 100644 --- a/src/parser/FStarC.Parser.Dep.fst +++ b/src/parser/FStarC.Parser.Dep.fst @@ -1696,18 +1696,20 @@ let collect_deps_of_decl (deps:deps) (filename:string) (ds:list decl) * to read the parsing data from checked files *) -(** Recursively find all F* files in a directory *) -let rec all_fstar_files_in_dir (dir:string) : ML (list file_name) = - let files = safe_readdir_for_include dir in - List.collect (fun f -> - let full_path = Filepath.join_paths dir f in - if Filepath.is_directory full_path then - all_fstar_files_in_dir full_path - else if List.existsb (fun ext -> Util.ends_with f ext) (all_file_suffixes ()) then - [full_path] - else - [] - ) files +(** Find all F* files in a directory, respecting fstar.include for subdirectory traversal. + Uses Find.expand_include_d to determine which subdirectories to visit. *) +let all_fstar_files_in_dir (dir:string) : ML (list file_name) = + let dirs = Find.expand_include_d dir in + List.collect (fun d -> + let files = safe_readdir_for_include d in + List.collect (fun f -> + let full_path = Filepath.join_paths d f in + if not (Filepath.is_directory full_path) + && List.existsb (fun ext -> Util.ends_with f ext) (all_file_suffixes ()) + then [full_path] + else [] + ) files + ) dirs (** Expand any directories in the command line file list to their contained F* files. When a module has both .fst and .fsti, only include the .fsti to avoid From 87ec61129d504cfed0654bd6b66e04f8451dea99 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 2 Apr 2026 10:07:23 -0700 Subject: [PATCH 2/2] Parser.Dep: remove strange fst filtering --- src/parser/FStarC.Parser.Dep.fst | 24 +++--------------------- 1 file changed, 3 insertions(+), 21 deletions(-) diff --git a/src/parser/FStarC.Parser.Dep.fst b/src/parser/FStarC.Parser.Dep.fst index 6242b54214a..e1d109c43b2 100644 --- a/src/parser/FStarC.Parser.Dep.fst +++ b/src/parser/FStarC.Parser.Dep.fst @@ -1711,32 +1711,14 @@ let all_fstar_files_in_dir (dir:string) : ML (list file_name) = ) files ) dirs -(** Expand any directories in the command line file list to their contained F* files. - When a module has both .fst and .fsti, only include the .fsti to avoid - "breaking abstraction" errors. *) +(** Expand any directories in the command line file list to their contained F* files. *) let expand_directories (files: list file_name) : ML (list file_name) = - let all_files = List.collect (fun f -> + files |> List.collect (fun f -> if Filepath.is_directory f then all_fstar_files_in_dir f else [f] - ) files in - (* Filter out .fst files when corresponding .fsti exists *) - let fsti_set : RBSet.t string = - List.fold_left (fun acc f -> - if Util.ends_with f ".fsti" then - let base = String.substring f 0 (String.length f - 1) in (* remove trailing 'i' to get .fst *) - RBSet.add base acc - else acc - ) (RBSet.empty ()) all_files - in - List.filter (fun f -> - if Util.ends_with f ".fst" && not (Util.ends_with f ".fsti") then - (* Only keep .fst if there's no corresponding .fsti *) - not (RBSet.mem f fsti_set) - else - true - ) all_files + ) (* In public interface *) let collect (all_cmd_line_files: list file_name)