From 684f601524b4c8bb93a2e226f8179936a1f2683d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 3 Jun 2024 17:59:11 +0200
Subject: [PATCH] [wip] [fleche] Basic .vo load cache.

---
 fleche/memo.ml | 31 ++++++++++++++++++++++++++-----
 1 file changed, 26 insertions(+), 5 deletions(-)

diff --git a/fleche/memo.ml b/fleche/memo.ml
index 7b0564dc3..04bfba58e 100644
--- a/fleche/memo.ml
+++ b/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) =