[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 <[email protected]>

CHANGES.md

@@ -56,6 +56,8 @@
    (@ejgallego, #660)
  - monitor all Coq-level calls under an interruption token
    (@ejgallego, #661)
+ - interpret require thru our own custom execution env-aware path
+   (@bhaktishh, @ejgallego, #642, #643, #644)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

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 ~token ~env ~uri ~raw ~version:1 in
     match Theory.Check.maybe_check ~io ~token with

controller/lsp_core.ml

@@ -263,7 +263,8 @@ let do_open ~io ~token ~(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 ~token ~env ~uri ~raw:text ~version
 
 let do_change ~ofn ~io ~token params =

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
@@ -634,11 +635,16 @@ end = struct
     | Completed (Error _) -> st
 end
 
-let interp_and_info ~token ~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 ~token ~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 ~token (st, ast)
+    interp_and_info ~token ~st ~files ast
   in
   let { Gc.major_words = mw_after; _ } = Gc.quick_stat () in
   let stats = Stats.dump () in
@@ -779,8 +785,10 @@ let document_action ~token ~st ~parsing_diags ~parsing_feedback ~parsing_time
     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 ~token ~parsing_time ~st ast in
+    let lines, files = (doc.contents.lines, doc.env.files) in
+    let process_res, info =
+      interp_and_info ~token ~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

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