[lsp] [petanque] Allow access to petanque protocol from the lsp ser…

…ver.

This will be very useful for quite a few users, in particular those
willing to interact with Coq from an editor context.

Things integrate pretty well, however we can still improve the
codebase a bit; thus, this PR is wip, but usable for testing.

Comments / todos:

- note the lack of uniformity w.r.t. the cancellation token and
  Rq.serve, in particular `Rq.Immediate` and `Rq.query` with result
  `Now` should do the same.

- the integration of start should be a bit better so we can use the
  `doc` provided in the handler callback.

CHANGES.md

@@ -54,6 +54,8 @@
    `Qed` time (@ejgallego, #773)
  - [fleche] Support meta-command `Abort All` (@ejgallego, #774, fixes
    #550)
+ - [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

@@ -428,6 +428,57 @@ let do_changeConfiguration ~io params =
   Rq_init.do_settings settings;
   ()
 
+(* Petanque bridge *)
+let petanque_init () =
+  let fn ~token:_ uri =
+    match Fleche.Theory.find_doc ~uri with
+    | Some doc -> Ok doc
+    | None ->
+      let msg = Format.asprintf "lsp_core: document not found" in
+      Error (Petanque.Agent.Error.System msg)
+  in
+  Petanque.Agent.fn := fn
+
+let petanque_handle_doc (module S : Petanque_json.Protocol.Request.S) ~params =
+  (* XXX fixme: doc is now retrieved by petanque callback, but we could use
+     this *)
+  let handler ~token ~doc:_ =
+    Petanque_json.Interp.do_request ~token (module S) ~params
+  in
+  (* XXX: The below wouldn't work due to params having uri in an incorrect
+     format, do_document_request expects the uri to be in the textDocument
+     field *)
+  let textDocument = string_field "uri" params in
+  let params =
+    ("textDocument", `Assoc [ ("uri", `String textDocument) ]) :: params
+  in
+  do_document_request ~postpone:true ~params ~handler
+
+let petanque_handle_now ~token (module S : Petanque_json.Protocol.Request.S)
+    ~params =
+  Rq.Action.now (Petanque_json.Interp.do_request ~token (module S) ~params)
+
+(* XXX: Deduplicate with Petanque_json.Protocol. *)
+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_doc (module Start) ~params
+  | s when String.equal RunTac.method_ s ->
+    petanque_handle_now ~token (module RunTac) ~params
+  | s when String.equal Goals.method_ s ->
+    petanque_handle_now ~token (module Goals) ~params
+  | s when String.equal Premises.method_ s ->
+    petanque_handle_now ~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 *)
@@ -484,6 +535,7 @@ let lsp_init_process ~ofn ~io ~cmdline ~debug msg : Init_effect.t =
         dirs
     in
     List.iter (log_workspace ~io) workspaces;
+    petanque_init ();
     Success workspaces
   | LSP.Message.Request { id; _ } ->
     (* per spec *)
@@ -532,7 +584,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" ->
@@ -555,15 +607,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/json_shell/interp.ml

@@ -2,44 +2,47 @@ open Protocol
 open Protocol_shell
 module A = Petanque.Agent
 
-let do_request ~token (module R : Request.S) ~id ~params =
+let do_request ~token (module R : Protocol.Request.S) ~params =
   match R.Handler.Params.of_yojson (`Assoc params) with
   | Ok params -> (
     match R.Handler.handler ~token params with
-    | Ok result ->
-      let result = R.Handler.Response.to_yojson result in
-      Lsp.Base.Response.mk_ok ~id ~result
+    | Ok result -> Ok (R.Handler.Response.to_yojson result)
     | Error err ->
-      let message = A.Error.to_string err in
-      let code = A.Error.to_code err in
-      Lsp.Base.Response.mk_error ~id ~code ~message)
+      let message = Petanque.Agent.Error.to_string err in
+      let code = Petanque.Agent.Error.to_code err in
+      Error (code, message))
   | Error message ->
     (* JSON-RPC Parse error *)
     let code = -32700 in
-    Lsp.Base.Response.mk_error ~id ~code ~message
+    Error (code, message)
 
-let handle_request ~token ~id ~method_ ~params =
+let handle_request ~token ~method_ ~params =
   match method_ with
   | s when String.equal SetWorkspace.method_ s ->
-    do_request ~token (module SetWorkspace) ~id ~params
+    do_request ~token (module SetWorkspace) ~params
   | s when String.equal Start.method_ s ->
-    do_request ~token (module Start) ~id ~params
+    do_request ~token (module Start) ~params
   | s when String.equal RunTac.method_ s ->
-    do_request ~token (module RunTac) ~id ~params
+    do_request ~token (module RunTac) ~params
   | s when String.equal Goals.method_ s ->
-    do_request ~token (module Goals) ~id ~params
+    do_request ~token (module Goals) ~params
   | s when String.equal Premises.method_ s ->
-    do_request ~token (module Premises) ~id ~params
+    do_request ~token (module Premises) ~params
   | _ ->
     (* JSON-RPC method not found *)
     let code = -32601 in
     let message = "method not found" in
-    Lsp.Base.Response.mk_error ~id ~code ~message
+    Error (code, message)
+
+let request ~token ~id ~method_ ~params =
+  match handle_request ~token ~method_ ~params with
+  | Ok result -> Lsp.Base.Response.mk_ok ~id ~result
+  | Error (code, message) -> Lsp.Base.Response.mk_error ~id ~code ~message
 
 let interp ~token (r : Lsp.Base.Message.t) : Lsp.Base.Message.t option =
   match r with
   | Request { id; method_; params } ->
-    let response = handle_request ~token ~id ~method_ ~params in
+    let response = request ~token ~id ~method_ ~params in
     Some (Lsp.Base.Message.response response)
   | Notification { method_; params = _ } ->
     let message = "unhandled notification: " ^ method_ in