Skip to content

Commit

Permalink
[loader] Don't fail on missing serlib plugins
Browse files Browse the repository at this point in the history
This was the wrong thing to do, I was just lazy.

We should refactor the loader so it works in a different
and doesn't depend on the hardcoded list.

This means we relax the SerAPI deps for 8.16
  • Loading branch information
ejgallego committed Feb 22, 2023
1 parent 62981e3 commit 02f59b9
Showing 1 changed file with 15 additions and 0 deletions.
15 changes: 15 additions & 0 deletions coq/loader.ml
Original file line number Diff line number Diff line change
Expand Up @@ -55,3 +55,18 @@ let plugin_handler user_loader =
loader [serlib_pkg]
| None ->
loader [fl_pkg]

(* 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 plugin_handler user_loader fl_pkg =
try plugin_handler user_loader fl_pkg
with
exn ->
let iexn = Exninfo.capture exn in
let exn_msg = CErrors.iprint iexn in
let _, fl_pkg = Mltop.PluginSpec.repr fl_pkg in
Feedback.msg_warning
Pp.(str "Loading serlib plugin: " ++ str fl_pkg
++ str "failed" ++ fnl () ++ exn_msg);
()

0 comments on commit 02f59b9

Please sign in to comment.