Merge pull request #778 from ejgallego/petanque_lsp

[lsp] [petanque] Allow access to `petanque` protocol from the lsp server

CHANGES.md

@@ -56,6 +56,8 @@
    #550)
  - [petanque] Allow memoization control on `petanque/run` via a new
    parameter `memo` (@ejgallego, #780)
+ - [lsp] [petanque] Allow acces to `petanque` protocol from the lsp
+   server (@ejgallego, #778)
 
 # coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_...
 ----------------------------------------------------

controller/dune

@@ -1,7 +1,7 @@
 (library
  (name controller)
  (modules :standard \ coq_lsp)
- (libraries coq fleche lsp dune-build-info))
+ (libraries coq fleche petanque petanque_json lsp dune-build-info))
 
 (executable
  (name coq_lsp)

controller/lsp_core.ml

@@ -427,6 +427,43 @@ let do_changeConfiguration ~io params =
   Rq_init.do_settings settings;
   ()
 
+(* EJGA: Note that our current configuration allow petanque calls to be
+   interrupted, this can become an issue with LSP. For now, clients must choose
+   a trade-off (we could disable interruption on petanque call, but that brings
+   other downsides)
+
+   The only real solution is to wait for OCaml 5.x support, so we can server
+   read-only queries without interrupting the main Coq thread. *)
+let petanque_handle ~token (module R : Petanque_json.Protocol.Request.S) ~params
+    =
+  let open Petanque_json in
+  match Interp.do_request (module R) ~params with
+  | Interp.Action.Now handler -> Rq.Action.now (handler ~token)
+  | Interp.Action.Doc { uri; handler } ->
+    (* Request document execution if not ready *)
+    let postpone = true in
+    Rq.Action.(Data (DocRequest { uri; postpone; handler }))
+
+let do_petanque ~token method_ params =
+  (* For now we do a manual brigde *)
+  let open Petanque_json.Protocol in
+  match method_ with
+  | s when String.equal Start.method_ s ->
+    petanque_handle ~token (module Start) ~params
+  | s when String.equal RunTac.method_ s ->
+    petanque_handle ~token (module RunTac) ~params
+  | s when String.equal Goals.method_ s ->
+    petanque_handle ~token (module Goals) ~params
+  | s when String.equal Premises.method_ s ->
+    petanque_handle ~token (module Premises) ~params
+  | _ ->
+    (* EJGA: should we allow this system to compose better with other LSP
+       extensions? *)
+    (* JSON-RPC method not found *)
+    let code = -32601 in
+    let message = "method not found" in
+    Rq.Action.error (code, message)
+
 (***********************************************************************)
 
 (** LSP Init routine *)
@@ -529,7 +566,7 @@ let dispatch_state_notification ~io ~ofn ~token ~state ~method_ ~params :
     dispatch_notification ~io ~ofn ~token ~state ~method_ ~params;
     state
 
-let dispatch_request ~method_ ~params : Rq.Action.t =
+let dispatch_request ~token ~method_ ~params : Rq.Action.t =
   match method_ with
   (* Lifecyle *)
   | "initialize" ->
@@ -552,15 +589,14 @@ let dispatch_request ~method_ ~params : Rq.Action.t =
   | "coq/getDocument" -> do_document ~params
   (* Petanque embedding *)
   | msg when Coq.Compat.Ocaml_413.String.starts_with ~prefix:"petanque/" msg ->
-    L.trace "delegating to petanque [wip]" "%s" msg;
-    Rq.Action.error (-32601, "method not found")
+    do_petanque msg ~token params
   (* Generic handler *)
   | msg ->
     L.trace "no_handler" "%s" msg;
     Rq.Action.error (-32601, "method not found")
 
 let dispatch_request ~ofn_rq ~token ~id ~method_ ~params =
-  dispatch_request ~method_ ~params |> Rq.serve ~ofn_rq ~token ~id
+  dispatch_request ~token ~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

editor/code/lib/types.ts

@@ -208,3 +208,15 @@ export interface CoqStoppedStatus {
 }
 
 export type CoqServerStatus = CoqBusyStatus | CoqIdleStatus | CoqStoppedStatus;
+
+// Petanque types, canonical source agent.mli
+export interface PetStartParams {
+  uri: string;
+  pre_commands: string | null;
+  thm: string;
+}
+
+export interface PetRunParams {
+  st: number;
+  tac: string;
+}

editor/code/package.json

@@ -132,6 +132,14 @@
       {
         "command": "coq-lsp.heatmap.toggle",
         "title": "Coq LSP: Toggle heatmap"
+      },
+      {
+        "command": "coq-lsp.petanque.start",
+        "title": "Coq LSP: Start a petanque session for theorem (Coq developer-only command)"
+      },
+      {
+        "command": "coq-lsp.petanque.run",
+        "title": "Coq LSP: Run a tactic over a petanque session (Coq developer-only command)"
       }
     ],
     "keybindings": [

editor/code/src/client.ts

@@ -15,6 +15,7 @@ import {
   languages,
   Uri,
   TextEditorVisibleRangesChangeEvent,
+  InputBoxOptions,
 } from "vscode";
 
 import * as vscode from "vscode";
@@ -54,6 +55,7 @@ import { FileProgressManager } from "./progress";
 import { coqPerfData, PerfDataView } from "./perf";
 import { sentenceNext, sentencePrevious } from "./edit";
 import { HeatMap, HeatMapConfig } from "./heatmap";
+import { petanqueStart, petanqueRun, petSetClient } from "./petanque";
 import { debounce, throttle } from "throttle-debounce";
 
 // Convert perf data to VSCode format
@@ -154,6 +156,7 @@ export function activateCoqLSP(
     );
     context.subscriptions.push(disposable);
   }
+
   function checkForVSCoq() {
     let vscoq =
       extensions.getExtension("maximedenes.vscoq") ||
@@ -216,6 +219,7 @@ export function activateCoqLSP(
 
     let cP = new Promise<BaseLanguageClient>((resolve) => {
       client = clientFactory(context, clientOptions, wsConfig);
+      petSetClient(client);
       fileProgress = new FileProgressManager(client);
       perfDataHook = client.onNotification(coqPerfData, (data) => {
         perfDataView.update(data);
@@ -519,6 +523,9 @@ export function activateCoqLSP(
 
   coqEditorCommand("heatmap.toggle", heatMapToggle);
 
+  coqEditorCommand("petanque.start", petanqueStart);
+  coqEditorCommand("petanque.run", petanqueRun);
+
   createEnableButton();
 
   // Fix for bug #750

editor/code/src/petanque.ts

@@ -0,0 +1,60 @@
+import { window, InputBoxOptions, TextEditor } from "vscode";
+import { BaseLanguageClient, RequestType } from "vscode-languageclient";
+import { PetRunParams, PetStartParams } from "../lib/types";
+
+const petStartReq = new RequestType<PetStartParams, number, void>(
+  "petanque/start"
+);
+let client: BaseLanguageClient;
+
+export function petSetClient(newClient: BaseLanguageClient) {
+  client = newClient;
+}
+
+export const petanqueStart = (editor: TextEditor) => {
+  let uri = editor.document.uri.toString();
+  let pre_commands = null;
+
+  // Imput theorem name
+  let inputOptions: InputBoxOptions = {
+    title: "Petanque Start",
+    prompt: "Name of the theorem to start a session ",
+  };
+  window
+    .showInputBox(inputOptions)
+    .then<PetStartParams>((thm_user) => {
+      let thm = thm_user ?? "petanque_debug";
+      let params: PetStartParams = { uri, pre_commands, thm };
+      return Promise.resolve<PetStartParams>(params);
+    })
+    .then((params: PetStartParams) => {
+      client
+        .sendRequest(petStartReq, params)
+        .then((id) =>
+          window.setStatusBarMessage(`petanque/start succeed ${id}`, 5000)
+        )
+        .catch((error) => {
+          let err_message = error.toString();
+          console.log(`error in save: ${err_message}`);
+          window.showErrorMessage(err_message);
+        });
+    });
+};
+
+const petRunReq = new RequestType<PetRunParams, any, void>("petanque/run");
+
+export const petanqueRun = (editor: TextEditor) => {
+  // XXX Read from user
+  let params: PetRunParams = { st: 1, tac: "idtac." };
+  client
+    .sendRequest(petRunReq, params)
+    .then((answer: any) => {
+      let res = JSON.stringify(answer);
+      window.setStatusBarMessage(`petanque/run succeed ${res}`, 5000);
+    })
+    .catch((error) => {
+      let err_message = error.toString();
+      console.log(`error in save: ${err_message}`);
+      window.showErrorMessage(err_message);
+    });
+};

examples/petanque.v

@@ -0,0 +1,2 @@
+Theorem petanque_debug : True.
+Proof. now auto. Qed.

fleche/theory.ml

@@ -405,3 +405,7 @@ module Request = struct
     | FullDoc -> Handle.remove_cp_request ~uri ~id
     | PosInDoc { point; _ } -> Handle.remove_pt_request ~uri ~id ~point
 end
+
+(* xxx to remove *)
+let find_doc ~uri =
+  Handle._find_opt ~uri |> Option.map (fun { Handle.doc; _ } -> doc)

fleche/theory.mli

@@ -93,3 +93,6 @@ module Register : sig
     val add : t -> unit
   end
 end
+
+(* XXX this is temporal for petanque, will fix before merge *)
+val find_doc : uri:Lang.LUri.File.t -> Doc.t option

petanque/README.md

@@ -50,11 +50,18 @@ See the contributing guide for instructions on how to do the last.
 
 ## Running `petanque` JSON shell
 
-You can use `petanque` in 2 different ways:
+You can use `petanque` in 3 different ways:
 
-- call the API directly from your OCaml program
+- call the API using JSON-RPC directly in `coq-lsp`, over the LSP
+  protocol
 - use the provided `pet` and `pet-server` JSON-RPC shells, usually
-  with a library such as Pytanque.
+  with a library such as Pytanque
+- call the API directly from your OCaml program
+
+See `agent.mli` for an overview of the API. The
+`petanque/setWorkspace` method is only available in the `pet` and
+`pet-server` shells; when `petanque` is used from LSP, the workspace
+needs to be set using LSP in the usual way.
 
 To execute the `pet` JSON-RPC shell do:
 ```

petanque/agent.ml

@@ -101,17 +101,12 @@ let protect_to_result (r : _ Coq.Protect.E.t) : (_, _) Result.t =
     Error (Error.Anomaly (Pp.string_of_ppcmds msg))
   | { r = Completed (Ok r); feedback = _ } -> Ok r
 
-let fn = ref (fun ~token:_ _uri -> Error (Error.System "No handler for fn"))
-
-let start ~token ~uri ?pre_commands ~thm () =
-  match !fn ~token uri with
-  | Ok doc ->
-    let open Coq.Compat.Result.O in
-    let* node = find_thm ~doc ~thm in
-    (* Usually single shot, so we don't memoize *)
-    let memo = false in
-    execute_precommands ~token ~memo ~pre_commands ~node |> protect_to_result
-  | Error err -> Error err
+let start ~token ~doc ?pre_commands ~thm () =
+  let open Coq.Compat.Result.O in
+  let* node = find_thm ~doc ~thm in
+  (* Usually single shot, so we don't memoize *)
+  let memo = false in
+  execute_precommands ~token ~memo ~pre_commands ~node |> protect_to_result
 
 let proof_finished { Coq.Goals.goals; stack; shelf; given_up; _ } =
   List.for_all CList.is_empty [ goals; shelf; given_up ] && CList.is_empty stack

petanque/agent.mli

@@ -40,16 +40,34 @@ module Run_result : sig
     | Current_state of 'a
 end
 
-val fn : (token:Coq.Limits.Token.t -> Lang.LUri.File.t -> Fleche.Doc.t R.t) ref
+(** Protocol notes:
 
-(** [start ~token ~fn ~uri ~pre_commands ~thm] start a new proof for theorem
-    [thm] in file [uri] under [fn]. [token] can be used to interrupt the
-    computation. Returns the proof state or error otherwise. [pre_commands] is a
-    string of dot-separated Coq commands that will be executed before the proof
-    starts. *)
+    The idea is that the types of the functions here have a direct translation
+    to the JSON-RPC (or any other) protocol.
+
+    Thus, types here correspond to types in the wire, except for cases where the
+    protocol layer performs an implicit mapping on types.
+
+    So far, the mappings are:
+
+    - [uri] <-> [Doc.t]
+    - [int] <-> [State.t]
+
+    The [State.t] mapping is easy to do at the protocol level with a simple
+    mapping, however [uri -> Doc.t] may need to yield to the document manager to
+    build the corresponding [doc]. This is very convenient for users, but
+    introduces a little bit more machinery.
+
+    We could imagine a future where [State.t] need to be managed asynchronously,
+    then the same approach that we use for [Doc.t] could happen. *)
+
+(** [start ~token ~doc ~pre_commands ~thm] start a new proof for theorem [thm]
+    in file [uri] under [fn]. [token] can be used to interrupt the computation.
+    Returns the proof state or error otherwise. [pre_commands] is a string of
+    dot-separated Coq commands that will be executed before the proof starts. *)
 val start :
      token:Coq.Limits.Token.t
-  -> uri:Lang.LUri.File.t
+  -> doc:Fleche.Doc.t
   -> ?pre_commands:string
   -> thm:string
   -> unit