Merge branch 'v8.18' into v8.17

Author: ejgallego

.github/workflows/build.yml

@@ -114,8 +114,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

CHANGES.md

@@ -1,5 +1,12 @@
-# unreleased
-------------
+# 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 !
+------------------------
 
  - [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
@@ -34,6 +41,18 @@
    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
 -----------------------------------

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

Makefile

@@ -159,6 +159,9 @@ _LIBROOT=$(shell opam var lib)
 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
 
@@ -169,8 +172,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 ") \
@@ -197,6 +200,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

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.
 

controller-js/coq_lsp_worker.ml

@@ -14,42 +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)
-    else
-      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"
 
@@ -65,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
@@ -74,20 +38,29 @@ external interrupt_setup : opaque (* Uint32Array *) -> unit = "interrupt_setup"
 
 let interrupt_is_setup = ref false
 
+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 parse_msg msg =
-  if Js.instanceof msg Js.array_length then (
+  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 obj_to_json msg |> Lsp.Base.Message.of_yojson
+  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
@@ -112,14 +85,17 @@ 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
     with
     | 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 =

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

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

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 *)

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 =

controller/rq_action.ml

@@ -0,0 +1,65 @@
+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)
+
+(* 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
+  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_qfs ~range doc in
+  let bf (d, qf) =
+    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.concat_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))

controller/rq_action.mli

@@ -0,0 +1 @@
+val request : range:Lang.Range.t -> Request.document