Skip to content

Commit

Permalink
[doc] Wait for documents that are non-built.
Browse files Browse the repository at this point in the history
This needs more work, we need a Coq API that we don't have access yet.
  • Loading branch information
ejgallego committed Jan 20, 2024
1 parent 0e58917 commit 53c9e37
Show file tree
Hide file tree
Showing 6 changed files with 108 additions and 32 deletions.
31 changes: 31 additions & 0 deletions coq/files.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
11 changes: 11 additions & 0 deletions coq/files.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
84 changes: 57 additions & 27 deletions fleche/doc.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand All @@ -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
Expand Down Expand Up @@ -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 *)
Expand Down Expand Up @@ -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 =
Expand Down
4 changes: 2 additions & 2 deletions fleche/doc.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 6 additions & 2 deletions fleche/theory.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)))
Expand Down
2 changes: 1 addition & 1 deletion test/compiler/_CoqProject
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-R proj1 .
-R . proj1

a.v
b.v

0 comments on commit 53c9e37

Please sign in to comment.