Merge pull request #559 from ejgallego/windows_install

[doc] Add pointers to Windows installers

CHANGES.md

@@ -19,6 +19,7 @@
    failure, the previous loose behavior was more convenient for the
    early releases, but it doesn't make sense now and made things
    pretty hard to debug on the Windows installer (@ejgallego, #557)
+ - Add pointers to Windows installers (@ejgallego, #559)
 
 # coq-lsp 0.1.7: Just-in-time
 -----------------------------

CONTRIBUTING.md

@@ -59,8 +59,10 @@ 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.
+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)
 
 1. Install the dependencies (the complete updated list of dependencies can be found in `coq-lsp.opam`).
 
@@ -69,7 +71,7 @@ Dune.
     ```
 
 2. Initialize submodules (the `main` branch uses some submodules, which we plan to get rid of soon. Branches `v8.x` can already skip this step.)
-  
+
     ```sh
     make submodules-init
     ```
@@ -85,7 +87,7 @@ Alternatively, you can also use the regular `dune build @check` etc... targets.
 
 #### Nix
 
-We have a Nix flake that you can use. 
+We have a Nix flake that you can use.
 
 1. Dependencies: for development it suffices to run `nix develop` to spawn a shell with the corresponding dependencies.
 
@@ -100,7 +102,7 @@ We have a Nix flake that you can use.
     ```
 
 2. Initialize submodules (the `main` branch uses some submodules, which we plan to get rid of soon. Branches `v8.x` can already skip this step.)
-  
+
     ```sh
     make submodules-init
     ```

README.md

@@ -8,18 +8,17 @@ Studio Code](https://code.visualstudio.com/) extension for the [Coq Proof
 Assistant](https://coq.inria.fr). Experimental support for [Vim](#vim) and
 [Neovim](#neovim) is also available in their own projects.
 
-**[Install: 🐧 Linux / 🍎 macOs]**:
+**Quick Install**:
+  - **🐧 Linux / 🍎 macOs:**
 ```
-$ opam install coq-lsp && code --install-extension ejgallego.coq-lsp
+$ opam install coq-lsp && code --install-extension ejgallego.coq-lsp`
 ```
+  - **🪟 Windows:** Download the [Coq Platform installer](#-server)
 
-**[Install: 🪟 Windows ]:**
-
-> see the [instructions](#-server); we will provide an `.exe` installer very soon
-
-Key [features](#Features) of `coq-lsp` are continuous and incremental document
-checking, advanced error recovery, markdown support, positional goals and
-information panel, performance data, and more.
+**Key [features](#Features)** of `coq-lsp` are: continuous and incremental
+document checking, advanced error recovery, hybrid Coq/markdown document
+support, multiple workspace support, positional goals and information panel,
+performance data, extensible command-line compiler, plugin system, and more.
 
 `coq-lsp` aims to provide a seamless, modern interactive theorem proving
 experience, as well as to serve as a maintainable platform for research and UI
@@ -250,18 +249,23 @@ guide](./CONTRIBUTING.md)
   - In nixpkgs: [coqPackages.coq-lsp](https://github.com/NixOS/nixpkgs/tree/master/pkgs/development/coq-modules/coq-lsp)
   - An example of a `flake` that uses `coq-lsp` in a development environment is here
      https://github.com/HoTT/Coq-HoTT/blob/master/flake.nix .
-- **Windows**: To install `coq-lsp` on windows, you need to build the Coq Platform:
-  - Download and uncompress the Platform Script: https://github.com/coq/platform/archive/refs/tags/2023.03.0.zip
-  - From a shell, execute `./coq_platform_make_windows.bat`
-  - Select `C:\cp_817` as the install path, select the packages you want
-  - Run `C:\cp_817\Cygwin.bat`
-  - Run `opam install coq-lsp`
-  - Run `cp /cygdrive/c/cp_817/usr/x86_64-w64-mingw32/sys-root/mingw/bin/libgmp-10.dll /home/User/.opam/CP.2023.03.0~8.17~2023.08/bin`
-  - In VSCode native, you can now set the `Coq-lsp: Path` setting to `C:\cp_817\home\User\.opam\CP.2023.03.0~8.17~2023.08\bin\coq-lsp.exe`
-  - Things should work !
-- **Coq Platform** (coming soon)
-  - See the [bug tracking coq-lsp inclusion](https://github.com/coq/platform/issues/319)
-- [Do it yourself!](#server-1)
+- **Windows**:
+  Experimental Windows installers based on the [Coq
+  Platform](https://github.com/coq/platform) are available at https://www.irif.fr/~gallego/coq-lsp/
+
+  This provides a Windows native binary that can be executed from VSCode
+  normally. As of today a bit of configuration is still needed:
+  - In VSCode, set the `Coq-lsp: Path` to:
+    + `C:\Coq-Platform~8.17-lsp\bin\coq-lsp.exe`
+  - In VSCode, set the `Coq-lsp: Args` to:
+    + `--coqlib=C:\Coq-Platform~8.17-lsp\lib\coq\`
+    + `--coqcorelib=C:\Coq-Platform~8.17-lsp\lib\coq-core\`
+    + `--ocamlpath=C:\Coq-Platform~8.17-lsp\lib\`
+  - Replace `C:\Coq-Platform~8.17-lsp\` by the path you have installed Coq above as needed
+  - Note that the installers are unsigned (for now), so you'll have to click on
+    "More info" then "Run anyway" inside the "Windows Protected your PC" dialog
+  - Also note that the installers are work in progress, and may change often.
+- **Do it yourself!** [Compilation from sources](./CONTRIBUTING.md#compilation)
 
 <!-- TODO 🟣 Emacs, 🪖 Proof general, 🐔 CoqIDE -->