From 96b7052d634e49f32af4822f9895ae128ceccbaf Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Tue, 27 Dec 2022 03:10:05 +0100
Subject: [PATCH] [new release] coq-lsp (0.1.1+v8.16)

CHANGES:

-------------------------

 - Don't crash if the log file can't be created (@ejgallego, ejgallego/coq-lsp#87)
 - Use LSP functions for client-side logging (@ejgallego, ejgallego/coq-lsp#87)
 - Log `_CoqProject` detection settings to client window (@ejgallego, ejgallego/coq-lsp#88)
 - Use plugin include paths from `_CoqProject` (@ejgallego, ejgallego/coq-lsp#88)
 - Support OCaml >= 4.12 (@ejgallego, ejgallego/coq-lsp#93)
 - Optimize the number of diagnostics sent in eager mode (@ejgallego, ejgallego/coq-lsp#104)
 - Improved syntax highlighting on VSCode client (@artagnon, ejgallego/coq-lsp#105)
 - Resume document checking from the point it was interrupted
   (@ejgallego, ejgallego/coq-lsp#95, ejgallego/coq-lsp#99)
 - Don't convert Coq "Info" messages such as "Foo is defined" to
   feedback by default; users willing to see them can set the
   corresponding option (@ejgallego, ejgallego/coq-lsp#113)
 - Send `$/coq/fileProgress` progress notifications from server,
   similarly to what Lean does; display them in Code's right gutter
   (@ejgallego, ejgallego/coq-lsp#106, fixes ejgallego/coq-lsp#54)
 - Show goals on click by default, allow users to configure the
   behavior to follow cursor in different ways (@ejgallego, ejgallego/coq-lsp#116,
   fixes ejgallego/coq-lsp#89)
 - Show file position in goal buffer, use collapsible elements for
   goal list (@ejgallego, ejgallego/coq-lsp#115, fixes ejgallego/coq-lsp#109)
 - Resume checking from common prefix on document update (@ejgallego,
   ejgallego/coq-lsp#111, fixes ejgallego/coq-lsp#110)
 - Only serve goals, hover, and symbols requests when the document
   has been sufficiently processed (@ejgallego, ejgallego/coq-lsp#120, fixes ejgallego/coq-lsp#100)
---
 packages/coq-lsp/coq-lsp.0.1.1+v8.16/opam | 41 +++++++++++++++++++++++
 1 file changed, 41 insertions(+)
 create mode 100644 packages/coq-lsp/coq-lsp.0.1.1+v8.16/opam

diff --git a/packages/coq-lsp/coq-lsp.0.1.1+v8.16/opam b/packages/coq-lsp/coq-lsp.0.1.1+v8.16/opam
new file mode 100644
index 00000000000..5617faed098
--- /dev/null
+++ b/packages/coq-lsp/coq-lsp.0.1.1+v8.16/opam
@@ -0,0 +1,41 @@
+synopsis: "Language Server Protocol native server for Coq"
+description:
+"""
+Language Server Protocol native server for Coq
+"""
+opam-version: "2.0"
+maintainer: "e@x80.org"
+bug-reports: "https://github.com/ejgallego/coq-lsp/issues"
+homepage: "https://github.com/ejgallego/coq-lsp"
+dev-repo: "git+https://github.com/ejgallego/coq-lsp.git"
+authors: [
+  "Emilio Jesús Gallego Arias <e@x80.org>"
+]
+license: "LGPL-2.1-or-later"
+doc: "https://ejgallego.github.io/coq-lsp/"
+
+depends: [
+  "ocaml"        { >= "4.12.0" }
+  "dune"         { >= "3.2"  }
+
+  # Not yet required, install Coq deps instead
+  "coq"            {         >= "8.16.0" & < "8.17" }
+  "coq-serapi"     {         >= "8.16.0" & < "8.17" }
+  "camlp-streams"  {         >= "5.0"               }
+
+  # lsp dependencies
+  "cmdliner"     { >= "1.1.0" }
+  "yojson"       { >= "1.7.0" }
+]
+
+build: [ [ "dune" "build" "-p" name "-j" jobs ] ]
+run-test: [ [ "dune" "runtest" "-p" name "-j" jobs ] ]
+url {
+  src:
+    "https://github.com/ejgallego/coq-lsp/releases/download/0.1.1%2Bv8.16/coq-lsp-0.1.1.v8.16.tbz"
+  checksum: [
+    "sha256=be48fd1449d8a0eb209e83ebbcde95090e94ba74ee7e744a399c3a5b67cc4acb"
+    "sha512=c711b953346d3e45ed61c75d5f3825d877820dec38e5dc803cd1ab9a32d6b4a850232a84984c3c340d3939c459ea0595f606d303e1ba714e4245a784b3507ab0"
+  ]
+}
+x-commit-hash: "5a7a5de8784061f46b58a00dae9365aabd9daa31"