[require] Basic cache for .vo file interp.

coq/interp.ml

@@ -15,10 +15,27 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
+let hc : (Names.DirPath.t, Library.library_t) Hashtbl.t = Hashtbl.create 1000
+
+let use_cache = true
+
+let intern dp =
+  if use_cache then
+    match Hashtbl.find_opt hc dp with
+    | Some lib -> lib
+    | None ->
+      let lib_resolver = Loadpath.try_locate_absolute_library in
+      let lib = Library.intern_from_file ~lib_resolver dp in
+      let () = Hashtbl.add hc dp lib in
+      lib
+  else
+      let lib_resolver = Loadpath.try_locate_absolute_library in
+      Library.intern_from_file ~lib_resolver dp
+
 let coq_interp ~st cmd =
   let st = State.to_coq st in
   let cmd = Ast.to_coq cmd in
-  Vernacinterp.interp ~st cmd |> State.of_coq
+  Vernacinterp.interp ~intern ~st cmd |> State.of_coq
 
 let interp ~st cmd = Protect.eval cmd ~f:(coq_interp ~st)
 
@@ -28,7 +45,7 @@ module Require = struct
   let interp ~st _files
       { Ast.Require.from; export; mods; loc = _; attrs; control } =
     let () = Vernacstate.unfreeze_full_state (State.to_coq st) in
-    let fn () = Vernacentries.vernac_require from export mods in
+    let fn () = Vernacentries.vernac_require ~intern from export mods in
     (* Check generic attributes *)
     let fn () =
       Synterp.with_generic_atts ~check:true attrs (fun ~atts ->

coq/workspace.ml

@@ -248,13 +248,17 @@ let describe_guess = function
   | Ok w -> describe w
   | Error msg -> (msg, "")
 
+let intern dp =
+  let lib_resolver = Loadpath.try_locate_absolute_library in
+  Library.intern_from_file ~lib_resolver dp
+
 (* Require a set of libraries *)
 let load_objs libs =
   let rq_file (dir, from, exp) =
     let mp = Libnames.qualid_of_string dir in
     let mfrom = Option.map Libnames.qualid_of_string from in
     Flags_.silently
-      (Vernacentries.vernac_require mfrom exp)
+      (Vernacentries.vernac_require ~intern mfrom exp)
       [ (mp, Vernacexpr.ImportAll) ]
   in
   List.(iter rq_file (rev libs))