Merge pull request #421 from ejgallego/dont_fail_on_missing_serlib

[loader] Don't fail on missing serlib plugins

CHANGES.md

@@ -1,9 +1,13 @@
-# coq-lsp 0.1.7:
----------------------
+# coq-lsp 0.1.7: Just-in-time
+-----------------------------
 
  - Improvements and clenaups on hover display, in particular we don't
    print repeated `Notation` strings (@ejgallego, #422)
 
+ - Don't fail on missing serlib plugins, they are indeed an
+   optimization; this mostly impacts 8.16 by lowering the SerAPI
+   requirements (@ejgallego, #421)
+
 # coq-lsp 0.1.6: Peek
 ---------------------
 

README.md

@@ -223,18 +223,18 @@ don't hesitate to get in touch with us.
    ```
 - **Windows**: To install `coq-lsp` on windows, we recommend you use a cygwin
   build, such as the [one described
-  here](https://github.com/coq/platform/blob/main/doc/README_Windows.md#installation-by-compiling-from-sources-using-opam-on-cygwin). We
-  will improve this process soon, as of today, follow these steps:
-  - `opam pin add serapi https://github.com/ejgallego/coq-serapi`
-    this will likely fail due to paths being too long, to fix this do
-    + `cd .opam/$switch/build/coq-serapi-v8.16.0+0.16.1/ && mv serlib/plugins/syntax s && dune build -p coq-serapi && dune install coq-serapi`
-  - build `coq-lsp` from source (Windows support requires release 0.1.6, usually you'll want branch 8.16)
+  here](https://github.com/coq/platform/blob/main/doc/README_Windows.md#installation-by-compiling-from-sources-using-opam-on-cygwin), tho
+  any OCaml env where Coq can be built should work.
+  - build `coq-lsp` from source (branch `v8.16`, which will become 0.1.7)
   - Set the path to `coq-lsp.exe` binary in VS Code settings
-  - Set the `--ocamlpath=c:\$path_to_opam\lib` argument in VS Code settings, as
-    Coq Platform ships with an unconfigured binary
-  - If the binary doesn't work, try to run it from the file explorer, often you'll
-    need to copy `libgmp-10.dll` to `C:\Windows` for it work.
+  - Set the `--ocamlpath=c:\$path_to_opam\lib` argument in VS Code settings if
+    you get a findlib error. The Coq Platform ships with an un-configured
+    binary. Note, the path should be unquoted
+  - If the binary doesn't work, try to run it from the file explorer; if you get
+    a `.dll` error you'll need to copy that dll (often `libgmp-10.dll`) to the
+    `C:\Windows` folder for `coq-lsp` to work.
 - **Coq Platform** (coming soon)
+  - See the [bug tracking coq-lsp inclusion](https://github.com/coq/platform/issues/319)
 - [Do it yourself!](#server-1)
 
 <!-- TODO 🟣 Emacs, 🪖 Proof general, 🐔 CoqIDE -->

coq/loader.ml

@@ -18,6 +18,17 @@
 
 let list_last l = List.(nth l (length l - 1))
 
+let check_package_exists fl_pkg =
+  try
+    let _ = Findlib.package_directory fl_pkg in
+    Some fl_pkg
+  with
+  | Findlib.No_such_package (_, info) ->
+    Feedback.msg_warning
+      Pp.(str "Serlib plugin: " ++ str fl_pkg
+         ++ str "is not installed: " ++ str info);
+    None
+
 (* Should improve *)
 let map_serlib fl_pkg =
   let supported = match fl_pkg with
@@ -43,15 +54,31 @@ let map_serlib fl_pkg =
   if supported
   then
     let plugin_name = String.split_on_char '.' fl_pkg |> list_last in
-    Some ("coq-serapi.serlib." ^ plugin_name)
+    let serlib_name = "coq-serapi.serlib." ^ plugin_name in
+    check_package_exists serlib_name
   else None
 
+(* We are more liberal in the case a SerAPI plugin is not availabe, as
+   the fallbacks are "safe", tho will yield way worse incremental
+   behavior for expressions defined by the plugin *)
+let safe_loader loader fl_pkg =
+  try loader [fl_pkg]
+  with
+    exn ->
+    let iexn = Exninfo.capture exn in
+    let exn_msg = CErrors.iprint iexn in
+     Feedback.msg_warning
+      Pp.(str "Loading findlib plugin: " ++ str fl_pkg
+          ++ str "failed" ++ fnl () ++ exn_msg);
+    ()
+
 let plugin_handler user_loader =
   let loader = Option.default (Fl_dynload.load_packages ~debug:false) user_loader in
+  let safe_loader = safe_loader loader in
   fun fl_pkg ->
     let _, fl_pkg = Mltop.PluginSpec.repr fl_pkg in
     match map_serlib fl_pkg with
     | Some serlib_pkg ->
-      loader [serlib_pkg]
+      safe_loader serlib_pkg
     | None ->
-      loader [fl_pkg]
+      safe_loader fl_pkg