Improve error message for dependency loading

Currently LSP display just generic `[E] Failed to load deps` which does not give a clue about what happens. Pass underlying error information, so user can at least guess what's going on
FStarLang · Apr 3, 2022 · 89f7858 · 89f7858
1 parent 46cbaf0
commit 89f7858
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 3 deletions.
diff --git a/src/fstar/FStar.Interactive.PushHelper.fst b/src/fstar/FStar.Interactive.PushHelper.fst
@@ -350,7 +350,8 @@ let ld_deps st =
     | Inr st -> Inr st
     | Inl st -> Inl (st, deps)
   with
-  | _ -> U.print_error "[E] Failed to load deps"; Inr st
+  | Err (e, msg, ctx) -> U.print1_error "[E] Failed to load deps. %s" msg; Inr st
+  | exn -> U.print1_error "[E] Failed to load deps. Message: %s" (message_of_exn exn); Inr st
 
 let add_module_completions this_fname deps table =
   let capitalize str = if str = "" then str

diff --git a/src/ocaml-output/FStar_Interactive_PushHelper.ml b/src/ocaml-output/FStar_Interactive_PushHelper.ml