[doc] Wait for documents that are non-built.

This needs more work, we need a Coq API that we don't have access yet.

coq/files.ml

@@ -15,10 +15,41 @@
 (* Written by: Emilio J. Gallego Arias & Bhakti Shah                    *)
 (************************************************************************)
 
+open Base
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
 
 type t = int [@@deriving hash, compare]
 
 let make () = 0
 let bump i = i + 1
+
+let qualid_to_dirpath qid =
+  let hd, tl = Libnames.repr_qualid qid in
+  Libnames.add_dirpath_suffix hd tl
+
+module Require_result = struct
+  type t =
+    | Ready of
+        (Names.DirPath.t * CUnix.physical_path, Loadpath.locate_error) Result.t
+        list
+    | Wait of CUnix.physical_path list
+end
+
+let check_file_ready ?root (m, _imports) =
+  match Loadpath.locate_qualified_library ?root m with
+  | Ok (dirpath, file) ->
+    let () =
+      Stdlib.Format.eprintf "found file: %s for library %s@\n%!" file
+        (Names.DirPath.to_string dirpath)
+    in
+    let ready = true in
+    (* Hook for the document manager *)
+    if ready then Ok (Ok (dirpath, file)) else Error file
+  | Error e -> Ok (Error e)
+
+let requires_are_ready ~files:_ { Ast.Require.from; export = _; mods; _ } =
+  let root = Option.map ~f:qualid_to_dirpath from in
+  match List.map ~f:(check_file_ready ?root) mods |> Result.combine_errors with
+  | Ok r -> Require_result.Ready r
+  | Error f -> Wait f

coq/files.mli

@@ -21,3 +21,14 @@ val make : unit -> t
 
 (** [bump ()] Signal the files have changed *)
 val bump : t -> t
+
+(** Check if a file is ready *)
+module Require_result : sig
+  type t =
+    | Ready of
+        (Names.DirPath.t * CUnix.physical_path, Loadpath.locate_error) Result.t
+        list
+    | Wait of CUnix.physical_path list
+end
+
+val requires_are_ready : files:t -> Ast.Require.t -> Require_result.t

fleche/doc.ml

@@ -206,7 +206,7 @@ module Completion = struct
   type t =
     | Yes of Lang.Range.t  (** Location of the last token in the document *)
     | Stopped of Lang.Range.t  (** Location of the last valid token *)
-    | Waiting of Lang.Range.t * Lang.LUri.File.t
+    | Waiting of Lang.Range.t * string list
     | Failed of Lang.Range.t  (** Critical failure, like an anomaly *)
     | FailedPermanent of Lang.Range.t
         (** Temporal Coq hack, avoids any computation *)
@@ -231,8 +231,8 @@ module Completion = struct
     | _ -> false
 
   let is_waiting_for = function
-    | Waiting (_, doc) -> Some doc
-    | _ -> None
+    | Waiting (_, doc) -> doc
+    | _ -> []
 end
 
 (** Enviroment external to the document, this includes for now the [init] Coq
@@ -640,23 +640,35 @@ end = struct
     | Completed (Error _) -> st
 end
 
+(* Returns [Left st] if requires are ready, [Right *)
 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)
+  | None -> Either.Left (Memo.Interp.eval (st, ast))
+  | Some ast -> (
+    let res = Coq.Files.requires_are_ready ~files ast in
+    match res with
+    | Coq.Files.Require_result.Ready _ ->
+      Left (Memo.Require.eval (st, files, ast))
+    | Coq.Files.Require_result.Wait files -> Right files)
 
 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 } =
-    interp_and_info ~st ~files ast
-  in
+  let res = interp_and_info ~st ~files ast in
   let { Gc.major_words = mw_after; _ } = Gc.quick_stat () in
   let stats = Stats.dump () in
-  let info =
-    Node.Info.make ~cache_hit ~parsing_time ~time ~mw_prev ~mw_after ~stats ()
-  in
-  (res, info)
+  match res with
+  | Either.Left { Memo.Stats.res; cache_hit; memory = _; time } ->
+    let info =
+      Node.Info.make ~cache_hit ~parsing_time ~time ~mw_prev ~mw_after ~stats ()
+    in
+    Either.Left (res, info)
+  | Right files ->
+    let time = 0.0 in
+    let info =
+      Node.Info.make ~parsing_time ~time ~mw_prev ~mw_after ~stats ()
+    in
+    Right (files, info)
 
 type parse_action =
   | EOF of Completion.t (* completed *)
@@ -793,25 +805,43 @@ let document_action ~st ~parsing_diags ~parsing_feedback ~parsing_time ~doc
   (* We can interpret the command now *)
   | Process ast -> (
     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
-    | Coq.Protect.R.Interrupted ->
-      (* Exit *)
-      Interrupted last_tok
-    | Coq.Protect.R.Completed res ->
+    match interp_and_info ~parsing_time ~st ~files ast with
+    | Right (files, info) ->
       let ast_loc = Coq.Ast.loc ast |> Option.get in
       let ast_range = Coq.Utils.to_range ~lines ast_loc in
       let ast =
-        Node.Ast.{ v = ast; ast_info = Coq.Ast.make_info ~lines ~st ast }
+        Some Node.Ast.{ v = ast; ast_info = Coq.Ast.make_info ~lines ~st ast }
+      in
+      (* XXX add waiting for *)
+      let diags, messages =
+        assemble_diags ~range:ast_range ~parsing_diags ~parsing_feedback
+          ~diags:[] ~feedback:[]
+      in
+      let node =
+        { Node.range = ast_range; ast; state = st; diags; messages; info }
+      in
+      Stop (Completion.Waiting (last_tok, files), node)
+    | Left (process_res, info) -> (
+      let f = Coq.Utils.to_range ~lines in
+      let { Coq.Protect.E.r; feedback } =
+        Coq.Protect.E.map_loc ~f process_res
       in
-      (* The evaluation by Coq fully completed, then we can resume checking from
-         this point then, hence the new last valid token last_tok_new *)
-      let last_tok_new = Coq.Parsing.Parsable.loc doc_handle in
-      let last_tok_new = Coq.Utils.to_range ~lines last_tok_new in
-      node_of_coq_result ~doc ~range:ast_range ~ast ~st ~parsing_diags
-        ~parsing_feedback ~feedback ~info last_tok_new res)
+      match r with
+      | Coq.Protect.R.Interrupted ->
+        (* Exit *)
+        Interrupted last_tok
+      | Coq.Protect.R.Completed res ->
+        let ast_loc = Coq.Ast.loc ast |> Option.get in
+        let ast_range = Coq.Utils.to_range ~lines ast_loc in
+        let ast =
+          Node.Ast.{ v = ast; ast_info = Coq.Ast.make_info ~lines ~st ast }
+        in
+        (* The evaluation by Coq fully completed, then we can resume checking
+           from this point then, hence the new last valid token last_tok_new *)
+        let last_tok_new = Coq.Parsing.Parsable.loc doc_handle in
+        let last_tok_new = Coq.Utils.to_range ~lines last_tok_new in
+        node_of_coq_result ~doc ~range:ast_range ~ast ~st ~parsing_diags
+          ~parsing_feedback ~feedback ~info last_tok_new res))
 
 module Target = struct
   type t =

fleche/doc.mli

@@ -51,13 +51,13 @@ module Completion : sig
   type t = private
     | Yes of Lang.Range.t  (** Location of the last token in the document *)
     | Stopped of Lang.Range.t  (** Location of the last valid token *)
-    | Waiting of Lang.Range.t * Lang.LUri.File.t
+    | Waiting of Lang.Range.t * string list  (** Waiting for files *)
     | Failed of Lang.Range.t  (** Critical failure, like an anomaly *)
     | FailedPermanent of Lang.Range.t
         (** Temporal Coq hack, avoids any computation *)
 
   val is_completed : t -> bool
-  val is_waiting_for : t -> Lang.LUri.File.t option
+  val is_waiting_for : t -> string list
 end
 
 (** Enviroment external to the document, this includes for now the [init] Coq

fleche/theory.ml

@@ -227,8 +227,12 @@ end = struct
         if Doc.Completion.is_completed doc.completed then
           pending := pend_pop !pending;
         match Doc.Completion.is_waiting_for doc.completed with
-        | None -> Some (requests, doc)
-        | Some uri ->
+        | [] -> Some (requests, doc)
+        | file :: _ ->
+          let uri =
+            Lang.LUri.of_string (Format.asprintf "file:///%s" file)
+            |> Lang.LUri.File.of_uri |> Result.get_ok
+          in
           schedule ~uri;
           (* todo add to handler: rev_dep of uri *)
           Some (requests, doc)))

test/compiler/_CoqProject

@@ -1,4 +1,4 @@
--R proj1 .
+-R . proj1
 
 a.v
 b.v