diff --git a/CHANGES.md b/CHANGES.md index ff9f61f99..26d8af6f7 100644 --- a/CHANGES.md +++ b/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_... ---------------------------------------------------- diff --git a/controller/dune b/controller/dune index 5a9170eda..2a470ba33 100644 --- a/controller/dune +++ b/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) diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index 627e67682..2e63d5a72 100644 --- a/controller/lsp_core.ml +++ b/controller/lsp_core.ml @@ -427,6 +427,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 *) @@ -481,6 +532,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 *) @@ -529,7 +581,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 +604,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 diff --git a/editor/code/lib/types.ts b/editor/code/lib/types.ts index 1e196f070..76c98ac7a 100644 --- a/editor/code/lib/types.ts +++ b/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; +} diff --git a/editor/code/package.json b/editor/code/package.json index d4ccf71ee..a5278d669 100644 --- a/editor/code/package.json +++ b/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": [ diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts index abc3f27e1..d8dbf3522 100644 --- a/editor/code/src/client.ts +++ b/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((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 diff --git a/editor/code/src/petanque.ts b/editor/code/src/petanque.ts new file mode 100644 index 000000000..87d5b1a13 --- /dev/null +++ b/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( + "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((thm_user) => { + let thm = thm_user ?? "petanque_debug"; + let params: PetStartParams = { uri, pre_commands, thm }; + return Promise.resolve(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("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); + }); +}; diff --git a/examples/petanque.v b/examples/petanque.v new file mode 100644 index 000000000..8616a823f --- /dev/null +++ b/examples/petanque.v @@ -0,0 +1,2 @@ +Theorem petanque_debug : True. +Proof. now auto. Qed. diff --git a/fleche/theory.ml b/fleche/theory.ml index d4234974e..6f573eafd 100644 --- a/fleche/theory.ml +++ b/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) diff --git a/fleche/theory.mli b/fleche/theory.mli index e20c2cf78..2c037158e 100644 --- a/fleche/theory.mli +++ b/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 diff --git a/petanque/README.md b/petanque/README.md index 43d149e11..cdb470562 100644 --- a/petanque/README.md +++ b/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: ``` diff --git a/petanque/json_shell/interp.ml b/petanque/json_shell/interp.ml index cc6517a3a..94f134548 100644 --- a/petanque/json_shell/interp.ml +++ b/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