[lsp] Implement LSP client-side logging, don't crash on log file creation

CHANGES.md

@@ -1,5 +1,11 @@
-# coq-lsp 0.1.1: Location
------------------------
+# coq-lsp 0.2.0: Location
+-------------------------
+
+# coq-lsp 0.1.1:
+----------------
+
+ - Don't crash if the log file can't be created (@ejgallego , #87)
+ - Use LSP functions for client-side logging (@ejgallego , #87)
 
 # coq-lsp 0.1.0: Memory
 -----------------------

README.md

@@ -32,7 +32,8 @@ hesitate to stop by.
 
 - Most problems can be resolved by restarting `coq-lsp`, in Visual
   Studio Code, `Ctrl+Shift+P` will give you access to the
-  `coq-lsp.restart` command.
+  `coq-lsp.restart` command. You can also look for messages in the
+  "Output" window in VSCode, "Coq LSP Server Events" channel.
 
 ## Features
 

controller/coq_lsp.ml

@@ -67,6 +67,7 @@ module TraceValue = struct
 end
 
 module LIO = Lsp.Io
+module Log = Lsp.Log
 module LSP = Lsp.Base
 
 (* Request Handling: The client expects a reply *)
@@ -75,8 +76,8 @@ module CoqLspOption = struct
 end
 
 let do_client_options coq_lsp_options =
-  LIO.log_error "init" "custom client options:";
-  LIO.log_object "init" (`Assoc coq_lsp_options);
+  Log.log_error "init" "custom client options:";
+  Log.log_object "init" (`Assoc coq_lsp_options);
   match CoqLspOption.of_yojson (`Assoc coq_lsp_options) with
   | Ok v -> Fleche.Config.v := v
   | Error _msg -> ()
@@ -85,12 +86,12 @@ let do_initialize ofmt ~id params =
   let coq_lsp_options = odict_field "initializationOptions" params in
   do_client_options coq_lsp_options;
   let client_capabilities = odict_field "capabilities" params in
-  LIO.log_error "init" "client capabilities:";
-  LIO.log_object "init" (`Assoc client_capabilities);
+  Log.log_error "init" "client capabilities:";
+  Log.log_object "init" (`Assoc client_capabilities);
   let trace =
     ostring_field "trace" params |> option_cata TraceValue.parse TraceValue.Off
   in
-  LIO.log_error "init" ("trace: " ^ TraceValue.to_string trace);
+  Log.log_error "init" ("trace: " ^ TraceValue.to_string trace);
   let capabilities =
     [ ("textDocumentSync", `Int 1)
     ; ("documentSymbolProvider", `Bool true)
@@ -145,7 +146,7 @@ let do_open ofmt ~state params =
   (match Hashtbl.find_opt doc_table uri with
   | None -> ()
   | Some _ ->
-    LIO.log_error "do_open" ("file " ^ uri ^ " not properly closed by client"));
+    Log.log_error "do_open" ("file " ^ uri ^ " not properly closed by client"));
   Hashtbl.add doc_table uri doc;
   do_check_text ofmt ~state ~doc
 
@@ -161,12 +162,12 @@ let do_change ofmt ~state params =
   let uri, version =
     (string_field "uri" document, int_field "version" document)
   in
-  LIO.log_error "checking file" (uri ^ " / version: " ^ string_of_int version);
+  Log.log_error "checking file" (uri ^ " / version: " ^ string_of_int version);
   let changes = List.map U.to_assoc @@ list_field "contentChanges" params in
   match changes with
   | [] -> ()
   | _ :: _ :: _ ->
-    LIO.log_error "do_change"
+    Log.log_error "do_change"
       "more than one change unsupported due to sync method";
     assert false
   | change :: _ ->
@@ -281,9 +282,9 @@ let memo_cache_file = ".coq-lsp.cache"
 let memo_save_to_disk () =
   try
     Fleche.Memo.save_to_disk ~file:memo_cache_file;
-    LIO.log_error "memo" "cache saved to disk"
+    Log.log_error "memo" "cache saved to disk"
   with exn ->
-    LIO.log_error "memo" (Printexc.to_string exn);
+    Log.log_error "memo" (Printexc.to_string exn);
     Sys.remove memo_cache_file;
     ()
 
@@ -293,12 +294,12 @@ let memo_save_to_disk () = if false then memo_save_to_disk ()
 let memo_read_from_disk () =
   try
     if Sys.file_exists memo_cache_file then (
-      LIO.log_error "memo" "trying to load cache file";
+      Log.log_error "memo" "trying to load cache file";
       Fleche.Memo.load_from_disk ~file:memo_cache_file;
-      LIO.log_error "memo" "cache file loaded")
-    else LIO.log_error "memo" "cache file not present"
+      Log.log_error "memo" "cache file loaded")
+    else Log.log_error "memo" "cache file not present"
   with exn ->
-    LIO.log_error "memo" ("loading cache failed: " ^ Printexc.to_string exn);
+    Log.log_error "memo" ("loading cache failed: " ^ Printexc.to_string exn);
     Sys.remove memo_cache_file;
     ()
 
@@ -351,27 +352,27 @@ let dispatch_message ofmt ~state dict =
   | "exit" -> raise Lsp_exit
   (* NOOPs *)
   | "initialized" | "workspace/didChangeWatchedFiles" -> ()
-  | msg -> LIO.log_error "no_handler" msg
+  | msg -> Log.log_error "no_handler" msg
 
 let dispatch_message ofmt ~state com =
   try dispatch_message ofmt ~state com with
-  | U.Type_error (msg, obj) -> LIO.log_object msg obj
+  | U.Type_error (msg, obj) -> Log.log_object msg obj
   | Lsp_exit -> raise Lsp_exit
   | exn ->
     let bt = Printexc.get_backtrace () in
     let iexn = Exninfo.capture exn in
-    LIO.log_error "process_queue"
+    Log.log_error "process_queue"
       (if Printexc.backtrace_status () then "bt=true" else "bt=false");
     let method_name = string_field "method" com in
-    LIO.log_error "process_queue" ("exn in method: " ^ method_name);
-    LIO.log_error "process_queue" (Printexc.to_string exn);
-    LIO.log_error "process_queue" Pp.(string_of_ppcmds CErrors.(iprint iexn));
-    LIO.log_error "BT" bt
+    Log.log_error "process_queue" ("exn in method: " ^ method_name);
+    Log.log_error "process_queue" (Printexc.to_string exn);
+    Log.log_error "process_queue" Pp.(string_of_ppcmds CErrors.(iprint iexn));
+    Log.log_error "BT" bt
 
 let rec process_queue ofmt ~state =
   (match Queue.peek_opt request_queue with
   | None -> (
-    (* LIO.log_error "process_queue" "queue is empty, yielding!"; *)
+    (* Log.log_error "process_queue" "queue is empty, yielding!"; *)
     match !change_pending with
     | Some com ->
       Control.interrupt := false;
@@ -384,46 +385,47 @@ let rec process_queue ofmt ~state =
     Control.interrupt := false;
     (* TODO we should optimize the queue *)
     ignore (Queue.pop request_queue);
-    LIO.log_error "process_queue" "We got job to do";
+    Log.log_error "process_queue" "We got job to do";
     dispatch_message ofmt ~state com);
   process_queue ofmt ~state
 
 let lsp_cb oc =
   Fleche.Io.CallBack.
-    { log_error = Lsp.Io.log_error
+    { log_error = Log.log_error
     ; send_diagnostics =
         (fun ~uri ~version diags ->
           lsp_of_diags ~uri ~version diags |> Lsp.Io.send_json oc)
     }
 
+let lvl_to_severity (lvl : Feedback.level) =
+  match lvl with
+  | Feedback.Debug -> 5
+  | Feedback.Info -> 4
+  | Feedback.Notice -> 3
+  | Feedback.Warning -> 2
+  | Feedback.Error -> 1
+
+let mk_fb_handler () =
+  let q = ref [] in
+  ( (fun Feedback.{ contents; _ } ->
+      match contents with
+      | Message (lvl, loc, msg) ->
+        let lvl = lvl_to_severity lvl in
+        q := (loc, lvl, msg) :: !q
+      | _ -> ())
+  , q )
+
 let lsp_main log_file std vo_load_path ml_include_path =
   LSP.std_protocol := std;
   Exninfo.record_backtrace true;
 
   let oc = F.std_formatter in
-  let debug_oc = open_out log_file in
-  LIO.debug_fmt := F.formatter_of_out_channel debug_oc;
-
-  (* Dedukti stuff *)
-  let lvl_to_severity (lvl : Feedback.level) =
-    match lvl with
-    | Feedback.Debug -> 5
-    | Feedback.Info -> 4
-    | Feedback.Notice -> 3
-    | Feedback.Warning -> 2
-    | Feedback.Error -> 1
-  in
 
-  let fb_handler, fb_queue =
-    let q = ref [] in
-    ( (fun Feedback.{ contents; _ } ->
-        match contents with
-        | Message (lvl, loc, msg) ->
-          let lvl = lvl_to_severity lvl in
-          q := (loc, lvl, msg) :: !q
-        | _ -> ())
-    , q )
-  in
+  (* Setup logging *)
+  let client_cb message = LIO.logMessage oc ~lvl:2 ~message in
+  Log.start_log ~client_cb log_file;
+
+  let fb_handler, fb_queue = mk_fb_handler () in
 
   Fleche.Io.CallBack.set (lsp_cb oc);
 
@@ -445,27 +447,29 @@ let lsp_main log_file std vo_load_path ml_include_path =
   let rec loop () =
     (* XXX: Implement a queue, compact *)
     let com = LIO.read_request stdin in
-    if Fleche.Debug.read then LIO.log_object "read" com;
+    if Fleche.Debug.read then Log.log_object "read" com;
     process_input com;
     loop ()
   in
   try loop () with
   | (LIO.ReadError "EOF" | Lsp_exit) as exn ->
-    LIO.log_error "main"
-      ("exiting" ^ if exn = Lsp_exit then "" else " [uncontrolled LSP shutdown]");
-    LIO.flush_log ();
-    flush_all ();
-    close_out debug_oc
+    let reason =
+      "exiting" ^ if exn = Lsp_exit then "" else " [uncontrolled LSP shutdown]"
+    in
+    Log.log_error "main" reason;
+    LIO.logMessage oc ~lvl:1 ~message:("server " ^ reason);
+    Log.end_log ();
+    flush_all ()
   | exn ->
     let bt = Printexc.get_backtrace () in
     let exn, info = Exninfo.capture exn in
     let exn_msg = Printexc.to_string exn in
-    LIO.log_error "fatal error" (exn_msg ^ bt);
-    LIO.log_error "fatal_error [coq iprint]"
+    Log.log_error "fatal error" (exn_msg ^ bt);
+    Log.log_error "fatal_error [coq iprint]"
       Pp.(string_of_ppcmds CErrors.(iprint (exn, info)));
-    LIO.flush_log ();
-    flush_all ();
-    close_out debug_oc
+    LIO.logMessage oc ~lvl:1 ~message:("server crash: " ^ exn_msg ^ bt);
+    Log.end_log ();
+    flush_all ()
 
 (* Arguments handling *)
 open Cmdliner

editor/code/src/client.ts

@@ -1,5 +1,5 @@
 import { window, commands, ExtensionContext, workspace, WebviewPanel, ViewColumn, Uri } from "vscode";
-import { LanguageClient } from "vscode-languageclient/node";
+import { LanguageClient, LanguageClientOptions } from "vscode-languageclient/node";
 import { GoalPanel } from "./goals";
 
 let client : LanguageClient;
@@ -11,6 +11,7 @@ export function panelFactory(context : ExtensionContext) {
     const styleUri = panel.webview.asWebviewUri(Uri.joinPath(context.extensionUri, 'media', 'styles.css'));
     return new GoalPanel(client, panel, styleUri);
 }
+
 export function activate (context : ExtensionContext) : void {
     window.showInformationMessage('Going to activate!');
 
@@ -32,10 +33,12 @@ export function activate (context : ExtensionContext) : void {
             ok_diagnostics: config.ok_diagnostics
         };
 
-        const clientOptions = {
+        const clientOptions : LanguageClientOptions = {
             documentSelector: [
                 {scheme: 'file', language: 'coq'}
             ],
+            outputChannelName: "Coq LSP Server Events",
+            revealOutputChannelOn: 1,
             initializationOptions
         };
         const serverOptions = { command: config.path, args: config.args };

lsp/base.ml

@@ -34,9 +34,12 @@ let _parse_uri str =
 let mk_reply ~id ~result =
   `Assoc [ ("jsonrpc", `String "2.0"); ("id", `Int id); ("result", result) ]
 
-let mk_event m p =
+let mk_notification ~method_ ~params =
   `Assoc
-    [ ("jsonrpc", `String "2.0"); ("method", `String m); ("params", `Assoc p) ]
+    [ ("jsonrpc", `String "2.0")
+    ; ("method", `String method_)
+    ; ("params", `Assoc params)
+    ]
 
 (* let json_of_goal g = let pr_hyp (s,(_,t)) = `Assoc ["hname", `String s;
    "htype", `String (Format.asprintf "%a" Print.pp_term (Bindlib.unbox t))] in
@@ -74,8 +77,9 @@ let mk_diagnostic
     ]
 
 let mk_diagnostics ~uri ~version ld : J.t =
-  mk_event "textDocument/publishDiagnostics"
-  @@ [ ("uri", `String uri)
-     ; ("version", `Int version)
-     ; ("diagnostics", `List List.(map mk_diagnostic ld))
-     ]
+  mk_notification ~method_:"textDocument/publishDiagnostics"
+    ~params:
+      [ ("uri", `String uri)
+      ; ("version", `Int version)
+      ; ("diagnostics", `List List.(map mk_diagnostic ld))
+      ]

lsp/base.mli

@@ -16,6 +16,12 @@
 (************************************************************************)
 
 val mk_range : Fleche.Types.Range.t -> Yojson.Safe.t
+
+(** Build notification *)
+val mk_notification :
+  method_:string -> params:(string * Yojson.Safe.t) list -> Yojson.Safe.t
+
+(** Answer to a request *)
 val mk_reply : id:int -> result:Yojson.Safe.t -> Yojson.Safe.t
 
 (* val mk_diagnostic : Range.t * int * string * unit option -> Yojson.Basic.t *)

lsp/io.ml

@@ -11,29 +11,13 @@
 (************************************************************************)
 (* Coq Language Server Protocol                                         *)
 (* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
+(* Copyright 2019-2022 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
-(* Status: Experimental                                                 *)
-(************************************************************************)
 
 module F = Format
 module J = Yojson.Safe
 
-let mut = Mutex.create ()
-let debug_fmt = ref F.err_formatter
-
-let log_error hdr msg =
-  Mutex.lock mut;
-  F.fprintf !debug_fmt "[%s]: @[%s@]@\n%!" hdr msg;
-  Mutex.unlock mut
-
-let log_object hdr obj =
-  F.fprintf !debug_fmt "[%s]: @[%a@]@\n%!" hdr J.(pretty_print ~std:false) obj
-
-let flush_log () = F.pp_print_flush !debug_fmt ()
-
-exception ReadError of string
-
 let read_request_raw ic =
   let cl = input_line ic in
   let sin = Scanf.Scanning.from_string cl in
@@ -54,6 +38,8 @@ let read_request_raw ic =
   in
   J.from_string raw_obj
 
+exception ReadError of string
+
 let read_request ic =
   try read_request_raw ic with
   (* if the end of input is encountered while some more characters are needed to
@@ -66,10 +52,25 @@ let read_request ic =
   (* if the format string is invalid. *)
   | Invalid_argument msg -> raise (ReadError msg)
 
+let mut = Mutex.create ()
+
 let send_json fmt obj =
   Mutex.lock mut;
-  if Fleche.Debug.send then log_object "send" obj;
+  if Fleche.Debug.send then Log.log_object "send" obj;
   let msg = F.asprintf "%a" J.(pretty_print ~std:true) obj in
   let size = String.length msg in
   F.fprintf fmt "Content-Length: %d\r\n\r\n%s%!" size msg;
   Mutex.unlock mut
+
+let logMessage fmt ~lvl ~message =
+  let method_ = "window/logMessage" in
+  let params = [ ("type", `Int lvl); ("message", `String message) ] in
+  let msg = Base.mk_notification ~method_ ~params in
+  send_json fmt msg
+
+let logTrace fmt ~message ?verbose () =
+  let method_ = "$/logTrace" in
+  let verbose = Option.cata (fun v -> [ ("verbose", `String v) ]) [] verbose in
+  let params = [ ("message", `String message) ] @ verbose in
+  let msg = Base.mk_notification ~method_ ~params in
+  send_json fmt msg