Merge branch 'v8.20' into v8.19

CHANGES.md

@@ -1,5 +1,5 @@
-# unreleased
-------------
+# coq-lsp 0.2.0: From Green to Blue
+-----------------------------------
 
  - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI
    dependency, and will greatly easy the development of tools that
@@ -66,6 +66,10 @@
    configurable with different methods; moreover, `petanque/run` can
    compute some extra data like state hashing without a round-trip
    (@ejgallego @gbdrt, #779)
+ - [petanque] New methods to hash proof states; use proof state hash
+   by default in petanque agent (@ejgallego, @gbdrt, #808)
+ - [petanque] New shell method `petanque/toc` that returns a document
+   outline in LSP-style (@ejgallego, #794)
 
 # coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_...
 ----------------------------------------------------

CONTRIBUTING.md

@@ -383,20 +383,26 @@ README there for more details.
 
 The checklist for the release as of today is the following:
 
+### Pre-release
+
+- update the version number at `editor/code/package.json`, do `npm i`
+- update the version number at `fleche/version.ml`
+
 ### Client:
 
 - update the client changelog at `editor/code/CHANGELOG.md`, commit
 - for the `main` branch: `dune release tag $coq_lsp_version`
+- build the extension with `npm run vscode:prepublish`
 - check with `vsce ls` that the client contents are OK
 - `vsce publish`
+- upload vsix to OpenVSX marketplace
 
 ### Server:
 
 - sync branches for previous Coq versions, using `git merge`, test and push to CI.
 - `dune release tag` for each `$coq_lsp_version+$coq_version`
 - `dune release` for each version that should to the main opam repos
-- [optional] update pre-release packages to coq-opam-archive
-- [important] after the release, bump `version.ml` and `package.json` version string
+- [deprecated] update pre-release packages to coq-opam-archive
 
 The above can be done with:
 ```
@@ -408,6 +414,11 @@ git checkout v8.18 && git merge v8.19  && make && dune-release tag ${COQLSPV}+8.
 git checkout v8.17 && git merge v8.18 && make && dune-release tag ${COQLSPV}+8.17 && dune-release
 ```
 
+### After release
+
+- [important] bump `version.ml` and `editor/code/package.json` version
+  string to a `-dev` suffix
+
 ## Emacs
 
 You should be able to use `coq-lsp` with

coq/loader.ml

@@ -40,8 +40,10 @@ let map_serlib fl_pkg =
   let supported = match fl_pkg with
     (* Supported by serlib *)             (* directory   *)
     | "coq-core.plugins.btauto"           (* btauto *)
+    | "coq-core.plugins.cc_core"          (* cc_core  *)
     | "coq-core.plugins.cc"               (* cc  *)
     | "coq-core.plugins.extraction"       (* extraction  *)
+    | "coq-core.plugins.firstorder_core"  (* firstorder_core  *)
     | "coq-core.plugins.firstorder"       (* firstorder  *)
     | "coq-core.plugins.funind"           (* funind      *)
     | "coq-core.plugins.ltac"             (* ltac        *)

coq/state.ml

@@ -78,6 +78,13 @@ module Proof = struct
   type t = Vernacstate.LemmaStack.t
 
   let to_coq x = x
+  let equal x y = x == y
+
+  (* OCaml's defaults are 10, 100, we use this as to give best precision for
+     petanque-like users *)
+  let hash x =
+    let meaningful, total = (128, 256) in
+    Hashtbl.hash_param meaningful total x
 end
 
 let lemmas ~st = st.Vernacstate.interp.lemmas

coq/state.mli

@@ -10,6 +10,8 @@ val parsing : st:t -> Vernacstate.Parser.t
 module Proof : sig
   type t
 
+  val equal : t -> t -> bool
+  val hash : t -> int
   val to_coq : t -> Vernacstate.LemmaStack.t
 end
 

editor/code/CHANGELOG.md

@@ -1,3 +1,35 @@
+# coq-lsp 0.2.0: From Green to Blue
+-----------------------------------
+
+ - [fleche] Preserve view hint across document changes. With this
+   change, we get local continuous checking mode when the view-port
+   heuristic is enabled (@ejgallego, #748)
+ - [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego,
+   #755, cc: #722, #725)
+ - [hover] Show input howto for unicode characters on hover
+   (@ejgallego, Léo Stefanesco, #756)
+ - [lsp] [definition] Support for jump to definition across workspace
+   files. The location information is obtained from `.glob` files, so
+   it is often not perfect. (@ejgallego, #762, fixes #317)
+ - [lsp] [hover] Show full name and provenance of identifiers
+   (@ejgallego, #762)
+ - [lsp] [definition] Try also to resolve and locate module imports
+   (@ejgallego, #764)
+ - [code] Don't start server on extension activation, unless an editor
+   we own is active. We also auto-start the server if a document that
+   we own is opened later (@ejgallego, #758, fixes #750)
+ - [hover] New option `show_universes_on_hover` that will display
+   universe data on hover (@ejgallego, @SkySkimmer, #666)
+ - [hover] New plugin `unidiff` that will elaborate a summary of
+   universe data a file, in particular regarding universes added at
+   `Qed` time (@ejgallego, #773)
+ - [fleche] Support meta-command `Abort All` (@ejgallego, #774, fixes
+   #550)
+ - [lsp] [petanque] Allow acces to `petanque` protocol from the lsp
+   server (@ejgallego, #778)
+
+  See server changelog for full server-side changes.
+
 # coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_...
 ----------------------------------------------------
 

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-dev",
+  "version": "0.2.0",
   "contributors": [
     "Emilio Jesús Gallego Arias <[email protected]>",
     "Ali Caglayan <[email protected]>",

examples/ltac2_simple.v

@@ -3,4 +3,3 @@ From Ltac2 Require Import Ltac2.
 Goal True /\ True.
   split; exact I.
 Qed.
-

fleche/version.ml

@@ -12,6 +12,6 @@ type t = string
 
 (************************************************************************)
 (*                        UPDATE VERSION HERE                           *)
-let server = "0.2.0-dev"
+let server = "0.2.0"
 (*                        UPDATE VERSION HERE                           *)
 (************************************************************************)

lang/ast.mli

@@ -4,7 +4,7 @@ end
 
 (** Information about the Ast, to move to lang *)
 module Info : sig
-  type t = private
+  type t =
     { range : Range.t
     ; name : Name.t With_range.t
     ; kind : int

petanque/agent.ml

@@ -30,6 +30,19 @@ module State = struct
       fun st1 st2 ->
         let st1, st2 = (Coq.State.lemmas ~st:st1, Coq.State.lemmas ~st:st2) in
         Option.equal Coq.Goals.Equality.equal_goals st1 st2
+
+  module Proof = struct
+    type t = Coq.State.Proof.t
+
+    let equal ?(kind = Inspect.Physical) =
+      match kind with
+      | Physical -> Coq.State.Proof.equal
+      | Goals -> Coq.Goals.Equality.equal_goals
+
+    let hash = Coq.State.Proof.hash
+  end
+
+  let lemmas st = Coq.State.lemmas ~st
 end
 
 (** Petanque errors *)
@@ -132,6 +145,21 @@ let protect_to_result (r : _ Coq.Protect.E.t) : (_, _) Result.t =
 let proof_finished { Coq.Goals.goals; stack; shelf; given_up; _ } =
   List.for_all CList.is_empty [ goals; shelf; given_up ] && CList.is_empty stack
 
+(* At some point we want to return both hashes *)
+module Hash_kind = struct
+  type t =
+    | Full
+    | Proof
+  [@@warning "-37"]
+
+  let hash ~kind st =
+    match kind with
+    | Full -> Some (State.hash st)
+    | Proof -> Option.map State.Proof.hash (State.lemmas st)
+end
+
+let hash_mode = Hash_kind.Proof
+
 let analyze_after_run ~hash st =
   let proof_finished =
     let goals = Fleche.Info.Goals.get_goals_unit ~st in
@@ -140,7 +168,7 @@ let analyze_after_run ~hash st =
     | Some goals when proof_finished goals -> true
     | _ -> false
   in
-  let hash = if hash then Some (State.hash st) else None in
+  let hash = if hash then Hash_kind.hash ~kind:hash_mode st else None in
   Run_result.{ st; hash; proof_finished }
 
 (* Would be nice to keep this in sync with the type annotations. *)

petanque/agent.mli

@@ -6,14 +6,13 @@
 (************************************************************************)
 
 (** Petanque.Agent *)
-
 module State : sig
+  (** Full state of Coq *)
   type t
 
   val name : string
 
-  (** Fleche-based Coq state hash; it has been designed for interactive use, so
-      please report back *)
+  (** OCaml poly Coq state hash; tuned for interactive edition. *)
   val hash : t -> int
 
   module Inspect : sig
@@ -28,6 +27,18 @@ module State : sig
 
   (** [equal ?kind st1 st2] [kind] defaults to [Inspect.Physical] *)
   val equal : ?kind:Inspect.t -> t -> t -> bool
+
+  module Proof : sig
+    (** OCaml poly hash for Coq proof state. *)
+    type t
+
+    (** [equal ?kind st1 st2] [kind] defaults to [Inspect.Physical] *)
+    val equal : ?kind:Inspect.t -> t -> t -> bool
+
+    val hash : t -> int
+  end
+
+  val lemmas : t -> Proof.t option
 end
 
 (** Petanque errors *)
@@ -62,6 +73,7 @@ module Run_result : sig
   type 'a t =
     { st : 'a
     ; hash : int option [@default None]
+          (** [State.Proof.hash st] if enabled / proof is open. *)
     ; proof_finished : bool
     }
 end

petanque/json/interp.ml

@@ -65,4 +65,8 @@ let handle_request ~(do_handle : 'a handle) ~unhandled ~token ~method_ ~params =
     do_handle ~token (do_request (module StateEqual) ~params)
   | s when String.equal StateHash.method_ s ->
     do_handle ~token (do_request (module StateHash) ~params)
+  | s when String.equal StateProofEqual.method_ s ->
+    do_handle ~token (do_request (module StateProofEqual) ~params)
+  | s when String.equal StateProofHash.method_ s ->
+    do_handle ~token (do_request (module StateProofHash) ~params)
   | _ -> unhandled ~token ~method_

petanque/json/jAgent.ml

@@ -54,6 +54,27 @@ module Lang = struct
   module Range = struct
     type t = Lsp.JLang.Range.t [@@deriving yojson]
   end
+
+  module With_range = struct
+    type 'a t = [%import: ('a Lang.With_range.t[@with Lang.Range.t := Range.t])]
+    [@@deriving yojson]
+  end
+
+  module Ast = struct
+    module Name = struct
+      type t = [%import: Lang.Ast.Name.t] [@@deriving yojson]
+    end
+
+    module Info = struct
+      type t =
+        [%import:
+          (Lang.Ast.Info.t
+          [@with
+            Lang.Range.t := Range.t;
+            Lang.With_range.t := With_range.t])]
+      [@@deriving yojson]
+    end
+  end
 end
 
 module Premise = struct

petanque/json/protocol.ml

@@ -67,15 +67,7 @@ module Start = struct
   end
 
   module Handler = struct
-    module Params = struct
-      type t =
-        { uri : Lsp.JLang.LUri.File.t
-        ; opts : Run_opts.t option [@default None]
-        ; pre_commands : string option [@default None]
-        ; thm : string
-        }
-      [@@deriving yojson]
-    end
+    module Params = Params
 
     module Response = struct
       type t = State.t Run_result.t [@@deriving yojson]
@@ -236,3 +228,42 @@ module StateHash = struct
       HType.Immediate (fun ~token:_ { Params.st } -> Ok (Agent.State.hash st))
   end
 end
+
+module StateProofEqual = struct
+  let method_ = "petanque/state/proof/equal"
+
+  module Params = StateEqual.Params
+  module Response = StateEqual.Response
+
+  module Handler = struct
+    module Params = StateEqual.Handler.Params
+    module Response = Response
+
+    let handler =
+      HType.Immediate
+        (fun ~token:_ { Params.kind; st1; st2 } ->
+          let pst1, pst2 = Agent.State.(lemmas st1, lemmas st2) in
+          Ok (Option.equal (Agent.State.Proof.equal ?kind) pst1 pst2))
+  end
+end
+
+module StateProofHash = struct
+  let method_ = "petanque/state/proof/hash"
+
+  module Params = StateHash.Params
+
+  module Response = struct
+    type t = int option [@@deriving yojson]
+  end
+
+  module Handler = struct
+    module Params = StateHash.Handler.Params
+    module Response = Response
+
+    let handler =
+      HType.Immediate
+        (fun ~token:_ { Params.st } ->
+          let pst = Agent.State.lemmas st in
+          Ok (Option.map Agent.State.Proof.hash pst))
+  end
+end

petanque/json_shell/client.ml

@@ -71,10 +71,16 @@ module S (C : Chans) = struct
   open Protocol
   open Protocol_shell
 
+  (* Shell calls (they do have an equivalent version in LSP) *)
   let set_workspace =
     let module M = Wrap (SetWorkspace) (C) in
     M.call
 
+  let toc =
+    let module M = Wrap (TableOfContents) (C) in
+    M.call
+
+  (* Standard calls *)
   let start =
     let module M = Wrap (Start) (C) in
     M.call
@@ -98,4 +104,12 @@ module S (C : Chans) = struct
   let state_hash =
     let module M = Wrap (StateHash) (C) in
     M.call
+
+  let state_proof_equal =
+    let module M = Wrap (StateProofEqual) (C) in
+    M.call
+
+  let state_proof_hash =
+    let module M = Wrap (StateProofHash) (C) in
+    M.call
 end