coqchk: do not validate dependencies of -norec libraries

For instance this halves the time it takes to check
the test-suite/arithmetic/ files.

on mod: 7.5s to 3.4s

1 files changed, 15 insertions, 10 deletions

diff --git a/checker/check.ml b/checker/check.ml
index b2930d9535..1582570530 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -292,6 +292,8 @@ let name_clash_message dir mdir f =
   pr_dirpath mdir ++ spc () ++ str "and not library" ++ spc() ++
   pr_dirpath dir
 
+type intern_mode = Rec | Root | Dep (* Rec = standard, Root = -norec, Dep = dependency of norec *)
+
 (* Dependency graph *)
 let depgraph = ref LibraryMap.empty
 
@@ -304,7 +306,8 @@ let marshal_in_segment f ch =
   with _ ->
     user_err (str "Corrupted file " ++ quote (str f))
 
-let intern_from_file (dir, f) =
+let intern_from_file ~intern_mode (dir, f) =
+  let validate a b c = if intern_mode <> Dep then Validate.validate a b c in
   Flags.if_verbose chk_pp (str"[intern "++str f++str" ...");
   let (sd,md,table,opaque_csts,digest) =
     try
@@ -334,12 +337,12 @@ let intern_from_file (dir, f) =
         user_err ~hdr:"intern_from_file"
           (str "The file "++str f++str " is still a .vio"))
         opaque_csts;
-      Validate.validate !Flags.debug Values.v_univopaques opaque_csts;
+      validate !Flags.debug Values.v_univopaques opaque_csts;
       end;
       (* Verification of the unmarshalled values *)
-      Validate.validate !Flags.debug Values.v_libsum sd;
-      Validate.validate !Flags.debug Values.v_lib md;
-      Validate.validate !Flags.debug Values.v_opaques table;
+      validate !Flags.debug Values.v_libsum sd;
+      validate !Flags.debug Values.v_lib md;
+      validate !Flags.debug Values.v_opaques table;
       Flags.if_verbose chk_pp (str" done]" ++ fnl ());
       let digest =
         if opaque_csts <> None then Safe_typing.Dvivo (digest,udg)
@@ -365,7 +368,7 @@ let get_deps (dir, f) =
 
 (* Read a compiled library and all dependencies, in reverse order.
    Do not include files that are already in the context. *)
-let rec intern_library seen (dir, f) needed =
+let rec intern_library ~intern_mode seen (dir, f) needed =
   if LibrarySet.mem dir seen then failwith "Recursive dependencies!";
   (* Look if in the current logical environment *)
   try let _ = find_library dir in needed
@@ -374,12 +377,13 @@ let rec intern_library seen (dir, f) needed =
   if List.mem_assoc_f DirPath.equal dir needed then needed
   else
     (* [dir] is an absolute name which matches [f] which must be in loadpath *)
-    let m = intern_from_file (dir,f) in
+    let m = intern_from_file ~intern_mode (dir,f) in
     let seen' = LibrarySet.add dir seen in
     let deps =
       Array.map (fun (d,_) -> try_locate_absolute_library d) m.library_deps
     in
-    (dir,m) :: Array.fold_right (intern_library seen') deps needed
+    let intern_mode = match intern_mode with Rec -> Rec | Root | Dep -> Dep in
+    (dir,m) :: Array.fold_right (intern_library ~intern_mode seen') deps needed
 
 (* Compute the reflexive transitive dependency closure *)
 let rec fold_deps seen ff (dir,f) (s,acc) =
@@ -402,8 +406,9 @@ let recheck_library senv ~norec ~admit ~check =
   let ml = List.map try_locate_qualified_library check in
   let nrl = List.map try_locate_qualified_library norec in
   let al =  List.map try_locate_qualified_library admit in
-  let needed = List.rev
-    (List.fold_right (intern_library LibrarySet.empty) (ml@nrl) []) in
+  let needed = List.fold_right (intern_library ~intern_mode:Rec LibrarySet.empty) ml [] in
+  let needed = List.fold_right (intern_library ~intern_mode:Root LibrarySet.empty) nrl needed in
+  let needed = List.rev needed in
   (* first compute the closure of norec, remove closure of check,
      add closure of admit, and finally remove norec and check *)
   let nochk = fold_deps_list LibrarySet.add nrl LibrarySet.empty in