Merge branch 'v8.18' into v8.17

CHANGES.md

@@ -1,5 +1,5 @@
-# coq-lsp 0.1.8: Dot / Bracket
-------------------------------
+# coq-lsp 0.1.8: Trick-or-treat
+-------------------------------
 
  - Update VSCode client dependencies, should bring some performance
    improvements to goal pretty printing (@ejgallego, #530)
@@ -39,6 +39,25 @@
  - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48,
    @CohenCyril, #572, via
    https://github.com/coq-community/coq-nix-toolbox/pull/164 )
+ - Support for `-rifrom` in `_CoqProject` and in command line
+   (`--rifrom`). Thanks to Lasse Blaauwbroek for the report.
+   (@ejgallego, #581, fixes #579)
+ - Export Query Goals API in VSCode client; this way other extensions
+   can implement their own commands that query Coq goals (@amblafont,
+   @ejgallego, #576, closes #558)
+ - New `pretac` field for preprocessing of goals with a tactic using
+   speculative execution, this is experimental for now (@amblafont,
+   @ejgallego, #573, helps with #558)
+ - Implement `textDocument/selectionRange` request, that will return
+   the range of the Coq sentence underlying the cursor. In VSCode,
+   this is triggered by the "Expand Selection" command. The
+   implementation is partial: we only take into account the first
+   position, and we only return a single range (Coq sentence) without
+   parents. (@ejgallego, #582)
+ - Be more robust to mixed-separator windows paths in workspace
+   detection (@ejgallego, #583, fixes #569)
+ - Adjust printing breaks in error and message panels (@ejgallego,
+   @Alizter, #586, fixes #457 , fixes #458 , fixes #571)
 
 # coq-lsp 0.1.7: Just-in-time
 -----------------------------

CONTRIBUTING.md

@@ -314,9 +314,10 @@ The checklist for the release as of today is the following:
 
 The above can be done with:
 ```
-export COQLSPV=0.1.7
+export COQLSPV=0.1.8
 git checkout main  && make                    && dune-release tag ${COQLSPV}
-git checkout v8.17 && git merge main  && make && dune-release tag ${COQLSPV}+8.17 && dune-release
+git checkout v8.18 && git merge main  && make && dune-release tag ${COQLSPV}+8.18 && dune-release
+git checkout v8.17 && git merge v8.18 && make && dune-release tag ${COQLSPV}+8.17 && dune-release
 git checkout v8.16 && git merge v8.17 && make && dune-release tag ${COQLSPV}+8.16 && dune-release
 ```
 

README.md

@@ -65,7 +65,7 @@ and web native usage, providing quite a few extra features from vanilla Coq.
   - [📂 Working With Multiple Files](#-working-with-multiple-files)
 - [📔 Planned Features](#-planned-features)
 - [📕 Protocol Documentation](#-protocol-documentation)
-- [🤸 Contributing](#-contributing)
+- [🤸 Contributing and Extending the System](#-contributing-and-extending-the-system)
 - [🥷 Team](#-team)
   - [🕰️ Past Contributors](#️-past-contributors)
 - [©️ Licensing Information](#️-licensing-information)
@@ -368,7 +368,7 @@ plus some extensions specific to Coq.
 
 Check [the `coq-lsp` protocol documentation](etc/doc/PROTOCOL.md) for more details.
 
-## 🤸 Contributing
+## 🤸 Contributing and Extending the System
 
 Contributions are very welcome! Feel free to chat with the dev team in
 [Zulip](https://coq.zulipchat.com/#narrow/stream/329642-coq-lsp) for any
@@ -381,6 +381,10 @@ Here is a [list of project ideas](etc/ContributionIdeas.md) that could be of
 help in case you are looking for contribution ideas, tho we are convinced that
 the best ideas will arise from using `coq-lsp` in your own Coq projects.
 
+Both Flèche and `coq-lsp` have a preliminary _plugin system_. The VSCode
+extension also exports and API so other extensions use its functionality
+to query and interact with Coq documents.
+
 ## 🥷 Team
 
 - Ali Caglayan (co-coordinator)

compiler/fcc.ml

@@ -3,7 +3,7 @@ open Cmdliner
 open Fcc_lib
 
 let fcc_main roots display debug plugins files coqlib coqcorelib ocamlpath
-    rload_path load_path =
+    rload_path load_path require_libraries =
   let vo_load_path = rload_path @ load_path in
   let ml_include_path = [] in
   let args = [] in
@@ -14,6 +14,7 @@ let fcc_main roots display debug plugins files coqlib coqcorelib ocamlpath
     ; vo_load_path
     ; ml_include_path
     ; args
+    ; require_libraries
     }
   in
   let args = Args.{ cmdline; roots; display; files; debug; plugins } in
@@ -98,6 +99,18 @@ let plugins : string list Term.t =
   let doc = "Compiler plugins to load" in
   Arg.(value & opt_all string [] & info [ "plugin" ] ~docv:"PLUGINS" ~doc)
 
+let rifrom : (string option * string) list Term.t =
+  let doc =
+    "FROM Require Import LIBRARY before creating the document, à la From Coq \
+     Require Import Prelude"
+  in
+  Term.(
+    const (List.map (fun (x, y) -> (Some x, y)))
+    $ Arg.(
+        value
+        & opt_all (pair string string) []
+        & info [ "rifrom"; "require-import-from" ] ~docv:"FROM,LIBRARY" ~doc))
+
 let fcc_cmd : unit Cmd.t =
   let doc = "Flèche Coq Compiler" in
   let man =
@@ -111,7 +124,7 @@ let fcc_cmd : unit Cmd.t =
   let fcc_term =
     Term.(
       const fcc_main $ roots $ display $ debug $ plugins $ file $ coqlib
-      $ coqcorelib $ ocamlpath $ rload_path $ load_path)
+      $ coqcorelib $ ocamlpath $ rload_path $ load_path $ rifrom)
   in
   Cmd.(v (Cmd.info "fcc" ~version ~doc ~man) fcc_term)
 

controller/coq_lsp.ml

@@ -89,7 +89,8 @@ let rec lsp_init_loop ~ifn ~ofn ~cmdline ~debug =
     | Init_effect.Loop -> lsp_init_loop ~ifn ~ofn ~cmdline ~debug
     | Init_effect.Success w -> w)
 
-let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path delay =
+let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path
+    require_libraries delay =
   (* Try to be sane w.r.t. \r\n in Windows *)
   Stdlib.set_binary_mode_in stdin true;
   Stdlib.set_binary_mode_out stdout true;
@@ -116,6 +117,7 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path delay =
     ; vo_load_path
     ; ml_include_path
     ; args = []
+    ; require_libraries
     }
   in
 
@@ -231,6 +233,18 @@ let ml_include_path : string list Term.t =
   Arg.(
     value & opt_all dir [] & info [ "I"; "ml-include-path" ] ~docv:"DIR" ~doc)
 
+let rifrom : (string option * string) list Term.t =
+  let doc =
+    "FROM Require Import LIBRARY before creating the document, à la From Coq \
+     Require Import Prelude"
+  in
+  Term.(
+    const (List.map (fun (x, y) -> (Some x, y)))
+    $ Arg.(
+        value
+        & opt_all (pair string string) []
+        & info [ "rifrom"; "require-import-from" ] ~docv:"FROM,LIBRARY" ~doc))
+
 let delay : float Term.t =
   let doc = "Delay value in seconds when server is idle" in
   Arg.(value & opt float 0.1 & info [ "D"; "idle-delay" ] ~docv:"DELAY" ~doc)
@@ -253,7 +267,7 @@ let lsp_cmd : unit Cmd.t =
       (Cmd.info "coq-lsp" ~version:Fleche.Version.server ~doc ~man)
       Term.(
         const lsp_main $ bt $ coqcorelib $ coqlib $ ocamlpath $ vo_load_path
-        $ ml_include_path $ delay))
+        $ ml_include_path $ rifrom $ delay))
 
 let main () =
   let ecode = Cmd.eval lsp_cmd in

controller/lsp_core.ml

@@ -25,7 +25,6 @@ module U = Yojson.Safe.Util
 
 let field name dict = List.(assoc name dict)
 let int_field name dict = U.to_int (field name dict)
-let dict_field name dict = U.to_assoc (field name dict)
 let list_field name dict = U.to_list (field name dict)
 let string_field name dict = U.to_string (field name dict)
 let ofield name dict = List.(assoc_opt name dict)
@@ -70,10 +69,18 @@ module Helpers = struct
     let Lsp.Doc.VersionedTextDocumentIdentifier.{ uri; version } = document in
     (uri, version)
 
-  let get_position params =
-    let pos = dict_field "position" params in
+  let lsp_position_to_tuple (pos : J.t) =
+    let pos = U.to_assoc pos in
     let line, character = (int_field "line" pos, int_field "character" pos) in
     (line, character)
+
+  let get_position params =
+    let pos = field "position" params in
+    lsp_position_to_tuple pos
+
+  let get_position_array params =
+    let pos_list = list_field "positions" params in
+    List.map lsp_position_to_tuple pos_list
 end
 
 (** LSP loop internal state: mainly the data needed to create a new document. In
@@ -108,7 +115,17 @@ module State = struct
     let dir = Lang.LUri.File.to_string_file uri in
     { state with workspaces = List.remove_assoc dir state.workspaces }
 
-  let is_in_dir ~dir ~file = CString.is_prefix dir file
+  let split_in_components path =
+    let phase1 = String.split_on_char '/' path in
+    let phase2 = List.map (String.split_on_char '\\') phase1 in
+    List.concat phase2
+
+  (* This is a bit more tricky in Windows, due to \ vs / paths appearing, so we
+     need to first split the dir *)
+  let is_in_dir ~dir ~file =
+    let dir_c = split_in_components dir in
+    let file_c = split_in_components file in
+    CList.prefix_of String.equal dir_c file_c
 
   let workspace_of_uri ~uri ~state =
     let { root_state; workspaces; _ } = state in
@@ -276,8 +293,24 @@ let do_position_request ~postpone ~params ~handler =
   Rq.Action.Data
     (Request.Data.PosRequest { uri; handler; point; version; postpone })
 
+(* For now we only pick the first item *)
+let do_position_list_request ~postpone ~params ~handler =
+  let uri, version = Helpers.get_uri_oversion params in
+  let points = Helpers.get_position_array params in
+  match points with
+  | [] ->
+    let point, handler = ((0, 0), Request.empty) in
+    Rq.Action.Data
+      (Request.Data.PosRequest { uri; handler; point; version; postpone })
+  | point :: _ ->
+    Rq.Action.Data
+      (Request.Data.PosRequest { uri; handler; point; version; postpone })
+
 let do_hover = do_position_request ~postpone:false ~handler:Rq_hover.hover
 
+let do_selectionRange =
+  do_position_list_request ~postpone:false ~handler:Rq_selectionRange.request
+
 (* We get the format from the params *)
 let get_pp_format_from_config () =
   match !Fleche.Config.v.pp_type with
@@ -297,9 +330,12 @@ let get_pp_format params =
     get_pp_format_from_config ()
   | None -> get_pp_format_from_config ()
 
+let get_pretac params = ostring_field "pretac" params
+
 let do_goals ~params =
   let pp_format = get_pp_format params in
-  let handler = Rq_goals.goals ~pp_format in
+  let pretac = get_pretac params in
+  let handler = Rq_goals.goals ~pp_format ?pretac () in
   do_position_request ~postpone:true ~handler ~params
 
 let do_definition =
@@ -420,6 +456,7 @@ let dispatch_request ~method_ ~params : Rq.Action.t =
   | "textDocument/documentSymbol" -> do_symbols ~params
   | "textDocument/hover" -> do_hover ~params
   | "textDocument/codeLens" -> do_lens ~params
+  | "textDocument/selectionRange" -> do_selectionRange ~params
   (* Proof-specific stuff *)
   | "proof/goals" -> do_goals ~params
   (* Proof-specific stuff *)

controller/request.ml

@@ -58,3 +58,5 @@ module Data = struct
     | PosRequest { uri = _; point; version = _; postpone = _; handler } ->
       handler ~point ~doc
 end
+
+let empty ~doc:_ ~point:_ = Ok (`List [])

controller/request.mli

@@ -42,3 +42,5 @@ module Data : sig
   val dm_request : t -> Fleche.Theory.Request.request
   val serve : doc:Fleche.Doc.t -> t -> R.t
 end
+
+val empty : position

controller/rq_goals.ml

@@ -35,26 +35,55 @@ let pp ~pp_format pp =
   | Pp -> Lsp.JCoq.Pp.to_yojson pp
   | Str -> `String (Pp.string_of_ppcmds pp)
 
-let get_goals_info ~doc ~point =
+(* XXX: Speculative execution here requires more thought, about errors,
+   location, we need to make the request fail if it is not good, etc... Moreover
+   we should tune whether we cache the results; we try this for now. *)
+let parse_and_execute_in tac st =
+  (* Parse tac, loc==FIXME *)
+  let str = Gramlib.Stream.of_string tac in
+  let str = Coq.Parsing.Parsable.make ?loc:None str in
+  match Coq.Parsing.parse ~st str with
+  | Coq.Protect.E.{ r = Interrupted; feedback = _ }
+  | Coq.Protect.E.{ r = Completed (Error _); feedback = _ }
+  | Coq.Protect.E.{ r = Completed (Ok None); feedback = _ } -> None
+  | Coq.Protect.E.{ r = Completed (Ok (Some ast)); feedback = _ } -> (
+    let open Fleche.Memo in
+    (* XXX use the bind in Coq.Protect.E *)
+    match (Interp.eval (st, ast)).res with
+    | Coq.Protect.E.{ r = Interrupted; feedback = _ }
+    | Coq.Protect.E.{ r = Completed (Error _); feedback = _ } -> None
+    | Coq.Protect.E.{ r = Completed (Ok st); feedback = _ } -> Some st)
+
+let run_pretac ?pretac st =
+  match pretac with
+  | None ->
+    (* Debug option *)
+    (* Lsp.Io.trace "goals" "pretac empty"; *)
+    Some st
+  | Some tac -> Fleche.Info.in_state ~st ~f:(parse_and_execute_in tac) st
+
+let get_goal_info ~doc ~point ?pretac () =
   let open Fleche in
   let goals_mode = get_goals_mode () in
   let node = Info.LC.node ~doc ~point goals_mode in
   match node with
   | None -> (None, None)
-  | Some node ->
-    let st = node.Doc.Node.state in
-    let goals = Info.Goals.goals ~st in
-    let program = Info.Goals.program ~st in
-    (goals, Some program)
+  | Some node -> (
+    match run_pretac ?pretac node.Doc.Node.state with
+    | None -> (None, None)
+    | Some st ->
+      let goals = Info.Goals.goals ~st in
+      let program = Info.Goals.program ~st in
+      (goals, Some program))
 
-let goals ~pp_format ~doc ~point =
+let goals ~pp_format ?pretac () ~doc ~point =
   let open Fleche in
   let uri, version = (doc.Doc.uri, doc.version) in
   let textDocument = Lsp.Doc.VersionedTextDocumentIdentifier.{ uri; version } in
   let position =
     Lang.Point.{ line = fst point; character = snd point; offset = -1 }
   in
-  let goals, program = get_goals_info ~doc ~point in
+  let goals, program = get_goal_info ~doc ~point ?pretac () in
   let node = Info.LC.node ~doc ~point Exact in
   let messages = mk_messages node in
   let error = Option.bind node mk_error in

controller/rq_goals.mli

@@ -9,4 +9,6 @@ type format =
   | Pp
   | Str
 
-val goals : pp_format:format -> Request.position
+(** [goals ~pp_format ?pretac] Serve goals at point; users can request
+    pre-processing and formatting using the provided parameters. *)
+val goals : pp_format:format -> ?pretac:string -> unit -> Request.position

controller/rq_hover.ml

@@ -173,7 +173,7 @@ module type HoverProvider = sig
 end
 
 module Loc_info : HoverProvider = struct
-  let enabled = false
+  let enabled = true
 
   let h ~contents:_ ~point:_ ~node =
     match node with

controller/rq_init.ml

@@ -128,6 +128,7 @@ let do_initialize ~params =
           ] )
     ; ("definitionProvider", `Bool true)
     ; ("codeLensProvider", `Assoc [])
+    ; ("selectionRangeProvider", `Bool true)
     ; ( "workspace"
       , `Assoc
           [ ( "workspaceFolders"

controller/rq_selectionRange.ml

@@ -0,0 +1,26 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(************************************************************************)
+(* Coq Language Server Protocol                                         *)
+(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
+(* Copyright 2019-2023 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias                                  *)
+(************************************************************************)
+
+let request ~doc ~point =
+  let approx = Fleche.Info.Exact in
+  match Fleche.Info.LC.node ~doc ~point approx with
+  | None -> Ok `Null
+  | Some node ->
+    let range = Fleche.Doc.Node.range node in
+    let parent = None in
+    let answer = Lsp.Core.SelectionRange.({ range; parent } |> to_yojson) in
+    Ok (`List [ answer ])