Improve the error messages

3 files changed, 18 insertions, 6 deletions

diff --git a/compiler/Errors.ml b/compiler/Errors.ml
index 04fd708b..53e56c44 100644
--- a/compiler/Errors.ml
+++ b/compiler/Errors.ml
@@ -1,3 +1,5 @@
+let log = Logging.errors_log
+
 let meta_to_string (span : Meta.span) =
   let file = match span.file with Virtual s | Local s -> s in
   let loc_to_string (l : Meta.loc) : string =
@@ -14,7 +16,7 @@ let format_error_message (meta : Meta.meta option) (msg : string) =
 
 let format_error_message_with_file_line (file : string) (line : int)
     (meta : Meta.meta option) (msg : string) =
-  "In file:" ^ file ^ ", line:" ^ string_of_int line ^ "\n"
+  "In file " ^ file ^ ", line " ^ string_of_int line ^ ":\n"
   ^ format_error_message meta msg
 
 exception CFailure of (Meta.meta option * string)
@@ -28,13 +30,17 @@ let push_error (meta : Meta.meta option) (msg : string) =
 let save_error (file : string) (line : int) ?(throw : bool = false)
     (meta : Meta.meta option) (msg : string) =
   push_error meta msg;
-  if !Config.fail_hard && throw then
-    raise (Failure (format_error_message_with_file_line file line meta msg))
+  if !Config.fail_hard && throw then (
+    let msg = format_error_message_with_file_line file line meta msg in
+    log#serror (msg ^ "\n");
+    raise (Failure msg))
 
 let craise_opt_meta (file : string) (line : int) (meta : Meta.meta option)
     (msg : string) =
-  if !Config.fail_hard then
-    raise (Failure (format_error_message_with_file_line file line meta msg))
+  if !Config.fail_hard then (
+    let msg = format_error_message_with_file_line file line meta msg in
+    log#serror (msg ^ "\n");
+    raise (Failure (format_error_message_with_file_line file line meta msg)))
   else
     let () = push_error meta msg in
     raise (CFailure (meta, msg))
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 1a9b3baa..ad204f7a 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -2234,7 +2234,10 @@ let extract_trait_impl_register_names (ctx : extraction_ctx)
   (* For now we do not support overriding provided methods *)
   cassert __FILE__ __LINE__
     (trait_impl.provided_methods = [])
-    trait_impl.meta "Overriding provided methods is not supported yet";
+    trait_impl.meta
+    ("Overriding provided methods is not supported yet (overriden methods: "
+    ^ String.concat ", " (List.map fst trait_impl.provided_methods)
+    ^ ")");
   (* Everything is taken care of by {!extract_trait_decl_register_names} *but*
      the name of the implementation itself *)
   (* Compute the name *)
diff --git a/compiler/Logging.ml b/compiler/Logging.ml
index 9c20f32f..9b8019b2 100644
--- a/compiler/Logging.ml
+++ b/compiler/Logging.ml
@@ -3,6 +3,9 @@ include Charon.Logging
 (** Below, we create subgloggers for various submodules, so that we can precisely
     toggle logging on/off, depending on which information we need *)
 
+(** Logger for Errors *)
+let errors_log = L.get_logger "MainLogger.Errors"
+
 (** Logger for PrePasses *)
 let pre_passes_log = L.get_logger "MainLogger.PrePasses"