From 1d3e516b409583c4565cfb3a41e34d8fcdeeb9be Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Fri, 19 Jan 2024 17:53:54 +0100
Subject: [PATCH] [fleche] [doc] Interpret require via special custom path.

This will allow us to:

- postpone the document checking when the require is not ready
- correctly track file dependencies in memoization
- apply the .vo parsing optimization, by intercepting the call

Co-authored-by: BHAKTISHAH <shahbhakti21@gmail.com>
---
 CHANGES.md             |  2 ++
 compiler/compile.ml    |  3 ++-
 controller/lsp_core.ml |  3 ++-
 fleche/doc.ml          | 16 +++++++++++-----
 fleche/doc.mli         |  4 +++-
 5 files changed, 20 insertions(+), 8 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index ec0986a1f..fee8cbd0b 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -51,6 +51,8 @@
  - new option `--no_vo` for `fcc`, which will skip the `.vo` saving
    step. `.vo` saving is now an `fcc` plugins, but for now, it is
    enabled by default (@ejgallego, #650)
+ - interpret require thru our own custom execution env-aware path
+   (@bhaktishh, @ejgallego, #642, #643, #644)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------
diff --git a/compiler/compile.ml b/compiler/compile.ml
index f99ba0199..4d67929a2 100644
--- a/compiler/compile.ml
+++ b/compiler/compile.ml
@@ -33,7 +33,8 @@ let compile_file ~cc file =
   | Error _ -> ()
   | Ok uri -> (
     let workspace = workspace_of_uri ~io ~workspaces ~uri ~default in
-    let env = Doc.Env.make ~init:root_state ~workspace in
+    let files = Coq.Files.make () in
+    let env = Doc.Env.make ~init:root_state ~workspace ~files in
     let raw = Util.input_all file in
     let () = Theory.create ~io ~env ~uri ~raw ~version:1 in
     match Theory.Check.maybe_check ~io with
diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml
index 2ab779e37..27995887c 100644
--- a/controller/lsp_core.ml
+++ b/controller/lsp_core.ml
@@ -256,7 +256,8 @@ let do_open ~io ~(state : State.t) params =
   in
   let Lsp.Doc.TextDocumentItem.{ uri; version; text; _ } = document in
   let init, workspace = State.workspace_of_uri ~uri ~state in
-  let env = Fleche.Doc.Env.make ~init ~workspace in
+  let files = Coq.Files.make () in
+  let env = Fleche.Doc.Env.make ~init ~workspace ~files in
   Fleche.Theory.create ~io ~env ~uri ~raw:text ~version
 
 let do_change ~ofn ~io params =
diff --git a/fleche/doc.ml b/fleche/doc.ml
index 4385d6ac0..7990cda0f 100644
--- a/fleche/doc.ml
+++ b/fleche/doc.ml
@@ -231,9 +231,10 @@ module Env = struct
   type t =
     { init : Coq.State.t
     ; workspace : Coq.Workspace.t
+    ; files : Coq.Files.t
     }
 
-  let make ~init ~workspace = { init; workspace }
+  let make ~init ~workspace ~files = { init; workspace; files }
 end
 
 (** A Flèche document is basically a [node list], which is a crude form of a
@@ -626,11 +627,16 @@ end = struct
     | Completed (Error _) -> st
 end
 
-let interp_and_info ~parsing_time ~st ast =
+let interp_and_info ~st ~files ast =
+  match Coq.Ast.Require.extract ast with
+  | None -> Memo.Interp.eval (st, ast)
+  | Some ast -> Memo.Require.eval (st, files, ast)
+
+let interp_and_info ~parsing_time ~st ~files ast =
   let { Gc.major_words = mw_prev; _ } = Gc.quick_stat () in
   (* memo memory stats are disabled: slow and misleading *)
   let { Memo.Stats.res; cache_hit; memory = _; time } =
-    Memo.Interp.eval (st, ast)
+    interp_and_info ~st ~files ast
   in
   let { Gc.major_words = mw_after; _ } = Gc.quick_stat () in
   let stats = Stats.dump () in
@@ -771,8 +777,8 @@ let document_action ~st ~parsing_diags ~parsing_feedback ~parsing_time ~doc
     Continue { state = st; last_tok; node }
   (* We can interpret the command now *)
   | Process ast -> (
-    let lines = doc.contents.lines in
-    let process_res, info = interp_and_info ~parsing_time ~st ast in
+    let lines, files = (doc.contents.lines, doc.env.files) in
+    let process_res, info = interp_and_info ~parsing_time ~st ~files ast in
     let f = Coq.Utils.to_range ~lines in
     let { Coq.Protect.E.r; feedback } = Coq.Protect.E.map_loc ~f process_res in
     match r with
diff --git a/fleche/doc.mli b/fleche/doc.mli
index ec1b2e2e2..b1e2bf32b 100644
--- a/fleche/doc.mli
+++ b/fleche/doc.mli
@@ -65,9 +65,11 @@ module Env : sig
   type t = private
     { init : Coq.State.t
     ; workspace : Coq.Workspace.t
+    ; files : Coq.Files.t
     }
 
-  val make : init:Coq.State.t -> workspace:Coq.Workspace.t -> t
+  val make :
+    init:Coq.State.t -> workspace:Coq.Workspace.t -> files:Coq.Files.t -> t
 end
 
 (** A Flèche document is basically a [node list], which is a crude form of a