From 89f7858385a60a551ab424da2cfd45f5cb10462d Mon Sep 17 00:00:00 2001 From: Andrii Kurdiumov Date: Sun, 3 Apr 2022 15:07:32 +0600 Subject: [PATCH] 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 --- src/fstar/FStar.Interactive.PushHelper.fst | 3 ++- src/ocaml-output/FStar_Interactive_PushHelper.ml | 10 ++++++++-- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/src/fstar/FStar.Interactive.PushHelper.fst b/src/fstar/FStar.Interactive.PushHelper.fst index f4154f25b01..ee89bd1f428 100644 --- 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 index a97f297bc8c..173c4b90699 100644 --- a/src/ocaml-output/FStar_Interactive_PushHelper.ml +++ b/src/ocaml-output/FStar_Interactive_PushHelper.ml @@ -788,8 +788,14 @@ let (ld_deps : | FStar_Pervasives.Inl st2 -> FStar_Pervasives.Inl (st2, deps)))) () with - | uu___ -> - (FStar_Compiler_Util.print_error "[E] Failed to load deps"; + | FStar_Errors.Err (e, msg, ctx) -> + (FStar_Compiler_Util.print1_error "[E] Failed to load deps. Error %s" + msg; + FStar_Pervasives.Inr st) + | exn -> + ((let uu___2 = FStar_Compiler_Util.message_of_exn exn in + FStar_Compiler_Util.print1_error "[E] Failed to load deps %s" + uu___2); FStar_Pervasives.Inr st) let (add_module_completions : Prims.string ->