Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[protocol] Rework verbosity into more granular options. #517

Merged
merged 1 commit into from
Jun 28, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,8 @@
- Be more resilient when serializing unknowns Asts (@ejgallego, #503,
reported by Gijs Pennings)
- Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, #511)
- More granular options `send_perf_data` `send_diags`, `verbosity`
will set them now (@ejgallego, #)

# coq-lsp 0.1.6: Peek
---------------------
Expand Down
2 changes: 2 additions & 0 deletions controller/coq_lsp.ml
Original file line number Diff line number Diff line change
Expand Up @@ -136,6 +136,8 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path delay =
let workspaces = lsp_init_loop ~ifn ~ofn ~cmdline ~debug in
let io =
if !Fleche.Config.v.verbosity < 2 then (
Fleche.Config.(
v := { !v with send_diags = false; send_perf_data = false });
LIO.set_log_fn (fun _obj -> ());
let io = concise_cb ofn in
Fleche.Io.CallBack.set io;
Expand Down
13 changes: 11 additions & 2 deletions fleche/config.ml
Original file line number Diff line number Diff line change
Expand Up @@ -36,9 +36,16 @@ type t =
; pp_type : int [@default 0]
(** Pretty-printing type in Info Panel Request, 0 = string; 1 = Pp.t; 2
= Coq Layout Engine *)
; show_stats_on_hover : bool [@default false]
; verbosity : int [@default 2]
; show_stats_on_hover : bool [@default false] (** Show stats on hover *)
; pp_json : bool [@default false]
(** Whether to pretty print the protocol JSON on the wire *)
; send_perf_data : bool [@default true]
(** Whether to send the perf data notification *)
; send_diags : bool [@default true]
(** Whether to send the diagnostics notification *)
; verbosity : int [@default 2]
(** Verbosity, 1 = reduced, 2 = default. As of today reduced will
disable all logging, and the diagnostics and perf_data notification *)
}

let default =
Expand All @@ -57,6 +64,8 @@ let default =
; show_stats_on_hover = false
; verbosity = 2
; pp_json = false
; send_perf_data = true
; send_diags = true
}

let v = ref default
4 changes: 2 additions & 2 deletions fleche/theory.ml
Original file line number Diff line number Diff line change
Expand Up @@ -137,7 +137,7 @@ 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 || !Config.v.verbosity > 1 then
if List.length diags > 0 || !Config.v.send_diags then
let uri, version = (doc.uri, doc.version) in
Io.Report.diagnostics ~io ~uri ~version diags

Expand Down Expand Up @@ -173,7 +173,7 @@ end = struct
let doc = Doc.check ~io ~target ~doc:handle.doc () in
let requests = Handle.update_doc_info ~handle ~doc in
send_diags ~io ~doc;
if !Config.v.verbosity > 1 then
if !Config.v.send_perf_data then
if (* Only if completed! *)
completed ~doc then send_perf_data ~io ~doc;
(* Only if completed! *)
Expand Down