From 0a2a26e7d2ab5e747912a27b5d65f287529fb5ec Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 19 Jan 2024 23:45:55 +0100 Subject: [PATCH] [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 | 31 ++++++++++++++++++ coq/files.mli | 11 +++++++ fleche/doc.ml | 84 ++++++++++++++++++++++++++++++++---------------- fleche/doc.mli | 4 +-- fleche/theory.ml | 8 +++-- 5 files changed, 107 insertions(+), 31 deletions(-) diff --git a/coq/files.ml b/coq/files.ml index f83c03ef..8342dc6a 100644 --- a/coq/files.ml +++ b/coq/files.ml @@ -15,6 +15,7 @@ (* Written by: Emilio J. Gallego Arias & Bhakti Shah *) (************************************************************************) +open Base open Ppx_hash_lib.Std.Hash.Builtin open Ppx_compare_lib.Builtin @@ -22,3 +23,33 @@ 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 diff --git a/coq/files.mli b/coq/files.mli index daec288c..6866b87d 100644 --- a/coq/files.mli +++ b/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 diff --git a/fleche/doc.ml b/fleche/doc.ml index e5fffeba..a71bb2bd 100644 --- a/fleche/doc.ml +++ b/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 = diff --git a/fleche/doc.mli b/fleche/doc.mli index 358d234e..153f68e5 100644 --- a/fleche/doc.mli +++ b/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 diff --git a/fleche/theory.ml b/fleche/theory.ml index 78663f4b..df119606 100644 --- a/fleche/theory.ml +++ b/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)))