From cadd3318d09f71893bf824a97443106f5bcacd2d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 26 Jun 2023 14:28:46 +0200
Subject: [PATCH 1/2] [fleche] Abstract IO callbacks from LSP transport detail.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This ensures that Flèche knows nothing about LSP, which is required
for #507 and also for the next commit that will move the `Doc_manager`
to Flèche (where it belongs)
---
 controller/coq_lsp.ml           | 37 ++++++++++++++----------
 controller/doc_manager.ml       | 51 +++++++++++++++------------------
 controller/doc_manager.mli      |  7 ++---
 controller/lsp_core.ml          | 36 +++++++++++------------
 controller/lsp_core.mli         |  5 +++-
 controller/perf.ml              | 44 ----------------------------
 editor/code/lib/types.ts        |  1 +
 fleche/doc.ml                   | 22 +++++++-------
 fleche/doc.mli                  |  8 +++---
 fleche/io.ml                    | 26 +++++++----------
 fleche/io.mli                   | 19 +++++-------
 fleche/perf.ml                  | 19 ++++++++++++
 {controller => fleche}/perf.mli | 13 ++++++++-
 fleche/perf_analysis.ml         | 38 ++++++++++++++++++++++++
 fleche/perf_analysis.mli        |  1 +
 fleche/progress.ml              |  1 -
 lsp/jFleche.ml                  | 16 +++++------
 lsp/jFleche.mli                 | 18 +++++++-----
 18 files changed, 191 insertions(+), 171 deletions(-)
 delete mode 100644 controller/perf.ml
 create mode 100644 fleche/perf.ml
 rename {controller => fleche}/perf.mli (72%)
 create mode 100644 fleche/perf_analysis.ml
 create mode 100644 fleche/perf_analysis.mli

diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml
index 69355930..8bb0050d 100644
--- a/controller/coq_lsp.ml
+++ b/controller/coq_lsp.ml
@@ -31,10 +31,10 @@ let exit_message () =
 
 let lsp_cleanup () = exit_message ()
 
-let rec process_queue ~delay ~ofn ~state : unit =
+let rec process_queue ~delay ~io ~ofn ~state : unit =
   if Fleche.Debug.sched_wakeup then
     LIO.trace "<- dequeue" (Format.asprintf "%.2f" (Unix.gettimeofday ()));
-  match dispatch_or_resume_check ~ofn ~state with
+  match dispatch_or_resume_check ~io ~ofn ~state with
   | None ->
     (* As of now, we exit the whole program here, we could try an experiment to
        invert the threads, so the I/O routine is a thread and process_queue is
@@ -45,28 +45,28 @@ let rec process_queue ~delay ~ofn ~state : unit =
     exit 0
   | Some (Yield state) ->
     Thread.delay delay;
-    process_queue ~delay ~ofn ~state
-  | Some (Cont state) -> process_queue ~delay ~ofn ~state
+    process_queue ~delay ~io ~ofn ~state
+  | Some (Cont state) -> process_queue ~delay ~io ~ofn ~state
 
-let concise_cb =
+let concise_cb ofn =
   Fleche.Io.CallBack.
     { trace = (fun _hdr ?extra:_ _msg -> ())
     ; send_diagnostics =
-        (fun ~ofn ~uri ~version diags ->
+        (fun ~uri ~version diags ->
           if List.length diags > 0 then
             Lsp.JLang.mk_diagnostics ~uri ~version diags |> ofn)
-    ; send_fileProgress = (fun ~ofn:_ ~uri:_ ~version:_ _progress -> ())
+    ; send_fileProgress = (fun ~uri:_ ~version:_ _progress -> ())
     }
 
 (* Main loop *)
-let lsp_cb =
+let lsp_cb ofn =
   Fleche.Io.CallBack.
     { trace = LIO.trace
     ; send_diagnostics =
-        (fun ~ofn ~uri ~version diags ->
+        (fun ~uri ~version diags ->
           Lsp.JLang.mk_diagnostics ~uri ~version diags |> ofn)
     ; send_fileProgress =
-        (fun ~ofn ~uri ~version progress ->
+        (fun ~uri ~version progress ->
           Lsp.JFleche.mk_progress ~uri ~version progress |> ofn)
     }
 
@@ -97,7 +97,9 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path delay =
   (* Set log channels *)
   let ofn = LIO.send_json Format.std_formatter in
   LIO.set_log_fn ofn;
-  Fleche.Io.CallBack.set lsp_cb;
+
+  let io = lsp_cb ofn in
+  Fleche.Io.CallBack.set io;
 
   (* IMPORTANT: LSP spec forbids any message from server to client before
      initialize is received *)
@@ -130,9 +132,14 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path delay =
   try
     (* LSP Server server initialization *)
     let workspaces = lsp_init_loop ~ifn ~ofn ~cmdline ~debug in
-    if !Fleche.Config.v.verbosity < 2 then (
-      LIO.set_log_fn (fun _obj -> ());
-      Fleche.Io.CallBack.set concise_cb);
+    let io =
+      if !Fleche.Config.v.verbosity < 2 then (
+        LIO.set_log_fn (fun _obj -> ());
+        let io = concise_cb ofn in
+        Fleche.Io.CallBack.set io;
+        io)
+      else io
+    in
 
     (* Core LSP loop context *)
     let state = { State.root_state; cmdline; workspaces } in
@@ -140,7 +147,7 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path delay =
     (* Read workspace state (noop for now) *)
     Cache.read_from_disk ();
 
-    let pfn () : unit = process_queue ~delay ~ofn ~state in
+    let pfn () : unit = process_queue ~delay ~io ~ofn ~state in
     let (_ : Thread.t) = Thread.create pfn () in
 
     read_loop ()
diff --git a/controller/doc_manager.ml b/controller/doc_manager.ml
index e71588a6..39529a5c 100644
--- a/controller/doc_manager.ml
+++ b/controller/doc_manager.ml
@@ -138,19 +138,17 @@ end
 let diags_of_doc doc =
   List.concat_map Fleche.Doc.Node.diags doc.Fleche.Doc.nodes
 
-let send_diags ~ofn ~doc =
+let send_diags ~io ~doc =
   let diags = diags_of_doc doc in
   if List.length diags > 0 || !Fleche.Config.v.verbosity > 1 then
-    let diags =
-      Lsp.JLang.mk_diagnostics ~uri:doc.uri ~version:doc.version diags
-    in
-    ofn diags
+    let uri, version = (doc.uri, doc.version) in
+    Fleche.Io.Report.diagnostics ~io ~uri ~version diags
 
-let send_perf_data ~ofn ~(doc : Fleche.Doc.t) =
+let send_perf_data ~io ~(doc : Fleche.Doc.t) =
   match doc.completed with
   | Yes _ ->
-    let params = Perf.make doc in
-    Lsp.Base.mk_notification ~method_:"$/coq/filePerfData" ~params |> ofn
+    let uri, version = (doc.uri, doc.version) in
+    Fleche.Io.Report.perfData ~io ~uri ~version (Fleche.Perf_analysis.make doc)
   | _ -> ()
 
 let completed ~(doc : Fleche.Doc.t) =
@@ -161,9 +159,7 @@ let completed ~(doc : Fleche.Doc.t) =
 module Check : sig
   val schedule : uri:Lang.LUri.File.t -> unit
   val deschedule : uri:Lang.LUri.File.t -> unit
-
-  val maybe_check :
-    ofn:(Yojson.Safe.t -> unit) -> (Int.Set.t * Fleche.Doc.t) option
+  val maybe_check : io:Fleche.Io.CallBack.t -> (Int.Set.t * Fleche.Doc.t) option
 end = struct
   let pending = ref None
 
@@ -173,17 +169,17 @@ end = struct
       (List.nth_opt pt_requests 0)
 
   (* Notification handling; reply is optional / asynchronous *)
-  let check ~ofn ~uri =
+  let check ~io ~uri =
     LIO.trace "process_queue" "resuming document checking";
     match Handle.find_opt ~uri with
     | Some handle ->
       let target = get_check_target handle.pt_requests in
-      let doc = Fleche.Doc.check ~ofn ~target ~doc:handle.doc () in
+      let doc = Fleche.Doc.check ~io ~target ~doc:handle.doc () in
       let requests = Handle.update_doc_info ~handle ~doc in
-      send_diags ~ofn ~doc;
+      send_diags ~io ~doc;
       if !Fleche.Config.v.verbosity > 1 then
         if (* Only if completed! *)
-           completed ~doc then send_perf_data ~ofn ~doc;
+           completed ~doc then send_perf_data ~io ~doc;
       (* Only if completed! *)
       if completed ~doc then pending := None;
       Some (requests, doc)
@@ -192,7 +188,7 @@ end = struct
         ("file " ^ Lang.LUri.File.to_string_uri uri ^ " not available");
       None
 
-  let maybe_check ~ofn = Option.bind !pending (fun uri -> check ~ofn ~uri)
+  let maybe_check ~io = Option.bind !pending (fun uri -> check ~io ~uri)
   let schedule ~uri = pending := Some uri
 
   let deschedule ~uri =
@@ -200,16 +196,15 @@ end = struct
       pending := None
 end
 
-let send_error_permanent_fail ~ofn ~uri ~version message =
+let send_error_permanent_fail ~io ~uri ~version message =
   let open Lang in
   let start = Point.{ line = 0; character = 0; offset = 0 } in
   let end_ = Point.{ line = 0; character = 1; offset = 1 } in
   let range = Range.{ start; end_ } in
   let d = Lang.Diagnostic.{ range; severity = 1; message; extra = None } in
-  let diags = Lsp.JLang.mk_diagnostics ~uri ~version [ d ] in
-  ofn diags
+  Fleche.Io.Report.diagnostics ~io ~uri ~version [ d ]
 
-let create ~ofn ~root_state ~workspace ~uri ~raw ~version =
+let create ~io ~root_state ~workspace ~uri ~raw ~version =
   let r = Fleche.Doc.create ~state:root_state ~workspace ~uri ~raw ~version in
   match r with
   | Completed (Result.Ok doc) ->
@@ -224,7 +219,7 @@ let create ~ofn ~root_state ~workspace ~uri ~raw ~version =
       Format.asprintf "Fleche.Doc.create, internal error: @[%a@]" Pp.pp_with msg
     in
     LIO.logMessage ~lvl:1 ~message;
-    send_error_permanent_fail ~ofn ~uri ~version (Pp.str message)
+    send_error_permanent_fail ~io ~uri ~version (Pp.str message)
   | Interrupted -> ()
 
 (* Set this to false for < 8.18, we could parse the version but not worth it. *)
@@ -242,7 +237,7 @@ let sane_coq_version =
 (* Can't wait for the day this goes away *)
 let tainted = ref false
 
-let create ~ofn ~root_state ~workspace ~uri ~raw ~version =
+let create ~io ~root_state ~workspace ~uri ~raw ~version =
   if !tainted && not sane_coq_version then (
     (* Error due to Coq bug *)
     let message =
@@ -258,12 +253,12 @@ let create ~ofn ~root_state ~workspace ~uri ~raw ~version =
      with
     | Fleche.Contents.R.Error _e -> ()
     | Ok doc -> Handle.create ~uri ~doc);
-    send_error_permanent_fail ~ofn ~uri ~version (Pp.str message))
+    send_error_permanent_fail ~io ~uri ~version (Pp.str message))
   else (
     tainted := true;
-    create ~ofn ~root_state ~workspace ~uri ~raw ~version)
+    create ~io ~root_state ~workspace ~uri ~raw ~version)
 
-let change ~ofn ~(doc : Fleche.Doc.t) ~version ~raw =
+let change ~io ~(doc : Fleche.Doc.t) ~version ~raw =
   let uri = doc.uri in
   LIO.trace "bump file"
     (Lang.LUri.File.to_string_uri uri ^ " / version: " ^ string_of_int version);
@@ -272,7 +267,7 @@ let change ~ofn ~(doc : Fleche.Doc.t) ~version ~raw =
   | Fleche.Contents.R.Error e ->
     (* Send diagnostics for content conversion *)
     let message = Pp.(str "Error in document conversion: " ++ str e) in
-    send_error_permanent_fail ~ofn ~uri ~version message;
+    send_error_permanent_fail ~io ~uri ~version message;
     Handle.clear_requests ~uri
   | Fleche.Contents.R.Ok doc ->
     let diff = Unix.gettimeofday () -. tb in
@@ -281,14 +276,14 @@ let change ~ofn ~(doc : Fleche.Doc.t) ~version ~raw =
     Check.schedule ~uri;
     invalid_reqs
 
-let change ~ofn ~uri ~version ~raw =
+let change ~io ~uri ~version ~raw =
   match Handle.find_opt ~uri with
   | None ->
     LIO.trace "DocHandle.find"
       ("file " ^ Lang.LUri.File.to_string_uri uri ^ " not available");
     Int.Set.empty
   | Some { doc; _ } ->
-    if version > doc.version then change ~ofn ~doc ~version ~raw
+    if version > doc.version then change ~io ~doc ~version ~raw
     else
       (* That's a weird case, get got changes without a version bump? Do nothing
          for now *)
diff --git a/controller/doc_manager.mli b/controller/doc_manager.mli
index a3b39da1..d5a09958 100644
--- a/controller/doc_manager.mli
+++ b/controller/doc_manager.mli
@@ -19,13 +19,12 @@ module Check : sig
   (** Check pending documents, return [None] if there is none pending, or
       [Some rqs] the list of requests ready to execute after the check. Sends
       progress and diagnostics notifications using output function [ofn]. *)
-  val maybe_check :
-    ofn:(Yojson.Safe.t -> unit) -> (Int.Set.t * Fleche.Doc.t) option
+  val maybe_check : io:Fleche.Io.CallBack.t -> (Int.Set.t * Fleche.Doc.t) option
 end
 
 (** Create a document *)
 val create :
-     ofn:(Yojson.Safe.t -> unit)
+     io:Fleche.Io.CallBack.t
   -> root_state:Coq.State.t
   -> workspace:Coq.Workspace.t
   -> uri:Lang.LUri.File.t
@@ -35,7 +34,7 @@ val create :
 
 (** Update a document, returns the list of not valid requests *)
 val change :
-     ofn:(Yojson.Safe.t -> unit)
+     io:Fleche.Io.CallBack.t
   -> uri:Lang.LUri.File.t
   -> version:int
   -> raw:string
diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml
index ab2541ba..400e6276 100644
--- a/controller/lsp_core.ml
+++ b/controller/lsp_core.ml
@@ -218,16 +218,16 @@ end
 (***********************************************************************)
 (* Start of protocol handlers: document notifications                  *)
 
-let do_open ~ofn ~(state : State.t) params =
+let do_open ~io ~(state : State.t) params =
   let document =
     field "textDocument" params
     |> Lsp.Doc.TextDocumentItem.of_yojson |> Result.get_ok
   in
   let Lsp.Doc.TextDocumentItem.{ uri; version; text; _ } = document in
   let root_state, workspace = State.workspace_of_uri ~uri ~state in
-  Doc_manager.create ~ofn ~root_state ~workspace ~uri ~raw:text ~version
+  Doc_manager.create ~io ~root_state ~workspace ~uri ~raw:text ~version
 
-let do_change ~ofn params =
+let do_change ~ofn ~io params =
   let uri, version = Helpers.get_uri_version params in
   let changes = List.map U.to_assoc @@ list_field "contentChanges" params in
   match changes with
@@ -240,7 +240,7 @@ let do_change ~ofn params =
     ()
   | change :: _ ->
     let raw = string_field "text" change in
-    let invalid_rq = Doc_manager.change ~ofn ~uri ~version ~raw in
+    let invalid_rq = Doc_manager.change ~io ~uri ~version ~raw in
     let code = -32802 in
     let message = "Request got old in server" in
     Int.Set.iter (Rq.cancel ~ofn ~code ~message) invalid_rq
@@ -369,15 +369,15 @@ let lsp_init_process ~ofn ~cmdline ~debug msg : Init_effect.t =
     Loop
 
 (** Dispatching *)
-let dispatch_notification ~ofn ~state ~method_ ~params : unit =
+let dispatch_notification ~io ~ofn ~state ~method_ ~params : unit =
   match method_ with
   (* Lifecycle *)
   | "exit" -> raise Lsp_exit
   (* setTrace *)
   | "$/setTrace" -> do_trace params
   (* Document lifetime *)
-  | "textDocument/didOpen" -> do_open ~ofn ~state params
-  | "textDocument/didChange" -> do_change ~ofn params
+  | "textDocument/didOpen" -> do_open ~io ~state params
+  | "textDocument/didChange" -> do_change ~io ~ofn params
   | "textDocument/didClose" -> do_close ~ofn params
   | "textDocument/didSave" -> Cache.save_to_disk ()
   (* Cancel Request *)
@@ -387,13 +387,13 @@ let dispatch_notification ~ofn ~state ~method_ ~params : unit =
   (* Generic handler *)
   | msg -> LIO.trace "no_handler" msg
 
-let dispatch_state_notification ~ofn ~state ~method_ ~params : State.t =
+let dispatch_state_notification ~io ~ofn ~state ~method_ ~params : State.t =
   match method_ with
   (* Workspace *)
   | "workspace/didChangeWorkspaceFolders" ->
     do_changeWorkspaceFolders ~ofn ~state params
   | _ ->
-    dispatch_notification ~ofn ~state ~method_ ~params;
+    dispatch_notification ~io ~ofn ~state ~method_ ~params;
     state
 
 let dispatch_request ~method_ ~params : Rq.Action.t =
@@ -424,10 +424,10 @@ let dispatch_request ~method_ ~params : Rq.Action.t =
 let dispatch_request ~ofn ~id ~method_ ~params =
   dispatch_request ~method_ ~params |> Rq.serve ~ofn ~id
 
-let dispatch_message ~ofn ~state (com : LSP.Message.t) : State.t =
+let dispatch_message ~io ~ofn ~state (com : LSP.Message.t) : State.t =
   match com with
   | Notification { method_; params } ->
-    dispatch_state_notification ~ofn ~state ~method_ ~params
+    dispatch_state_notification ~io ~ofn ~state ~method_ ~params
   | Request { id; method_; params } ->
     dispatch_request ~ofn ~id ~method_ ~params;
     state
@@ -445,8 +445,8 @@ type 'a cont =
   | Cont of 'a
   | Yield of 'a
 
-let check_or_yield ~ofn ~state =
-  match Doc_manager.Check.maybe_check ~ofn with
+let check_or_yield ~io ~ofn ~state =
+  match Doc_manager.Check.maybe_check ~io with
   | None -> Yield state
   | Some (ready, doc) ->
     let () = Rq.serve_postponed ~ofn ~doc ready in
@@ -454,13 +454,13 @@ let check_or_yield ~ofn ~state =
 
 let request_queue = Queue.create ()
 
-let dispatch_or_resume_check ~ofn ~state =
+let dispatch_or_resume_check ~io ~ofn ~state =
   match Queue.peek_opt request_queue with
   | None ->
     (* This is where we make progress on document checking; kind of IDLE
        workqueue. *)
     Control.interrupt := false;
-    check_or_yield ~ofn ~state
+    check_or_yield ~io ~ofn ~state
   | Some com ->
     (* TODO: optimize the queue? EJGA: I've found that VS Code as a client keeps
        the queue tidy by itself, so this works fine as now *)
@@ -468,11 +468,11 @@ let dispatch_or_resume_check ~ofn ~state =
     LIO.trace "process_queue" ("Serving Request: " ^ LSP.Message.method_ com);
     (* We let Coq work normally now *)
     Control.interrupt := false;
-    Cont (dispatch_message ~ofn ~state com)
+    Cont (dispatch_message ~io ~ofn ~state com)
 
 (* Wrapper for the top-level call *)
-let dispatch_or_resume_check ~ofn ~state =
-  try Some (dispatch_or_resume_check ~ofn ~state) with
+let dispatch_or_resume_check ~io ~ofn ~state =
+  try Some (dispatch_or_resume_check ~io ~ofn ~state) with
   | U.Type_error (msg, obj) ->
     LIO.trace_object msg obj;
     Some (Yield state)
diff --git a/controller/lsp_core.mli b/controller/lsp_core.mli
index 3afdb4c3..c42f7d88 100644
--- a/controller/lsp_core.mli
+++ b/controller/lsp_core.mli
@@ -52,7 +52,10 @@ type 'a cont =
 (** Core scheduler: dispatch an LSP request or notification, check document and
     wake up pending requests *)
 val dispatch_or_resume_check :
-  ofn:(Yojson.Safe.t -> unit) -> state:State.t -> State.t cont option
+     io:Fleche.Io.CallBack.t
+  -> ofn:(Yojson.Safe.t -> unit)
+  -> state:State.t
+  -> State.t cont option
 
 (** Add a message to the queue *)
 val enqueue_message : Lsp.Base.Message.t -> unit
diff --git a/controller/perf.ml b/controller/perf.ml
deleted file mode 100644
index 91173990..00000000
--- a/controller/perf.ml
+++ /dev/null
@@ -1,44 +0,0 @@
-(************************************************************************)
-(* Coq Language Server Protocol -- Requests                             *)
-(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
-(* Copyright 2019-2023 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
-(* Written by: Emilio J. Gallego Arias                                  *)
-(************************************************************************)
-
-let rec list_take n = function
-  | [] -> []
-  | x :: xs -> if n = 0 then [] else x :: list_take (n - 1) xs
-
-let mk_loc_time (n : Fleche.Doc.Node.t) =
-  let time = Option.default 0.0 n.info.time in
-  let mem = n.info.mw_after -. n.info.mw_prev in
-  let loc = n.Fleche.Doc.Node.range in
-  Lsp.JFleche.SentencePerfData.{ loc; time; mem }
-
-let get_stats ~(doc : Fleche.Doc.t) =
-  match List.rev doc.nodes with
-  | [] -> "no stats"
-  | n :: _ -> Fleche.Stats.to_string n.info.stats
-
-(** Turn into a config option at some point? This is very expensive *)
-let display_cache_size = false
-
-let make (doc : Fleche.Doc.t) =
-  let n_stm = List.length doc.nodes in
-  let stats = get_stats ~doc in
-  let cache_size =
-    if display_cache_size then Fleche.Memo.Interp.size () |> float_of_int
-    else 0.0
-  in
-  let summary =
-    Format.asprintf "{ num sentences: %d@\n; stats: %s; cache: %a@\n}" n_stm
-      stats Fleche.Stats.pp_words cache_size
-  in
-  let top =
-    List.stable_sort
-      (fun (n1 : Fleche.Doc.Node.t) n2 -> compare n2.info.time n1.info.time)
-      doc.nodes
-  in
-  let top = list_take 10 top in
-  let timings = List.map mk_loc_time top in
-  Lsp.JFleche.DocumentPerfData.({ summary; timings } |> to_yojson)
diff --git a/editor/code/lib/types.ts b/editor/code/lib/types.ts
index 8a466324..11828445 100644
--- a/editor/code/lib/types.ts
+++ b/editor/code/lib/types.ts
@@ -117,6 +117,7 @@ export interface SentencePerfParams {
 }
 
 export interface DocumentPerfParams {
+  textDocument: VersionedTextDocumentIdentifier;
   summary: string;
   timings: SentencePerfParams[];
 }
diff --git a/fleche/doc.ml b/fleche/doc.ml
index 63c2da6a..c03d45d9 100644
--- a/fleche/doc.ml
+++ b/fleche/doc.ml
@@ -377,13 +377,13 @@ let add_node ~node doc =
 
 let concat_diags doc = List.concat_map (fun node -> node.Node.diags) doc.nodes
 
-let send_eager_diagnostics ~ofn ~uri ~version ~doc =
+let send_eager_diagnostics ~io ~uri ~version ~doc =
   (* this is too noisy *)
   (* let proc_diag = mk_diag loc 3 (Pp.str "Processing") in *)
   (* Io.Report.diagnostics ~uri ~version (proc_diag :: doc.diags)); *)
   if doc.diags_dirty && !Config.v.eager_diagnostics then (
     let diags = concat_diags doc in
-    Io.Report.diagnostics ~ofn ~uri ~version diags;
+    Io.Report.diagnostics ~io ~uri ~version diags;
     { doc with diags_dirty = false })
   else doc
 
@@ -401,9 +401,9 @@ let compute_progress end_ (last_done : Lang.Range.t) =
   let range = Lang.Range.{ start; end_ } in
   { Progress.Info.range; kind = 1 }
 
-let report_progress ~doc (last_tok : Lang.Range.t) =
+let report_progress ~io ~doc (last_tok : Lang.Range.t) =
   let progress = compute_progress doc.contents.last last_tok in
-  Io.Report.fileProgress ~uri:doc.uri ~version:doc.version [ progress ]
+  Io.Report.fileProgress ~io ~uri:doc.uri ~version:doc.version [ progress ]
 
 (* XXX: Save on close? *)
 (* let close_doc _modname = () *)
@@ -655,11 +655,11 @@ let max_errors_node ~state ~range =
     ~parsing_time:0.0
 
 (* main interpretation loop *)
-let process_and_parse ~ofn ~target ~uri ~version doc last_tok doc_handle =
+let process_and_parse ~io ~target ~uri ~version doc last_tok doc_handle =
   let rec stm doc st (last_tok : Lang.Range.t) acc_errors =
     (* Reporting of progress and diagnostics (if dirty) *)
-    let doc = send_eager_diagnostics ~ofn ~uri ~version ~doc in
-    report_progress ~ofn ~doc last_tok;
+    let doc = send_eager_diagnostics ~io ~uri ~version ~doc in
+    report_progress ~io ~doc last_tok;
     if Debug.parsing then Io.Log.trace "coq" "parsing sentence";
     if acc_errors > !Config.v.max_errors then
       let completed = Completion.Failed last_tok in
@@ -753,7 +753,7 @@ let loc_after ~lines ~uri (r : Lang.Range.t) =
   }
 
 (** Setup parser and call the main routine *)
-let resume_check ~ofn ~(last_tok : Lang.Range.t) ~doc ~target =
+let resume_check ~io ~(last_tok : Lang.Range.t) ~doc ~target =
   let uri, version, contents = (doc.uri, doc.version, doc.contents) in
   (* Compute resume point, basically [CLexer.after] + stream setup *)
   let lines = doc.contents.lines in
@@ -770,10 +770,10 @@ let resume_check ~ofn ~(last_tok : Lang.Range.t) ~doc ~target =
       Coq.Parsing.Parsable.make ~loc:resume_loc
         Gramlib.Stream.(of_string ~offset processed_content)
     in
-    process_and_parse ~ofn ~target ~uri ~version doc last_tok handle
+    process_and_parse ~io ~target ~uri ~version doc last_tok handle
 
 (** Check a document, if it was not completed already *)
-let check ~ofn ~target ~doc () =
+let check ~io ~target ~doc () =
   match doc.completed with
   | Yes _ ->
     Io.Log.trace "check" "resuming, completed=yes, nothing to do";
@@ -783,7 +783,7 @@ let check ~ofn ~target ~doc () =
     doc
   | Stopped last_tok ->
     DDebug.resume last_tok doc.version;
-    let doc = resume_check ~ofn ~last_tok ~doc ~target in
+    let doc = resume_check ~io ~last_tok ~doc ~target in
     log_doc_completion doc.completed;
     Util.print_stats ();
     doc
diff --git a/fleche/doc.mli b/fleche/doc.mli
index d9b131ca..5c22f15a 100644
--- a/fleche/doc.mli
+++ b/fleche/doc.mli
@@ -97,10 +97,10 @@ module Target : sig
   val reached : range:Lang.Range.t -> int * int -> bool
 end
 
-(** [check ~ofn ~target ~doc ()], check document [doc], [target] will have
-    Flèche stop after the point specified there has been reached. Output
-    function [ofn] is used to send partial results. *)
-val check : ofn:(Yojson.Safe.t -> unit) -> target:Target.t -> doc:t -> unit -> t
+(** [check ~io ~target ~doc ()], check document [doc], [target] will have Flèche
+    stop after the point specified there has been reached. Output functions are
+    in the [io] record, used to send partial updates. *)
+val check : io:Io.CallBack.t -> target:Target.t -> doc:t -> unit -> t
 
 (** [save ~doc] will save [doc] .vo file. It will fail if proofs are open, or if
     the document completion status is not [Yes] *)
diff --git a/fleche/io.ml b/fleche/io.ml
index e890e9bc..0c7214e9 100644
--- a/fleche/io.ml
+++ b/fleche/io.ml
@@ -2,23 +2,15 @@ module CallBack = struct
   type t =
     { trace : string -> ?extra:string -> string -> unit
     ; send_diagnostics :
-           ofn:(Yojson.Safe.t -> unit)
-        -> uri:Lang.LUri.File.t
-        -> version:int
-        -> Lang.Diagnostic.t list
-        -> unit
+        uri:Lang.LUri.File.t -> version:int -> Lang.Diagnostic.t list -> unit
     ; send_fileProgress :
-           ofn:(Yojson.Safe.t -> unit)
-        -> uri:Lang.LUri.File.t
-        -> version:int
-        -> Progress.Info.t list
-        -> unit
+        uri:Lang.LUri.File.t -> version:int -> Progress.Info.t list -> unit
     }
 
   let default =
     { trace = (fun _ ?extra:_ _ -> ())
-    ; send_diagnostics = (fun ~ofn:_ ~uri:_ ~version:_ _ -> ())
-    ; send_fileProgress = (fun ~ofn:_ ~uri:_ ~version:_ _ -> ())
+    ; send_diagnostics = (fun ~uri:_ ~version:_ _ -> ())
+    ; send_fileProgress = (fun ~uri:_ ~version:_ _ -> ())
     }
 
   let cb = ref default
@@ -37,9 +29,11 @@ module Log = struct
 end
 
 module Report = struct
-  let diagnostics ~ofn ~uri ~version d =
-    !CallBack.cb.send_diagnostics ~ofn ~uri ~version d
+  let diagnostics ~io ~uri ~version d =
+    io.CallBack.send_diagnostics ~uri ~version d
 
-  let fileProgress ~ofn ~uri ~version d =
-    !CallBack.cb.send_fileProgress ~ofn ~uri ~version d
+  let fileProgress ~io ~uri ~version d =
+    io.CallBack.send_fileProgress ~uri ~version d
+
+  let perfData ~io:_ ~uri:_ ~version:_ _ = ()
 end
diff --git a/fleche/io.mli b/fleche/io.mli
index 4d85b247..ec9d0a13 100644
--- a/fleche/io.mli
+++ b/fleche/io.mli
@@ -4,17 +4,9 @@ module CallBack : sig
           (** Send a log message, [extra] may contain information to be shown in
               verbose mode *)
     ; send_diagnostics :
-           ofn:(Yojson.Safe.t -> unit)
-        -> uri:Lang.LUri.File.t
-        -> version:int
-        -> Lang.Diagnostic.t list
-        -> unit
+        uri:Lang.LUri.File.t -> version:int -> Lang.Diagnostic.t list -> unit
     ; send_fileProgress :
-           ofn:(Yojson.Safe.t -> unit)
-        -> uri:Lang.LUri.File.t
-        -> version:int
-        -> Progress.Info.t list
-        -> unit
+        uri:Lang.LUri.File.t -> version:int -> Progress.Info.t list -> unit
     }
 
   val set : t -> unit
@@ -29,16 +21,19 @@ end
 
 module Report : sig
   val diagnostics :
-       ofn:(Yojson.Safe.t -> unit)
+       io:CallBack.t
     -> uri:Lang.LUri.File.t
     -> version:int
     -> Lang.Diagnostic.t list
     -> unit
 
   val fileProgress :
-       ofn:(Yojson.Safe.t -> unit)
+       io:CallBack.t
     -> uri:Lang.LUri.File.t
     -> version:int
     -> Progress.Info.t list
     -> unit
+
+  val perfData :
+    io:CallBack.t -> uri:Lang.LUri.File.t -> version:int -> Perf.t -> unit
 end
diff --git a/fleche/perf.ml b/fleche/perf.ml
new file mode 100644
index 00000000..346829ac
--- /dev/null
+++ b/fleche/perf.ml
@@ -0,0 +1,19 @@
+(************************************************************************)
+(* Coq Language Server Protocol -- Requests                             *)
+(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
+(* Copyright 2019-2023 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias                                  *)
+(************************************************************************)
+
+module Sentence = struct
+  type t =
+    { loc : Lang.Range.t
+    ; time : float
+    ; mem : float
+    }
+end
+
+type t =
+  { summary : string
+  ; timings : Sentence.t list
+  }
diff --git a/controller/perf.mli b/fleche/perf.mli
similarity index 72%
rename from controller/perf.mli
rename to fleche/perf.mli
index 64a4d723..5e8bb57a 100644
--- a/controller/perf.mli
+++ b/fleche/perf.mli
@@ -5,4 +5,15 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
-val make : Fleche.Doc.t -> Yojson.Safe.t
+module Sentence : sig
+  type t =
+    { loc : Lang.Range.t
+    ; time : float
+    ; mem : float
+    }
+end
+
+type t =
+  { summary : string
+  ; timings : Sentence.t list
+  }
diff --git a/fleche/perf_analysis.ml b/fleche/perf_analysis.ml
new file mode 100644
index 00000000..26946f8a
--- /dev/null
+++ b/fleche/perf_analysis.ml
@@ -0,0 +1,38 @@
+open Perf
+
+let rec list_take n = function
+  | [] -> []
+  | x :: xs -> if n = 0 then [] else x :: list_take (n - 1) xs
+
+let mk_loc_time (n : Doc.Node.t) =
+  let time = Option.default 0.0 n.info.time in
+  let mem = n.info.mw_after -. n.info.mw_prev in
+  let loc = n.Doc.Node.range in
+  Sentence.{ loc; time; mem }
+
+let get_stats ~(doc : Doc.t) =
+  match List.rev doc.nodes with
+  | [] -> "no stats"
+  | n :: _ -> Stats.to_string n.info.stats
+
+(** Turn into a config option at some point? This is very expensive *)
+let display_cache_size = false
+
+let make (doc : Doc.t) =
+  let n_stm = List.length doc.nodes in
+  let stats = get_stats ~doc in
+  let cache_size =
+    if display_cache_size then Memo.Interp.size () |> float_of_int else 0.0
+  in
+  let summary =
+    Format.asprintf "{ num sentences: %d@\n; stats: %s; cache: %a@\n}" n_stm
+      stats Stats.pp_words cache_size
+  in
+  let top =
+    List.stable_sort
+      (fun (n1 : Doc.Node.t) n2 -> compare n2.info.time n1.info.time)
+      doc.nodes
+  in
+  let top = list_take 10 top in
+  let timings = List.map mk_loc_time top in
+  { summary; timings }
diff --git a/fleche/perf_analysis.mli b/fleche/perf_analysis.mli
new file mode 100644
index 00000000..1936d7fe
--- /dev/null
+++ b/fleche/perf_analysis.mli
@@ -0,0 +1 @@
+val make : Doc.t -> Perf.t
diff --git a/fleche/progress.ml b/fleche/progress.ml
index a01211b7..986b6835 100644
--- a/fleche/progress.ml
+++ b/fleche/progress.ml
@@ -20,5 +20,4 @@ module Info = struct
     { range : Lang.Range.t
     ; kind : int
     }
-  [@@deriving yojson]
 end
diff --git a/lsp/jFleche.ml b/lsp/jFleche.ml
index e62c1052..e5e43ae3 100644
--- a/lsp/jFleche.ml
+++ b/lsp/jFleche.ml
@@ -46,7 +46,7 @@ module Config = struct
   type t = [%import: Fleche.Config.t] [@@deriving yojson]
 end
 
-module Progress = struct
+module FileProgress = struct
   module Info = struct
     type t = [%import: Fleche.Progress.Info.t] [@@deriving yojson]
   end
@@ -60,7 +60,9 @@ end
 
 let mk_progress ~uri ~version processing =
   let textDocument = { Doc.VersionedTextDocumentIdentifier.uri; version } in
-  let params = Progress.to_yojson { Progress.textDocument; processing } in
+  let params =
+    FileProgress.to_yojson { FileProgress.textDocument; processing }
+  in
   Base.mk_notification ~method_:"$/coq/fileProgress" ~params
 
 module Message = struct
@@ -115,17 +117,13 @@ module FlecheDocument = struct
 end
 
 module SentencePerfData = struct
-  type t =
-    { loc : JLang.Range.t
-    ; time : float
-    ; mem : float
-    }
-  [@@deriving yojson]
+  type t = [%import: Fleche.Perf.Sentence.t] [@@deriving yojson]
 end
 
 module DocumentPerfData = struct
   type t =
-    { summary : string
+    { textDocument : Doc.VersionedTextDocumentIdentifier.t
+    ; summary : string
     ; timings : SentencePerfData.t list
     }
   [@@deriving yojson]
diff --git a/lsp/jFleche.mli b/lsp/jFleche.mli
index 719f7902..4767bcc8 100644
--- a/lsp/jFleche.mli
+++ b/lsp/jFleche.mli
@@ -30,6 +30,14 @@ val mk_progress :
   -> Fleche.Progress.Info.t list
   -> Yojson.Safe.t
 
+module FileProgress : sig
+  type t =
+    { textDocument : Doc.VersionedTextDocumentIdentifier.t
+    ; processing : Fleche.Progress.Info.t list
+    }
+  [@@deriving yojson]
+end
+
 (** Goals *)
 module Message : sig
   type 'a t =
@@ -78,17 +86,13 @@ module FlecheDocument : sig
 end
 
 module SentencePerfData : sig
-  type t =
-    { loc : JLang.Range.t
-    ; time : float
-    ; mem : float
-    }
-  [@@deriving yojson]
+  type t = Fleche.Perf.Sentence.t [@@deriving yojson]
 end
 
 module DocumentPerfData : sig
   type t =
-    { summary : string
+    { textDocument : Doc.VersionedTextDocumentIdentifier.t
+    ; summary : string
     ; timings : SentencePerfData.t list
     }
   [@@deriving yojson]

From a4a2d6f851a7adf4ebd0177c7d0dd82ff338201b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 26 Jun 2023 15:22:12 +0200
Subject: [PATCH 2/2] [fleche] Move `Doc_manager` to `Fleche.Theory`

In the same way that `Fleche.Doc` takes care of checking inside
individual units, `Fleche.Theory  takes care of checking full
theories, and coordinating document checking.
---
 controller/coq_lsp.ml                         |  2 +
 controller/lsp_core.ml                        | 14 ++--
 controller/request.ml                         |  4 +-
 controller/request.mli                        |  2 +-
 fleche/io.ml                                  |  4 +
 fleche/io.mli                                 |  8 +-
 controller/doc_manager.ml => fleche/theory.ml | 80 +++++++++----------
 .../doc_manager.mli => fleche/theory.mli      | 12 +--
 8 files changed, 66 insertions(+), 60 deletions(-)
 rename controller/doc_manager.ml => fleche/theory.ml (84%)
 rename controller/doc_manager.mli => fleche/theory.mli (89%)

diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml
index 8bb0050d..2c264690 100644
--- a/controller/coq_lsp.ml
+++ b/controller/coq_lsp.ml
@@ -51,6 +51,7 @@ let rec process_queue ~delay ~io ~ofn ~state : unit =
 let concise_cb ofn =
   Fleche.Io.CallBack.
     { trace = (fun _hdr ?extra:_ _msg -> ())
+    ; message = (fun ~lvl:_ ~message:_ -> ())
     ; send_diagnostics =
         (fun ~uri ~version diags ->
           if List.length diags > 0 then
@@ -62,6 +63,7 @@ let concise_cb ofn =
 let lsp_cb ofn =
   Fleche.Io.CallBack.
     { trace = LIO.trace
+    ; message = LIO.logMessage
     ; send_diagnostics =
         (fun ~uri ~version diags ->
           Lsp.JLang.mk_diagnostics ~uri ~version diags |> ofn)
diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml
index 400e6276..2f95cf9d 100644
--- a/controller/lsp_core.ml
+++ b/controller/lsp_core.ml
@@ -168,7 +168,7 @@ end = struct
     let f pr =
       let () =
         let request = Request.Data.dm_request pr in
-        Doc_manager.Request.remove { id; request }
+        Fleche.Theory.Request.remove { id; request }
       in
       Error (code, message)
     in
@@ -188,7 +188,7 @@ end = struct
 
   let query ~ofn ~id (pr : Request.Data.t) =
     let request = Request.Data.dm_request pr in
-    match Doc_manager.Request.add { id; request } with
+    match Fleche.Theory.Request.add { id; request } with
     | Cancel ->
       let code = -32802 in
       let message = "Document is not ready" in
@@ -225,7 +225,7 @@ let do_open ~io ~(state : State.t) params =
   in
   let Lsp.Doc.TextDocumentItem.{ uri; version; text; _ } = document in
   let root_state, workspace = State.workspace_of_uri ~uri ~state in
-  Doc_manager.create ~io ~root_state ~workspace ~uri ~raw:text ~version
+  Fleche.Theory.create ~io ~root_state ~workspace ~uri ~raw:text ~version
 
 let do_change ~ofn ~io params =
   let uri, version = Helpers.get_uri_version params in
@@ -240,14 +240,14 @@ let do_change ~ofn ~io params =
     ()
   | change :: _ ->
     let raw = string_field "text" change in
-    let invalid_rq = Doc_manager.change ~io ~uri ~version ~raw in
+    let invalid_rq = Fleche.Theory.change ~io ~uri ~version ~raw in
     let code = -32802 in
     let message = "Request got old in server" in
     Int.Set.iter (Rq.cancel ~ofn ~code ~message) invalid_rq
 
 let do_close ~ofn:_ params =
   let uri = Helpers.get_uri params in
-  Doc_manager.close ~uri
+  Fleche.Theory.close ~uri
 
 let do_trace params =
   let trace = string_field "value" params in
@@ -435,7 +435,7 @@ let dispatch_message ~io ~ofn ~state (com : LSP.Message.t) : State.t =
 (* Queue handling *)
 
 (***********************************************************************)
-(* The queue strategy is: we keep pending document checks in Doc_manager, they
+(* The queue strategy is: we keep pending document checks in Fleche.Theory, they
    are only resumed when the rest of requests in the queue are served.
 
    Note that we should add a method to detect stale requests; maybe cancel them
@@ -446,7 +446,7 @@ type 'a cont =
   | Yield of 'a
 
 let check_or_yield ~io ~ofn ~state =
-  match Doc_manager.Check.maybe_check ~io with
+  match Fleche.Theory.Check.maybe_check ~io with
   | None -> Yield state
   | Some (ready, doc) ->
     let () = Rq.serve_postponed ~ofn ~doc ready in
diff --git a/controller/request.ml b/controller/request.ml
index 9f42e516..70c324ab 100644
--- a/controller/request.ml
+++ b/controller/request.ml
@@ -48,9 +48,9 @@ module Data = struct
 
   let dm_request pr =
     match pr with
-    | DocRequest { uri; handler = _ } -> Doc_manager.Request.(FullDoc { uri })
+    | DocRequest { uri; handler = _ } -> Fleche.Theory.Request.(FullDoc { uri })
     | PosRequest { uri; point; version; postpone; handler = _ } ->
-      Doc_manager.Request.(PosInDoc { uri; point; version; postpone })
+      Fleche.Theory.Request.(PosInDoc { uri; point; version; postpone })
 
   let serve ~doc pr =
     match pr with
diff --git a/controller/request.mli b/controller/request.mli
index 0608d6a1..d97c5a89 100644
--- a/controller/request.mli
+++ b/controller/request.mli
@@ -39,6 +39,6 @@ module Data : sig
 
   (* Debug printing *)
   val data : Format.formatter -> t -> unit
-  val dm_request : t -> Doc_manager.Request.request
+  val dm_request : t -> Fleche.Theory.Request.request
   val serve : doc:Fleche.Doc.t -> t -> R.t
 end
diff --git a/fleche/io.ml b/fleche/io.ml
index 0c7214e9..024a60e6 100644
--- a/fleche/io.ml
+++ b/fleche/io.ml
@@ -1,6 +1,7 @@
 module CallBack = struct
   type t =
     { trace : string -> ?extra:string -> string -> unit
+    ; message : lvl:int -> message:string -> unit
     ; send_diagnostics :
         uri:Lang.LUri.File.t -> version:int -> Lang.Diagnostic.t list -> unit
     ; send_fileProgress :
@@ -9,6 +10,7 @@ module CallBack = struct
 
   let default =
     { trace = (fun _ ?extra:_ _ -> ())
+    ; message = (fun ~lvl:_ ~message:_ -> ())
     ; send_diagnostics = (fun ~uri:_ ~version:_ _ -> ())
     ; send_fileProgress = (fun ~uri:_ ~version:_ _ -> ())
     }
@@ -29,6 +31,8 @@ module Log = struct
 end
 
 module Report = struct
+  let message ~io ~lvl ~message = io.CallBack.message ~lvl ~message
+
   let diagnostics ~io ~uri ~version d =
     io.CallBack.send_diagnostics ~uri ~version d
 
diff --git a/fleche/io.mli b/fleche/io.mli
index ec9d0a13..3a0ba565 100644
--- a/fleche/io.mli
+++ b/fleche/io.mli
@@ -3,6 +3,8 @@ module CallBack : sig
     { trace : string -> ?extra:string -> string -> unit
           (** Send a log message, [extra] may contain information to be shown in
               verbose mode *)
+    ; message : lvl:int -> message:string -> unit
+          (** Send a user-visible message *)
     ; send_diagnostics :
         uri:Lang.LUri.File.t -> version:int -> Lang.Diagnostic.t list -> unit
     ; send_fileProgress :
@@ -13,13 +15,17 @@ module CallBack : sig
 end
 
 module Log : sig
+  (** Debug trace *)
   val trace : string -> ?extra:string -> string -> unit
 
-  (** For unexpected feedback *)
+  (** For unexpected feedback, remove eventually or just assert false? *)
   val feedback : Loc.t Coq.Message.t list -> unit
 end
 
 module Report : sig
+  (** User-visible message *)
+  val message : io:CallBack.t -> lvl:int -> message:string -> unit
+
   val diagnostics :
        io:CallBack.t
     -> uri:Lang.LUri.File.t
diff --git a/controller/doc_manager.ml b/fleche/theory.ml
similarity index 84%
rename from controller/doc_manager.ml
rename to fleche/theory.ml
index 39529a5c..7e2c0f81 100644
--- a/controller/doc_manager.ml
+++ b/fleche/theory.ml
@@ -15,12 +15,10 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
-module LIO = Lsp.Io
-
 (* Handler for document *)
 module Handle = struct
   type t =
-    { doc : Fleche.Doc.t
+    { doc : Doc.t
     ; cp_requests : Int.Set.t
           (* For now we just store the request id to wake up on completion,
              later on we may want to store a more interesting type, for example
@@ -42,7 +40,7 @@ module Handle = struct
     (match Hashtbl.find_opt doc_table uri with
     | None -> ()
     | Some _ ->
-      LIO.trace "do_open"
+      Io.Log.trace "do_open"
         ("file "
         ^ Lang.LUri.File.to_string_uri uri
         ^ " not properly closed by client"));
@@ -52,7 +50,7 @@ module Handle = struct
   let close ~uri = Hashtbl.remove doc_table uri
   let find_opt ~uri = Hashtbl.find_opt doc_table uri
 
-  let _update_doc ~handle ~(doc : Fleche.Doc.t) =
+  let _update_doc ~handle ~(doc : Doc.t) =
     Hashtbl.replace doc_table doc.uri { handle with doc }
 
   let pt_ids l = List.map (fun (id, _) -> id) l |> Int.Set.of_list
@@ -68,7 +66,7 @@ module Handle = struct
       invalid_reqs
 
   (* Clear requests and update doc *)
-  let update_doc_version ~(doc : Fleche.Doc.t) =
+  let update_doc_version ~(doc : Doc.t) =
     let invalid_reqs = clear_requests ~uri:doc.uri in
     Hashtbl.replace doc_table doc.uri
       { doc; cp_requests = Int.Set.empty; pt_requests = [] };
@@ -121,7 +119,7 @@ module Handle = struct
     | Stopped range ->
       let fullfilled, delayed =
         List.partition
-          (fun (_id, point) -> Fleche.Doc.Target.reached ~range point)
+          (fun (_id, point) -> Doc.Target.reached ~range point)
           handle.pt_requests
       in
       let handle = { handle with pt_requests = delayed } in
@@ -129,29 +127,28 @@ module Handle = struct
     | Failed _ | FailedPermanent _ -> (handle, Int.Set.empty)
 
   (* trigger pending incremental requests *)
-  let update_doc_info ~handle ~(doc : Fleche.Doc.t) =
+  let update_doc_info ~handle ~(doc : Doc.t) =
     let handle, requests = do_requests ~doc ~handle in
     Hashtbl.replace doc_table doc.uri handle;
     requests
 end
 
-let diags_of_doc doc =
-  List.concat_map Fleche.Doc.Node.diags doc.Fleche.Doc.nodes
+let diags_of_doc doc = List.concat_map Doc.Node.diags doc.Doc.nodes
 
 let send_diags ~io ~doc =
   let diags = diags_of_doc doc in
-  if List.length diags > 0 || !Fleche.Config.v.verbosity > 1 then
+  if List.length diags > 0 || !Config.v.verbosity > 1 then
     let uri, version = (doc.uri, doc.version) in
-    Fleche.Io.Report.diagnostics ~io ~uri ~version diags
+    Io.Report.diagnostics ~io ~uri ~version diags
 
-let send_perf_data ~io ~(doc : Fleche.Doc.t) =
+let send_perf_data ~io ~(doc : Doc.t) =
   match doc.completed with
   | Yes _ ->
     let uri, version = (doc.uri, doc.version) in
-    Fleche.Io.Report.perfData ~io ~uri ~version (Fleche.Perf_analysis.make doc)
+    Io.Report.perfData ~io ~uri ~version (Perf_analysis.make doc)
   | _ -> ()
 
-let completed ~(doc : Fleche.Doc.t) =
+let completed ~(doc : Doc.t) =
   match doc.completed with
   | Yes _ | Failed _ | FailedPermanent _ -> true
   | Stopped _ -> false
@@ -159,32 +156,31 @@ let completed ~(doc : Fleche.Doc.t) =
 module Check : sig
   val schedule : uri:Lang.LUri.File.t -> unit
   val deschedule : uri:Lang.LUri.File.t -> unit
-  val maybe_check : io:Fleche.Io.CallBack.t -> (Int.Set.t * Fleche.Doc.t) option
+  val maybe_check : io:Io.CallBack.t -> (Int.Set.t * Doc.t) option
 end = struct
   let pending = ref None
 
   let get_check_target pt_requests =
-    let target_of_pt_handle (_, (l, c)) = Fleche.Doc.Target.Position (l, c) in
-    Option.cata target_of_pt_handle Fleche.Doc.Target.End
-      (List.nth_opt pt_requests 0)
+    let target_of_pt_handle (_, (l, c)) = Doc.Target.Position (l, c) in
+    Option.cata target_of_pt_handle Doc.Target.End (List.nth_opt pt_requests 0)
 
   (* Notification handling; reply is optional / asynchronous *)
   let check ~io ~uri =
-    LIO.trace "process_queue" "resuming document checking";
+    Io.Log.trace "process_queue" "resuming document checking";
     match Handle.find_opt ~uri with
     | Some handle ->
       let target = get_check_target handle.pt_requests in
-      let doc = Fleche.Doc.check ~io ~target ~doc:handle.doc () in
+      let doc = Doc.check ~io ~target ~doc:handle.doc () in
       let requests = Handle.update_doc_info ~handle ~doc in
       send_diags ~io ~doc;
-      if !Fleche.Config.v.verbosity > 1 then
+      if !Config.v.verbosity > 1 then
         if (* Only if completed! *)
            completed ~doc then send_perf_data ~io ~doc;
       (* Only if completed! *)
       if completed ~doc then pending := None;
       Some (requests, doc)
     | None ->
-      LIO.trace "Check.check"
+      Io.Log.trace "Check.check"
         ("file " ^ Lang.LUri.File.to_string_uri uri ^ " not available");
       None
 
@@ -202,10 +198,10 @@ let send_error_permanent_fail ~io ~uri ~version message =
   let end_ = Point.{ line = 0; character = 1; offset = 1 } in
   let range = Range.{ start; end_ } in
   let d = Lang.Diagnostic.{ range; severity = 1; message; extra = None } in
-  Fleche.Io.Report.diagnostics ~io ~uri ~version [ d ]
+  Io.Report.diagnostics ~io ~uri ~version [ d ]
 
 let create ~io ~root_state ~workspace ~uri ~raw ~version =
-  let r = Fleche.Doc.create ~state:root_state ~workspace ~uri ~raw ~version in
+  let r = Doc.create ~state:root_state ~workspace ~uri ~raw ~version in
   match r with
   | Completed (Result.Ok doc) ->
     Handle.create ~uri ~doc;
@@ -216,9 +212,9 @@ let create ~io ~root_state ~workspace ~uri ~raw ~version =
        ghost node for the implicit import, but we will phase that out in Coq
        upstream at some point. *)
     let message =
-      Format.asprintf "Fleche.Doc.create, internal error: @[%a@]" Pp.pp_with msg
+      Format.asprintf "Doc.create, internal error: @[%a@]" Pp.pp_with msg
     in
-    LIO.logMessage ~lvl:1 ~message;
+    Io.Report.message ~io ~lvl:1 ~message;
     send_error_permanent_fail ~io ~uri ~version (Pp.str message)
   | Interrupted -> ()
 
@@ -247,31 +243,29 @@ let create ~io ~root_state ~workspace ~uri ~raw ~version =
        Check coq-lsp webpage (Working with multiple files section) for\n\
        instructions on how to install a fixed branch for earlier Coq versions."
     in
-    LIO.logMessage ~lvl:1 ~message;
-    (match
-       Fleche.Doc.create_failed_permanent ~state:root_state ~uri ~raw ~version
-     with
-    | Fleche.Contents.R.Error _e -> ()
+    Io.Report.message ~io ~lvl:1 ~message;
+    (match Doc.create_failed_permanent ~state:root_state ~uri ~raw ~version with
+    | Contents.R.Error _e -> ()
     | Ok doc -> Handle.create ~uri ~doc);
     send_error_permanent_fail ~io ~uri ~version (Pp.str message))
   else (
     tainted := true;
     create ~io ~root_state ~workspace ~uri ~raw ~version)
 
-let change ~io ~(doc : Fleche.Doc.t) ~version ~raw =
+let change ~io ~(doc : Doc.t) ~version ~raw =
   let uri = doc.uri in
-  LIO.trace "bump file"
+  Io.Log.trace "bump file"
     (Lang.LUri.File.to_string_uri uri ^ " / version: " ^ string_of_int version);
   let tb = Unix.gettimeofday () in
-  match Fleche.Doc.bump_version ~version ~raw doc with
-  | Fleche.Contents.R.Error e ->
+  match Doc.bump_version ~version ~raw doc with
+  | Contents.R.Error e ->
     (* Send diagnostics for content conversion *)
     let message = Pp.(str "Error in document conversion: " ++ str e) in
     send_error_permanent_fail ~io ~uri ~version message;
     Handle.clear_requests ~uri
-  | Fleche.Contents.R.Ok doc ->
+  | Contents.R.Ok doc ->
     let diff = Unix.gettimeofday () -. tb in
-    LIO.trace "bump file took" (Format.asprintf "%f" diff);
+    Io.Log.trace "bump file took" (Format.asprintf "%f" diff);
     let invalid_reqs = Handle.update_doc_version ~doc in
     Check.schedule ~uri;
     invalid_reqs
@@ -279,7 +273,7 @@ let change ~io ~(doc : Fleche.Doc.t) ~version ~raw =
 let change ~io ~uri ~version ~raw =
   match Handle.find_opt ~uri with
   | None ->
-    LIO.trace "DocHandle.find"
+    Io.Log.trace "DocHandle.find"
       ("file " ^ Lang.LUri.File.to_string_uri uri ^ " not available");
     Int.Set.empty
   | Some { doc; _ } ->
@@ -311,25 +305,25 @@ module Request = struct
     }
 
   type action =
-    | Now of Fleche.Doc.t
+    | Now of Doc.t
     | Postpone
     | Cancel
 
   let with_doc ~f ~uri =
     match Handle.find_opt ~uri with
     | None ->
-      LIO.trace "Request.add"
+      Io.Log.trace "Request.add"
         ("document " ^ Lang.LUri.File.to_string_uri uri ^ " not available");
       (* XXX Should be cancelled *)
       Cancel
     | Some { doc; _ } -> f doc
 
-  let request_in_range ~(doc : Fleche.Doc.t) ~version (line, col) =
+  let request_in_range ~(doc : Doc.t) ~version (line, col) =
     let in_range =
       match doc.completed with
       | Yes _ -> true
       | Failed range | FailedPermanent range | Stopped range ->
-        Fleche.Doc.Target.reached ~range (line, col)
+        Doc.Target.reached ~range (line, col)
     in
     let in_range =
       match version with
diff --git a/controller/doc_manager.mli b/fleche/theory.mli
similarity index 89%
rename from controller/doc_manager.mli
rename to fleche/theory.mli
index d5a09958..42755496 100644
--- a/controller/doc_manager.mli
+++ b/fleche/theory.mli
@@ -19,12 +19,12 @@ module Check : sig
   (** Check pending documents, return [None] if there is none pending, or
       [Some rqs] the list of requests ready to execute after the check. Sends
       progress and diagnostics notifications using output function [ofn]. *)
-  val maybe_check : io:Fleche.Io.CallBack.t -> (Int.Set.t * Fleche.Doc.t) option
+  val maybe_check : io:Io.CallBack.t -> (Int.Set.t * Doc.t) option
 end
 
-(** Create a document *)
+(** Create a document inside a theory *)
 val create :
-     io:Fleche.Io.CallBack.t
+     io:Io.CallBack.t
   -> root_state:Coq.State.t
   -> workspace:Coq.Workspace.t
   -> uri:Lang.LUri.File.t
@@ -32,9 +32,9 @@ val create :
   -> version:int
   -> unit
 
-(** Update a document, returns the list of not valid requests *)
+(** Update a document inside a theory, returns the list of not valid requests *)
 val change :
-     io:Fleche.Io.CallBack.t
+     io:Io.CallBack.t
   -> uri:Lang.LUri.File.t
   -> version:int
   -> raw:string
@@ -59,7 +59,7 @@ module Request : sig
     }
 
   type action =
-    | Now of Fleche.Doc.t
+    | Now of Doc.t
     | Postpone
     | Cancel