Lef/everparse absolute fix

src/basic/FStarC.Filepath.fsti

@@ -35,3 +35,6 @@ val canonicalize : string -> string
 
 (* Like canonicalize, but always returns an absolute path. *)
 val normalize_file_path: string -> ML string
+
+(* Make a path relative to the current working directory. *)
+val make_relative_to_cwd: string -> ML string

src/ml/FStarC_Filepath.ml

@@ -63,3 +63,20 @@ let file_exists = Sys.file_exists
 (* Sys.is_directory raises Sys_error if the path does not exist *)
 let is_directory f = Sys.file_exists f && Sys.is_directory f
 
+let make_relative_to_cwd (path:string) : string =
+  if not (is_path_absolute path) then path
+  else
+    let path = normalize_file_path path in
+    let cwd  = normalize_file_path (Sys.getcwd ()) in
+    let split s = List.filter (fun x -> x <> "") (BatString.nsplit s ~by:"/") in
+    let path_parts = split path in
+    let cwd_parts  = split cwd  in
+    let rec skip_common pp cp =
+      match pp, cp with
+      | ph :: pt, ch :: ct when ph = ch -> skip_common pt ct
+      | _ -> (pp, cp)
+    in
+    let (remaining_path, remaining_cwd) = skip_common path_parts cwd_parts in
+    let ups = List.map (fun _ -> "..") remaining_cwd in
+    String.concat "/" (ups @ remaining_path)
+

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 
@@ -2065,7 +2067,10 @@ let print_full (outc : out_channel) (deps:deps) : ML unit =
     in
     let sb = FStarC.StringBuffer.create 10000 in
     let pr str = ignore <| FStarC.StringBuffer.add str sb in
-    let norm_path s = replace_chars (replace_chars s '\\' "/") ' ' "\\ " in
+    let norm_path s =
+      let s = Filepath.make_relative_to_cwd s in
+      replace_chars (replace_chars s '\\' "/") ' ' "\\ "
+    in
     let print_entry (target : string) (all_deps : list string) : ML unit =
         (* Print a target with dependencies. *)
         pr target; pr ":";