diff --git a/CHANGES.md b/CHANGES.md index 9a73963a..a41599d9 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,11 +1,6 @@ # unreleased ------------ - - Added new heatmap feature allowing timing data to be seen in the - editor. Can be enabled with the `Coq LSP: Toggle heatmap` - comamnd. Can be configured to show memory usage. Colors and - granularity are configurable. (@Alizter and @ejgallego, #686, - grants #681). - new option `show_loc_info_on_hover` that will display parsing debug information on hover; previous flag was fixed in code, which is way less flexible. This also fixes the option being on in 0.1.8 by @@ -132,19 +127,25 @@ #697) - Always dispose UI elements. This should improve some strange behaviors on extension restart (@ejgallego, #708) - - Support Coq meta-commands (Reset, Reset Initial, Back) They are - actually pretty useful to hint the incremental engine to ignore - changes in some part of the document (@ejgallego, #709) + - [code] Added new heatmap feature allowing timing data to be seen in + the editor. Can be enabled with the `Coq LSP: Toggle heatmap` + comamnd. Can be configured to show memory usage. Colors and + granularity are configurable. (@Alizter and @ejgallego, #686, + grants #681). + - [server] Support Coq meta-commands (Reset, Reset Initial, Back) + They are actually pretty useful to hint the incremental engine to + ignore changes in some part of the document (@ejgallego, #709) - JSON-RPC library now supports all kind of incoming messages (@ejgallego, #713) - - New `coq/viewRange` notification, from client to server, than hints - the scheduler for the visible area of the document; combined with - the new lazy checking mode, this provides checking on scroll, a - feature inspired from Isabelle IDE (@ejgallego, #717) - - Have VSCode wait for full LSP client shutdown on server + - [code/server] New `coq/viewRange` notification, from client to + server, than hints the scheduler for the visible area of the + document; combined with the new lazy checking mode, this provides + checking on scroll, a feature inspired from Isabelle IDE + (@ejgallego, #717) + - [code] Have VSCode wait for full LSP client shutdown on server restart. This fixes some bugs on extension restart (finally!) (@ejgallego, #719) - - Center the view if cursor goes out of scope in + - [code] Center the view if cursor goes out of scope in `sentenceNext/sentencePrevious` (@ejgallego, #718) - Switch Flèche range encoding to protocol native, this means UTF-16 code points for now (Léo Stefanesco, @ejgallego, #624, fixes #620, @@ -154,7 +155,7 @@ user navigates proofs (@Alidra @ejgallego, #722, #725) - `fcc`: new option `--diags_level` to control whether Coq's notice and info messages appear as diagnostics - - Display the continous/on-request checking mode in the status bar, + - [code] Display the continous/on-request checking mode in the status bar, allow to change it by clicking on it (@ejgallego, #721) - Add an example of multiple workspaces (@ejgallego, @Blaisorblade, #611) @@ -173,6 +174,10 @@ - [petanque] Return extra premise information: file name, position, raw_text, using the above support for reading .glob files (@ejgallego, #735) + - [code] Display server status using the `LanguageStatusItem` + facility, for now we display version and checking status + information (moved from #721), and we also allow to toggle the + checking mode from there (@ejgallego, #728) # coq-lsp 0.1.8.1: Spring fix ----------------------------- diff --git a/README.md b/README.md index 985b6d60..6014718b 100644 --- a/README.md +++ b/README.md @@ -39,6 +39,7 @@ and web native usage, providing quite a few extra features from vanilla Coq. - [🎁 Features](#-features) - [⏩ Incremental Compilation and Continuous Document Checking](#-incremental-compilation-and-continuous-document-checking) + - [👁 On-demand, Follow The Viewport Document Checking](#-on-demand-follow-the-viewport-document-checking) - [🧠 Smart, Cache-Aware Error Recovery](#-smart-cache-aware-error-recovery) - [🥅 Whole-Document Goal Display](#-whole-document-goal-display) - [🗒️ Markdown Support](#️-markdown-support) @@ -89,6 +90,14 @@ restart your proof session where you left it at the last time. Incremental support is undergoing refinement, if `coq-lsp` rechecks when it should not, please file a bug! +### 👁 On-demand, Follow The Viewport Document Checking + +`coq-lsp` does also support on-demand checking. Two modes are available: follow +the cursor, or follow the viewport; the modes can be toggled using the Language +Status Item in Code's bottom right corner: + +On-demand checking + ### 🧠 Smart, Cache-Aware Error Recovery `coq-lsp` won't stop checking on errors, but supports (and encourages) working diff --git a/compiler/output.ml b/compiler/output.ml index 323586c8..bbf66a2a 100644 --- a/compiler/output.ml +++ b/compiler/output.ml @@ -9,7 +9,6 @@ let pp_diags fmt dl = (* We will use this when we set eager diagnotics to true *) let diagnostics ~uri:_ ~version:_ _diags = () let fileProgress ~uri:_ ~version:_ _progress = () -let perfData ~uri:_ ~version:_ _perf = () (* We print trace and messages, and perfData summary *) module Fcc_verbose = struct @@ -24,26 +23,30 @@ module Fcc_verbose = struct let perfData ~uri:_ ~version:_ { Fleche.Perf.summary; _ } = Format.(eprintf "[perfdata]@\n@[%s@]@\n%!" summary) + let serverVersion _ = () + let serverStatus _ = () + let cb = - Fleche.Io.CallBack.{ trace; message; diagnostics; fileProgress; perfData } + Fleche.Io.CallBack. + { trace + ; message + ; diagnostics + ; fileProgress + ; perfData + ; serverVersion + ; serverStatus + } end (* We print trace, messages *) module Fcc_normal = struct let trace _ ?extra:_ _ = () - let message = Fcc_verbose.message - let perfData = Fcc_verbose.perfData - - let cb = - Fleche.Io.CallBack.{ trace; message; diagnostics; fileProgress; perfData } + let cb = { Fcc_verbose.cb with trace } end module Fcc_quiet = struct - let trace _ ?extra:_ _ = () let message ~lvl:_ ~message:_ = () - - let cb = - Fleche.Io.CallBack.{ trace; message; diagnostics; fileProgress; perfData } + let cb = { Fcc_normal.cb with message } end let set_callbacks (display : Args.Display.t) = diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index dff2d0c9..25caf87d 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -49,35 +49,52 @@ let rec process_queue ~delay ~io ~ofn ~state : unit = | Some (Cont state) -> process_queue ~delay ~io ~ofn ~state let concise_cb ofn = + let send_notification nt = + Lsp.Base.Message.(Notification nt |> to_yojson) |> ofn + in + let diagnostics ~uri ~version diags = + if List.length diags > 0 then + Lsp.JLang.mk_diagnostics ~uri ~version diags |> send_notification + in Fleche.Io.CallBack. { trace = (fun _hdr ?extra:_ _msg -> ()) ; message = (fun ~lvl:_ ~message:_ -> ()) - ; diagnostics = - (fun ~uri ~version diags -> - if List.length diags > 0 then - Lsp.JLang.mk_diagnostics ~uri ~version diags |> ofn) + ; diagnostics ; fileProgress = (fun ~uri:_ ~version:_ _progress -> ()) ; perfData = (fun ~uri:_ ~version:_ _perf -> ()) + ; serverVersion = (fun _ -> ()) + ; serverStatus = (fun _ -> ()) } (* Main loop *) let lsp_cb ofn = + let send_notification nt = + Lsp.Base.Message.(Notification nt |> to_yojson) |> ofn + in + let trace = LIO.trace in let message ~lvl ~message = let lvl = Fleche.Io.Level.to_int lvl in LIO.logMessageInt ~lvl ~message in + let diagnostics ~uri ~version diags = + Lsp.JLang.mk_diagnostics ~uri ~version diags |> send_notification + in + let fileProgress ~uri ~version progress = + Lsp.JFleche.mk_progress ~uri ~version progress |> send_notification + in + let perfData ~uri ~version perf = + Lsp.JFleche.mk_perf ~uri ~version perf |> send_notification + in + let serverVersion vi = Lsp.JFleche.mk_serverVersion vi |> send_notification in + let serverStatus st = Lsp.JFleche.mk_serverStatus st |> send_notification in Fleche.Io.CallBack. - { trace = LIO.trace + { trace ; message - ; diagnostics = - (fun ~uri ~version diags -> - Lsp.JLang.mk_diagnostics ~uri ~version diags |> ofn) - ; fileProgress = - (fun ~uri ~version progress -> - Lsp.JFleche.mk_progress ~uri ~version progress |> ofn) - ; perfData = - (fun ~uri ~version perf -> - Lsp.JFleche.mk_perf ~uri ~version perf |> ofn) + ; diagnostics + ; fileProgress + ; perfData + ; serverVersion + ; serverStatus } let coq_init ~debug = @@ -116,7 +133,7 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path let json_fn = LIO.send_json Format.std_formatter in let ofn response = - let response = Lsp.Base.Response.to_yojson response in + let response = Lsp.Base.Message.to_yojson response in LIO.send_json Format.std_formatter response in diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index aa593abb..abc0c48c 100644 --- a/controller/lsp_core.ml +++ b/controller/lsp_core.ml @@ -164,28 +164,28 @@ module Rq : sig end val serve : - ofn:(LSP.Response.t -> unit) + ofn_rq:(LSP.Response.t -> unit) -> token:Coq.Limits.Token.t -> id:int -> Action.t -> unit val cancel : - ofn:(LSP.Response.t -> unit) -> code:int -> message:string -> int -> unit + ofn_rq:(LSP.Response.t -> unit) -> code:int -> message:string -> int -> unit val serve_postponed : - ofn:(LSP.Response.t -> unit) + ofn_rq:(LSP.Response.t -> unit) -> token:Coq.Limits.Token.t -> doc:Fleche.Doc.t -> Int.Set.t -> unit end = struct (* Answer a request, private *) - let answer ~ofn ~id result = + let answer ~ofn_rq ~id result = (match result with | Result.Ok result -> LSP.Response.mk_ok ~id ~result | Error (code, message) -> LSP.Response.mk_error ~id ~code ~message) - |> ofn + |> ofn_rq (* private to the Rq module, just used not to retrigger canceled requests *) let _rtable : (int, Request.Data.t) Hashtbl.t = Hashtbl.create 673 @@ -196,16 +196,16 @@ end = struct Hashtbl.add _rtable id pr (* Consumes a request, if alive, it answers mandatorily *) - let consume_ ~ofn ~f id = + let consume_ ~ofn_rq ~f id = match Hashtbl.find_opt _rtable id with | Some pr -> Hashtbl.remove _rtable id; - f pr |> answer ~ofn ~id + f pr |> answer ~ofn_rq ~id | None -> LIO.trace "can't consume cancelled request: " (string_of_int id); () - let cancel ~ofn ~code ~message id : unit = + let cancel ~ofn_rq ~code ~message id : unit = (* fail the request, do cleanup first *) let f pr = let () = @@ -214,30 +214,30 @@ end = struct in Error (code, message) in - consume_ ~ofn ~f id + consume_ ~ofn_rq ~f id let debug_serve id pr = if Fleche.Debug.request_delay then LIO.trace "serving" (Format.asprintf "rq: %d | %a" id Request.Data.data pr) - let serve_postponed ~ofn ~token ~doc id = + let serve_postponed ~ofn_rq ~token ~doc id = let f pr = debug_serve id pr; Request.Data.serve ~token ~doc pr in - consume_ ~ofn ~f id + consume_ ~ofn_rq ~f id - let query ~ofn ~token ~id (pr : Request.Data.t) = + let query ~ofn_rq ~token ~id (pr : Request.Data.t) = let uri, postpone, request = Request.Data.dm_request pr in match Fleche.Theory.Request.add { id; uri; postpone; request } with | Cancel -> let code = -32802 in let message = "Document is not ready" in - Error (code, message) |> answer ~ofn ~id + Error (code, message) |> answer ~ofn_rq ~id | Now doc -> debug_serve id pr; - Request.Data.serve ~token ~doc pr |> answer ~ofn ~id + Request.Data.serve ~token ~doc pr |> answer ~ofn_rq ~id | Postpone -> postpone_ ~id pr module Action = struct @@ -249,13 +249,13 @@ end = struct let error (code, msg) = now (Error (code, msg)) end - let serve ~ofn ~token ~id action = + let serve ~ofn_rq ~token ~id action = match action with - | Action.Immediate r -> answer ~ofn ~id r - | Action.Data p -> query ~ofn ~token ~id p + | Action.Immediate r -> answer ~ofn_rq ~id r + | Action.Data p -> query ~ofn_rq ~token ~id p - let serve_postponed ~ofn ~token ~doc rl = - Int.Set.iter (serve_postponed ~ofn ~token ~doc) rl + let serve_postponed ~ofn_rq ~token ~doc rl = + Int.Set.iter (serve_postponed ~ofn_rq ~token ~doc) rl end (***********************************************************************) @@ -272,7 +272,7 @@ let do_open ~io ~token ~(state : State.t) params = let env = Fleche.Doc.Env.make ~init ~workspace ~files in Fleche.Theory.create ~io ~token ~env ~uri ~raw:text ~version -let do_change ~ofn ~io ~token params = +let do_change ~ofn_rq ~io ~token 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 @@ -288,7 +288,7 @@ let do_change ~ofn ~io ~token params = let invalid_rq = Fleche.Theory.change ~io ~token ~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 + Int.Set.iter (Rq.cancel ~ofn_rq ~code ~message) invalid_rq let do_close ~ofn:_ params = let uri = Helpers.get_uri params in @@ -403,11 +403,11 @@ let do_document = do_document_request_maybe ~handler:Rq_document.request let do_save_vo = do_document_request_maybe ~handler:Rq_save.request let do_lens = do_document_request_maybe ~handler:Rq_lens.request -let do_cancel ~ofn ~params = +let do_cancel ~ofn_rq ~params = let id = int_field "id" params in let code = -32800 in let message = "Cancelled by client" in - Rq.cancel ~ofn ~code ~message id + Rq.cancel ~ofn_rq ~code ~message id let do_cache_trim () = Nt_cache_trim.notification () @@ -456,6 +456,7 @@ module Init_effect = struct end let lsp_init_process ~ofn ~cmdline ~debug msg : Init_effect.t = + let ofn_rq r = Lsp.Base.Message.response r |> ofn in match msg with | LSP.Message.Request { method_ = "initialize"; id; params } -> (* At this point logging is allowed per LSP spec *) @@ -465,7 +466,14 @@ let lsp_init_process ~ofn ~cmdline ~debug msg : Init_effect.t = LIO.logMessage ~lvl:Info ~message; let token = Coq.Limits.Token.create () in let result, dirs = Rq_init.do_initialize ~params in - Rq.Action.now (Ok result) |> Rq.serve ~ofn ~token ~id; + Rq.Action.now (Ok result) |> Rq.serve ~ofn_rq ~token ~id; + let vi = + let coq = Coq_config.version in + let ocaml = Sys.ocaml_version in + let coq_lsp = Fleche.Version.server in + Fleche.ServerInfo.Version.{ coq; ocaml; coq_lsp } + in + Lsp.JFleche.mk_serverVersion vi |> Lsp.Base.Message.notification |> ofn; let message = Format.asprintf "Server initializing (int_backend: %s)" (Coq.Limits.name ()) @@ -483,7 +491,7 @@ let lsp_init_process ~ofn ~cmdline ~debug msg : Init_effect.t = | LSP.Message.Request { id; _ } -> (* per spec *) LSP.Response.mk_error ~id ~code:(-32002) ~message:"server not initialized" - |> ofn; + |> ofn_rq; Loop | LSP.Message.Notification { method_ = "exit"; params = _ } -> Exit | LSP.Message.Notification _ -> @@ -495,6 +503,7 @@ let lsp_init_process ~ofn ~cmdline ~debug msg : Init_effect.t = (** Dispatching *) let dispatch_notification ~io ~ofn ~token ~state ~method_ ~params : unit = + let ofn_rq r = Lsp.Base.Message.response r |> ofn in match method_ with (* Lifecycle *) | "exit" -> raise Lsp_exit @@ -503,14 +512,14 @@ let dispatch_notification ~io ~ofn ~token ~state ~method_ ~params : unit = | "workspace/didChangeConfiguration" -> do_changeConfiguration params (* Document lifetime *) | "textDocument/didOpen" -> do_open ~io ~token ~state params - | "textDocument/didChange" -> do_change ~io ~ofn ~token params + | "textDocument/didChange" -> do_change ~io ~ofn_rq ~token params | "textDocument/didClose" -> do_close ~ofn params | "textDocument/didSave" -> Cache.save_to_disk () (* Specific to coq-lsp *) | "coq/viewRange" -> do_viewRange params | "coq/trimCaches" -> do_cache_trim () (* Cancel Request *) - | "$/cancelRequest" -> do_cancel ~ofn ~params + | "$/cancelRequest" -> do_cancel ~ofn_rq ~params (* NOOPs *) | "initialized" -> () (* Generic handler *) @@ -552,17 +561,18 @@ let dispatch_request ~method_ ~params : Rq.Action.t = LIO.trace "no_handler" msg; Rq.Action.error (-32601, "method not found") -let dispatch_request ~ofn ~token ~id ~method_ ~params = - dispatch_request ~method_ ~params |> Rq.serve ~ofn ~token ~id +let dispatch_request ~ofn_rq ~token ~id ~method_ ~params = + dispatch_request ~method_ ~params |> Rq.serve ~ofn_rq ~token ~id let dispatch_message ~io ~ofn ~token ~state (com : LSP.Message.t) : State.t = + let ofn_rq r = Lsp.Base.Message.response r |> ofn in match com with | Notification { method_; params } -> LIO.trace "process_queue" ("Serving notification: " ^ method_); dispatch_state_notification ~io ~ofn ~token ~state ~method_ ~params | Request { id; method_; params } -> LIO.trace "process_queue" ("Serving Request: " ^ method_); - dispatch_request ~ofn ~token ~id ~method_ ~params; + dispatch_request ~ofn_rq ~token ~id ~method_ ~params; state | Response r -> LIO.trace "process_queue" @@ -597,10 +607,11 @@ type 'a cont = | Yield of 'a let check_or_yield ~io ~ofn ~token ~state = + let ofn_rq r = Lsp.Base.Message.response r |> ofn in match Fleche.Theory.Check.maybe_check ~io ~token with | None -> Yield state | Some (ready, doc) -> - let () = Rq.serve_postponed ~ofn ~token ~doc ready in + let () = Rq.serve_postponed ~ofn_rq ~token ~doc ready in Cont state module LspQueue : sig diff --git a/controller/lsp_core.mli b/controller/lsp_core.mli index e05be395..8581e189 100644 --- a/controller/lsp_core.mli +++ b/controller/lsp_core.mli @@ -41,7 +41,7 @@ module Init_effect : sig end val lsp_init_process : - ofn:(Lsp.Base.Response.t -> unit) + ofn:(Lsp.Base.Message.t -> unit) -> cmdline:Coq.Workspace.CmdLine.t -> debug:bool -> Lsp.Base.Message.t @@ -56,7 +56,7 @@ type 'a cont = wake up pending requests *) val dispatch_or_resume_check : io:Fleche.Io.CallBack.t - -> ofn:(Lsp.Base.Response.t -> unit) + -> ofn:(Lsp.Base.Message.t -> unit) -> state:State.t -> State.t cont option diff --git a/editor/code/lib/types.ts b/editor/code/lib/types.ts index f5065a9b..1e196f07 100644 --- a/editor/code/lib/types.ts +++ b/editor/code/lib/types.ts @@ -184,3 +184,27 @@ export interface ViewRangeParams { textDocument: VersionedTextDocumentIdentifier; range: Range; } + +// Server version and status notifications + +export interface CoqServerVersion { + coq: string; + ocaml: string; + coq_lsp: string; +} + +export interface CoqBusyStatus { + status: "Busy"; + modname: string; +} + +export interface CoqIdleStatus { + status: "Idle"; + mem: string; +} + +export interface CoqStoppedStatus { + status: "Stopped"; +} + +export type CoqServerStatus = CoqBusyStatus | CoqIdleStatus | CoqStoppedStatus; diff --git a/editor/code/package.json b/editor/code/package.json index 1bdcb9bf..ca1e6731 100644 --- a/editor/code/package.json +++ b/editor/code/package.json @@ -100,6 +100,10 @@ "command": "coq-lsp.toggle", "title": "Coq LSP: Toggle the running status of Coq Language Server" }, + { + "command": "coq-lsp.toggle_mode", + "title": "Coq LSP: Toggle checking mode between continous / on-demand" + }, { "command": "coq-lsp.goals", "title": "Coq LSP: Show Goals at point" @@ -304,13 +308,13 @@ }, "coq-lsp.check_only_on_request": { "type": "boolean", - "default": false, - "description": "Check files lazily, that is to say, goal state for a point will only be computed when the data is actually demanded. Note that this feature is experimental." + "default": true, + "description": "(Experimental) Check files lazily, that is to say, goal state for a point will only be computed when the data is actually demanded." }, "coq-lsp.check_on_scroll": { "type": "boolean", - "default": false, - "description": "When in lazy mode, check files on scroll. Note that this feature is experimental." + "default": true, + "description": "(Experimental) When in lazy mode, check files on scroll." } } }, diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts index 63230017..c600a556 100644 --- a/editor/code/src/client.ts +++ b/editor/code/src/client.ts @@ -41,6 +41,13 @@ import { ViewRangeParams, } from "../lib/types"; +import { + CoqLanguageStatus, + defaultVersion, + defaultStatus, + coqServerVersion, + coqServerStatus, +} from "./status"; import { CoqLspClientConfig, CoqLspServerConfig, CoqSelector } from "./config"; import { InfoPanel, goalReq } from "./goals"; import { FileProgressManager } from "./progress"; @@ -78,6 +85,11 @@ let fileProgress: FileProgressManager; // Status Bar Button let lspStatusItem: StatusBarItem; +// Language Status Indicators +let languageStatus: CoqLanguageStatus; +let languageVersionHook: Disposable; +let languageStatusHook: Disposable; + // Lifetime of the perf data setup == client lifetime for the hook, extension for the webview let perfDataView: PerfDataView; let perfDataHook: Disposable; @@ -127,7 +139,10 @@ export function activateCoqLSP( return settings; } - function coqCommand(command: string, fn: () => void | Promise) { + function coqCommand( + command: string, + fn: (...args: any[]) => void | Promise + ) { let disposable = commands.registerCommand("coq-lsp." + command, fn); context.subscriptions.push(disposable); } @@ -177,6 +192,8 @@ export function activateCoqLSP( fileProgress.dispose(); perfDataHook.dispose(); heatMap.dispose(); + languageVersionHook.dispose(); + languageStatusHook.dispose(); }); } else return Promise.resolve(); }; @@ -205,6 +222,14 @@ export function activateCoqLSP( heatMap.update(toVsCodePerf(data)); }); + languageVersionHook = client.onNotification(coqServerVersion, (data) => { + languageStatus.updateVersion(data); + }); + + languageStatusHook = client.onNotification(coqServerStatus, (data) => { + languageStatus.updateStatus(data, serverConfig.check_only_on_request); + }); + resolve(client); }); @@ -233,22 +258,24 @@ export function activateCoqLSP( await stop().finally(start); }; - const set_lazy_checking = async (value: boolean) => { + const toggle_lazy_checking = async () => { let wsConfig = workspace.getConfiguration(); - await wsConfig.update("coq-lsp.check_only_on_request", value); + let newValue = !wsConfig.get("coq-lsp.check_only_on_request"); + await wsConfig.update("coq-lsp.check_only_on_request", newValue); + languageStatus.updateStatus({ status: "Idle", mem: "" }, newValue); }; // switches between the different status of the server const toggle = async () => { if (client && client.isRunning() && !serverConfig.check_only_on_request) { // Server on, and in continous mode, set lazy - await set_lazy_checking(true).then(updateStatusBar); + await toggle_lazy_checking().then(updateStatusBar); } else if (client && client.isRunning()) { // Server on, and in lazy mode, stop await stop(); } else { // Server is off, set continous mode and start - await set_lazy_checking(false).then(start); + await toggle_lazy_checking().then(start); } }; @@ -438,6 +465,9 @@ export function activateCoqLSP( context.subscriptions.push(lspStatusItem); }; + // This stuff should likely go in the CoqLSP client class + languageStatus = new CoqLanguageStatus(defaultVersion, defaultStatus, false); + // Ali notes about the status item text: we should keep it short // We violate this on the error case, but only because it is exceptional. const updateStatusBar = () => { @@ -478,6 +508,8 @@ export function activateCoqLSP( coqCommand("toggle", toggle); coqCommand("trim", cacheTrim); + coqCommand("toggle_mode", toggle_lazy_checking); + coqEditorCommand("goals", goals); coqEditorCommand("document", getDocument); coqEditorCommand("save", saveDocument); diff --git a/editor/code/src/status.ts b/editor/code/src/status.ts new file mode 100644 index 00000000..f9a5f406 --- /dev/null +++ b/editor/code/src/status.ts @@ -0,0 +1,104 @@ +import { LanguageStatusItem, LanguageStatusSeverity, languages } from "vscode"; +import { NotificationType } from "vscode-languageclient"; + +import { CoqSelector } from "./config"; + +import { CoqServerVersion, CoqServerStatus } from "../lib/types"; + +export const coqServerVersion = new NotificationType( + "$/coq/serverVersion" +); + +export const coqServerStatus = new NotificationType( + "$/coq/serverStatus" +); + +// We should likely have one class per item, but not a big deal yet +export class CoqLanguageStatus { + // Checking and what + status: LanguageStatusItem; + // Version info + version: LanguageStatusItem; + // Root: one or multiple, to be done soon + // root : LanguageStatusItem; + + constructor( + version: CoqServerVersion, + status: CoqServerStatus, + lazy_mode: boolean + ) { + // Version info + this.version = languages.createLanguageStatusItem( + "coq.version", + CoqSelector.all + ); + this.version.name = "Version"; + + // Server status + this.status = languages.createLanguageStatusItem( + "coq.status", + CoqSelector.all + ); + this.status.name = "Running Status"; + + // this.status.command = "start continous toogle continous"; + // root = languages.createLanguageStatusItem("coq.root", CoqSelector.all); + + this.updateVersion(version); + this.updateStatus(status, lazy_mode); + } + + updateVersion(version: CoqServerVersion) { + this.version.text = `coq-lsp ${version.coq_lsp}`; + this.version.detail = `Coq ${version.coq}, OCaml ${version.ocaml}`; + } + + updateStatus(status: CoqServerStatus, lazy_mode: boolean) { + let command = lazy_mode + ? { + title: "Enable Continous Mode", + command: "coq-lsp.toggle_mode", + } + : { + title: "Enable On-Demand Mode", + command: "coq-lsp.toggle_mode", + args: true, + }; + + let status_name = lazy_mode ? "On-demand" : "Continous"; + + if (status.status == "Busy") { + this.status.busy = true; + this.status.text = `coq-lsp: Checking ${status.modname}`; + this.status.detail = `set mode`; + this.status.command = command; + this.status.severity = LanguageStatusSeverity.Information; + } else if (status.status == "Idle") { + // Idle + this.status.busy = false; + this.status.text = `coq-lsp: Idle (${status_name} |${status.mem})`; + this.status.detail = ""; + this.status.command = command; + this.status.severity = LanguageStatusSeverity.Information; + } else if (status.status == "Stopped") { + this.status.busy = false; + this.status.text = `Stopped`; + this.status.detail = ""; + this.status.command = { title: "Start Server", command: "coq-lsp.start" }; + this.status.severity = LanguageStatusSeverity.Error; + } + } + + dispose() { + this.status.dispose(); + this.version.dispose(); + // root.dispose(); + } +} + +export const defaultVersion: CoqServerVersion = { + coq: "N/A", + ocaml: "N/A", + coq_lsp: "N/A", +}; +export const defaultStatus: CoqServerStatus = { status: "Idle", mem: "" }; diff --git a/etc/doc/PROTOCOL.md b/etc/doc/PROTOCOL.md index c3e303b4..8da3b04c 100644 --- a/etc/doc/PROTOCOL.md +++ b/etc/doc/PROTOCOL.md @@ -400,3 +400,45 @@ client. #### Changelog - v0.1.9: First public documentation. + +### Server Version Notification + +The server will send the `$/coq/serverVersion` notification to inform +the client about `coq-lsp` version specific info. + +The parameters are: +```typescript +export interface CoqServerVersion { + coq: string; + ocaml: string; + coq_lsp: string; +} +``` + +#### Changelog + +- v0.1.9: First public documentation. + +### Server Status Notification + +The server will send the `$/coq/serverStatus` notification to inform +the client of checking status (start / end checking file) + +The parameters are: +```typescript + +export interface CoqBusyStatus { + status: "Busy"; + modname: string; +} + +export interface CoqIdleStatus { + status: "Idle" | "Stopped"; +} + +export type CoqServerStatus = CoqBusyStatus | CoqIdleStatus; +``` + +#### Changelog + +- v0.1.9: First public documentation. diff --git a/etc/doc/USER_MANUAL.md b/etc/doc/USER_MANUAL.md index ca32ea31..bed0f86d 100644 --- a/etc/doc/USER_MANUAL.md +++ b/etc/doc/USER_MANUAL.md @@ -39,10 +39,15 @@ facilities. In VSCode, these settings can be usually displayed in the disables some useful features such as `documentSymbol` as they can only be implemented by checking the full file. - This mode provides the `check_on_scroll` option, which improves + This mode can use the `check_on_scroll` option, which improves latency by telling `coq-lsp` to check eagerly what is on view on user's screen. +Users can change between on-demand/continuous mode by clicking on the +"Coq language status" item in the bottom right corner for VSCode. We +recommend pinning the language status item to see server status in +real-time. + ### Goal display By default, `coq-lsp` will follow cursor and show goals at cursor diff --git a/etc/img/on_demand.gif b/etc/img/on_demand.gif new file mode 100644 index 00000000..8ed14f48 Binary files /dev/null and b/etc/img/on_demand.gif differ diff --git a/fleche/config.ml b/fleche/config.ml index e8ee723e..2ad0b302 100644 --- a/fleche/config.ml +++ b/fleche/config.ml @@ -52,6 +52,8 @@ type t = (** Experimental setting to check document lazily *) ; send_diags_extra_data : bool [@default false] (** Send extra diagnostic data on the `data` diagnostic field. *) + ; send_serverStatus : bool [@default true] + (** Send server status client notification to the client *) } let default = @@ -75,6 +77,7 @@ let default = ; send_diags = true ; check_only_on_request = false ; send_diags_extra_data = false + ; send_serverStatus = true } let v = ref default diff --git a/fleche/io.ml b/fleche/io.ml index 0a4c34f1..1f376f2b 100644 --- a/fleche/io.ml +++ b/fleche/io.ml @@ -19,6 +19,8 @@ module CallBack = struct ; fileProgress : uri:Lang.LUri.File.t -> version:int -> Progress.Info.t list -> unit ; perfData : uri:Lang.LUri.File.t -> version:int -> Perf.t -> unit + ; serverVersion : ServerInfo.Version.t -> unit + ; serverStatus : ServerInfo.Status.t -> unit } let default = @@ -27,6 +29,8 @@ module CallBack = struct ; diagnostics = (fun ~uri:_ ~version:_ _ -> ()) ; fileProgress = (fun ~uri:_ ~version:_ _ -> ()) ; perfData = (fun ~uri:_ ~version:_ _ -> ()) + ; serverVersion = (fun _ -> ()) + ; serverStatus = (fun _ -> ()) } let cb = ref default @@ -52,4 +56,6 @@ module Report = struct io.CallBack.fileProgress ~uri ~version d let perfData ~io ~uri ~version pd = io.CallBack.perfData ~uri ~version pd + let serverVersion ~io vi = io.CallBack.serverVersion vi + let serverStatus ~io st = io.CallBack.serverStatus st end diff --git a/fleche/io.mli b/fleche/io.mli index fefc30ee..822c3710 100644 --- a/fleche/io.mli +++ b/fleche/io.mli @@ -23,6 +23,8 @@ module CallBack : sig ; fileProgress : uri:Lang.LUri.File.t -> version:int -> Progress.Info.t list -> unit ; perfData : uri:Lang.LUri.File.t -> version:int -> Perf.t -> unit + ; serverVersion : ServerInfo.Version.t -> unit + ; serverStatus : ServerInfo.Status.t -> unit } val set : t -> unit @@ -56,4 +58,7 @@ module Report : sig val perfData : io:CallBack.t -> uri:Lang.LUri.File.t -> version:int -> Perf.t -> unit + + val serverVersion : io:CallBack.t -> ServerInfo.Version.t -> unit + val serverStatus : io:CallBack.t -> ServerInfo.Status.t -> unit end diff --git a/fleche/serverInfo.ml b/fleche/serverInfo.ml new file mode 100644 index 00000000..85c8b8c4 --- /dev/null +++ b/fleche/serverInfo.ml @@ -0,0 +1,21 @@ +(************************************************************************) +(* Coq Language Server Protocol *) +(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) +(* Copyright 2019-202r Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Written by: Emilio J. Gallego Arias *) +(************************************************************************) + +module Version = struct + type t = + { coq : string + ; ocaml : string + ; coq_lsp : string + } +end + +module Status = struct + type t = + | Stopped + | Idle of string (* memory use *) + | Running of string (* modname *) +end diff --git a/fleche/theory.ml b/fleche/theory.ml index 2c25f7ef..1c79e714 100644 --- a/fleche/theory.ml +++ b/fleche/theory.ml @@ -244,8 +244,17 @@ end = struct pending := pend_pop !pending; None | (None | Some _) as tgt -> + let uri_short = + Lang.LUri.File.to_string_file uri |> Filename.basename + in let target = Option.default Doc.Target.End tgt in + Io.Report.serverStatus ~io (ServerInfo.Status.Running uri_short); let doc = Doc.check ~io ~token ~target ~doc:handle.doc () in + let mem = + Format.asprintf "%a" Stats.pp_words + (Gc.((quick_stat ()).heap_words) |> Float.of_int) + in + Io.Report.serverStatus ~io (ServerInfo.Status.Idle mem); let requests = Handle.update_doc_info ~handle ~doc in if Doc.Completion.is_completed doc.completed then Register.Completed.fire ~io ~token ~doc; diff --git a/lsp/base.ml b/lsp/base.ml index fb628880..4a84481e 100644 --- a/lsp/base.ml +++ b/lsp/base.ml @@ -138,6 +138,9 @@ module Message = struct | Notification n -> Notification.to_yojson n | Request r -> Request.to_yojson r | Response r -> Response.to_yojson r + + let notification n = Notification n + let response r = Response r end module ProgressToken : sig diff --git a/lsp/base.mli b/lsp/base.mli index e8570f57..3643ac11 100644 --- a/lsp/base.mli +++ b/lsp/base.mli @@ -72,6 +72,9 @@ module Message : sig | Request of Request.t | Response of Response.t [@@deriving yojson] + + val notification : Notification.t -> t + val response : Response.t -> t end (** Build request *) diff --git a/lsp/jFleche.ml b/lsp/jFleche.ml index cb8bf70f..7df22a2f 100644 --- a/lsp/jFleche.ml +++ b/lsp/jFleche.ml @@ -64,7 +64,7 @@ let mk_progress ~uri ~version processing = FileProgress.to_yojson { FileProgress.textDocument; processing } |> Yojson.Safe.Util.to_assoc in - Base.Notification.(make ~method_:"$/coq/fileProgress" ~params () |> to_yojson) + Base.Notification.make ~method_:"$/coq/fileProgress" ~params () module Message = struct type 'a t = @@ -141,4 +141,22 @@ let mk_perf ~uri ~version perf = DocumentPerfData.( to_yojson { textDocument; summary; timings } |> Yojson.Safe.Util.to_assoc) in - Base.Notification.(make ~method_:"$/coq/filePerfData" ~params () |> to_yojson) + Base.Notification.make ~method_:"$/coq/filePerfData" ~params () + +module ServerVersion = struct + type t = [%import: Fleche.ServerInfo.Version.t] [@@deriving yojson] +end + +let mk_serverVersion vi = + let params = ServerVersion.to_yojson vi |> Yojson.Safe.Util.to_assoc in + Base.Notification.make ~method_:"$/coq/serverVersion" ~params () + +let mk_serverStatus (st : Fleche.ServerInfo.Status.t) = + let params = + match st with + | Stopped -> [ ("status", `String "Stopped") ] + | Idle mem -> [ ("status", `String "Idle"); ("mem", `String mem) ] + | Running modname -> + [ ("status", `String "Busy"); ("modname", `String modname) ] + in + Base.Notification.make ~method_:"$/coq/serverStatus" ~params () diff --git a/lsp/jFleche.mli b/lsp/jFleche.mli index ba99218a..57a5091b 100644 --- a/lsp/jFleche.mli +++ b/lsp/jFleche.mli @@ -28,7 +28,7 @@ val mk_progress : uri:Lang.LUri.File.t -> version:int -> Fleche.Progress.Info.t list - -> Yojson.Safe.t + -> Base.Notification.t module FileProgress : sig type t = @@ -99,4 +99,8 @@ module DocumentPerfData : sig end val mk_perf : - uri:Lang.LUri.File.t -> version:int -> Fleche.Perf.t -> Yojson.Safe.t + uri:Lang.LUri.File.t -> version:int -> Fleche.Perf.t -> Base.Notification.t + +(* Server status notifications *) +val mk_serverVersion : Fleche.ServerInfo.Version.t -> Base.Notification.t +val mk_serverStatus : Fleche.ServerInfo.Status.t -> Base.Notification.t diff --git a/lsp/jLang.ml b/lsp/jLang.ml index e7f7f3ca..304b8c66 100644 --- a/lsp/jLang.ml +++ b/lsp/jLang.ml @@ -89,7 +89,7 @@ module Diagnostic = struct _t_to_yojson { range; severity; message; data } end -let mk_diagnostics ~uri ~version ld : Yojson.Safe.t = +let mk_diagnostics ~uri ~version ld : Base.Notification.t = let diags = List.map Diagnostic.to_yojson ld in let uri = Lang.LUri.File.to_string_uri uri in let params = @@ -98,5 +98,4 @@ let mk_diagnostics ~uri ~version ld : Yojson.Safe.t = ; ("diagnostics", `List diags) ] in - Base.Notification.( - make ~method_:"textDocument/publishDiagnostics" ~params () |> to_yojson) + Base.Notification.make ~method_:"textDocument/publishDiagnostics" ~params () diff --git a/lsp/jLang.mli b/lsp/jLang.mli index 73f2df3a..9772fea7 100644 --- a/lsp/jLang.mli +++ b/lsp/jLang.mli @@ -40,4 +40,7 @@ module Diagnostic : sig end val mk_diagnostics : - uri:Lang.LUri.File.t -> version:int -> Lang.Diagnostic.t list -> Yojson.Safe.t + uri:Lang.LUri.File.t + -> version:int + -> Lang.Diagnostic.t list + -> Base.Notification.t diff --git a/petanque/agent.ml b/petanque/agent.ml index 0dabf0cc..dcb846a8 100644 --- a/petanque/agent.ml +++ b/petanque/agent.ml @@ -84,7 +84,16 @@ let io = let diagnostics ~uri:_ ~version:_ _diags = () in let fileProgress ~uri:_ ~version:_ _pinfo = () in let perfData ~uri:_ ~version:_ _perf = () in - { Fleche.Io.CallBack.trace; message; diagnostics; fileProgress; perfData } + let serverVersion _ = () in + let serverStatus _ = () in + { Fleche.Io.CallBack.trace + ; message + ; diagnostics + ; fileProgress + ; perfData + ; serverVersion + ; serverStatus + } let read_raw ~uri = let file = Lang.LUri.File.to_string_file uri in