index: rely on size when mtime differ

voodoos · Jan 8, 2024 · 5d74c46 · 5d74c46
1 parent 69dcc55
commit 5d74c46
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 4 deletions.
diff --git a/src/analysis/index_format.ml b/src/analysis/index_format.ml
@@ -28,12 +28,13 @@ let add tbl uid locs =
     Hashtbl.replace tbl uid (LidSet.union locs locations)
   with Not_found -> Hashtbl.add tbl uid locs
 
+type stat = { mtime : float; size : int }
 type index = {
   defs : (Shape.Uid.t, LidSet.t) Hashtbl.t;
   approximated : (Shape.Uid.t, LidSet.t) Hashtbl.t;
   load_path : string list;
   cu_shape : (string, Shape.t) Hashtbl.t;
-  stats : float Stats.t;
+  stats : stat Stats.t;
 }
 
 let pp_partials (fmt : Format.formatter)

diff --git a/src/analysis/index_format.mli b/src/analysis/index_format.mli
@@ -7,12 +7,13 @@ val add : ('a, LidSet.t) Hashtbl.t -> 'a -> LidSet.t -> unit
 
 module Stats : Map.S with type key = String.t
 
+type stat = { mtime : float; size : int }
 type index = {
   defs : (Shape.Uid.t, LidSet.t) Hashtbl.t;
   approximated : (Shape.Uid.t, LidSet.t) Hashtbl.t;
   load_path : string list;
   cu_shape : (string, Shape.t) Hashtbl.t;
-  stats : float Stats.t;
+  stats : stat Stats.t;
 }
 
 type file_content = Cmt of Cmt_format.cmt_infos | Index of index | Unknown

diff --git a/src/analysis/occurrences.ml b/src/analysis/occurrences.ml
@@ -152,9 +152,13 @@ let check Index_format.{ stats; _ } file =
   let open Index_format in
   match Stats.find_opt file stats with
   | None -> log ~title:"stat_check" "No mtime found for file %S." file; true
-  | Some mtime ->
+  | Some { mtime; size } ->
     try
-      let equal = Float.equal (Unix.stat file).st_mtime mtime in
+      let stats = Unix.stat file in
+      let equal =
+        Float.equal stats.st_mtime mtime
+        || Int.equal stats.st_size size
+      in
       log ~title:"stat_check"
         "File %s has been modified since the index was built." file;
       equal