[wip] [fleche] Basic .vo load cache.

fleche/memo.ml

@@ -1,5 +1,30 @@
 module CS = Stats
 
+(* XXX: We are missing good error handling here! Fix upstream. *)
+module Intern = struct
+  let hc :
+      ( Names.DirPath.t
+      , Library.library_t * Library.Intern.Provenance.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 file = Loadpath.try_locate_absolute_library dp in
+        let lib = (Library.intern_from_file file, ("file", file)) in
+        let () = Hashtbl.add hc dp lib in
+        lib
+    else Vernacinterp.fs_intern dp
+end
+
+let intern = Intern.intern
+
+(* Regular memo table *)
 module Stats = struct
   type t =
     { stats : Stats.t
@@ -287,9 +312,7 @@ module VernacEval = struct
 
   type output = Coq.State.t
 
-  let eval ~token (st, stm) =
-    let intern = Vernacinterp.fs_intern in
-    Coq.Interp.interp ~token ~intern ~st stm
+  let eval ~token (st, stm) = Coq.Interp.interp ~token ~intern ~st stm
 end
 
 module Interp = CEval (VernacEval)
@@ -318,7 +341,6 @@ module RequireEval = struct
   type output = Coq.State.t
 
   let eval ~token (st, files, stm) =
-    let intern = Vernacinterp.fs_intern in
     Coq.Interp.Require.interp ~token ~intern ~st files stm
 end
 
@@ -350,7 +372,6 @@ module InitEval = struct
   type output = Coq.State.t
 
   let eval ~token (root_state, workspace, uri) =
-    let intern = Vernacinterp.fs_intern in
     Coq.Init.doc_init ~token ~intern ~root_state ~workspace ~uri
 
   let input_info (st, ws, file) =