Merge pull request #557 from ejgallego/loader_strict

[coq] [loader] Don't swallow plugin loading errors.

CHANGES.md

@@ -15,6 +15,10 @@
    `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, #555)
  - Describe findlib status in `Workspace.describe`, which is printed
    in the output windows (@ejgallego, #556)
+ - `coq-lsp` plugin loader will now be strict in case of a plugin
+   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)
 
 # coq-lsp 0.1.7: Just-in-time
 -----------------------------

coq/loader.ml

@@ -62,9 +62,12 @@ let map_serlib fl_pkg =
     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 *)
+(* We used to be liberal here in the case a SerAPI plugin was not available.
+   This proved to be a bad choice as Coq got confused when plugin loading
+   failed. Par-contre, we now need to make the list in `map_serlib` open, so
+   plugins can register whether they support serialization. I'm afraid that'll
+   have to happen via the finlib database as we cannot load anticipatedly a
+   plugin that may not exist. *)
 let safe_loader loader fl_pkg =
   try loader [fl_pkg]
   with
@@ -74,7 +77,7 @@ let safe_loader loader fl_pkg =
      Feedback.msg_warning
       Pp.(str "Loading findlib plugin: " ++ str fl_pkg
           ++ str "failed" ++ fnl () ++ exn_msg);
-    ()
+    Exninfo.iraise iexn
 
 let plugin_handler user_loader =
   let loader = Option.default (Fl_dynload.load_packages ~debug:false) user_loader in