From b99d66fbe9a962e20c72f2ec4cbeae15785ead3e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 30 Sep 2024 12:27:16 +0200 Subject: [PATCH 01/22] [lang] Move `Lang.Diagnostics.Data.t` from a list to name field This fits our use case better. --- CHANGES.md | 2 ++ etc/doc/PROTOCOL.md | 14 ++++++++++++++ fleche/doc.ml | 25 +++++++++++++------------ lang/diagnostic.ml | 17 +++++++++++------ lang/diagnostic.mli | 17 +++++++++++------ lsp/jLang.ml | 7 ++++++- 6 files changed, 57 insertions(+), 25 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index de4884e10..93b4e5603 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -34,6 +34,8 @@ info that is needed is at hand. It could also be tried to set the build target for immediate requests to the view hint, but we should see some motivation for that (@ejgallego, #841) + - [lsp] [diagnostics] (! breaking change) change type of diagnostics + extra data from list to named record (@ejgallego, #843) # coq-lsp 0.2.0: From Green to Blue ----------------------------------- diff --git a/etc/doc/PROTOCOL.md b/etc/doc/PROTOCOL.md index a9d3322b7..6b167e774 100644 --- a/etc/doc/PROTOCOL.md +++ b/etc/doc/PROTOCOL.md @@ -164,6 +164,20 @@ today we offer two kinds of extra information on errors: - range of the full sentence that displayed the error, - if the error was on a Require, information about the library that failed. +As of today, this extra data is passed via member parameters +```typescript +// From `prefix` Require `refs` +type failedRequire = { + prefix ?: qualid + refs : qualid list +} + +type DiagnosticsData = { + sentenceRange ?: Range; + failedRequire ?: FailedRequire +} +``` + ### Goal Display In order to display proof goals and information at point, `coq-lsp` supports the `proof/goals` request, parameters are: diff --git a/fleche/doc.ml b/fleche/doc.ml index fbde2b1ef..4c02c7b2e 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -145,7 +145,7 @@ module Diags : sig (** Build simple diagnostic *) val make : - ?data:Lang.Diagnostic.Data.t list + ?data:Lang.Diagnostic.Data.t -> Lang.Range.t -> Lang.Diagnostic.Severity.t -> Pp.t @@ -175,17 +175,18 @@ end = struct (* ast-dependent error diagnostic generation *) let extra_diagnostics_of_ast stm_range ast = - let stm_range = Lang.Diagnostic.Data.SentenceRange stm_range in - match - Option.bind ast (fun (ast : Node.Ast.t) -> Coq.Ast.Require.extract ast.v) - with - | Some { Coq.Ast.Require.from; mods; _ } -> - let refs = List.map fst mods in - Some - [ stm_range - ; Lang.Diagnostic.Data.FailedRequire { prefix = from; refs } - ] - | _ -> Some [ stm_range ] + let sentenceRange = Some stm_range in + let failedRequire = + match + Option.bind ast (fun (ast : Node.Ast.t) -> + Coq.Ast.Require.extract ast.v) + with + | Some { Coq.Ast.Require.from; mods; _ } -> + let refs = List.map fst mods in + Some [ { Lang.Diagnostic.FailedRequire.prefix = from; refs } ] + | _ -> None + in + Some { Lang.Diagnostic.Data.sentenceRange; failedRequire } let extra_diagnostics_of_ast stm_range ast = if !Config.v.send_diags_extra_data then diff --git a/lang/diagnostic.ml b/lang/diagnostic.ml index 393b1168c..84b307536 100644 --- a/lang/diagnostic.ml +++ b/lang/diagnostic.ml @@ -4,13 +4,18 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) +module FailedRequire = struct + type t = + { prefix : Libnames.qualid option + ; refs : Libnames.qualid list + } +end + module Data = struct type t = - | SentenceRange of Range.t - | FailedRequire of - { prefix : Libnames.qualid option - ; refs : Libnames.qualid list - } + { sentenceRange : Range.t option [@default None] + ; failedRequire : FailedRequire.t list option [@default None] + } end module Severity = struct @@ -27,7 +32,7 @@ type t = { range : Range.t ; severity : Severity.t ; message : Pp.t - ; data : Data.t list option [@default None] + ; data : Data.t option [@default None] } let is_error { severity; _ } = severity = 1 diff --git a/lang/diagnostic.mli b/lang/diagnostic.mli index 220d85470..282d10f6d 100644 --- a/lang/diagnostic.mli +++ b/lang/diagnostic.mli @@ -4,13 +4,18 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) +module FailedRequire : sig + type t = + { prefix : Libnames.qualid option + ; refs : Libnames.qualid list + } +end + module Data : sig type t = - | SentenceRange of Range.t - | FailedRequire of - { prefix : Libnames.qualid option - ; refs : Libnames.qualid list - } + { sentenceRange : Range.t option [@default None] + ; failedRequire : FailedRequire.t list option [@default None] + } end module Severity : sig @@ -29,7 +34,7 @@ type t = { range : Range.t ; severity : Severity.t ; message : Pp.t - ; data : Data.t list option [@default None] + ; data : Data.t option [@default None] } val is_error : t -> bool diff --git a/lsp/jLang.ml b/lsp/jLang.ml index e54907036..27e17c045 100644 --- a/lsp/jLang.ml +++ b/lsp/jLang.ml @@ -37,9 +37,14 @@ end module Diagnostic = struct module Libnames = Serlib.Ser_libnames + module FailedRequire = struct + type t = [%import: Lang.Diagnostic.FailedRequire.t] [@@deriving yojson] + end + module Data = struct module Lang = struct module Range = Range + module FailedRequire = FailedRequire module Diagnostic = Lang.Diagnostic end @@ -78,7 +83,7 @@ module Diagnostic = struct { range : Range.t ; severity : int ; message : string - ; data : Data.t list option [@default None] + ; data : Data.t option [@default None] } [@@deriving yojson] From b70ba5f6986e0875d151a459f307c71df9104019 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 29 Sep 2024 15:37:07 +0200 Subject: [PATCH 02/22] [fleche] Aesthetic refactoring. --- fleche/doc.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/fleche/doc.ml b/fleche/doc.ml index 4c02c7b2e..f21c548ba 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -670,16 +670,17 @@ let search_node ~command ~doc ~st = (fun (node : Node.t) -> Option.default Memo.Stats.zero node.info.stats) Memo.Stats.zero node in + let back_overflow num = + let ll = List.length doc.nodes in + Pp.( + str "not enough nodes: [" ++ int num ++ str " > " ++ int ll + ++ str "] available document nodes") + in match command with | Coq.Ast.Meta.Command.Back num -> ( match Base.List.nth doc.nodes num with | None -> - let ll = List.length doc.nodes in - let message = - Pp.( - str "not enough nodes: [" ++ int num ++ str " > " ++ int ll - ++ str "] available document nodes") - in + let message = back_overflow num in (Coq.Protect.E.error message, nstats None) | Some node -> (Coq.Protect.E.ok node.state, nstats (Some node))) | Restart -> ( From 64943ff21997ea1de6e769936633d64a8e767550 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 30 Sep 2024 13:22:03 +0200 Subject: [PATCH 03/22] [internal] Don't make severity type private. This wasn't a good tradeoff in the end, but a nuisance. --- controller/rq_goals.ml | 4 +--- fleche/doc.ml | 6 ++++-- lang/diagnostic.ml | 1 - lang/diagnostic.mli | 13 +++++-------- lsp/jLang.ml | 1 - 5 files changed, 10 insertions(+), 15 deletions(-) diff --git a/controller/rq_goals.ml b/controller/rq_goals.ml index 2299de66b..e420b8842 100644 --- a/controller/rq_goals.ml +++ b/controller/rq_goals.ml @@ -6,9 +6,7 @@ (************************************************************************) (* Replace by ppx when we can print goals properly in the client *) -let mk_message (range, level, text) = - let level = Lang.Diagnostic.Severity.to_int level in - Lsp.JFleche.Message.{ range; level; text } +let mk_message (range, level, text) = Lsp.JFleche.Message.{ range; level; text } let mk_messages node = Option.map Fleche.Doc.Node.messages node diff --git a/fleche/doc.ml b/fleche/doc.ml index f21c548ba..282afeccd 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -225,8 +225,10 @@ end = struct else 3 in let f (_, lvl, _) = - let lvl = Lang.Diagnostic.Severity.to_int lvl in - if lvl = 2 then Both else if lvl < cutoff then Left else Right + (* warning = 2 *) + if lvl = Lang.Diagnostic.Severity.warning then Both + else if lvl < cutoff then Left + else Right in let diags, messages = partition ~f fbs in (List.map (of_feed ~drange) diags, messages) diff --git a/lang/diagnostic.ml b/lang/diagnostic.ml index 84b307536..db01508ce 100644 --- a/lang/diagnostic.ml +++ b/lang/diagnostic.ml @@ -25,7 +25,6 @@ module Severity = struct let warning = 2 let information = 3 let hint = 4 - let to_int x = x end type t = diff --git a/lang/diagnostic.mli b/lang/diagnostic.mli index 282d10f6d..1087171f4 100644 --- a/lang/diagnostic.mli +++ b/lang/diagnostic.mli @@ -19,15 +19,12 @@ module Data : sig end module Severity : sig - type t + type t = int - val error : t - val warning : t - val information : t - val hint : t - - (** Convert to LSP-like levels *) - val to_int : t -> int + val error : t (* 1 *) + val warning : t (* 2 *) + val information : t (* 3 *) + val hint : t (* 4 *) end type t = diff --git a/lsp/jLang.ml b/lsp/jLang.ml index 27e17c045..631d902ab 100644 --- a/lsp/jLang.ml +++ b/lsp/jLang.ml @@ -89,7 +89,6 @@ module Diagnostic = struct let to_yojson { Lang.Diagnostic.range; severity; message; data } = let range = Range.conv range in - let severity = Lang.Diagnostic.Severity.to_int severity in let message = Pp.to_string message in _t_to_yojson { range; severity; message; data } end From 624279815728d4445744e7830747f60a22fddd3d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 30 Sep 2024 16:37:59 +0200 Subject: [PATCH 04/22] [build] [worker] [ci] Fixup mistake in #842 For some reason I didn't get to test this properly, the paths are now right, and the worker can load again. --- Makefile | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 00cceaa66..21f55c73a 100644 --- a/Makefile +++ b/Makefile @@ -160,6 +160,9 @@ VENDORED_SETUP:=true ifdef VENDORED_SETUP _CCROOT=_build/install/default/lib/coq-core else +# We could use `opam var lib` as well here, as the idea to rely on +# coqc was to avoid having a VENDORED_SETUP variable, which we now +# have anyways. _CCROOT=$(shell coqc -where)/../coq-core endif @@ -170,8 +173,8 @@ controller-js/coq-fs-core.js: coq_boot for i in $$(find $(_CCROOT)/plugins -name *.cma); do js_of_ocaml --dynlink $$i; done for i in $$(find _build/install/default/lib/coq-lsp/serlib -wholename */*.cma); do js_of_ocaml --dynlink $$i; done js_of_ocaml build-fs -o controller-js/coq-fs-core.js \ - $$(find $(_CCROOT)/ \( -wholename '*/plugins/*/*.js' -or -wholename '*/META' \) -printf "%p:/static/lib/%p ") \ - $$(find _build/install/default/lib/coq-lsp/ \( -wholename '*/serlib/*/*.js' -or -wholename '*/META' \) -printf "%p:/static/lib/%p ") \ + $$(find $(_CCROOT)/ \( -wholename '*/plugins/*/*.js' -or -wholename '*/META' \) -printf "%p:/static/lib/coq-core/%P ") \ + $$(find _build/install/default/lib/coq-lsp/ \( -wholename '*/serlib/*/*.js' -or -wholename '*/META' \) -printf "%p:/static/lib/coq-lsp/%P ") \ ./etc/META.threads:/static/lib/threads/META \ $$(find $(_LIBROOT) -wholename '*/str/META' -printf "%p:/static/lib/%P ") \ $$(find $(_LIBROOT) -wholename '*/seq/META' -printf "%p:/static/lib/%P ") \ @@ -198,6 +201,11 @@ controller-js/coq-fs-core.js: coq_boot # These libs are actually linked, so no cma is needed. # $$(find $(_LIBROOT) -wholename '*/zarith/*.cma' -printf "%p:/static/lib/%P " -or -wholename '*/zarith/META' -printf "%p:/static/lib/%P ") +.PHONY: check-js-fs-sanity +check-js-fs-sanity: controller-js/coq-fs-core.js js + cat _build/default/controller-js/coq-fs.js | grep '/static/' + cat controller-js/coq-fs-core.js | grep '/static/' + # Serlib plugins require: # ppx_compare.runtime-lib # ppx_deriving.runtime From f4a029012f5ca0f90b73dd806171acae58dac9f1 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 30 Sep 2024 17:38:06 +0200 Subject: [PATCH 05/22] [ci] [worker] Remove temporal pin for JSOO The branch has been merged upstream. --- .github/workflows/build.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index e8ea7dd54..4bda2900c 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -116,8 +116,8 @@ jobs: - name: 🐫🐪🐫 Get dependencies run: | opam exec -- make opam-deps - opam pin add js_of_ocaml-compiler https://github.com/ejgallego/js_of_ocaml.git#fix_build_fs_target -y - opam pin add js_of_ocaml https://github.com/ejgallego/js_of_ocaml.git#fix_build_fs_target -y + opam pin add js_of_ocaml-compiler --dev -y + opam pin add js_of_ocaml --dev -y opam install zarith_stubs_js js_of_ocaml-ppx -y - name: 💉💉💉 Patch Coq From 94f321cf997555bea71d9f7b039b3cfeb4343975 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 1 Oct 2024 06:47:21 +0200 Subject: [PATCH 06/22] [js] Misc improvements - document correct flag for interruptions setup - log interruption setup - improve `< .. > Js.t` to `Yojson.Safe.t` converter away from printing/re-parsing, this code is critical in the LSP case due to the size of the messages being significantly larger than in jsCoq.. --- controller-js/README.md | 2 +- controller-js/coq_lsp_worker.ml | 37 +++++++++++++++++++++++++++++---- editor/code/package.json | 5 +++++ 3 files changed, 39 insertions(+), 5 deletions(-) diff --git a/controller-js/README.md b/controller-js/README.md index 244cc00ca..885b76f60 100644 --- a/controller-js/README.md +++ b/controller-js/README.md @@ -62,7 +62,7 @@ extension + Coq build. As of Feb 2023, due to security restrictions, you may need to either: - pass `--enable-coi` to `code` - - use ``?enable-coi=` in the vscode dev setup + - append `?vscode-coi` in the vscode dev setup URL in order to have interruptions (`SharedBufferArray`) working. diff --git a/controller-js/coq_lsp_worker.ml b/controller-js/coq_lsp_worker.ml index 2fabd2f7b..07d35d106 100644 --- a/controller-js/coq_lsp_worker.ml +++ b/controller-js/coq_lsp_worker.ml @@ -29,9 +29,26 @@ let rec obj_to_json (cobj : < .. > Js.t) : Yojson.Safe.t = `String (Typed_array.String.of_arrayBuffer @@ coerce cobj) else if instanceof cobj Typed_array.uint8Array then `String (Typed_array.String.of_uint8Array @@ coerce cobj) - else - let json_string = Js.to_string (Json.output cobj) in - Yojson.Safe.from_string json_string + (* Careful in case we miss cases here *) + else if instanceof cobj Unsafe.global##._Object then + Js.array_map + (fun key -> (Js.to_string key, obj_to_json (Js.Unsafe.get cobj key))) + (Js.object_keys cobj) + |> Js.to_array |> Array.to_list + |> fun al -> `Assoc al + else if Js.Opt.(strict_equals (some cobj) null) then `Null + else if Js.Optdef.(strict_equals (def cobj) undefined) then ( + Firebug.console##info "undefined branch!!!!"; + `Null) + else ( + Firebug.console##error "failure in coq_lsp_worker:obj_to_json"; + Firebug.console##error cobj; + Firebug.console##error (Json.output cobj); + raise (Failure "coq_lsp_worker:obj_to_json")) + +(* Old code, which is only useful for debug *) +(* let json_string = Js.to_string (Json.output cobj) in *) +(* Yojson.Safe.from_string json_string *) let rec json_to_obj (cobj : < .. > Js.t) (json : Yojson.Safe.t) : < .. > Js.t = let open Js.Unsafe in @@ -83,6 +100,15 @@ let parse_msg msg = Error "processed interrupt_setup") else obj_to_json msg |> Lsp.Base.Message.of_yojson +let log_interrupt () = + let lvl, message = + if not !interrupt_is_setup then + (* Maybe set one step mode, but usually that's done in the client. *) + (Lsp.Io.Lvl.Error, "Interrupt is not setup: Functionality will suffer") + else (Lsp.Io.Lvl.Info, "Interrupt setup: [Control.interrupt] backend") + in + Lsp.Io.logMessage ~lvl ~message + let on_msg msg = match parse_msg msg with | Error _ -> @@ -112,7 +138,9 @@ let rec process_queue ~state () = let on_init ~io ~root_state ~cmdline ~debug msg = match parse_msg msg with - | Error _ -> () + | Error _ -> + (* This is called one for interrupt setup *) + () | Ok msg -> ( match Lsp_core.lsp_init_process ~ofn:post_message ~io ~cmdline ~debug msg @@ -120,6 +148,7 @@ let on_init ~io ~root_state ~cmdline ~debug msg = | Lsp_core.Init_effect.Exit -> (* XXX: bind to worker.close () *) () | Lsp_core.Init_effect.Loop -> () | Lsp_core.Init_effect.Success workspaces -> + log_interrupt (); Worker.set_onmessage on_msg; let default_workspace = Coq.Workspace.default ~debug ~cmdline in let state = diff --git a/editor/code/package.json b/editor/code/package.json index 9db5b6922..71fb741cd 100644 --- a/editor/code/package.json +++ b/editor/code/package.json @@ -209,6 +209,11 @@ "type": "boolean", "default": false, "description": "Send extra diagnostics data, usually on error" + }, + "coq-lsp.send_perf_data" : { + "type": "boolean", + "default": true, + "description": "Update Perf Data Coq Panel" } } }, From 5cca78153abff44807fac32876b92b2e5f6925a6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 1 Oct 2024 06:55:44 +0200 Subject: [PATCH 07/22] [js] Place conversion functions on their own file. --- controller-js/coq_lsp_worker.ml | 77 +++++---------------------------- controller-js/jsso.ml | 57 ++++++++++++++++++++++++ controller-js/jsso.mli | 5 +++ 3 files changed, 74 insertions(+), 65 deletions(-) create mode 100644 controller-js/jsso.ml create mode 100644 controller-js/jsso.mli diff --git a/controller-js/coq_lsp_worker.ml b/controller-js/coq_lsp_worker.ml index 07d35d106..cf56e29d4 100644 --- a/controller-js/coq_lsp_worker.ml +++ b/controller-js/coq_lsp_worker.ml @@ -14,59 +14,6 @@ module LSP = Lsp.Base open Js_of_ocaml open Controller -let rec obj_to_json (cobj : < .. > Js.t) : Yojson.Safe.t = - let open Js in - let open Js.Unsafe in - let typeof_cobj = to_string (typeof cobj) in - match typeof_cobj with - | "string" -> `String (to_string @@ coerce cobj) - | "boolean" -> `Bool (to_bool @@ coerce cobj) - | "number" -> `Int (int_of_float @@ float_of_number @@ coerce cobj) - | _ -> - if instanceof cobj array_empty then - `List Array.(to_list @@ map obj_to_json @@ to_array @@ coerce cobj) - else if instanceof cobj Typed_array.arrayBuffer then - `String (Typed_array.String.of_arrayBuffer @@ coerce cobj) - else if instanceof cobj Typed_array.uint8Array then - `String (Typed_array.String.of_uint8Array @@ coerce cobj) - (* Careful in case we miss cases here *) - else if instanceof cobj Unsafe.global##._Object then - Js.array_map - (fun key -> (Js.to_string key, obj_to_json (Js.Unsafe.get cobj key))) - (Js.object_keys cobj) - |> Js.to_array |> Array.to_list - |> fun al -> `Assoc al - else if Js.Opt.(strict_equals (some cobj) null) then `Null - else if Js.Optdef.(strict_equals (def cobj) undefined) then ( - Firebug.console##info "undefined branch!!!!"; - `Null) - else ( - Firebug.console##error "failure in coq_lsp_worker:obj_to_json"; - Firebug.console##error cobj; - Firebug.console##error (Json.output cobj); - raise (Failure "coq_lsp_worker:obj_to_json")) - -(* Old code, which is only useful for debug *) -(* let json_string = Js.to_string (Json.output cobj) in *) -(* Yojson.Safe.from_string json_string *) - -let rec json_to_obj (cobj : < .. > Js.t) (json : Yojson.Safe.t) : < .. > Js.t = - let open Js.Unsafe in - let ofresh j = json_to_obj (obj [||]) j in - match json with - | `Bool b -> coerce @@ Js.bool b - | `Null -> pure_js_expr "null" - | `Assoc l -> - List.iter (fun (p, js) -> set cobj p (ofresh js)) l; - cobj - | `List l -> Array.(Js.array @@ map ofresh (of_list l)) - | `Float f -> coerce @@ Js.number_of_float f - | `String s -> coerce @@ Js.string s - | `Int m -> coerce @@ Js.number_of_float (float_of_int m) - | `Intlit s -> coerce @@ Js.number_of_float (float_of_string s) - | `Tuple t -> Array.(Js.array @@ map ofresh (of_list t)) - | `Variant (_, _) -> pure_js_expr "undefined" - let findlib_conf = "\ndestdir=\"/static/lib\"path=\"/static/lib\"" let findlib_path = "/static/lib/findlib.conf" @@ -82,7 +29,7 @@ let setup_std_printers () = let post_message (msg : Lsp.Base.Message.t) = let json = Lsp.Base.Message.to_yojson msg in - let js = json_to_obj (Js.Unsafe.obj [||]) json in + let js = Jsso.json_to_obj json in Worker.post_message js type opaque @@ -91,15 +38,6 @@ external interrupt_setup : opaque (* Uint32Array *) -> unit = "interrupt_setup" let interrupt_is_setup = ref false -let parse_msg msg = - if Js.instanceof msg Js.array_length then ( - let _method_ = Js.array_get msg 0 in - let handle = Js.array_get msg 1 |> Obj.magic in - interrupt_setup handle; - interrupt_is_setup := true; - Error "processed interrupt_setup") - else obj_to_json msg |> Lsp.Base.Message.of_yojson - let log_interrupt () = let lvl, message = if not !interrupt_is_setup then @@ -109,11 +47,20 @@ let log_interrupt () = in Lsp.Io.logMessage ~lvl ~message +let parse_msg msg = + if Js.instanceof msg Js.array_empty then ( + let _method_ = Js.array_get msg 0 in + let handle = Js.array_get msg 1 |> Obj.magic in + interrupt_setup handle; + interrupt_is_setup := true; + Error "processed interrupt_setup") + else Jsso.obj_to_json msg |> Lsp.Base.Message.of_yojson + let on_msg msg = match parse_msg msg with | Error _ -> - Lsp.Io.logMessage ~lvl:Lsp.Io.Lvl.Error - ~message:"Error in JSON RPC Message Parsing" + let message = "Error in JSON RPC Message Parsing" in + Lsp.Io.logMessage ~lvl:Lsp.Io.Lvl.Error ~message | Ok msg -> (* Lsp.Io.trace "interrupt_setup" (string_of_bool !interrupt_is_setup); *) Lsp_core.enqueue_message msg diff --git a/controller-js/jsso.ml b/controller-js/jsso.ml new file mode 100644 index 000000000..ec653d436 --- /dev/null +++ b/controller-js/jsso.ml @@ -0,0 +1,57 @@ +open Js_of_ocaml + +let rec obj_to_json (cobj : < .. > Js.t) : Yojson.Safe.t = + let open Js in + let open Js.Unsafe in + let typeof_cobj = to_string (typeof cobj) in + match typeof_cobj with + | "string" -> `String (to_string @@ coerce cobj) + | "boolean" -> `Bool (to_bool @@ coerce cobj) + | "number" -> `Int (int_of_float @@ float_of_number @@ coerce cobj) + | _ -> + if instanceof cobj array_empty then + `List Array.(to_list @@ map obj_to_json @@ to_array @@ coerce cobj) + else if instanceof cobj Typed_array.arrayBuffer then + `String (Typed_array.String.of_arrayBuffer @@ coerce cobj) + else if instanceof cobj Typed_array.uint8Array then + `String (Typed_array.String.of_uint8Array @@ coerce cobj) + (* Careful in case we miss cases here, what about '{}' for example, we + should also stop on functions? *) + else if instanceof cobj Unsafe.global##._Object then + Js.array_map + (fun key -> (Js.to_string key, obj_to_json (Js.Unsafe.get cobj key))) + (Js.object_keys cobj) + |> Js.to_array |> Array.to_list + |> fun al -> `Assoc al + else if Js.Opt.(strict_equals (some cobj) null) then `Null + else if Js.Optdef.(strict_equals (def cobj) undefined) then ( + Firebug.console##info "undefined branch!!!!"; + `Null) + else ( + Firebug.console##error "failure in coq_lsp_worker:obj_to_json"; + Firebug.console##error cobj; + Firebug.console##error (Json.output cobj); + raise (Failure "coq_lsp_worker:obj_to_json")) + +(* Old code, which is only useful for debug *) +(* let json_string = Js.to_string (Json.output cobj) in *) +(* Yojson.Safe.from_string json_string *) + +let rec json_to_obj (cobj : < .. > Js.t) (json : Yojson.Safe.t) : < .. > Js.t = + let open Js.Unsafe in + let ofresh j = json_to_obj (obj [||]) j in + match json with + | `Bool b -> coerce @@ Js.bool b + | `Null -> pure_js_expr "null" + | `Assoc l -> + List.iter (fun (p, js) -> set cobj p (ofresh js)) l; + coerce @@ cobj + | `List l -> coerce @@ Array.(Js.array @@ map ofresh (of_list l)) + | `Float f -> coerce @@ Js.number_of_float f + | `String s -> coerce @@ Js.string s + | `Int m -> coerce @@ Js.number_of_float (float_of_int m) + | `Intlit s -> coerce @@ Js.number_of_float (float_of_string s) + | `Tuple t -> coerce @@ Array.(Js.array @@ map ofresh (of_list t)) + | `Variant (_, _) -> pure_js_expr "undefined" + +let json_to_obj json = json_to_obj (Js.Unsafe.obj [||]) json diff --git a/controller-js/jsso.mli b/controller-js/jsso.mli new file mode 100644 index 000000000..f7620fef0 --- /dev/null +++ b/controller-js/jsso.mli @@ -0,0 +1,5 @@ +open Js_of_ocaml + +(* Object to Yojson converter *) +val obj_to_json : < .. > Js.t -> Yojson.Safe.t +val json_to_obj : Yojson.Safe.t -> < .. > Js.t From 3301018fb7067a297eaf35cbb38e5a0df2a4adac Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 23 Sep 2024 12:42:27 +0200 Subject: [PATCH 08/22] Adapt to coq/coq#19575 (ltac2 parsing uses attributes) --- serlib/plugins/ltac2/ser_tac2expr.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/serlib/plugins/ltac2/ser_tac2expr.ml b/serlib/plugins/ltac2/ser_tac2expr.ml index dd25268c3..9671ffa51 100644 --- a/serlib/plugins/ltac2/ser_tac2expr.ml +++ b/serlib/plugins/ltac2/ser_tac2expr.ml @@ -12,6 +12,7 @@ module Loc = Ser_loc module CAst = Ser_cAst module Names = Ser_names module Libnames = Ser_libnames +module Attributes = Ser_attributes open Sexplib.Std open Ppx_hash_lib.Std.Hash.Builtin From 4012c753b0376773a82a3a51eeb7467260095d80 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 1 Oct 2024 15:35:30 +0200 Subject: [PATCH 09/22] [editor] [fmt] Fix formatting nit to make CI green again. --- editor/code/package.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/editor/code/package.json b/editor/code/package.json index 71fb741cd..257aab11e 100644 --- a/editor/code/package.json +++ b/editor/code/package.json @@ -210,7 +210,7 @@ "default": false, "description": "Send extra diagnostics data, usually on error" }, - "coq-lsp.send_perf_data" : { + "coq-lsp.send_perf_data": { "type": "boolean", "default": true, "description": "Update Perf Data Coq Panel" From ee95987944bf40f2de6e33260c933d50b8c0e105 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 3 Oct 2024 17:24:54 +0200 Subject: [PATCH 10/22] [coq] Abstract the feedback / error payloads better. This is in preparation for cleaner code in #840 --- controller/request.ml | 2 +- controller/rq_goals.ml | 3 ++- coq/init.ml | 5 +++-- coq/message.ml | 14 ++++++++++++- coq/message.mli | 22 +++++++++++++++++++- coq/protect.ml | 22 ++++++++++---------- coq/protect.mli | 8 +++---- coq/workspace.ml | 4 ++-- fleche/doc.ml | 38 +++++++++++++++++++--------------- fleche/doc.mli | 2 +- petanque/agent.ml | 4 ++-- plugins/explain_errors/main.ml | 6 ++++-- plugins/goaldump/main.ml | 7 +++---- 13 files changed, 87 insertions(+), 50 deletions(-) diff --git a/controller/request.ml b/controller/request.ml index 3ea2fac4b..27abf50e9 100644 --- a/controller/request.ml +++ b/controller/request.ml @@ -26,7 +26,7 @@ module R = struct let print_err ~name e = match e with - | Coq.Protect.Error.Anomaly (_loc, msg) | User (_loc, msg) -> + | Coq.Protect.Error.Anomaly { msg; _ } | User { msg; _ } -> Format.asprintf "Error in %s request: %a" name Pp.pp_with msg let of_execution ~name ~f x : t = diff --git a/controller/rq_goals.ml b/controller/rq_goals.ml index e420b8842..47d672db1 100644 --- a/controller/rq_goals.ml +++ b/controller/rq_goals.ml @@ -6,7 +6,8 @@ (************************************************************************) (* Replace by ppx when we can print goals properly in the client *) -let mk_message (range, level, text) = Lsp.JFleche.Message.{ range; level; text } +let mk_message (level, { Coq.Message.Payload.range; msg }) = + Lsp.JFleche.Message.{ range; level; text = msg } let mk_messages node = Option.map Fleche.Doc.Node.messages node diff --git a/coq/init.ml b/coq/init.ml index 3eaeaf4f1..eaabe9edf 100644 --- a/coq/init.ml +++ b/coq/init.ml @@ -36,9 +36,10 @@ let coq_lvl_to_severity (lvl : Feedback.level) = | Feedback.Warning -> warning | Feedback.Error -> error -let add_message lvl loc msg q = +let add_message lvl range msg q = let lvl = coq_lvl_to_severity lvl in - q := (loc, lvl, msg) :: !q + let payload = Message.Payload.make ?range msg in + q := (lvl, payload) :: !q let mk_fb_handler q Feedback.{ contents; _ } = match contents with diff --git a/coq/message.ml b/coq/message.ml index dfba4ccd9..f48644d20 100644 --- a/coq/message.ml +++ b/coq/message.ml @@ -1,2 +1,14 @@ (** Messages from Coq *) -type 'l t = 'l option * Lang.Diagnostic.Severity.t * Pp.t +module Payload = struct + type 'l t = + { range : 'l option + ; msg : Pp.t + } + + let make ?range msg = { range; msg } + let map ~f { range; msg } = { range = Option.map f range; msg } +end + +type 'l t = Lang.Diagnostic.Severity.t * 'l Payload.t + +let map ~f (lvl, pl) = (lvl, Payload.map ~f pl) diff --git a/coq/message.mli b/coq/message.mli index dfba4ccd9..2935dd5bb 100644 --- a/coq/message.mli +++ b/coq/message.mli @@ -1,2 +1,22 @@ (** Messages from Coq *) -type 'l t = 'l option * Lang.Diagnostic.Severity.t * Pp.t + +(** Coq provides payload to our layer via two different mechanisms: + - feedback messages + - error exceptions + + In both cases, the payload is the same, and it comes via different ways due + to historical reasons. We abstract the payload as to better handle the + common paths. *) +module Payload : sig + type 'l t = + { range : 'l option + ; msg : Pp.t + } + + val make : ?range:'l -> Pp.t -> 'l t + val map : f:('l -> 'm) -> 'l t -> 'm t +end + +type 'l t = Lang.Diagnostic.Severity.t * 'l Payload.t + +val map : f:('l -> 'm) -> 'l t -> 'm t diff --git a/coq/protect.ml b/coq/protect.ml index c768e1e9e..f9560312a 100644 --- a/coq/protect.ml +++ b/coq/protect.ml @@ -1,9 +1,7 @@ module Error = struct - type 'l payload = 'l option * Pp.t - type 'l t = - | User of 'l payload - | Anomaly of 'l payload + | User of 'l Message.Payload.t + | Anomaly of 'l Message.Payload.t let map ~f = function | User e -> User (f e) @@ -15,7 +13,9 @@ module R = struct | Completed of ('a, 'l Error.t) result | Interrupted (* signal sent, eval didn't complete *) - let error e = Completed (Error (Error.User (None, e))) + let error msg = + let payload = Message.Payload.make msg in + Completed (Error (Error.User payload)) let map ~f = function | Completed (Result.Ok r) -> Completed (Result.Ok (f r)) @@ -28,7 +28,7 @@ module R = struct | Interrupted -> Interrupted let map_loc ~f = - let f (loc, msg) = (Option.map f loc, msg) in + let f = Message.Payload.map ~f in map_error ~f end @@ -41,11 +41,12 @@ let eval_exn ~token ~f x = R.Interrupted | exception exn -> let e, info = Exninfo.capture exn in - let loc = Loc.(get_loc info) in + let range = Loc.(get_loc info) in let msg = CErrors.iprint (e, info) in + let payload = Message.Payload.make ?range msg in Vernacstate.Interp.invalidate_cache (); - if CErrors.is_anomaly e then R.Completed (Error (Anomaly (loc, msg))) - else R.Completed (Error (User (loc, msg))) + if CErrors.is_anomaly e then R.Completed (Error (Anomaly payload)) + else R.Completed (Error (User payload)) let _bind_exn ~f x = match x with @@ -68,10 +69,9 @@ module E = struct { r; feedback } let map ~f { r; feedback } = { r = R.map ~f r; feedback } - let map_message ~f (loc, lvl, msg) = (Option.map f loc, lvl, msg) let map_loc ~f { r; feedback } = - { r = R.map_loc ~f r; feedback = List.map (map_message ~f) feedback } + { r = R.map_loc ~f r; feedback = List.map (Message.map ~f) feedback } let bind ~f { r; feedback } = match r with diff --git a/coq/protect.mli b/coq/protect.mli index c0c2fe732..cfbd6595a 100644 --- a/coq/protect.mli +++ b/coq/protect.mli @@ -4,11 +4,9 @@ As of today this includes feedback and exceptions. *) module Error : sig - type 'l payload = 'l option * Pp.t - type 'l t = private - | User of 'l payload - | Anomaly of 'l payload + | User of 'l Message.Payload.t + | Anomaly of 'l Message.Payload.t end (** This "monad" could be related to "Runners in action" (Ahman, Bauer), thanks @@ -22,7 +20,7 @@ module R : sig val map : f:('a -> 'b) -> ('a, 'l) t -> ('b, 'l) t val map_error : - f:('l Error.payload -> 'm Error.payload) -> ('a, 'l) t -> ('a, 'm) t + f:('l Message.Payload.t -> 'm Message.Payload.t) -> ('a, 'l) t -> ('a, 'm) t (** Update the loc stored in the result, this is used by our cache-aware location *) diff --git a/coq/workspace.ml b/coq/workspace.ml index 365e29d70..56a6ccbc3 100644 --- a/coq/workspace.ml +++ b/coq/workspace.ml @@ -387,8 +387,8 @@ let guess ~token ~debug ~cmdline ~dir = ignore feedback; match r with | Protect.R.Interrupted -> Error "Workspace Scanning Interrupted" - | Protect.R.Completed (Error (User (_, msg))) - | Protect.R.Completed (Error (Anomaly (_, msg))) -> + | Protect.R.Completed (Error (User { msg; _ })) + | Protect.R.Completed (Error (Anomaly { msg; _ })) -> Error (Format.asprintf "Workspace Scanning Errored: %a" Pp.pp_with msg) | Protect.R.Completed (Ok workspace) -> Ok workspace diff --git a/fleche/doc.ml b/fleche/doc.ml index 282afeccd..cd73263e4 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -116,8 +116,9 @@ module Node = struct module Message = struct type t = Lang.Range.t Coq.Message.t - let feedback_to_message ~lines (loc, lvl, msg) = - (Coq.Utils.to_orange ~lines loc, lvl, msg) + let feedback_to_message ~lines message = + let f = Coq.Utils.to_range ~lines in + Coq.Message.map ~f message end type t = @@ -197,9 +198,10 @@ end = struct let data = extra_diagnostics_of_ast stm_range ast in make ?data err_range Lang.Diagnostic.Severity.error msg - let of_feed ~drange (range, severity, message) = + let of_feed ~drange (severity, payload) = + let { Coq.Message.Payload.range; msg } = payload in let range = Option.default drange range in - make range severity message + make range severity msg type partition_kind = | Left @@ -224,7 +226,7 @@ end = struct else if !Config.v.show_notices_as_diagnostics then 4 else 3 in - let f (_, lvl, _) = + let f (lvl, _) = (* warning = 2 *) if lvl = Lang.Diagnostic.Severity.warning then Both else if lvl < cutoff then Left @@ -354,8 +356,9 @@ let empty_doc ~uri ~contents ~version ~env ~root ~nodes ~completed = let completed = completed init_range in { uri; contents; toc; version; env; root; nodes; diags_dirty; completed } -let error_doc ~loc ~message ~uri ~contents ~version ~env = - let feedback = [ (loc, Diags.err, Pp.str message) ] in +let error_doc ~range ~message ~uri ~contents ~version ~env = + let payload = Coq.Message.Payload.make ?range (Pp.str message) in + let feedback = [ (Diags.err, payload) ] in let root = env.Env.init in let nodes = [] in let completed range = Completion.Failed range in @@ -365,7 +368,8 @@ let conv_error_doc ~raw ~uri ~version ~env ~root err = let contents = Contents.make_raw ~raw in let lines = contents.lines in let err = - (None, Diags.err, Pp.(str "Error in document conversion: " ++ str err)) + let msg = Pp.(str "Error in document conversion: " ++ str err) in + (Diags.err, Coq.Message.Payload.make msg) in (* No execution to add *) let stats = None in @@ -394,14 +398,14 @@ let handle_doc_creation_exec ~token ~env ~uri ~version ~contents = match r with | Interrupted -> let message = "Document Creation Interrupted!" in - let loc = None in - error_doc ~loc ~message ~uri ~version ~contents ~env - | Completed (Error (User (loc, err_msg))) - | Completed (Error (Anomaly (loc, err_msg))) -> + let range = None in + error_doc ~range ~message ~uri ~version ~contents ~env + | Completed (Error (User { range; msg = err_msg })) + | Completed (Error (Anomaly { range; msg = err_msg })) -> let message = Format.asprintf "Doc.create, internal error: @[%a@]" Pp.pp_with err_msg in - error_doc ~loc ~message ~uri ~version ~contents ~env + error_doc ~range ~message ~uri ~version ~contents ~env | Completed (Ok doc) -> (doc, []) in let state = doc.root in @@ -749,7 +753,7 @@ let parse_action ~token ~lines ~st last_tok doc_handle = | Ok (Some ast) -> let () = if Debug.parsing then DDebug.parsed_sentence ~ast in (Process ast, [], feedback, time) - | Error (Anomaly (_, msg)) | Error (User (None, msg)) -> + | Error (Anomaly { msg; _ }) | Error (User { range = None; msg }) -> (* We don't have a better alternative :(, usually missing error loc here means an anomaly, so we stop *) let err_range = last_tok in @@ -757,7 +761,7 @@ let parse_action ~token ~lines ~st last_tok doc_handle = [ Diags.error ~err_range ~msg ~stm_range:err_range () ] in (EOF (Failed last_tok), parse_diags, feedback, time) - | Error (User (Some err_range, msg)) -> + | Error (User { range = Some err_range; msg }) -> Coq.Parsing.discard_to_dot doc_handle; let last_tok = Coq.Parsing.Parsable.loc doc_handle in let last_tok_range = Coq.Utils.to_range ~lines last_tok in @@ -816,8 +820,8 @@ let node_of_coq_result ~token ~doc ~range ~prev ~ast ~st ~parsing_diags ~diags:[] ~feedback ~info in Continue { state; last_tok; node } - | Error (Coq.Protect.Error.Anomaly (err_range, msg) as coq_err) - | Error (User (err_range, msg) as coq_err) -> + | Error (Coq.Protect.Error.Anomaly { range = err_range; msg } as coq_err) + | Error (User { range = err_range; msg } as coq_err) -> let err_range = Option.default range err_range in let err_diags = [ Diags.error ~err_range ~msg ~stm_range:range ~ast () ] in let contents, nodes = (doc.contents, doc.nodes) in diff --git a/fleche/doc.mli b/fleche/doc.mli index f309d9bc1..ff2a0c247 100644 --- a/fleche/doc.mli +++ b/fleche/doc.mli @@ -24,7 +24,7 @@ module Node : sig end module Message : sig - type t = Lang.Range.t option * Lang.Diagnostic.Severity.t * Pp.t + type t = Lang.Range.t Coq.Message.t end type t = private diff --git a/petanque/agent.ml b/petanque/agent.ml index 7a74b2418..320b890dd 100644 --- a/petanque/agent.ml +++ b/petanque/agent.ml @@ -137,9 +137,9 @@ let execute_precommands ~token ~memo ~pre_commands ~(node : Fleche.Doc.Node.t) = let protect_to_result (r : _ Coq.Protect.E.t) : (_, _) Result.t = match r with | { r = Interrupted; feedback = _ } -> Error Error.Interrupted - | { r = Completed (Error (User (_loc, msg))); feedback = _ } -> + | { r = Completed (Error (User { msg; _ })); feedback = _ } -> Error (Error.Coq (Pp.string_of_ppcmds msg)) - | { r = Completed (Error (Anomaly (_loc, msg))); feedback = _ } -> + | { r = Completed (Error (Anomaly { msg; _ })); feedback = _ } -> Error (Error.Anomaly (Pp.string_of_ppcmds msg)) | { r = Completed (Ok r); feedback = _ } -> Ok r diff --git a/plugins/explain_errors/main.ml b/plugins/explain_errors/main.ml index 599a856e7..fb72c4ba2 100644 --- a/plugins/explain_errors/main.ml +++ b/plugins/explain_errors/main.ml @@ -10,8 +10,10 @@ let pp_goals ~token ~st = | Some proof -> ( match Coq.Print.pr_goals ~token ~proof with | { Coq.Protect.E.r = Completed (Ok goals); _ } -> goals - | { Coq.Protect.E.r = Completed (Error (User msg | Anomaly msg)); _ } -> - Pp.(str "error when printing goals: " ++ snd msg) + | { Coq.Protect.E.r = + Completed (Error (User { msg; _ } | Anomaly { msg; _ })) + ; _ + } -> Pp.(str "error when printing goals: " ++ msg) | { Coq.Protect.E.r = Interrupted; _ } -> Pp.str "goal printing was interrupted") diff --git a/plugins/goaldump/main.ml b/plugins/goaldump/main.ml index 4f7539459..474e1facd 100644 --- a/plugins/goaldump/main.ml +++ b/plugins/goaldump/main.ml @@ -6,11 +6,10 @@ let of_execution ~io ~what (v : (_, _) Coq.Protect.E.t) = | { r; feedback = _ } -> ( match r with | Coq.Protect.R.Completed (Ok goals) -> goals - | Coq.Protect.R.Completed (Error (Anomaly err)) - | Coq.Protect.R.Completed (Error (User err)) -> + | Coq.Protect.R.Completed (Error (Anomaly { msg; _ })) + | Coq.Protect.R.Completed (Error (User { msg; _ })) -> let lvl = Io.Level.Error in - Io.Report.msg ~io ~lvl "error when retrieving %s: %a" what Pp.pp_with - (snd err); + Io.Report.msg ~io ~lvl "error when retrieving %s: %a" what Pp.pp_with msg; None | Coq.Protect.R.Interrupted -> None) From bf59fb0f0bde00a7a080a565c231b1e80f044c7b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 2 Oct 2024 15:47:22 +0200 Subject: [PATCH 11/22] [vendor] [deps] Bump Coq deps for more codeAction test cases. --- vendor/coq | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vendor/coq b/vendor/coq index b68052328..6633e8151 160000 --- a/vendor/coq +++ b/vendor/coq @@ -1 +1 @@ -Subproject commit b68052328b65a3e85cd48a4718713fdd0c24f08d +Subproject commit 6633e8151afa194ea8378ac3598564cfbf571ca4 From 9f66f3c25c3e11427c8f3feabfc17ff20202ace6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 29 Sep 2024 03:02:06 +0200 Subject: [PATCH 12/22] [fleche] [lsp] Implement codeAction, using Coq Quickfix.t Not sure I'm happy about the impact of this, but not sure either how to make it more minimal. Some more abstraction w.r.t. async events would be welcome, the error / diagnostic separation as of now either is not super user-friendly. --- controller/lsp_core.ml | 15 ++++++++++++ controller/rq_action.ml | 52 ++++++++++++++++++++++++++++++++++++++++ controller/rq_action.mli | 1 + controller/rq_goals.ml | 2 +- controller/rq_init.ml | 2 +- coq/init.ml | 12 +++++++--- coq/message.ml | 8 +++++-- coq/message.mli | 3 ++- coq/protect.ml | 20 +++++++++++++++- examples/codeAction.v | 44 ++++++++++++++++++++++++++++++++++ fleche/doc.ml | 48 ++++++++++++++++++++++++------------- lang/diagnostic.ml | 1 + lang/diagnostic.mli | 1 + lang/qf.ml | 12 ++++++++++ lang/qf.mli | 12 ++++++++++ lsp/core.ml | 30 +++++++++++++++++++++++ lsp/core.mli | 30 +++++++++++++++++++++++ lsp/jCoq.ml | 1 + lsp/jLang.ml | 19 +++++++++++++++ lsp/jLang.mli | 4 +++- lsp/workspace.ml | 21 ++++++++++++++++ lsp/workspace.mli | 13 ++++++++++ 22 files changed, 324 insertions(+), 27 deletions(-) create mode 100644 controller/rq_action.ml create mode 100644 controller/rq_action.mli create mode 100644 examples/codeAction.v create mode 100644 lang/qf.ml create mode 100644 lang/qf.mli diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index eb33483e5..5479d96ef 100644 --- a/controller/lsp_core.ml +++ b/controller/lsp_core.ml @@ -416,6 +416,20 @@ 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 +(* could be smarter *) +let do_action ~params = + let range = field "range" params in + match Lsp.JLang.Diagnostic.Range.of_yojson range with + | Ok range -> + let range = Lsp.JLang.Diagnostic.Range.vnoc range in + do_immediate ~params ~handler:(Rq_action.request ~range) + | Error err -> + (* XXX: We really need to fix the parsing error handling in lsp_core, we got + it right in petanque haha *) + (* JSON-RPC Parse error (EJGA: is this the right code) *) + let code = -32700 in + Rq.Action.error (code, err) + let do_cancel ~ofn_rq ~params = let id = int_field "id" params in let code = -32800 in @@ -584,6 +598,7 @@ let dispatch_request ~token ~method_ ~params : Rq.Action.t = | "textDocument/hover" -> do_hover ~params | "textDocument/codeLens" -> do_lens ~params | "textDocument/selectionRange" -> do_selectionRange ~params + | "textDocument/codeAction" -> do_action ~params (* Proof-specific stuff *) | "proof/goals" -> do_goals ~params (* Proof-specific stuff *) diff --git a/controller/rq_action.ml b/controller/rq_action.ml new file mode 100644 index 000000000..4108e1659 --- /dev/null +++ b/controller/rq_action.ml @@ -0,0 +1,52 @@ +let dqf (d : Lang.Diagnostic.t) : _ option = + Option.bind d.data (function + | { Lang.Diagnostic.Data.quickFix = Some qf; _ } -> Some (d, qf) + | _ -> None) + +let point_lt { Lang.Point.line = l1; Lang.Point.character = c1; offset = _ } + { Lang.Point.line = l2; Lang.Point.character = c2; offset = _ } = + l1 < l2 || (l1 = l2 && c1 < c2) + +let point_gt { Lang.Point.line = l1; Lang.Point.character = c1; offset = _ } + { Lang.Point.line = l2; Lang.Point.character = c2; offset = _ } = + l1 > l2 || (l1 = l2 && c1 > c2) + +let get_qf ~range (doc : Fleche.Doc.t) = + let diags = + List.filter_map + (fun (node : Fleche.Doc.Node.t) -> + let open Lang.Range in + (* let open Lang.Point in *) + let nrange = node.range in + if point_lt nrange.end_ range.start || point_gt nrange.start range.end_ + then None + else Some node.diags) + doc.nodes + |> List.concat + in + List.filter_map dqf diags + +let request ~range ~token:_ ~(doc : Fleche.Doc.t) = + let kind = Some "quickfix" in + let isPreferred = Some true in + let qf = get_qf ~range doc in + let bf (d, qf) = + let mm = + match qf with + | [ q ] -> q.Lang.Qf.newText + | _ -> "correct code" + in + let title = "Replace with " ^ mm in + let diagnostics = [ d ] in + let qff { Lang.Qf.range; newText } = + Lsp.Workspace.TextEdit.{ range; newText } + in + let changes = [ (doc.uri, List.map qff qf) ] in + let edit = Some Lsp.Workspace.WorkspaceEdit.{ changes } in + Lsp.Core.CodeAction.{ title; kind; diagnostics; isPreferred; edit } + in + List.map bf qf + +let request ~range ~token ~(doc : Fleche.Doc.t) = + let res = request ~range ~token ~doc in + Ok (`List (List.map Lsp.Core.CodeAction.to_yojson res)) diff --git a/controller/rq_action.mli b/controller/rq_action.mli new file mode 100644 index 000000000..959b0a03d --- /dev/null +++ b/controller/rq_action.mli @@ -0,0 +1 @@ +val request : range:Lang.Range.t -> Request.document diff --git a/controller/rq_goals.ml b/controller/rq_goals.ml index 47d672db1..fa1cb1421 100644 --- a/controller/rq_goals.ml +++ b/controller/rq_goals.ml @@ -6,7 +6,7 @@ (************************************************************************) (* Replace by ppx when we can print goals properly in the client *) -let mk_message (level, { Coq.Message.Payload.range; msg }) = +let mk_message (level, { Coq.Message.Payload.range; msg; quickFix = _ }) = Lsp.JFleche.Message.{ range; level; text = msg } let mk_messages node = diff --git a/controller/rq_init.ml b/controller/rq_init.ml index 3b008cd6e..b5f7bd9a8 100644 --- a/controller/rq_init.ml +++ b/controller/rq_init.ml @@ -117,7 +117,7 @@ let do_initialize ~io ~params = [ ("textDocumentSync", `Int 1) ; ("documentSymbolProvider", `Bool true) ; ("hoverProvider", `Bool true) - ; ("codeActionProvider", `Bool false) + ; ("codeActionProvider", `Bool true) ; ( "completionProvider" , `Assoc [ ("triggerCharacters", `List [ `String "\\" ]) diff --git a/coq/init.ml b/coq/init.ml index eaabe9edf..891075c2c 100644 --- a/coq/init.ml +++ b/coq/init.ml @@ -36,14 +36,20 @@ let coq_lvl_to_severity (lvl : Feedback.level) = | Feedback.Warning -> warning | Feedback.Error -> error -let add_message lvl range msg q = +let qf_of_coq qf = + let range = Quickfix.loc qf in + let newText = Quickfix.pp qf |> Pp.string_of_ppcmds in + { Lang.Qf.range; newText } + +let add_message lvl range qf msg q = let lvl = coq_lvl_to_severity lvl in - let payload = Message.Payload.make ?range msg in + let quickFix = if qf = [] then None else Some (List.map qf_of_coq qf) in + let payload = Message.Payload.make ?range ?quickFix msg in q := (lvl, payload) :: !q let mk_fb_handler q Feedback.{ contents; _ } = match contents with - | Message (lvl, loc, _, msg) -> add_message lvl loc msg q + | Message (lvl, loc, qf, msg) -> add_message lvl loc qf msg q | _ -> () let coq_init opts = diff --git a/coq/message.ml b/coq/message.ml index f48644d20..715573918 100644 --- a/coq/message.ml +++ b/coq/message.ml @@ -2,11 +2,15 @@ module Payload = struct type 'l t = { range : 'l option + ; quickFix : 'l Lang.Qf.t list option ; msg : Pp.t } - let make ?range msg = { range; msg } - let map ~f { range; msg } = { range = Option.map f range; msg } + let make ?range ?quickFix msg = { range; quickFix; msg } + + let map ~f { range; quickFix; msg } = + let quickFix = Option.map (List.map (Lang.Qf.map ~f)) quickFix in + { range = Option.map f range; quickFix; msg } end type 'l t = Lang.Diagnostic.Severity.t * 'l Payload.t diff --git a/coq/message.mli b/coq/message.mli index 2935dd5bb..f6bc0957a 100644 --- a/coq/message.mli +++ b/coq/message.mli @@ -10,10 +10,11 @@ module Payload : sig type 'l t = { range : 'l option + ; quickFix : 'l Lang.Qf.t list option ; msg : Pp.t } - val make : ?range:'l -> Pp.t -> 'l t + val make : ?range:'l -> ?quickFix:'l Lang.Qf.t list -> Pp.t -> 'l t val map : f:('l -> 'm) -> 'l t -> 'm t end diff --git a/coq/protect.ml b/coq/protect.ml index f9560312a..f6bcb7361 100644 --- a/coq/protect.ml +++ b/coq/protect.ml @@ -27,11 +27,24 @@ module R = struct | Completed (Ok r) -> Completed (Ok r) | Interrupted -> Interrupted + (* Similar to Message.map, but missing the priority field, this is due to Coq + having to sources of feedback, an async one, and the exn sync one. + Ultimately both carry the same [payload]. + + See coq/coq#5479 for some information about this, among some other relevant + issues. AFAICT, the STM tried to use a full async error reporting however + due to problems the more "legacy" exn is the actuall error mechanism in + use *) let map_loc ~f = let f = Message.Payload.map ~f in map_error ~f end +let qf_of_coq qf = + let range = Quickfix.loc qf in + let newText = Quickfix.pp qf |> Pp.string_of_ppcmds in + { Lang.Qf.range; newText } + (* Eval and reify exceptions *) let eval_exn ~token ~f x = match Limits.limit ~token ~f x with @@ -43,7 +56,12 @@ let eval_exn ~token ~f x = let e, info = Exninfo.capture exn in let range = Loc.(get_loc info) in let msg = CErrors.iprint (e, info) in - let payload = Message.Payload.make ?range msg in + let quickFix = + match Quickfix.from_exception exn with + | Ok [] | Error _ -> None + | Ok qf -> Some (List.map qf_of_coq qf) + in + let payload = Message.Payload.make ?range ?quickFix msg in Vernacstate.Interp.invalidate_cache (); if CErrors.is_anomaly e then R.Completed (Error (Anomaly payload)) else R.Completed (Error (User payload)) diff --git a/examples/codeAction.v b/examples/codeAction.v new file mode 100644 index 000000000..aea7a3255 --- /dev/null +++ b/examples/codeAction.v @@ -0,0 +1,44 @@ +(* Example codeAction, from Coq's test suite *) + +Module M. Definition y := 4. End M. +Import M. + +#[deprecated(use=y)] +Definition x := 3. + +Module N. Definition y := 5. End N. +Import N. + +Definition d1 := x = 3. + +Module M1. +Notation w := x. +End M1. +Import M1. + +#[deprecated(use=w)] +Notation v := 3. + +Module M2. +Notation w := 5. +End M2. +Import M2. + +Definition d2 := v = 3. + +Fail #[deprecated(use=w)] +Notation "a +++ b" := (a + b) (at level 2). + +Fail #[deprecated(use=nonexisting)] +Definition y := 2. + +(***********************************************) +Module A. +End B. + +(***********************************************) +Require Import Extraction. + +Module nat. End nat. + +Extraction nat. diff --git a/fleche/doc.ml b/fleche/doc.ml index cd73263e4..bb06a0cc5 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -155,6 +155,7 @@ module Diags : sig (** Build advanced diagnostic with AST analysis *) val error : err_range:Lang.Range.t + -> quickFix:Lang.Range.t Lang.Qf.t list option -> msg:Pp.t -> stm_range:Lang.Range.t (* range for the sentence *) -> ?ast:Node.Ast.t @@ -175,7 +176,7 @@ end = struct Lang.Diagnostic.{ range; severity; message; data } (* ast-dependent error diagnostic generation *) - let extra_diagnostics_of_ast stm_range ast = + let extra_diagnostics_of_ast quickFix stm_range ast = let sentenceRange = Some stm_range in let failedRequire = match @@ -187,21 +188,29 @@ end = struct Some [ { Lang.Diagnostic.FailedRequire.prefix = from; refs } ] | _ -> None in - Some { Lang.Diagnostic.Data.sentenceRange; failedRequire } + Some { Lang.Diagnostic.Data.sentenceRange; failedRequire; quickFix } - let extra_diagnostics_of_ast stm_range ast = + let extra_diagnostics_of_ast qf stm_range ast = if !Config.v.send_diags_extra_data then - extra_diagnostics_of_ast stm_range ast + extra_diagnostics_of_ast qf stm_range ast else None - let error ~err_range ~msg ~stm_range ?ast () = - let data = extra_diagnostics_of_ast stm_range ast in + let error ~err_range ~quickFix ~msg ~stm_range ?ast () = + let data = extra_diagnostics_of_ast quickFix stm_range ast in make ?data err_range Lang.Diagnostic.Severity.error msg let of_feed ~drange (severity, payload) = - let { Coq.Message.Payload.range; msg } = payload in + let { Coq.Message.Payload.range; quickFix; msg } = payload in let range = Option.default drange range in - make range severity msg + (* Be careful to avoid defining data if quickFix = None *) + let data = + Option.map + (fun qf -> + let sentenceRange, failedRequire, quickFix = (None, None, Some qf) in + Lang.Diagnostic.Data.{ sentenceRange; failedRequire; quickFix }) + quickFix + in + make ?data range severity msg type partition_kind = | Left @@ -400,8 +409,8 @@ let handle_doc_creation_exec ~token ~env ~uri ~version ~contents = let message = "Document Creation Interrupted!" in let range = None in error_doc ~range ~message ~uri ~version ~contents ~env - | Completed (Error (User { range; msg = err_msg })) - | Completed (Error (Anomaly { range; msg = err_msg })) -> + | Completed (Error (User { range; msg = err_msg; quickFix = _ })) + | Completed (Error (Anomaly { range; msg = err_msg; quickFix = _ })) -> let message = Format.asprintf "Doc.create, internal error: @[%a@]" Pp.pp_with err_msg in @@ -663,6 +672,7 @@ end = struct | Completed (Ok st) -> st | Completed (Error _) -> st end +(* end [module Recovery = struct...] *) let interp_and_info ~token ~st ~files ast = match Coq.Ast.Require.extract ast with @@ -753,22 +763,23 @@ let parse_action ~token ~lines ~st last_tok doc_handle = | Ok (Some ast) -> let () = if Debug.parsing then DDebug.parsed_sentence ~ast in (Process ast, [], feedback, time) - | Error (Anomaly { msg; _ }) | Error (User { range = None; msg }) -> + | Error (Anomaly { range = _; quickFix; msg }) + | Error (User { range = None; quickFix; msg }) -> (* We don't have a better alternative :(, usually missing error loc here means an anomaly, so we stop *) let err_range = last_tok in let parse_diags = - [ Diags.error ~err_range ~msg ~stm_range:err_range () ] + [ Diags.error ~err_range ~quickFix ~msg ~stm_range:err_range () ] in (EOF (Failed last_tok), parse_diags, feedback, time) - | Error (User { range = Some err_range; msg }) -> + | Error (User { range = Some err_range; quickFix; msg }) -> Coq.Parsing.discard_to_dot doc_handle; let last_tok = Coq.Parsing.Parsable.loc doc_handle in let last_tok_range = Coq.Utils.to_range ~lines last_tok in let span_loc = Util.build_span start_loc last_tok in let span_range = Coq.Utils.to_range ~lines span_loc in let parse_diags = - [ Diags.error ~err_range ~msg ~stm_range:span_range () ] + [ Diags.error ~err_range ~quickFix ~msg ~stm_range:span_range () ] in (Skip (span_range, last_tok_range), parse_diags, feedback, time)) @@ -820,10 +831,13 @@ let node_of_coq_result ~token ~doc ~range ~prev ~ast ~st ~parsing_diags ~diags:[] ~feedback ~info in Continue { state; last_tok; node } - | Error (Coq.Protect.Error.Anomaly { range = err_range; msg } as coq_err) - | Error (User { range = err_range; msg } as coq_err) -> + | Error + (Coq.Protect.Error.Anomaly { range = err_range; quickFix; msg } as coq_err) + | Error (User { range = err_range; quickFix; msg } as coq_err) -> let err_range = Option.default range err_range in - let err_diags = [ Diags.error ~err_range ~msg ~stm_range:range ~ast () ] in + let err_diags = + [ Diags.error ~err_range ~quickFix ~msg ~stm_range:range ~ast () ] + in let contents, nodes = (doc.contents, doc.nodes) in let context = Recovery_context.make ~contents ~last_tok ~nodes ~ast:ast.v () diff --git a/lang/diagnostic.ml b/lang/diagnostic.ml index db01508ce..f88f4902f 100644 --- a/lang/diagnostic.ml +++ b/lang/diagnostic.ml @@ -15,6 +15,7 @@ module Data = struct type t = { sentenceRange : Range.t option [@default None] ; failedRequire : FailedRequire.t list option [@default None] + ; quickFix : Range.t Qf.t list option [@default None] } end diff --git a/lang/diagnostic.mli b/lang/diagnostic.mli index 1087171f4..7368ab860 100644 --- a/lang/diagnostic.mli +++ b/lang/diagnostic.mli @@ -15,6 +15,7 @@ module Data : sig type t = { sentenceRange : Range.t option [@default None] ; failedRequire : FailedRequire.t list option [@default None] + ; quickFix : Range.t Qf.t list option [@default None] } end diff --git a/lang/qf.ml b/lang/qf.ml new file mode 100644 index 000000000..15d645934 --- /dev/null +++ b/lang/qf.ml @@ -0,0 +1,12 @@ +(************************************************************************) +(* Flèche => document manager: Language Support *) +(* Copyright 2019-2024 Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Written by: Emilio J. Gallego Arias *) +(************************************************************************) + +type 'l t = + { range : 'l + ; newText : string + } + +let map ~f { range; newText } = { range = f range; newText } diff --git a/lang/qf.mli b/lang/qf.mli new file mode 100644 index 000000000..c3965d045 --- /dev/null +++ b/lang/qf.mli @@ -0,0 +1,12 @@ +(************************************************************************) +(* Flèche => document manager: Language Support *) +(* Copyright 2019-2024 Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Written by: Emilio J. Gallego Arias *) +(************************************************************************) + +type 'l t = + { range : 'l + ; newText : string + } + +val map : f:('l -> 'm) -> 'l t -> 'm t diff --git a/lsp/core.ml b/lsp/core.ml index 7284656ce..24799f4c5 100644 --- a/lsp/core.ml +++ b/lsp/core.ml @@ -177,3 +177,33 @@ module DocumentDiagnosticReportPartialResult = struct } [@@deriving to_yojson] end + +(* CodeAction *) +module CodeActionContext = struct + type t = + { diagnostics : Lang.Diagnostic.t list + ; only : string option [@default None] + ; triggerKind : int option [@default None] + } + [@@deriving to_yojson] +end + +module CodeActionParams = struct + type t = + { textDocument : Doc.TextDocumentIdentifier.t + ; range : Lang.Range.t + ; context : CodeActionContext.t + } + [@@deriving to_yojson] +end + +module CodeAction = struct + type t = + { title : string + ; kind : string option [@default None] + ; diagnostics : Lang.Diagnostic.t list [@default []] + ; isPreferred : bool option [@default None] + ; edit : Workspace.WorkspaceEdit.t option [@default None] + } + [@@deriving to_yojson] +end diff --git a/lsp/core.mli b/lsp/core.mli index ae706ef89..c222d34eb 100644 --- a/lsp/core.mli +++ b/lsp/core.mli @@ -180,3 +180,33 @@ module DocumentDiagnosticReportPartialResult : sig } [@@deriving to_yojson] end + +(* CodeAction *) +module CodeActionContext : sig + type t = + { diagnostics : Lang.Diagnostic.t list + ; only : string option [@default None] + ; triggerKind : int option [@default None] + } + [@@deriving to_yojson] +end + +module CodeActionParams : sig + type t = + { textDocument : Doc.TextDocumentIdentifier.t + ; range : Lang.Range.t + ; context : CodeActionContext.t + } + [@@deriving to_yojson] +end + +module CodeAction : sig + type t = + { title : string + ; kind : string option [@default None] + ; diagnostics : Lang.Diagnostic.t list [@default []] + ; isPreferred : bool option [@default None] + ; edit : Workspace.WorkspaceEdit.t option [@default None] + } + [@@deriving to_yojson] +end diff --git a/lsp/jCoq.ml b/lsp/jCoq.ml index 3497091a1..fabdda660 100644 --- a/lsp/jCoq.ml +++ b/lsp/jCoq.ml @@ -26,6 +26,7 @@ let rec pp_opt d = module Pp = struct include Serlib.Ser_pp + let str = Pp.str let string_of_ppcmds = Pp.string_of_ppcmds let to_string = Pp.string_of_ppcmds let to_yojson x = to_yojson (pp_opt x) diff --git a/lsp/jLang.ml b/lsp/jLang.ml index 631d902ab..a486ac030 100644 --- a/lsp/jLang.ml +++ b/lsp/jLang.ml @@ -34,6 +34,10 @@ module LUri = struct end end +module Qf = struct + type 'l t = [%import: 'l Lang.Qf.t] [@@deriving yojson] +end + module Diagnostic = struct module Libnames = Serlib.Ser_libnames @@ -44,6 +48,7 @@ module Diagnostic = struct module Data = struct module Lang = struct module Range = Range + module Qf = Qf module FailedRequire = FailedRequire module Diagnostic = Lang.Diagnostic end @@ -61,6 +66,7 @@ module Diagnostic = struct [@@deriving yojson] let conv { Lang.Point.line; character; offset = _ } = { line; character } + let vnoc { line; character } = { Lang.Point.line; character; offset = -1 } end module Range = struct @@ -74,6 +80,11 @@ module Diagnostic = struct let start = Point.conv start in let end_ = Point.conv end_ in { start; end_ } + + let vnoc { start; end_ } = + let start = Point.vnoc start in + let end_ = Point.vnoc end_ in + { Lang.Range.start; end_ } end (* Current Flèche diagnostic is not LSP-standard compliant, this one is *) @@ -91,6 +102,14 @@ module Diagnostic = struct let range = Range.conv range in let message = Pp.to_string message in _t_to_yojson { range; severity; message; data } + + let of_yojson json = + match _t_of_yojson json with + | Ok { range; severity; message; data } -> + let range = Range.vnoc range in + let message = Pp.str message in + Ok { Lang.Diagnostic.range; severity; message; data } + | Error err -> Error err end module Stdlib = JStdlib diff --git a/lsp/jLang.mli b/lsp/jLang.mli index 2b59f7b82..11b624c06 100644 --- a/lsp/jLang.mli +++ b/lsp/jLang.mli @@ -20,7 +20,7 @@ module LUri : sig end module Diagnostic : sig - type t = Lang.Diagnostic.t [@@deriving to_yojson] + type t = Lang.Diagnostic.t [@@deriving yojson] module Point : sig type t = @@ -36,6 +36,8 @@ module Diagnostic : sig ; end_ : Point.t [@key "end"] } [@@deriving yojson] + + val vnoc : t -> Lang.Range.t end end diff --git a/lsp/workspace.ml b/lsp/workspace.ml index d457453f6..912037eeb 100644 --- a/lsp/workspace.ml +++ b/lsp/workspace.ml @@ -4,6 +4,7 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) +module Lang_ = Lang module Lang = JLang module WorkspaceFolder = struct @@ -25,3 +26,23 @@ end module DidChangeWorkspaceFoldersParams = struct type t = { event : WorkspaceFoldersChangeEvent.t } [@@deriving yojson] end + +module TextEdit = struct + type t = + { range : Lang.Range.t + ; newText : string + } + [@@deriving yojson] +end + +module WorkspaceEdit = struct + type t = { changes : (Lang.LUri.File.t * TextEdit.t list) list } + [@@deriving of_yojson] + + let tok (uri, edits) = + ( Lang_.LUri.File.to_string_uri uri + , `List (List.map TextEdit.to_yojson edits) ) + + let to_yojson { changes } = + `Assoc [ ("changes", `Assoc (List.map tok changes)) ] +end diff --git a/lsp/workspace.mli b/lsp/workspace.mli index f8b856338..ae684d56f 100644 --- a/lsp/workspace.mli +++ b/lsp/workspace.mli @@ -23,3 +23,16 @@ end module DidChangeWorkspaceFoldersParams : sig type t = { event : WorkspaceFoldersChangeEvent.t } [@@deriving yojson] end + +module TextEdit : sig + type t = + { range : Lang.Range.t + ; newText : string + } + [@@deriving yojson] +end + +module WorkspaceEdit : sig + type t = { changes : (Lang.LUri.File.t * TextEdit.t list) list } + [@@deriving yojson] +end From fcf29e6c3a3ba38dd184a95ee108d16cfabcab81 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 29 Sep 2024 22:38:34 +0200 Subject: [PATCH 13/22] [coq] make `Protect.E.t` private. Just a nit really. --- coq/protect.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/coq/protect.mli b/coq/protect.mli index cfbd6595a..6868a6ad8 100644 --- a/coq/protect.mli +++ b/coq/protect.mli @@ -28,7 +28,7 @@ module R : sig end module E : sig - type ('a, 'l) t = + type ('a, 'l) t = private { r : ('a, 'l) R.t ; feedback : 'l Message.t list } From 76cdf49eabe4267a2fad07def81a0eca93a6d7bd Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 29 Sep 2024 16:18:10 +0200 Subject: [PATCH 14/22] [codeAction] Improvements in efficiency and correctness --- controller/rq_action.ml | 79 ++++++++++++++++++++++++----------------- 1 file changed, 46 insertions(+), 33 deletions(-) diff --git a/controller/rq_action.ml b/controller/rq_action.ml index 4108e1659..8e9563992 100644 --- a/controller/rq_action.ml +++ b/controller/rq_action.ml @@ -1,8 +1,3 @@ -let dqf (d : Lang.Diagnostic.t) : _ option = - Option.bind d.data (function - | { Lang.Diagnostic.Data.quickFix = Some qf; _ } -> Some (d, qf) - | _ -> None) - let point_lt { Lang.Point.line = l1; Lang.Point.character = c1; offset = _ } { Lang.Point.line = l2; Lang.Point.character = c2; offset = _ } = l1 < l2 || (l1 = l2 && c1 < c2) @@ -11,41 +6,59 @@ let point_gt { Lang.Point.line = l1; Lang.Point.character = c1; offset = _ } { Lang.Point.line = l2; Lang.Point.character = c2; offset = _ } = l1 > l2 || (l1 = l2 && c1 > c2) -let get_qf ~range (doc : Fleche.Doc.t) = - let diags = - List.filter_map - (fun (node : Fleche.Doc.Node.t) -> - let open Lang.Range in - (* let open Lang.Point in *) - let nrange = node.range in - if point_lt nrange.end_ range.start || point_gt nrange.start range.end_ - then None - else Some node.diags) - doc.nodes - |> List.concat +(* To move to doc.ml *) +let filter_map_range ~range ~nodes ~f = + let rec aux (nodes : Fleche.Doc.Node.t list) acc = + match nodes with + | [] -> List.rev acc + | node :: nodes -> ( + let open Lang.Range in + let nrange = node.range in + if point_lt nrange.end_ range.start then aux nodes acc + else if point_gt nrange.start range.end_ then List.rev acc + else + (* Node in scope *) + match f node with + | Some res -> aux nodes (res :: acc) + | None -> aux nodes acc) in - List.filter_map dqf diags + aux nodes [] + +(* util *) +let filter_map_cut f l = + match List.filter_map f l with + | [] -> None + | res -> Some res + +(* Return list of pairs of diags, qf *) +let get_qf (d : Lang.Diagnostic.t) : _ option = + Option.bind d.data (function + | { Lang.Diagnostic.Data.quickFix = Some qf; _ } -> Some (d, qf) + | _ -> None) + +let get_qfs ~range (doc : Fleche.Doc.t) = + let f { Fleche.Doc.Node.diags; _ } = filter_map_cut get_qf diags in + filter_map_range ~range ~nodes:doc.nodes ~f |> List.concat let request ~range ~token:_ ~(doc : Fleche.Doc.t) = let kind = Some "quickfix" in let isPreferred = Some true in - let qf = get_qf ~range doc in + let qf = get_qfs ~range doc in let bf (d, qf) = - let mm = - match qf with - | [ q ] -> q.Lang.Qf.newText - | _ -> "correct code" - in - let title = "Replace with " ^ mm in - let diagnostics = [ d ] in - let qff { Lang.Qf.range; newText } = - Lsp.Workspace.TextEdit.{ range; newText } - in - let changes = [ (doc.uri, List.map qff qf) ] in - let edit = Some Lsp.Workspace.WorkspaceEdit.{ changes } in - Lsp.Core.CodeAction.{ title; kind; diagnostics; isPreferred; edit } + List.map + (fun { Lang.Qf.range; newText } -> + let oldText = + Fleche.Contents.extract_raw ~contents:doc.contents ~range + in + let title = Format.asprintf "Replace `%s` by `%s`" oldText newText in + let diagnostics = [ d ] in + let qf = [ Lsp.Workspace.TextEdit.{ range; newText } ] in + let changes = [ (doc.uri, qf) ] in + let edit = Some Lsp.Workspace.WorkspaceEdit.{ changes } in + Lsp.Core.CodeAction.{ title; kind; diagnostics; isPreferred; edit }) + qf in - List.map bf qf + List.concat_map bf qf let request ~range ~token ~(doc : Fleche.Doc.t) = let res = request ~range ~token ~doc in From d54663d0c27c6861b760129a95e0ae7aaf5e7d60 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 29 Sep 2024 17:05:19 +0200 Subject: [PATCH 15/22] [examples] [codeAction] Examples for coq/coq#19618 --- examples/codeAction.v | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/examples/codeAction.v b/examples/codeAction.v index aea7a3255..e56fd4021 100644 --- a/examples/codeAction.v +++ b/examples/codeAction.v @@ -1,3 +1,12 @@ +(* Test for Coq's QF for Coq to Stdlib PRs *) + +Require Import Coq.ssr.ssrbool. +From Coq Require Import ssreflect ssrbool. + +(* Note: this tests the two different lookup modes *) +About Coq.Init.Nat.add. +Check Coq.Init.Nat.add. + (* Example codeAction, from Coq's test suite *) Module M. Definition y := 4. End M. @@ -42,3 +51,4 @@ Require Import Extraction. Module nat. End nat. Extraction nat. + From 5ef11594c490d869ac21cf6d4ec50e572a97cfea Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 29 Sep 2024 18:50:08 +0200 Subject: [PATCH 16/22] [examples] Update Pff.v for Coq master --- examples/Pff.v | 26 ++++++++++++++++++++------ 1 file changed, 20 insertions(+), 6 deletions(-) diff --git a/examples/Pff.v b/examples/Pff.v index 252b89f3b..3db572bd1 100644 --- a/examples/Pff.v +++ b/examples/Pff.v @@ -14,7 +14,7 @@ Require Import Psatz. Set Warnings "-deprecated". (* Compatibility workaround, remove once requiring Coq >= 8.16 *) -Module Import Compat. +Module Import Compat816. Lemma Even_0 : Nat.Even 0. Proof. exists 0; reflexivity. Qed. @@ -67,7 +67,21 @@ Proof proj1 (proj1 (Even_Odd_double n)). Definition Odd_double n : Nat.Odd n -> n = S (Nat.double (Nat.div2 n)). Proof proj1 (proj2 (Even_Odd_double n)). -End Compat. +Definition Rinv_mult_distr := Rinv_mult_distr. +Definition Rabs_Rinv := Rabs_Rinv. +Definition Rinv_pow := Rinv_pow. +Definition Rinv_involutive := Rinv_involutive. +Definition Rlt_Rminus := Rlt_Rminus. +Definition powerRZ_inv := powerRZ_inv. +Definition powerRZ_neg := powerRZ_neg. + +End Compat816. + +Module Import Compat819. + +Definition IZR_neq := IZR_neq. + +End Compat819. (*** was file sTactic.v ***) @@ -17553,7 +17567,7 @@ apply Z.le_trans with (Nat.double (Nat.div2 t)). unfold Nat.double; rewrite inj_plus; auto with zarith. rewrite <- Even_double; auto with zarith. apply Z.le_trans with (-1+(S ( Nat.double (Nat.div2 t))))%Z. -rewrite inj_S; unfold Z.succ; auto with zarith. +rewrite inj_S; unfold Z.succ; auto with zarith; unfold Nat.double; rewrite inj_plus; auto with zarith. rewrite <- Odd_double by easy. lia. Qed. @@ -17568,9 +17582,9 @@ case (Nat.Even_or_Odd t); intros I. apply Z.le_trans with ((Nat.double (Nat.div2 t)+1))%Z. 2:unfold Nat.double; rewrite inj_plus; auto with zarith. rewrite <- Even_double; auto with zarith. -apply Z.le_trans with ((S ( Nat.double (Nat.div2 t))))%Z; auto with zarith. -2: rewrite inj_S; unfold Z.succ; auto with zarith. -2: unfold Nat.double; rewrite inj_plus; auto with zarith. +apply Z.le_trans with ((S ( Nat.double (Nat.div2 t))))%Z; auto with zarith; +try solve [rewrite inj_S; unfold Z.succ; auto with zarith; + unfold Nat.double; rewrite inj_plus; auto with zarith]. rewrite <- Odd_double; auto with zarith. Qed. From 5f915de1f746fe1fbaf068ccad1d5496e2cdd2be Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 3 Oct 2024 18:01:48 +0200 Subject: [PATCH 17/22] [changes] Changes for `codeAction` support. --- CHANGES.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index 93b4e5603..00a2858af 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -36,6 +36,8 @@ see some motivation for that (@ejgallego, #841) - [lsp] [diagnostics] (! breaking change) change type of diagnostics extra data from list to named record (@ejgallego, #843) + - [lsp] Implement support for `textDocument/codeAction`. For now, we + support Coq's 8.21 `quickFix` data (@ejgallego, #840, #843, #845) # coq-lsp 0.2.0: From Green to Blue ----------------------------------- From 97f6d53e8399f72854fe3b1ef70b461d5c6411e0 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 4 Oct 2024 16:15:17 +0200 Subject: [PATCH 18/22] [petanque] Pass SO_REUSE to TCP bind. This is convenient in some testing scenarios. Co-authored-by: Guillaume Baudart --- petanque/json_shell/server.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/petanque/json_shell/server.ml b/petanque/json_shell/server.ml index e59172fbb..4bc765db3 100644 --- a/petanque/json_shell/server.ml +++ b/petanque/json_shell/server.ml @@ -48,6 +48,11 @@ let accept_connection ~token conn = let create_socket ~address ~port ~backlog = let open Lwt_unix in let sock = socket PF_INET SOCK_STREAM 0 in + (* It is sometimes more convenient to allow pet-server to shadow a kind of + crashed one, so we allow to rebind the socket. It could be convenient at + some point to guard this over a command-line flag *) + let () = setsockopt sock SO_REUSEADDR true in + let () = setsockopt sock SO_REUSEPORT true in ( bind sock @@ ADDR_INET (Unix.inet_addr_of_string address, port) |> fun x -> ignore x ); listen sock backlog; From 3e9309dd5a576f34bf6bee4fb89c72f1d5af34c3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 4 Oct 2024 16:34:54 +0200 Subject: [PATCH 19/22] [petanque] Fix bug for detection of proof finished in deep stacks Co-authored-by: Guillaume Baudart --- CHANGES.md | 2 ++ petanque/agent.ml | 5 ++++- petanque/test/basic_api.ml | 38 ++++++++++++++++++++++++++++++++------ petanque/test/test.v | 10 ++++++++++ 4 files changed, 48 insertions(+), 7 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 00a2858af..e2568d5cd 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -38,6 +38,8 @@ extra data from list to named record (@ejgallego, #843) - [lsp] Implement support for `textDocument/codeAction`. For now, we support Coq's 8.21 `quickFix` data (@ejgallego, #840, #843, #845) + - [petanque] Fix bug for detection of proof finished in deep stacks + (@ejgallego, @gbdrt, #847) # coq-lsp 0.2.0: From Green to Blue ----------------------------------- diff --git a/petanque/agent.ml b/petanque/agent.ml index 320b890dd..cbf182b58 100644 --- a/petanque/agent.ml +++ b/petanque/agent.ml @@ -144,7 +144,10 @@ let protect_to_result (r : _ Coq.Protect.E.t) : (_, _) Result.t = | { r = Completed (Ok r); feedback = _ } -> Ok r let proof_finished { Coq.Goals.goals; stack; shelf; given_up; _ } = - List.for_all CList.is_empty [ goals; shelf; given_up ] && CList.is_empty stack + let check_stack stack = + CList.(for_all (fun (l, r) -> is_empty l && is_empty r)) stack + in + List.for_all CList.is_empty [ goals; shelf; given_up ] && check_stack stack (* At some point we want to return both hashes *) module Hash_kind = struct diff --git a/petanque/test/basic_api.ml b/petanque/test/basic_api.ml index a54eb6f2e..d4f7d865e 100644 --- a/petanque/test/basic_api.ml +++ b/petanque/test/basic_api.ml @@ -17,7 +17,7 @@ let trace hdr ?extra:_ msg = let message ~lvl:_ ~message = msgs := message :: !msgs let dump_msgs () = List.iter (Format.eprintf "%s@\n") (List.rev !msgs) -let start ~token = +let init ~token = let debug = false in Shell.trace_ref := trace; Shell.message_ref := message; @@ -30,19 +30,17 @@ let start ~token = let* () = Shell.set_workspace ~token ~debug ~root in (* Careful to call [build_doc] before we have set an environment! [pet] and [pet-server] are careful to always set a default one *) - let* doc = Shell.build_doc ~token ~uri in - Agent.start ~token ~doc ~thm:"rev_snoc_cons" () + Shell.build_doc ~token ~uri let extract_st { Agent.Run_result.st; _ } = st -let main () = +let snoc_test ~token ~doc = let open Coq.Compat.Result.O in - let token = Coq.Limits.create_atomic () in let r ~st ~tac = let st = extract_st st in Agent.run ~token ~st ~tac () in - let* { st; _ } = start ~token in + let* { st; _ } = Agent.start ~token ~doc ~thm:"rev_snoc_cons" () in let* _premises = Agent.premises ~token ~st in let* st = Agent.run ~token ~st ~tac:"induction l." () in let h1 = Agent.State.hash st.st in @@ -58,6 +56,34 @@ let main () = let* st = r ~st ~tac:"Qed." in Agent.goals ~token ~st:(extract_st st) +let finished_stack ~token ~doc = + let open Coq.Compat.Result.O in + let r ~st ~tac = + let st = extract_st st in + Agent.run ~token ~st ~tac () + in + let* { st; _ } = Agent.start ~token ~doc ~thm:"deepBullet" () in + let* st = Agent.run ~token ~st ~tac:"split." () in + let* st = r ~st ~tac:"-" in + let* st = r ~st ~tac:"now reflexivity." in + let* st = r ~st ~tac:"-" in + let* st = r ~st ~tac:"split." in + let* st = r ~st ~tac:"+" in + let* st = r ~st ~tac:"now reflexivity." in + let* st = r ~st ~tac:"+" in + let* { st; proof_finished; _ } = r ~st ~tac:"now reflexivity." in + (* Check that we properly detect no goals with deep stacks. *) + assert proof_finished; + let* st = Agent.run ~token ~st ~tac:"Qed." () in + Agent.goals ~token ~st:(extract_st st) + +let main () = + let open Coq.Compat.Result.O in + let token = Coq.Limits.create_atomic () in + let* doc = init ~token in + let* _goals = snoc_test ~token ~doc in + finished_stack ~token ~doc + let check_no_goals = function | Error err -> Format.eprintf "error: in execution: %s@\n%!" (Agent.Error.to_string err); diff --git a/petanque/test/test.v b/petanque/test/test.v index cf5ed8281..068876ebd 100644 --- a/petanque/test/test.v +++ b/petanque/test/test.v @@ -8,3 +8,13 @@ Proof. - reflexivity. - simpl. rewrite IHl. simpl. reflexivity. Qed. + +(* This is for testing proof finished *) +Lemma deepBullet : (1 = 1) /\ (21 = 21 /\ 22 = 22). +Proof. +split. +- now reflexivity. +- split. + + now reflexivity. + + now reflexivity. +Qed. From 81b8914f7828881d6b186f46b466cf0bbddb24d4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 18 Sep 2024 17:23:56 +0200 Subject: [PATCH 20/22] [goals] Allow `command` to process several Coq commands. This is a prototype extension. Note the important change here in behavior here, but IMHO it is needed: if the commands in `command` fail, we will now fail the request. I think in general we may allow some form of error recovery here, but for now we just let clients recover. It does seem that CoqPilot / Pytanque do need even a more powerful interface, but this will allow the them to make some progress for nwo. Thanks to CoqPilot devs for feedback on this. --- CHANGES.md | 6 ++++++ controller/rq_goals.ml | 17 +---------------- etc/doc/PROTOCOL.md | 9 ++++++++- fleche/doc.ml | 31 ++++++++++++++++++++++++++++++ fleche/doc.mli | 18 ++++++++++++++++++ petanque/agent.ml | 39 ++++++++++---------------------------- petanque/test/basic_api.ml | 35 ++++++++++++++++++++++++++-------- 7 files changed, 101 insertions(+), 54 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index e2568d5cd..572b18a0f 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -40,6 +40,12 @@ support Coq's 8.21 `quickFix` data (@ejgallego, #840, #843, #845) - [petanque] Fix bug for detection of proof finished in deep stacks (@ejgallego, @gbdrt, #847) + - [goals request] allow multiple Coq sentences in `command`. This is + backwards compatible in the case that commands do not error, and + users were sending just one command. (@ejgallego, #823, thanks to + CoqPilot devs and G. Baudart for feedback) + - [goals request] (! breaking) fail the request if the commands in + `command` fail (@ejgallego, #823) # coq-lsp 0.2.0: From Green to Blue ----------------------------------- diff --git a/controller/rq_goals.ml b/controller/rq_goals.ml index fa1cb1421..e6b5a93c0 100644 --- a/controller/rq_goals.ml +++ b/controller/rq_goals.ml @@ -31,25 +31,10 @@ let pp ~pp_format pp = | Pp -> Lsp.JCoq.Pp.to_yojson pp | Str -> `String (Pp.string_of_ppcmds pp) -let parse ~token ~loc tac st = - let str = Gramlib.Stream.of_string tac in - let str = Coq.Parsing.Parsable.make ?loc str in - Coq.Parsing.parse ~token ~st str - -let parse_and_execute_in ~token ~loc tac st = - let open Coq.Protect.E.O in - let* ast = parse ~token ~loc tac st in - match ast with - | Some ast -> Fleche.Memo.Interp.eval ~token (st, ast) - (* On EOF we return the previous state, the command was the empty string or a - comment *) - | None -> Coq.Protect.E.ok st - let run_pretac ~token ~loc ~st pretac = match pretac with | None -> Coq.Protect.E.ok st - | Some tac -> - Coq.State.in_stateM ~token ~st ~f:(parse_and_execute_in ~token ~loc tac) st + | Some tac -> Fleche.Doc.run ~token ?loc ~st tac let get_goal_info ~token ~doc ~point ~mode ~pretac () = let open Fleche in diff --git a/etc/doc/PROTOCOL.md b/etc/doc/PROTOCOL.md index 6b167e774..4a77e4bfd 100644 --- a/etc/doc/PROTOCOL.md +++ b/etc/doc/PROTOCOL.md @@ -187,12 +187,19 @@ interface GoalRequest { textDocument: VersionedTextDocumentIdentifier; position: Position; pp_format?: 'Pp' | 'Str'; - pretac?: string; command?: string; mode?: 'Prev' | 'After'; } ``` +The first parameters are standard, `pp_format` controls the pretty +printing format used in the results. + +The `command` parameter (experimental), is a list of Coq commands that +will be run just _after_ `position` in `textDocument`, but _before_ +goals are sent to the user. This is often useful for ephemeral +post-processing. + Answer to the request is a `Goal[]` object, where ```typescript diff --git a/fleche/doc.ml b/fleche/doc.ml index bb06a0cc5..1e3d7fce3 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -1094,3 +1094,34 @@ let save ~token ~doc = | _ -> let error = Pp.(str "Can't save document that failed to check") in Coq.Protect.E.error error + +(* run api, experimental *) + +(* Adaptor, should be supported in memo directly *) +let eval_no_memo ~token (st, cmd) = + Coq.Interp.interp ~token ~intern:Vernacinterp.fs_intern ~st cmd + +(* TODO, what to do with feedback, what to do with errors *) +let rec parse_execute_loop ~token ~memo pa st = + let open Coq.Protect.E.O in + let eval = if memo then Memo.Interp.eval else eval_no_memo in + let* ast = Coq.Parsing.parse ~token ~st pa in + match ast with + | Some ast -> ( + match eval ~token (st, ast) with + | Coq.Protect.E.{ r = Coq.Protect.R.Completed (Ok st); feedback = _ } -> + parse_execute_loop ~token ~memo pa st + | res -> res) + (* On EOF we return the previous state, the command was the empty string or a + comment *) + | None -> Coq.Protect.E.ok st + +let parse_and_execute_in ~token ~loc tac st = + let str = Gramlib.Stream.of_string tac in + let pa = Coq.Parsing.Parsable.make ?loc str in + parse_execute_loop ~token pa st + +let run ~token ?loc ?(memo = true) ~st cmds = + Coq.State.in_stateM ~token ~st + ~f:(parse_and_execute_in ~token ~loc ~memo cmds) + st diff --git a/fleche/doc.mli b/fleche/doc.mli index ff2a0c247..540ea890c 100644 --- a/fleche/doc.mli +++ b/fleche/doc.mli @@ -137,3 +137,21 @@ val check : (** [save ~doc] will save [doc] .vo file. It will fail if proofs are open, or if the document completion status is not [Yes] *) val save : token:Coq.Limits.Token.t -> doc:t -> (unit, Loc.t) Coq.Protect.E.t + +(** [run ~token ?loc ?memo ~st cmds] run commands [cmds] starting on state [st], + without commiting changes to the document. [loc] can be used to seed an + initial location if desired, if not the locations will be considered + relative to the initial location. [memo] controls if the execution is + memoized, by default [true]. + + This API is experimental, used for speculative execution + [petanque + and goals], the API is expected to change as to better adapt + to users. *) +val run : + token:Coq.Limits.Token.t + -> ?loc:Loc.t + -> ?memo:bool + -> st:Coq.State.t + -> string + -> (Coq.State.t, Loc.t) Coq.Protect.E.t diff --git a/petanque/agent.ml b/petanque/agent.ml index cbf182b58..58ab3b20d 100644 --- a/petanque/agent.ml +++ b/petanque/agent.ml @@ -106,30 +106,12 @@ let find_thm ~(doc : Fleche.Doc.t) ~thm = (* let point = (range.start.line, range.start.character) in *) Ok node -let parse ~loc tac st = - let str = Gramlib.Stream.of_string tac in - let str = Coq.Parsing.Parsable.make ?loc str in - Coq.Parsing.parse ~st str - -(* Adaptor, should be supported in memo directly *) -let eval_no_memo ~token (st, cmd) = - Coq.Interp.interp ~token ~intern:Vernacinterp.fs_intern ~st cmd - -let parse_and_execute_in ~token ~loc ~memo tac st = - (* To improve in memo *) - let eval = if memo then Fleche.Memo.Interp.eval else eval_no_memo in - let open Coq.Protect.E.O in - let* ast = parse ~token ~loc tac st in - match ast with - | Some ast -> eval ~token (st, ast) - | None -> Coq.Protect.E.ok st - let execute_precommands ~token ~memo ~pre_commands ~(node : Fleche.Doc.Node.t) = match (pre_commands, node.prev, node.ast) with | Some pre_commands, Some prev, Some ast -> let st = prev.state in let open Coq.Protect.E.O in - let* st = parse_and_execute_in ~token ~memo ~loc:None pre_commands st in + let* st = Fleche.Doc.run ~token ~memo ?loc:None ~st pre_commands in (* We re-interpret the lemma statement *) Fleche.Memo.Interp.eval ~token (st, ast.v) | _, _, _ -> Coq.Protect.E.ok node.state @@ -180,32 +162,31 @@ let default_opts = function | None -> { Run_opts.memo = true; hash = true } | Some opts -> opts -(* XXX: EJGA, we should not need the [Coq.State.in_stateM] here and in run *) let start ~token ~doc ?opts ?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 f () = - let opts = default_opts opts in - let memo, hash = (opts.memo, opts.hash) in + let opts = default_opts opts in + let memo, hash = (opts.memo, opts.hash) in + let execution = let open Coq.Protect.E.O in let+ st = execute_precommands ~token ~memo ~pre_commands ~node in + (* Note this runs on the resulting state, anyways it is purely functional *) analyze_after_run ~hash st in - let st = node.state in - Coq.State.in_stateM ~token ~st ~f () |> protect_to_result + protect_to_result execution let run ~token ?opts ~st ~tac () : (_ Run_result.t, Error.t) Result.t = let opts = default_opts opts in (* Improve with thm? *) - let loc = None in let memo, hash = (opts.memo, opts.hash) in - let f st = + let execution = let open Coq.Protect.E.O in - let+ st = parse_and_execute_in ~token ~memo ~loc tac st in + let+ st = Fleche.Doc.run ~token ~memo ?loc:None ~st tac in + (* Note this runs on the resulting state, anyways it is purely functional *) analyze_after_run ~hash st in - Coq.State.in_stateM ~token ~st ~f st |> protect_to_result + protect_to_result execution let goals ~token ~st = let f goals = diff --git a/petanque/test/basic_api.ml b/petanque/test/basic_api.ml index d4f7d865e..debbe7e7a 100644 --- a/petanque/test/basic_api.ml +++ b/petanque/test/basic_api.ml @@ -56,7 +56,7 @@ let snoc_test ~token ~doc = let* st = r ~st ~tac:"Qed." in Agent.goals ~token ~st:(extract_st st) -let finished_stack ~token ~doc = +let finished_stack_test ~token ~doc = let open Coq.Compat.Result.O in let r ~st ~tac = let st = extract_st st in @@ -77,22 +77,41 @@ let finished_stack ~token ~doc = let* st = Agent.run ~token ~st ~tac:"Qed." () in Agent.goals ~token ~st:(extract_st st) +let multi_shot_test ~token ~doc = + let open Coq.Compat.Result.O in + let* { st; _ } = Agent.start ~token ~doc ~thm:"rev_snoc_cons" () in + let* st = + Agent.run ~token ~st + ~tac:"induction l. idtac. - reflexivity. - now simpl; rewrite IHl. Qed." + () + in + Agent.goals ~token ~st:(extract_st st) + let main () = let open Coq.Compat.Result.O in let token = Coq.Limits.create_atomic () in let* doc = init ~token in - let* _goals = snoc_test ~token ~doc in - finished_stack ~token ~doc + let* g1 = snoc_test ~token ~doc in + let* g2 = finished_stack_test ~token ~doc in + let* g3 = multi_shot_test ~token ~doc in + Ok [ g1; g2; g3 ] + +let max = List.fold_left max min_int let check_no_goals = function | Error err -> Format.eprintf "error: in execution: %s@\n%!" (Agent.Error.to_string err); dump_msgs (); 129 - | Ok None -> 0 - | Ok (Some _goals) -> - dump_msgs (); - Format.eprintf "error: goals remaining@\n%!"; - 1 + | Ok glist -> + List.map + (function + | None -> 0 + | Some _goals -> + dump_msgs (); + Format.eprintf "error: goals remaining@\n%!"; + 1) + glist + |> max let () = main () |> check_no_goals |> exit From 013dc1a6b109fa61c2130e3d8e8055c856eea6cf Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 4 Oct 2024 17:15:20 +0200 Subject: [PATCH 21/22] [meta] Release 0.2.1 --- CHANGES.md | 4 +-- CONTRIBUTING.md | 2 +- editor/code/CHANGELOG.md | 55 +++++++++++++++++++++++++++++++++++ editor/code/package-lock.json | 4 +-- editor/code/package.json | 2 +- fleche/version.ml | 2 +- 6 files changed, 62 insertions(+), 7 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 572b18a0f..02f85218c 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,5 +1,5 @@ -# unreleased ------------- +# coq-lsp 0.2.1: Click ! +------------------------ - [deps] Bump toolchain so minimal `ppxlib` is 0.26, in order to fix some `ppx_import` oddities. This means our lower bound for the Jane diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 8255adc73..908bf9cc6 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -411,7 +411,7 @@ The checklist for the release as of today is the following: The above can be done with: ``` -export COQLSPV=0.2.0 +export COQLSPV=0.2.1 git checkout main && make && dune-release tag ${COQLSPV} git checkout v8.20 && git merge main && make && dune-release tag ${COQLSPV}+8.20 && dune-release git checkout v8.19 && git merge v8.20 && make && dune-release tag ${COQLSPV}+8.19 && dune-release diff --git a/editor/code/CHANGELOG.md b/editor/code/CHANGELOG.md index a85e940ab..a11be8f2b 100644 --- a/editor/code/CHANGELOG.md +++ b/editor/code/CHANGELOG.md @@ -1,3 +1,58 @@ +# coq-lsp 0.2.1: Click ! +------------------------ + + This release brings full Web Extension support for coq-lsp! + + You can now run Coq from your browser using https://vscode.dev or + https://github.dev . + + Some other highlights is `codeAction` support (for Coq quick fixes), + `Restart.` support, better API for our extension users, and many + bugfixes and improvements, in particular for `hover`. + + The detailed list of server and client changes is below: + + - [workspace] [coq] Support _CoqProject arguments `-type-in-type` and + `-allow-rewrite-rules` (for 8.20) (@ejgallego, #819) + - [serlib] Fix Ltac2 AST piercing bug, add test case that should help + in the future (@ejgallego, @jim-portegies, #821) + - [fleche] [8.20] understand rewrite rules and symbols on document + outline (@ejgallego, @Alizter, #825, fixes #824) + - [fleche] [coq] support `Restart` meta command (@ejgallego, + @Alizter, #828, fixes #827) + - [fleche] [plugins] New plugin example `explain_errors`, that will + print all errors on a file, with their goal context (@ejgallego, + #829, thanks to @gmalecha for the idea, c.f. Coq issue 19601) + - [fleche] Highlight the full first line of the document on + initialization error (@ejgallego, #832) + - [fleche] [jscoq] [js] Build worker version of `coq-lsp`. This + provides a full working Coq enviroment in `vscode.dev`. The web + worker version is build as an artifact on CI (@ejgallego + @corwin-of-amber, #433) + - [hover] Fix universe and level printing in hover (#839, fixes #835 + , @ejgallego , @Alizter) + - [fleche] New immediate request serving mode. In this mode, requests + are served with whatever document state we have. This is very + useful when we are not in continuous mode, and we don't have a good + reference as to what to build, for example in + `documentSymbols`. The mode actually works pretty well in practice + as often language requests will come after goals requests, so the + info that is needed is at hand. It could also be tried to set the + build target for immediate requests to the view hint, but we should + see some motivation for that (@ejgallego, #841) + - [lsp] [diagnostics] (! breaking change) change type of diagnostics + extra data from list to named record (@ejgallego, #843) + - [lsp] Implement support for `textDocument/codeAction`. For now, we + support Coq's 8.21 `quickFix` data (@ejgallego, #840, #843, #845) + - [petanque] Fix bug for detection of proof finished in deep stacks + (@ejgallego, @gbdrt, #847) + - [goals request] allow multiple Coq sentences in `command`. This is + backwards compatible in the case that commands do not error, and + users were sending just one command. (@ejgallego, #823, thanks to + CoqPilot devs and G. Baudart for feedback) + - [goals request] (! breaking) fail the request if the commands in + `command` fail (@ejgallego, #823) + # coq-lsp 0.2.0: From Green to Blue ----------------------------------- diff --git a/editor/code/package-lock.json b/editor/code/package-lock.json index ba496c85b..af119eb88 100644 --- a/editor/code/package-lock.json +++ b/editor/code/package-lock.json @@ -1,12 +1,12 @@ { "name": "coq-lsp", - "version": "0.2.0", + "version": "0.2.1", "lockfileVersion": 3, "requires": true, "packages": { "": { "name": "coq-lsp", - "version": "0.2.0", + "version": "0.2.1", "dependencies": { "@vscode/webview-ui-toolkit": "^1.2.2", "jquery": "^3.7.1", diff --git a/editor/code/package.json b/editor/code/package.json index 257aab11e..247188f09 100644 --- a/editor/code/package.json +++ b/editor/code/package.json @@ -2,7 +2,7 @@ "name": "coq-lsp", "displayName": "Coq LSP", "description": "Coq LSP provides native vsCode support for checking Coq proof documents", - "version": "0.2.0", + "version": "0.2.1", "contributors": [ "Emilio Jesús Gallego Arias ", "Ali Caglayan ", diff --git a/fleche/version.ml b/fleche/version.ml index 93c568871..c3a588d88 100644 --- a/fleche/version.ml +++ b/fleche/version.ml @@ -12,6 +12,6 @@ type t = string (************************************************************************) (* UPDATE VERSION HERE *) -let server = "0.2.0" +let server = "0.2.1" (* UPDATE VERSION HERE *) (************************************************************************) From 686aa26b19e14e64eb80e575e946f4e575a0ae04 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 4 Oct 2024 18:20:42 +0200 Subject: [PATCH 22/22] [vscode] Expand selectors to include `vscode-vfs://` URIs This is used in `github.dev`; we also document limited virtual workspace support. --- CHANGES.md | 7 +++++++ editor/code/CHANGELOG.md | 7 +++++++ editor/code/package-lock.json | 4 ++-- editor/code/package.json | 8 +++++++- editor/code/src/client.ts | 6 +++--- editor/code/src/config.ts | 8 ++++++++ fleche/version.ml | 2 +- 7 files changed, 35 insertions(+), 7 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 02f85218c..02225c39a 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,10 @@ +# coq-lsp 0.2.2: To Virtual or not To Virtual +--------------------------------------------- + + - [vscode] Expand selectors to include `vscode-vfs://` URIs used in + `github.dev`, document limited virtual workspace support in + `package.json` (@ejgallego, #849) + # coq-lsp 0.2.1: Click ! ------------------------ diff --git a/editor/code/CHANGELOG.md b/editor/code/CHANGELOG.md index a11be8f2b..0eab4ec0d 100644 --- a/editor/code/CHANGELOG.md +++ b/editor/code/CHANGELOG.md @@ -1,3 +1,10 @@ +# coq-lsp 0.2.2: To Virtual or not To Virtual +--------------------------------------------- + + - [vscode] Expand selectors to include `vscode-vfs://` URIs used in + `github.dev`, document limited virtual workspace support in + `package.json` (@ejgallego, #849) + # coq-lsp 0.2.1: Click ! ------------------------ diff --git a/editor/code/package-lock.json b/editor/code/package-lock.json index af119eb88..833da9cda 100644 --- a/editor/code/package-lock.json +++ b/editor/code/package-lock.json @@ -1,12 +1,12 @@ { "name": "coq-lsp", - "version": "0.2.1", + "version": "0.2.2", "lockfileVersion": 3, "requires": true, "packages": { "": { "name": "coq-lsp", - "version": "0.2.1", + "version": "0.2.2", "dependencies": { "@vscode/webview-ui-toolkit": "^1.2.2", "jquery": "^3.7.1", diff --git a/editor/code/package.json b/editor/code/package.json index 247188f09..de6ce5c0b 100644 --- a/editor/code/package.json +++ b/editor/code/package.json @@ -2,7 +2,7 @@ "name": "coq-lsp", "displayName": "Coq LSP", "description": "Coq LSP provides native vsCode support for checking Coq proof documents", - "version": "0.2.1", + "version": "0.2.2", "contributors": [ "Emilio Jesús Gallego Arias ", "Ali Caglayan ", @@ -32,6 +32,12 @@ "onLanguage:markdown", "onLanguage:latex" ], + "capabilities": { + "virtualWorkspaces": { + "supported": "limited", + "description": "File operations such as jump to definition are not supported in virtual workspaces. While almost fully functional, coq-lsp remains experiemental as a Web Extension." + } + }, "contributes": { "languages": [ { diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts index d8dbf3522..29faaf89f 100644 --- a/editor/code/src/client.ts +++ b/editor/code/src/client.ts @@ -210,7 +210,7 @@ export function activateCoqLSP( const initializationOptions: CoqLspServerConfig = configDidChange(wsConfig); const clientOptions: LanguageClientOptions = { - documentSelector: CoqSelector.local, + documentSelector: CoqSelector.owned, outputChannelName: "Coq LSP Server Events", revealOutputChannelOn: RevealOutputChannelOn.Info, initializationOptions, @@ -335,7 +335,7 @@ export function activateCoqLSP( let textDocument = { uri, version }; infoPanel.notifyLackOfVSLS(textDocument, position); return; - } else if (languages.match(CoqSelector.local, textEditor.document) < 1) + } else if (languages.match(CoqSelector.owned, textEditor.document) < 1) return; const kind = @@ -373,7 +373,7 @@ export function activateCoqLSP( if ( config.check_on_scroll && serverConfig.check_only_on_request && - languages.match(CoqSelector.local, evt.textEditor.document) > 0 && + languages.match(CoqSelector.owned, evt.textEditor.document) > 0 && evt.visibleRanges[0] ) { let uri = evt.textEditor.document.uri.toString(); diff --git a/editor/code/src/config.ts b/editor/code/src/config.ts index a55320fca..b72deadab 100644 --- a/editor/code/src/config.ts +++ b/editor/code/src/config.ts @@ -96,4 +96,12 @@ export namespace CoqSelector { export const vsls: TextDocumentFilter[] = all.map((selector) => { return { ...selector, scheme: "vsls" }; }); + + // Virtual workspaces such as github.dev + export const virtual: TextDocumentFilter[] = all.map((selector) => { + return { ...selector, scheme: "vscode-vfs" }; + }); + + // Files that are owned by our server, local + virtual + export const owned: TextDocumentFilter[] = local.concat(virtual); } diff --git a/fleche/version.ml b/fleche/version.ml index c3a588d88..2b22f1f75 100644 --- a/fleche/version.ml +++ b/fleche/version.ml @@ -12,6 +12,6 @@ type t = string (************************************************************************) (* UPDATE VERSION HERE *) -let server = "0.2.1" +let server = "0.2.2" (* UPDATE VERSION HERE *) (************************************************************************)