From 9d71a872639908eaa5ab43e4ec241faa32f4ae10 Mon Sep 17 00:00:00 2001 From: Yann Leray Date: Fri, 17 Jul 2026 14:45:14 +0200 Subject: [PATCH] Update coq-lsp.dev with latest opam file --- extra-dev/packages/coq-lsp/coq-lsp.dev/opam | 57 +++++++++++++++++---- 1 file changed, 48 insertions(+), 9 deletions(-) diff --git a/extra-dev/packages/coq-lsp/coq-lsp.dev/opam b/extra-dev/packages/coq-lsp/coq-lsp.dev/opam index 975cc3a513..7edccb90e1 100644 --- a/extra-dev/packages/coq-lsp/coq-lsp.dev/opam +++ b/extra-dev/packages/coq-lsp/coq-lsp.dev/opam @@ -5,9 +5,9 @@ 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" +bug-reports: "https://github.com/rocq-community/rocq-lsp/issues" +homepage: "https://github.com/rocq-community/rocq-lsp" +dev-repo: "git+https://github.com/rocq-community/rocq-lsp.git" authors: [ "Emilio Jesús Gallego Arias " "Ali Caglayan " @@ -18,19 +18,58 @@ license: "LGPL-2.1-or-later" doc: "https://ejgallego.github.io/coq-lsp/" depends: [ - "ocaml" { >= "4.11.0" } - "dune" { >= "3.2.0" } - "coq" { = "dev" } - "coq-serapi" { = "dev" } + ("ocaml" {>= "5.0"} & "ocaml" { < "5.3"} + | ("ocaml" {>= "4.12"} & "memprof-limits" { >= "0.2.1" } )) + "dune" { >= "3.13.0" } # Version interval [3.8-3.12] was + # broken for composed builds with Coq + "rocq-core" { = "dev" } + "rocq-stdlib" { >= "9" & with-test } + + # lsp dependencies "cmdliner" { >= "1.1.0" } "yojson" { >= "1.7.0" } + "uri" { >= "4.2.0" } + "dune-build-info" { >= "3.2.0" } + + # coq-layout-printer + "tyxml" { >= "4.5.0" } + + # for waterproof json parser + "menhir" { >= "20220210" } + + # unit testing + "ppx_inline_test" { >= "v0.15.0" } + + # This is now a hard dep due to API changes in 1.9.7 + "ocamlfind" { >= "1.9.8" } + + # serlib deps + "ppx_deriving" { >= "5.2" } + "ppx_deriving_yojson" { >= "3.7.0" } + "ppx_import" { >= "1.11.0" } + "sexplib" { >= "v0.15.0" & < "v0.18" } + "ppx_sexp_conv" { >= "v0.15.0" & < "v0.18" } + "ppx_compare" { >= "v0.15.0" & < "v0.18" } + "ppx_hash" { >= "v0.15.0" & < "v0.18" } ] -build: [ [ "dune" "build" "-p" name "-j" jobs ] ] +# older results get in mess with ppx_deriving, we cannot control how +# it gets pulled, often in min-bound rev-dep, so we conflict with it +conflicts: [ "result" { < "1.5" } ] + +depopts: ["lwt" "logs"] + +build: [ + [ "rm" "-rf" "vendor" ] + [ "dune" "build" "-p" name "-j" jobs ] +] run-test: [ [ "dune" "runtest" "-p" name "-j" jobs ] ] +x-maintenance-intent: [ "(latest)" ] +name: "coq-lsp" +version: "dev" url { - src: "git+https://github.com/ejgallego/coq-lsp.git#main" + src: "git+https://github.com/rocq-community/rocq-lsp.git" }