From d92dca74289e1c4ec61495af845f5f80236846c1 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 29 Sep 2023 16:16:28 +0200 Subject: [PATCH] [coq] [loader] Don't swallow plugin loading errors. `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. --- CHANGES.md | 4 ++++ coq/loader.ml | 11 +++++++---- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 462f0c84..7d05fbd3 100644 --- a/CHANGES.md +++ b/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 ----------------------------- diff --git a/coq/loader.ml b/coq/loader.ml index 9cc62cf4..922a4563 100644 --- a/coq/loader.ml +++ b/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