Skip to content

Commit

Permalink
[coq] [loader] Don't swallow plugin loading errors.
Browse files Browse the repository at this point in the history
`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.
  • Loading branch information
ejgallego committed Sep 29, 2023
1 parent 7bbfcc0 commit d92dca7
Show file tree
Hide file tree
Showing 2 changed files with 11 additions and 4 deletions.
4 changes: 4 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
-----------------------------
Expand Down
11 changes: 7 additions & 4 deletions coq/loader.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down

0 comments on commit d92dca7

Please sign in to comment.