From 81a61463213da3c1e2508cd747f5ca80a994f4af Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 17 May 2024 03:07:18 +0200 Subject: [PATCH] [fleche] Auto-check documents on scroll when in lazy mode. We introduce a new `coq/viewRange` notification, from client to server, than hints the scheduler about the visible area of the document. Combined with the new lazy checking mode, this provides checking on scroll, a feature inspired from Isabelle IDE. --- CHANGES.md | 5 +++++ controller/lsp_core.ml | 12 ++++++++++++ editor/code/lib/types.ts | 5 +++++ editor/code/package.json | 7 ++++++- editor/code/src/client.ts | 26 ++++++++++++++++++++++++++ editor/code/src/config.ts | 4 ++++ etc/doc/PROTOCOL.md | 12 ++++++++++++ etc/doc/USER_MANUAL.md | 37 ++++++++++++++++++++++++++++++++++--- fleche/theory.ml | 19 ++++++++++++++++++- fleche/theory.mli | 2 ++ lsp/jLang.mli | 16 ++++++++++++++++ 11 files changed, 140 insertions(+), 5 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 71e7c3f5..0a42dc98 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -111,6 +111,7 @@ (@ejgallego, @Alizter, #689, #693) - Better types `coq/perfData` call (@ejgallego @Alizter, #689) - New server option to enable / disable `coq/perfData` (@ejgallego, #689) + - New cleint option to enable / disable `coq/perfData` (@ejgallego, #717) - The `coq-lsp.document` VSCode command will now display the returned JSON data in a new editor (@ejgallego, #701) - New server option to enable / disable `coq/perfData` (@ejgallego, @@ -130,6 +131,10 @@ 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) # coq-lsp 0.1.8.1: Spring fix ----------------------------- diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index 1cbf2714..aa593abb 100644 --- a/controller/lsp_core.ml +++ b/controller/lsp_core.ml @@ -411,6 +411,17 @@ let do_cancel ~ofn ~params = let do_cache_trim () = Nt_cache_trim.notification () +let do_viewRange params = + match List.assoc "range" params |> Lsp.JLang.Diagnostic.Range.of_yojson with + | Ok range -> + let { Lsp.JLang.Diagnostic.Range.end_ = { line; character }; _ } = range in + let message = Format.asprintf "l: %d c:%d" line character in + LIO.trace "viewRange" message; + let uri = Helpers.get_uri params in + Fleche.Theory.Check.set_scheduler_hint ~uri ~point:(line, character); + () + | Error err -> LIO.trace "viewRange" ("error in parsing notification: " ^ err) + let do_changeConfiguration params = let message = "didChangeReceived" in let () = LIO.(logMessage ~lvl:Lvl.Info ~message) in @@ -496,6 +507,7 @@ let dispatch_notification ~io ~ofn ~token ~state ~method_ ~params : unit = | "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 diff --git a/editor/code/lib/types.ts b/editor/code/lib/types.ts index f4165b36..f5065a9b 100644 --- a/editor/code/lib/types.ts +++ b/editor/code/lib/types.ts @@ -179,3 +179,8 @@ export type PerfMessagePayload = PerfUpdate | PerfReset; export interface PerfMessageEvent extends MessageEvent { data: PerfMessagePayload; } + +export interface ViewRangeParams { + textDocument: VersionedTextDocumentIdentifier; + range: Range; +} diff --git a/editor/code/package.json b/editor/code/package.json index e69b8b1c..45901146 100644 --- a/editor/code/package.json +++ b/editor/code/package.json @@ -283,7 +283,12 @@ "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 option is experimental and not recommended for use yet; we expose it only for testing and further development." + "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." + }, + "coq-lsp.check_on_scroll": { + "type": "boolean", + "default": false, + "description": "When in lazy mode, check files on scroll. Note that this feature is experimental." } } }, diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts index ecf292e9..4e665912 100644 --- a/editor/code/src/client.ts +++ b/editor/code/src/client.ts @@ -14,6 +14,7 @@ import { Disposable, languages, Uri, + TextEditorVisibleRangesChangeEvent, } from "vscode"; import * as vscode from "vscode"; @@ -37,6 +38,7 @@ import { GoalAnswer, PpString, DocumentPerfParams, + ViewRangeParams, } from "../lib/types"; import { CoqLspClientConfig, CoqLspServerConfig, CoqSelector } from "./config"; @@ -45,6 +47,7 @@ import { FileProgressManager } from "./progress"; import { coqPerfData, PerfDataView } from "./perf"; import { sentenceNext, sentenceBack } from "./edit"; import { HeatMap, HeatMapConfig } from "./heatmap"; +import { debounce, throttle } from "throttle-debounce"; // Convert perf data to VSCode format function toVsCodePerf( @@ -314,6 +317,29 @@ export function activateCoqLSP( context.subscriptions.push(goalsHook); + const viewRangeNotification = new NotificationType( + "coq/viewRange" + ); + + let viewRangeHook = window.onDidChangeTextEditorVisibleRanges( + throttle(400, (evt: TextEditorVisibleRangesChangeEvent) => { + if ( + config.check_on_scroll && + languages.match(CoqSelector.local, evt.textEditor.document) > 0 && + evt.visibleRanges[0] + ) { + let uri = evt.textEditor.document.uri.toString(); + let version = evt.textEditor.document.version; + let textDocument = { uri, version }; + let range = client.code2ProtocolConverter.asRange(evt.visibleRanges[0]); + let params: ViewRangeParams = { textDocument, range }; + client.sendNotification(viewRangeNotification, params); + } + }) + ); + + context.subscriptions.push(viewRangeHook); + // Heatmap setup heatMap = new HeatMap( workspace.getConfiguration("coq-lsp").get("heatmap") as HeatMapConfig diff --git a/editor/code/src/config.ts b/editor/code/src/config.ts index 68614e57..a7437ee9 100644 --- a/editor/code/src/config.ts +++ b/editor/code/src/config.ts @@ -14,6 +14,7 @@ export interface CoqLspServerConfig { show_stats_on_hover: boolean; show_loc_info_on_hover: boolean; check_only_on_request: boolean; + send_perf_data: boolean; } export namespace CoqLspServerConfig { @@ -35,6 +36,7 @@ export namespace CoqLspServerConfig { show_stats_on_hover: wsConfig.show_stats_on_hover, show_loc_info_on_hover: wsConfig.show_loc_info_on_hover, check_only_on_request: wsConfig.check_only_on_request, + send_perf_data: wsConfig.send_perf_data, }; } } @@ -49,6 +51,7 @@ export enum ShowGoalsOnCursorChange { export interface CoqLspClientConfig { show_goals_on: ShowGoalsOnCursorChange; pp_format: "Pp" | "Str"; + check_on_scroll: boolean; } function pp_type_to_pp_format(pp_type: 0 | 1 | 2): "Pp" | "Str" { @@ -67,6 +70,7 @@ export namespace CoqLspClientConfig { let obj: CoqLspClientConfig = { show_goals_on: wsConfig.show_goals_on, pp_format: pp_type_to_pp_format(wsConfig.pp_type), + check_on_scroll: wsConfig.check_on_scroll, }; return obj; } diff --git a/etc/doc/PROTOCOL.md b/etc/doc/PROTOCOL.md index 1b933a80..c3e303b4 100644 --- a/etc/doc/PROTOCOL.md +++ b/etc/doc/PROTOCOL.md @@ -354,6 +354,18 @@ const coqPerfData : NotificationType> The `coq/trimCaches` notification from client to server tells the server to free memory. It has no parameters. +### Viewport notification + +The `coq/viewRange` notification from client to server tells the +server the visible range of the user. + +```typescript +interface ViewRangeParams { + textDocument: VersionedTextDocumentIdentifier; + range: Range; +} +``` + ### Did Change Configuration and Server Configuration parameters The server will listen to the `workspace/didChangeConfiguration` diff --git a/etc/doc/USER_MANUAL.md b/etc/doc/USER_MANUAL.md index 517f1bae..c51f5bdc 100644 --- a/etc/doc/USER_MANUAL.md +++ b/etc/doc/USER_MANUAL.md @@ -24,9 +24,37 @@ facilities. In VSCode, these settings can be usually displayed in the ## Key features: +### Continuous vs on-demand mode + +`coq-lsp` offers two checking modes: + +- continuous checking [default]: `coq-lsp` will check all your open + documents eagerly. This is best when working with powerful machines + to minimize latency. When using OCaml 4.x, `coq-lsp` uses the + `memprof-limits` library to interrupt Coq and stay responsive. + +- on-demand checking [set the `check_only_on_request` option]: In this + mode, `coq-lsp` will stay idle and only compute information that is + demanded, for example, when the user asks for goals. This mode + 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 + latency by telling `coq-lsp` to check eagerly what is on view on + user's screen. + +### Goal display + +By default, `coq-lsp` will follow cursor and show goals at cursor +position. This can be tweaked in options. There are commands to move +one Coq sentence forward / backwards. + ### Incremental proof edition -`coq-lsp` will recognize blocks of the form: +Once you have setup your basic proof style, you may want to work with +`coq-lsp` in a way that is friendly to incremental checking. + +For example, `coq-lsp` will recognize blocks of the form: ```coq Lemma foo : T. Proof. @@ -34,7 +62,8 @@ Proof. Qed. ``` -and will allow you to edit inside the `Proof.` `Qed.` block without rechecing what is outside. +and will allow you to edit inside the `Proof.` `Qed.` block without +re-checking what is outside. ### Error recovery @@ -42,7 +71,9 @@ and will allow you to edit inside the `Proof.` `Qed.` block without rechecing wh continue document edition later on. For example, it is not necessary to put `Admitted` in proofs that are -not fully completed. +not fully completed. Also, you can work with bullets and `coq-lsp` +will automatically admit unfinished ones, so you can follow the +natural proof structure. ## Settings diff --git a/fleche/theory.ml b/fleche/theory.ml index 29f4f827..2c25f7ef 100644 --- a/fleche/theory.ml +++ b/fleche/theory.ml @@ -194,6 +194,8 @@ module Check : sig val maybe_check : io:Io.CallBack.t -> token:Coq.Limits.Token.t -> (Int.Set.t * Doc.t) option + + val set_scheduler_hint : uri:Lang.LUri.File.t -> point:int * int -> unit end = struct let pending = ref [] @@ -214,9 +216,18 @@ end = struct | None -> pend_try f tt | Some r -> Some r) + let hint : (int * int) option ref = ref None + let get_check_target pt_requests = let target_of_pt_handle (_, (l, c)) = Doc.Target.Position (l, c) in - Option.map target_of_pt_handle (List.nth_opt pt_requests 0) + match Option.map target_of_pt_handle (List.nth_opt pt_requests 0) with + | None -> + Option.map + (fun (l, c) -> + hint := None; + Doc.Target.Position (l, c)) + !hint + | Some t -> Some t (* Notification handling; reply is optional / asynchronous *) let check ~io ~token ~uri = @@ -255,6 +266,12 @@ end = struct let deschedule ~uri = pending := CList.remove Lang.LUri.File.equal uri !pending + + let set_scheduler_hint ~uri ~point = + if CList.is_empty !pending then + let () = hint := Some point in + schedule ~uri (* if the hint is set we wanna override it *) + else if not (Option.is_empty !hint) then hint := Some point end let create ~io ~token ~env ~uri ~raw ~version = diff --git a/fleche/theory.mli b/fleche/theory.mli index 33bbb896..e20c2cf7 100644 --- a/fleche/theory.mli +++ b/fleche/theory.mli @@ -21,6 +21,8 @@ module Check : sig progress and diagnostics notifications using output function [ofn]. *) val maybe_check : io:Io.CallBack.t -> token:Coq.Limits.Token.t -> (Int.Set.t * Doc.t) option + + val set_scheduler_hint : uri:Lang.LUri.File.t -> point:int * int -> unit end (** Create a document inside a theory *) diff --git a/lsp/jLang.mli b/lsp/jLang.mli index 0ddf3d1a..73f2df3a 100644 --- a/lsp/jLang.mli +++ b/lsp/jLang.mli @@ -21,6 +21,22 @@ end module Diagnostic : sig type t = Lang.Diagnostic.t [@@deriving to_yojson] + + module Point : sig + type t = + { line : int + ; character : int + } + [@@deriving yojson] + end + + module Range : sig + type t = + { start : Point.t + ; end_ : Point.t [@key "end"] + } + [@@deriving yojson] + end end val mk_diagnostics :