From e2993f08d232171346883ba3675663f824b03b34 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Thu, 25 Apr 2024 16:40:09 +0200
Subject: [PATCH] [build] [doc] [ci] Document and test global opam dev install

Fixes #682 , cc: #479 #488
---
 .github/workflows/build.yml | 28 +++++++++++++++++++++++++
 CHANGES.md                  |  2 ++
 CONTRIBUTING.md             | 42 ++++++++++++++++++++++++++++++++++++-
 coq-lsp.opam                |  5 ++++-
 4 files changed, 75 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 996daaeec..b543333fe 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -83,6 +83,34 @@ jobs:
       - name: 🐛 Test fcc
         run: opam exec -- make test-compiler
 
+  build-opam:
+    name: Opam dev install
+    strategy:
+      fail-fast: false
+    runs-on: ubuntu-latest
+    steps:
+      - name: 🔭 Checkout code
+        uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - name: 🐫 Setup OCaml
+        uses: ocaml/setup-ocaml@v2
+        with:
+          ocaml-compiler: 4.14.x
+          dune-cache: true
+
+      - name: Install Coq and SerAPI into OPAM switch
+        run: |
+          opam install vendor/coq/{coq-core,coq-stdlib,coqide-server,coq}.opam
+          opam install vendor/coq-serapi/coq-serapi.opam
+
+      - name: Install `coq-lsp` into OPAM switch
+        run: opam install .
+
+      - name: Test `coq-lsp` in installed switch
+        run: opam exec -- fcc examples/Demo.v
+
   build-nix:
     name: Nix
     strategy:
diff --git a/CHANGES.md b/CHANGES.md
index ccc1239f4..a985a5ec2 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -91,6 +91,8 @@
    `--max_errors=0` to imitate `coqc` behavior (@ejgallego, #680)
  - Fix `fcc` exit status when checking terminates with fatal errors
    (@ejgallego, @Alizter, #680)
+ - Fix (@ejgallego, #683, fixes #682, cc #479 #488, thanks to
+   @Hazardouspeach for the report)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index f79b11ac3..96a07cdba 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -58,12 +58,27 @@ generate it from the relevant entries in `CHANGES.md` at release time.
 
 ### Compilation
 
-#### Opam/Dune
 The server project uses a standard OCaml development setup based on
 Opam and Dune. This also works on Windows using the [Coq Platform
 Source
 Install](https://github.com/coq/platform/blob/main/doc/README_Windows.md#installation-by-compiling-from-sources-using-opam-on-cygwin)
 
+The default development environment for `coq-lsp` is a "composed"
+build that includes git submodules for `coq` and `coq-serapi` in the
+`vendor/` directory. This allows us to easily work with PRs using
+experimental Coq branches, and some other advantages like a better CI
+build cache and easier bisects.
+
+This will however install a local Coq version which may not be
+convenient for all use cases; we thus detail below an alternative
+install method for those that would like to install a `coq-lsp`
+development branch into an OPAM switch.
+
+#### Default development setup, local Coq / `coq-lsp`
+
+This setup will build Coq and `coq-lsp` locally; it is the recommended
+way to develop `coq-lsp` itself.
+
 1. Install the dependencies (the complete updated list of dependencies can be found in `coq-lsp.opam`).
 
     ```sh
@@ -85,6 +100,31 @@ Install](https://github.com/coq/platform/blob/main/doc/README_Windows.md#install
 
 Alternatively, you can also use the regular `dune build @check` etc... targets.
 
+Now, binaries for Coq and `coq-lsp` can be found under
+`_build/install/default` and used via `dune exec -- fcc` or `dune exec
+-- $your_editor`.
+
+#### Global OPAM install
+
+This setup will build Coq and `coq-lsp` and install them to the
+current OPAM switch. This is a good setup for people looking to try
+out `coq-lsp` development versions with other OPAM packages.
+
+1. Install vendored Coq and SerAPI:
+
+    ```sh
+    opam install vendor/coq/coq{-core,-stdlib,}.opam
+    opam install vendor/coq-serapi
+    ```
+
+2. Install `coq-lsp`:
+    ```sh
+    opam install .
+    ```
+
+Then, you should get a working OPAM switch with Coq and `coq-lsp` from
+your chosen `coq-lsp` branch.
+
 #### Nix
 
 We have a Nix flake that you can use.
diff --git a/coq-lsp.opam b/coq-lsp.opam
index 09b567941..7286614da 100644
--- a/coq-lsp.opam
+++ b/coq-lsp.opam
@@ -54,5 +54,8 @@ depends: [
   "ppx_hash"            { >= "v0.13.0" & < "v0.17" }
 ]
 
-build: [ [ "dune" "build" "-p" name "-j" jobs ] ]
+build: [
+  [ "rm" "-rf" "vendor" ]
+  [ "dune" "build" "-p" name "-j" jobs ]
+]
 run-test: [ [ "dune" "runtest" "-p" name "-j" jobs ] ]