From 084638c12ae83ecfa975abd6bbc990f6a784a873 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= Date: Sun, 22 Apr 2018 00:27:45 -0400 Subject: [PATCH] ide: Print progress messages while loading dependencies --- src/fstar/FStar.Interactive.Ide.fs | 28 ++++++++++++++++++++++------ 1 file changed, 22 insertions(+), 6 deletions(-) diff --git a/src/fstar/FStar.Interactive.Ide.fs b/src/fstar/FStar.Interactive.Ide.fs index d88047e0edd..0026f14e118 100644 --- a/src/fstar/FStar.Interactive.Ide.fs +++ b/src/fstar/FStar.Interactive.Ide.fs @@ -401,8 +401,11 @@ current file's interface comes last. The original value of the ``repl_deps_stack`` field in ``st`` is used to skip already completed tasks. -This function is stateful: it uses ``push_repl`` and ``pop_repl``. **) -let run_repl_ld_transactions (st: repl_state) (tasks: list) = +This function is stateful: it uses ``push_repl`` and ``pop_repl``. + +`progress_callback` is called once per task, right before the task is run. **) +let run_repl_ld_transactions (st: repl_state) (tasks: list) + (progress_callback: repl_task -> unit) = let debug verb task = if Options.debug_any () then Util.print2 "%s %s" verb (string_of_repl_task task) in @@ -429,6 +432,7 @@ let run_repl_ld_transactions (st: repl_state) (tasks: list) = // run ``task`` and record the updated dependency stack in ``st``. | task :: tasks, [] -> debug "Loading" task; + progress_callback task; Options.restore_cmd_line_options false |> ignore; let timestamped_task = update_task_timestamps task in let push_kind = if Options.lax () then LaxCheck else FullCheck in @@ -571,7 +575,7 @@ let interactive_protocol_features = "describe-protocol"; "describe-repl"; "exit"; "lookup"; "lookup/context"; "lookup/documentation"; "lookup/definition"; "peek"; "pop"; "push"; "search"; "segment"; - "vfs-add"; "tactic-ranges"; "interrupt"] + "vfs-add"; "tactic-ranges"; "interrupt"; "progress"] exception InvalidQuery of string type query_status = | QueryOK | QueryNOK | QueryViolatesProtocol @@ -932,6 +936,18 @@ let run_pop st = let st' = pop_repl st in ((QueryOK, JsonNull), Inl st') +let write_progress stage contents_alist = + let stage = match stage with Some s -> JsonStr s | None -> JsonNull in + let js_contents = ("stage", stage) :: contents_alist in + write_json (json_of_message "progress" (JsonAssoc js_contents)) + +let write_repl_ld_task_progress task = + match task with + | LDInterleaved (_, tf) | LDSingle tf | LDInterfaceOfCurrentFile tf -> + let modname = Parser.Dep.module_name_of_file tf.tf_fname in + write_progress (Some "loading-dependency") [("modname", JsonStr modname)] + | PushFragment frag -> () + (** Compute and load all dependencies of `filename`. Return an new REPL state wrapped in ``Inr`` in case of failure, and a new REPL @@ -942,9 +958,9 @@ let load_deps st = | None -> Inr st | Some (deps, tasks, dep_graph) -> let st = {st with repl_env=FStar.TypeChecker.Env.set_dep_graph st.repl_env dep_graph} in - match run_repl_ld_transactions st tasks with - | Inr st -> Inr st - | Inl st -> Inl (st, deps) + match run_repl_ld_transactions st tasks write_repl_ld_task_progress with + | Inr st -> write_progress None []; Inr st + | Inl st -> write_progress None []; Inl (st, deps) let rephrase_dependency_error issue = { issue with issue_message =