[lsp] [controller] Add support for workspace folders

CHANGES.md

@@ -13,6 +13,9 @@
    (@ejgallego, #350)
  - Auto-ignore Coq object files; can be disabled in config
    (@ejgallego, #365)
+ - Support workspaces with multiple roots, this is very useful for
+   projects that contain several `_CoqProject` files in different
+   directories (@ejgallego, #374)
 
 # coq-lsp 0.1.5.1: Path
 -----------------------

controller/coq_lsp.ml

@@ -45,7 +45,8 @@ let dispatch_or_resume_check ~ofmt ~state =
     (* This is where we make progress on document checking; kind of IDLE
        workqueue. *)
     Control.interrupt := false;
-    check_or_yield ~ofmt
+    check_or_yield ~ofmt;
+    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 *)
@@ -58,7 +59,9 @@ let dispatch_or_resume_check ~ofmt ~state =
 (* Wrapper for the top-level call *)
 let dispatch_or_resume_check ~ofmt ~state =
   try dispatch_or_resume_check ~ofmt ~state with
-  | U.Type_error (msg, obj) -> LIO.trace_object msg obj
+  | U.Type_error (msg, obj) ->
+    LIO.trace_object msg obj;
+    state
   | Lsp_exit -> raise Lsp_exit
   | exn ->
     (* Note: We should never arrive here from Coq, as every call to Coq should
@@ -72,12 +75,13 @@ let dispatch_or_resume_check ~ofmt ~state =
     (* LIO.trace "process_queue" ("exn in method: " ^ method_name); *)
     LIO.trace "print_exn [OCaml]" (Printexc.to_string exn);
     LIO.trace "print_exn [Coq  ]" Pp.(string_of_ppcmds CErrors.(iprint iexn));
-    LIO.trace "print_bt  [OCaml]" bt
+    LIO.trace "print_bt  [OCaml]" bt;
+    state
 
 let rec process_queue ofmt ~state =
   if Fleche.Debug.sched_wakeup then
     LIO.trace "<- dequeue" (Format.asprintf "%.2f" (Unix.gettimeofday ()));
-  dispatch_or_resume_check ~ofmt ~state;
+  let state = dispatch_or_resume_check ~ofmt ~state in
   process_queue ofmt ~state
 
 let process_input (com : LSP.Message.t) =
@@ -155,10 +159,10 @@ let lsp_main bt coqlib vo_load_path ml_include_path =
   (* Input/output will happen now *)
   try
     (* LSP Server server initialization *)
-    let workspace = lsp_init_loop ic oc ~cmdline ~debug in
+    let workspaces = lsp_init_loop ic oc ~cmdline ~debug in
 
     (* Core LSP loop context *)
-    let state = { State.root_state; workspace } in
+    let state = { State.root_state; cmdline; workspaces } in
 
     (* Read workspace state (noop for now) *)
     Cache.read_from_disk ();
@@ -241,7 +245,7 @@ let lsp_cmd : unit Cmd.t =
   let doc = "Coq LSP Server" in
   let man =
     [ `S "DESCRIPTION"
-    ; `P "Experimental Coq LSP server"
+    ; `P "Coq LSP server"
     ; `S "USAGE"
     ; `P "See the documentation on the project's webpage for more information"
     ]

controller/lsp_core.ml

@@ -29,18 +29,62 @@ let list_field name dict = U.to_list List.(assoc name dict)
 let string_field name dict = U.to_string List.(assoc name dict)
 let oint_field name dict = Option.map U.to_int (List.assoc_opt name dict)
 
-(* LSP loop internal state, mainly the stuff needed to create a new document.
-   Note that we could [apply] [workspace] to the root_state, but for now we keep
-   the flexibility for a server to work with different workspaces. *)
+module LIO = Lsp.Io
+module LSP = Lsp.Base
+
+(** LSP loop internal state: mainly the data needed to create a new document. In
+    particular, we need:
+
+    - the core root state of Coq
+    - the list of workspaces configureda
+
+    Our notion of workspace corresponds to the usual notion in Coq of "theory",
+    (that is to say, a [_CoqProject] or [(coq.theory ...)] declaration), which
+    is to say a set of files that share a common logical path and logical
+    mappings to other theories.
+
+    [_CoqProject]-based workspaces need an explicit global flag setup, whereas
+    dune-based ones declare dependencies on other workspaces. *)
 module State = struct
   type t =
-    { root_state : Coq.State.t
-    ; workspace : Coq.Workspace.t
+    { cmdline : Coq.Workspace.CmdLine.t
+    ; root_state : Coq.State.t
+    ; workspaces : (string * Coq.Workspace.t) list
     }
+
+  open Lsp.Workspace
+
+  let add_workspace state { WorkspaceFolder.uri; _ } =
+    let dir = Lang.LUri.File.to_string_file uri in
+    let { cmdline; workspaces; _ } = state in
+    let ws = Coq.Workspace.guess ~debug:false ~cmdline ~dir in
+    { state with workspaces = (dir, ws) :: workspaces }
+
+  let del_workspace state { WorkspaceFolder.uri; _ } =
+    let dir = Lang.LUri.File.to_string_file uri in
+    { state with workspaces = List.remove_assoc dir state.workspaces }
+
+  let is_in_dir ~dir ~file = CString.is_prefix dir file
+
+  let workspace_of_uri ~uri ~state =
+    let { root_state; workspaces; _ } = state in
+    let file = Lang.LUri.File.to_string_file uri in
+    match List.find_opt (fun (dir, _) -> is_in_dir ~dir ~file) workspaces with
+    | None ->
+      LIO.logMessage ~lvl:1 ~message:"file not in workspace";
+      (root_state, snd (List.hd workspaces))
+    | Some (_, workspace) -> (root_state, workspace)
 end
 
-module LIO = Lsp.Io
-module LSP = Lsp.Base
+let do_changeWorkspaceFolders ~ofmt:_ ~state params =
+  let open Lsp.Workspace in
+  let { DidChangeWorkspaceFoldersParams.event } =
+    DidChangeWorkspaceFoldersParams.of_yojson (`Assoc params) |> Result.get_ok
+  in
+  let { WorkspaceFoldersChangeEvent.added; removed } = event in
+  let state = List.fold_left State.add_workspace state added in
+  let state = List.fold_left State.del_workspace state removed in
+  state
 
 module PendingRequest = struct
   type t =
@@ -151,24 +195,25 @@ let serve_postponed_requests ~ofmt rl = Int.Set.iter (Rq.serve ~ofmt) rl
 
 let do_shutdown ~params:_ = RAction.ok `Null
 
-let do_open ~state params =
+let do_open ~ofmt ~(state : State.t) params =
   let document = dict_field "textDocument" params in
   let uri, version, raw =
     ( string_field "uri" document
     , int_field "version" document
     , string_field "text" document )
   in
-  (* XXX: fix this *)
-  let uri = Lang.LUri.(File.of_uri (of_string uri)) |> Result.get_ok in
-  let root_state, workspace = State.(state.root_state, state.workspace) in
-  Doc_manager.create ~root_state ~workspace ~uri ~raw ~version
+  match Lang.LUri.(File.of_uri (of_string uri)) with
+  | Ok uri ->
+    let root_state, workspace = State.workspace_of_uri ~uri ~state in
+    Doc_manager.create ~ofmt ~root_state ~workspace ~uri ~raw ~version
+  | Error _msg -> LIO.logMessage ~lvl:1 ~message:"invalid URI in do_open"
 
 let do_change ~ofmt params =
   let document = dict_field "textDocument" params in
   let uri, version =
     (string_field "uri" document, int_field "version" document)
   in
-  (* XXX: fix this *)
+  (* XXX: fix this, factor with above *)
   let uri = Lang.LUri.(File.of_uri (of_string uri)) |> Result.get_ok in
   let changes = List.map U.to_assoc @@ list_field "contentChanges" params in
   match changes with
@@ -270,9 +315,9 @@ let do_cancel ~ofmt ~params =
 (** LSP Init routine *)
 exception Lsp_exit
 
-let log_workspace w =
+let log_workspace (dir, w) =
   let message, extra = Coq.Workspace.describe w in
-  LIO.trace "workspace" "initialized" ~extra;
+  LIO.trace "workspace" ("initialized " ^ dir) ~extra;
   LIO.logMessage ~lvl:3 ~message
 
 let version () =
@@ -284,22 +329,25 @@ let version () =
   Format.asprintf "version %s, dev: %s, Coq version: %s" Version.server
     dev_version Coq_config.version
 
-let rec lsp_init_loop ic ofmt ~cmdline ~debug : Coq.Workspace.t =
+let rec lsp_init_loop ic ofmt ~cmdline ~debug : (string * Coq.Workspace.t) list
+    =
   match LIO.read_request ic with
   | LSP.Message.Request { method_ = "initialize"; id; params } ->
     (* At this point logging is allowed per LSP spec *)
     let message =
       Format.asprintf "Initializing coq-lsp server %s" (version ())
     in
     LIO.logMessage ~lvl:3 ~message;
-    let result, dir = Rq_init.do_initialize ~params in
+    let result, dirs = Rq_init.do_initialize ~params in
     Rq.answer ~ofmt ~id (Result.ok result);
     LIO.logMessage ~lvl:3 ~message:"Server initialized";
     (* Workspace initialization *)
     let debug = debug || !Fleche.Config.v.debug in
-    let workspace = Coq.Workspace.guess ~cmdline ~debug ~dir in
-    log_workspace workspace;
-    workspace
+    let workspaces =
+      List.map (fun dir -> (dir, Coq.Workspace.guess ~cmdline ~debug ~dir)) dirs
+    in
+    List.iter log_workspace workspaces;
+    workspaces
   | LSP.Message.Request { id; _ } ->
     (* per spec *)
     LSP.mk_request_error ~id ~code:(-32002) ~message:"server not initialized"
@@ -329,6 +377,15 @@ let dispatch_notification ~ofmt ~state ~method_ ~params : unit =
   (* Generic handler *)
   | msg -> LIO.trace "no_handler" msg
 
+let dispatch_state_notification ~ofmt ~state ~method_ ~params : State.t =
+  match method_ with
+  (* Workspace *)
+  | "workspace/didChangeWorkspaceFolders" ->
+    do_changeWorkspaceFolders ~ofmt ~state params
+  | _ ->
+    dispatch_notification ~ofmt ~state ~method_ ~params;
+    state
+
 let dispatch_request ~method_ ~params : RAction.t =
   match method_ with
   (* Lifecyle *)
@@ -365,6 +422,7 @@ let dispatch_request ~ofmt ~id ~method_ ~params =
 let dispatch_message ~ofmt ~state (com : LSP.Message.t) =
   match com with
   | Notification { method_; params } ->
-    dispatch_notification ~ofmt ~state ~method_ ~params
+    dispatch_state_notification ~ofmt ~state ~method_ ~params
   | Request { id; method_; params } ->
-    dispatch_request ~ofmt ~id ~method_ ~params
+    dispatch_request ~ofmt ~id ~method_ ~params;
+    state

controller/lsp_core.mli

@@ -21,8 +21,9 @@
 
 module State : sig
   type t =
-    { root_state : Coq.State.t
-    ; workspace : Coq.Workspace.t
+    { cmdline : Coq.Workspace.CmdLine.t
+    ; root_state : Coq.State.t
+    ; workspaces : (string * Coq.Workspace.t) list
     }
 end
 
@@ -34,11 +35,11 @@ val lsp_init_loop :
   -> Format.formatter
   -> cmdline:Coq.Workspace.CmdLine.t
   -> debug:bool
-  -> Coq.Workspace.t
+  -> (string * Coq.Workspace.t) list
 
 (** Dispatch an LSP request or notification, requests may be postponed. *)
 val dispatch_message :
-  ofmt:Format.formatter -> state:State.t -> Lsp.Base.Message.t -> unit
+  ofmt:Format.formatter -> state:State.t -> Lsp.Base.Message.t -> State.t
 
 (** Serve postponed requests in the set, they can be stale *)
 val serve_postponed_requests : ofmt:Format.formatter -> Int.Set.t -> unit

controller/rq_init.ml

@@ -12,7 +12,9 @@ let option_cata f d x =
   | None -> d
   | Some x -> f x
 
+let string_field name dict = U.to_string (List.assoc name (U.to_assoc dict))
 let ostring_field name dict = Option.map U.to_string (List.assoc_opt name dict)
+let olist_field name dict = Option.map U.to_list (List.assoc_opt name dict)
 
 let odict_field name dict =
   option_default
@@ -41,18 +43,32 @@ let check_client_version client_version : unit =
 let default_workspace_root = "."
 let parse_furi x = Lang.LUri.of_string x |> Lang.LUri.File.of_uri
 
-let determine_workspace_root ~params : string =
+(* Poor man mapM *)
+let rec result_map ls =
+  match ls with
+  | [] -> Result.ok []
+  | r :: rs ->
+    Result.bind r (fun x ->
+        Result.bind (result_map rs) (fun xs -> Result.ok (x :: xs)))
+
+let parse_furis l = List.map parse_furi l |> result_map
+let parse_wf l = List.map (string_field "uri") l |> parse_furis
+
+let determine_workspace_root ~params : string list =
   let rootPath = ostring_field "rootPath" params |> Option.map parse_furi in
   let rootUri = ostring_field "rootUri" params |> Option.map parse_furi in
   (* XXX: enable when we advertise workspace folders support in the server *)
-  let _wsFolders = List.assoc_opt "workspaceFolders" params in
-  match (rootPath, rootUri) with
-  | None, None -> default_workspace_root
-  | _, Some (Ok dir_uri) -> Lang.LUri.File.to_string_file dir_uri
-  | Some (Ok dir_uri), None -> Lang.LUri.File.to_string_file dir_uri
-  | Some (Error msg), _ | _, Some (Error msg) ->
+  let wsFolders =
+    olist_field "workspaceFolders" params |> Option.map parse_wf
+  in
+  match (rootPath, rootUri, wsFolders) with
+  | None, None, None -> [ default_workspace_root ]
+  | _, Some (Ok dir_uri), None -> [ Lang.LUri.File.to_string_file dir_uri ]
+  | Some (Ok dir_uri), None, None -> [ Lang.LUri.File.to_string_file dir_uri ]
+  | Some (Error msg), _, _ | _, Some (Error msg), _ | _, _, Some (Error msg) ->
     LIO.trace "init" ("uri parsing failed: " ^ msg);
-    default_workspace_root
+    [ default_workspace_root ]
+  | _, _, Some (Ok folders) -> List.map Lang.LUri.File.to_string_file folders
 
 let do_initialize ~params =
   let dir = determine_workspace_root ~params in
@@ -79,6 +95,14 @@ let do_initialize ~params =
           ; ("resolveProvider", `Bool false)
           ] )
     ; ("definitionProvider", `Bool true)
+    ; ( "workspace"
+      , `Assoc
+          [ ( "workspaceFolders"
+            , `Assoc
+                [ ("supported", `Bool true)
+                ; ("changeNotifications", `Bool true)
+                ] )
+          ] )
     ]
   in
   ( `Assoc

controller/rq_init.mli

@@ -1,3 +1,3 @@
 (** Returns answer request + workspace root directory *)
 val do_initialize :
-  params:(string * Yojson.Safe.t) list -> Yojson.Safe.t * string
+  params:(string * Yojson.Safe.t) list -> Yojson.Safe.t * string list

lsp/workspace.ml

@@ -0,0 +1,27 @@
+(************************************************************************)
+(* Coq Language Server Protocol                                         *)
+(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias                                  *)
+(************************************************************************)
+
+module Lang = JLang
+
+module WorkspaceFolder = struct
+  type t =
+    { uri : Lang.LUri.File.t
+    ; name : string
+    }
+  [@@deriving yojson]
+end
+
+module WorkspaceFoldersChangeEvent = struct
+  type t =
+    { added : WorkspaceFolder.t list
+    ; removed : WorkspaceFolder.t list
+    }
+  [@@deriving yojson]
+end
+
+module DidChangeWorkspaceFoldersParams = struct
+  type t = { event : WorkspaceFoldersChangeEvent.t } [@@deriving yojson]
+end

lsp/workspace.mli

@@ -0,0 +1,25 @@
+(************************************************************************)
+(* Coq Language Server Protocol                                         *)
+(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias                                  *)
+(************************************************************************)
+
+module WorkspaceFolder : sig
+  type t =
+    { uri : Lang.LUri.File.t
+    ; name : string
+    }
+  [@@deriving yojson]
+end
+
+module WorkspaceFoldersChangeEvent : sig
+  type t =
+    { added : WorkspaceFolder.t list
+    ; removed : WorkspaceFolder.t list
+    }
+  [@@deriving yojson]
+end
+
+module DidChangeWorkspaceFoldersParams : sig
+  type t = { event : WorkspaceFoldersChangeEvent.t } [@@deriving yojson]
+end