From 084480c807b58947b8487eb3a7c6a71bb388a832 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Wed, 3 Apr 2024 17:01:27 +0200
Subject: added Error and EError to expressions and propagated related changes

---
 compiler/Errors.ml          | 5 +++--
 compiler/Extract.ml         | 8 ++++++++
 compiler/ExtractBase.ml     | 4 +++-
 compiler/ExtractTypes.ml    | 1 +
 compiler/Interpreter.ml     | 3 ++-
 compiler/PrintPure.ml       | 4 ++++
 compiler/Pure.ml            | 8 ++++++++
 compiler/PureMicroPasses.ml | 4 +++-
 compiler/PureTypeCheck.ml   | 1 +
 compiler/PureUtils.ml       | 3 +++
 compiler/SymbolicAst.ml     | 1 +
 compiler/SymbolicToPure.ml  | 4 ++++
 12 files changed, 41 insertions(+), 5 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Errors.ml b/compiler/Errors.ml
index 53e56c44..30887593 100644
--- a/compiler/Errors.ml
+++ b/compiler/Errors.ml
@@ -1,6 +1,7 @@
 let log = Logging.errors_log
 
-let meta_to_string (span : Meta.span) =
+let meta_to_string (meta : Meta.meta) =
+  let span = meta.span in
   let file = match span.file with Virtual s | Local s -> s in
   let loc_to_string (l : Meta.loc) : string =
     string_of_int l.line ^ ":" ^ string_of_int l.col
@@ -10,7 +11,7 @@ let meta_to_string (span : Meta.span) =
 
 let format_error_message (meta : Meta.meta option) (msg : string) =
   let meta =
-    match meta with None -> "" | Some meta -> "\n" ^ meta_to_string meta.span
+    match meta with None -> "" | Some meta -> "\n" ^ meta_to_string meta
   in
   msg ^ meta
 
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 1f9c9117..ef5d5dce 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -297,6 +297,13 @@ let lets_require_wrap_in_do (meta : Meta.meta)
     - application argument: [f (exp)]
     - match/if scrutinee: [if exp then _ else _]/[match exp | _ -> _]
  *)
+
+let extract_errors (fmt : F.formatter) =
+  match !Config.backend with
+  | FStar | Coq -> F.pp_print_string fmt "admit"
+  | Lean -> F.pp_print_string fmt "sorry"
+  | HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)"
+
 let rec extract_texpression (meta : Meta.meta) (ctx : extraction_ctx)
     (fmt : F.formatter) (inside : bool) (e : texpression) : unit =
   match e.e with
@@ -323,6 +330,7 @@ let rec extract_texpression (meta : Meta.meta) (ctx : extraction_ctx)
   | Loop _ ->
       (* The loop nodes should have been eliminated in {!PureMicroPasses} *)
       craise __FILE__ __LINE__ meta "Unreachable"
+  | EError (_, _) -> extract_errors fmt
 
 (* Extract an application *or* a top-level qualif (function extraction has
  * to handle top-level qualifiers, so it seemed more natural to merge the
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 74ac9e32..faca2bde 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1700,7 +1700,9 @@ let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx)
       | TLiteral lty -> (
           match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i")
       | TArrow _ -> "f"
-      | TTraitType (_, name) -> name_from_type_ident name)
+      | TTraitType (_, name) -> name_from_type_ident name
+      | Error -> "@Error")
+(* TODO : Check*)
 
 (** Generates a type variable basename. *)
 let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) :
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 1f0abf8a..350866e9 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -566,6 +566,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
               "Trait types are not supported yet when generating code for HOL4";
             extract_trait_ref meta ctx fmt no_params_tys false trait_ref;
             F.pp_print_string fmt ("." ^ add_brackets type_name))
+  | Error -> craise __FILE__ __LINE__ meta "TODO: Error message?"
 
 and extract_trait_ref (meta : Meta.meta) (ctx : extraction_ctx)
     (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool)
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index a65e1663..d0a54750 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -612,7 +612,8 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
 
   (* Evaluate the function *)
   let symbolic =
-    eval_function_body config (Option.get fdef.body).body cf_finish ctx
+    try eval_function_body config (Option.get fdef.body).body cf_finish ctx
+    with CFailure (meta, msg) -> Some (Error (meta, msg))
   in
 
   (* Return *)
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index d0c243bb..12d554f2 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -164,6 +164,7 @@ let rec ty_to_string (env : fmt_env) (inside : bool) (ty : ty) : string =
       let trait_ref = trait_ref_to_string env false trait_ref in
       let s = trait_ref ^ "::" ^ type_name in
       if inside then "(" ^ s ^ ")" else s
+  | Error -> "@Error"
 
 and generic_args_to_strings (env : fmt_env) (inside : bool)
     (generics : generic_args) : string list =
@@ -615,6 +616,9 @@ let rec texpression_to_string ?(metadata : Meta.meta option = None)
           let e = meta_s ^ "\n" ^ indent ^ e in
           if inside then "(" ^ e ^ ")" else e
       | MPlace _ -> "(" ^ meta_s ^ " " ^ e ^ ")")
+  | EError (meta, msg) ->
+      if Option.is_none meta then msg
+      else meta_to_string (Option.get meta) ^ " " ^ msg (* TODO formatting *)
 
 and app_to_string ?(meta : Meta.meta option = None) (env : fmt_env)
     (inside : bool) (indent : string) (indent_incr : string) (app : texpression)
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 7de7e0f4..7366783c 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -285,6 +285,7 @@ type ty =
   | TArrow of ty * ty
   | TTraitType of trait_ref * string
       (** The string is for the name of the associated type *)
+  | Error
 
 and trait_ref = {
   trait_id : trait_instance_id;
@@ -621,6 +622,7 @@ class ['self] iter_expression_base =
     method visit_qualif : 'env -> qualif -> unit = fun _ _ -> ()
     method visit_loop_id : 'env -> loop_id -> unit = fun _ _ -> ()
     method visit_field_id : 'env -> field_id -> unit = fun _ _ -> ()
+    method visit_meta : 'env -> Meta.meta -> unit = fun _ _ -> ()
   end
 
 (** Ancestor for {!map_expression} visitor *)
@@ -632,6 +634,7 @@ class ['self] map_expression_base =
     method visit_qualif : 'env -> qualif -> qualif = fun _ x -> x
     method visit_loop_id : 'env -> loop_id -> loop_id = fun _ x -> x
     method visit_field_id : 'env -> field_id -> field_id = fun _ x -> x
+    method visit_meta : 'env -> Meta.meta -> Meta.meta = fun _ x -> x
   end
 
 (** Ancestor for {!reduce_expression} visitor *)
@@ -643,6 +646,7 @@ class virtual ['self] reduce_expression_base =
     method visit_qualif : 'env -> qualif -> 'a = fun _ _ -> self#zero
     method visit_loop_id : 'env -> loop_id -> 'a = fun _ _ -> self#zero
     method visit_field_id : 'env -> field_id -> 'a = fun _ _ -> self#zero
+    method visit_meta : 'env -> Meta.meta -> 'a = fun _ _ -> self#zero
   end
 
 (** Ancestor for {!mapreduce_expression} visitor *)
@@ -662,6 +666,9 @@ class virtual ['self] mapreduce_expression_base =
 
     method visit_field_id : 'env -> field_id -> field_id * 'a =
       fun _ x -> (x, self#zero)
+
+    method visit_meta : 'env -> Meta.meta -> Meta.meta * 'a =
+      fun _ x -> (x, self#zero)
   end
 
 (** **Rk.:** here, {!expression} is not at all equivalent to the expressions
@@ -726,6 +733,7 @@ type expression =
   | Loop of loop  (** See the comments for {!loop} *)
   | StructUpdate of struct_update  (** See the comments for {!struct_update} *)
   | Meta of (emeta[@opaque]) * texpression  (** Meta-information *)
+  | EError of Meta.meta option * string
 
 and switch_body = If of texpression * texpression | Match of match_branch list
 and match_branch = { pat : typed_pattern; branch : texpression }
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 9fa07029..ebc5c65f 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -416,6 +416,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
       | StructUpdate supd -> update_struct_update supd ctx
       | Lambda (lb, e) -> update_lambda lb e ctx
       | Meta (meta, e) -> update_emeta meta e ctx
+      | EError (meta, msg) -> (ctx, EError (meta, msg))
     in
     (ctx, { e; ty })
   (* *)
@@ -1006,7 +1007,8 @@ let filter_useless (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
         match e with
         | Var _ | CVar _ | Const _ | App _ | Qualif _
         | Meta (_, _)
-        | StructUpdate _ | Lambda _ ->
+        | StructUpdate _ | Lambda _
+        | EError (_, _) ->
             super#visit_expression env e
         | Switch (scrut, switch) -> (
             match switch with
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index 53ff8983..098e2564 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -238,3 +238,4 @@ let rec check_texpression (meta : Meta.meta) (ctx : tc_ctx) (e : texpression) :
   | Meta (_, e_next) ->
       sanity_check __FILE__ __LINE__ (e_next.ty = e.ty) meta;
       check_texpression meta ctx e_next
+  | EError (meta, msg) -> craise_opt_meta __FILE__ __LINE__ meta msg
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 4bc90872..87f0b5f7 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -228,6 +228,9 @@ let rec let_group_requires_parentheses (meta : Meta.meta) (e : texpression) :
   | Loop _ ->
       (* Should have been eliminated *)
       craise __FILE__ __LINE__ meta "Unreachable"
+  | EError (meta, msg) ->
+      craise_opt_meta __FILE__ __LINE__ meta
+        msg (* TODO : check if true should'nt be returned instead ? *)
 
 let texpression_requires_parentheses meta e =
   match !Config.backend with
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index e164fd49..f15a2c23 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -212,6 +212,7 @@ type expression =
           TODO: merge this with Return.
        *)
   | Meta of emeta * expression  (** Meta information *)
+  | Error of Meta.meta option * string
 
 and loop = {
   loop_id : loop_id;
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 0c30f44c..1701891f 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1963,6 +1963,9 @@ let eval_ctx_to_symbolic_assignments_info (ctx : bs_ctx)
   (* Return the computed information *)
   !info
 
+let translate_meta (meta : Meta.meta option) (msg : string) : texpression =
+  { e = EError (meta, msg); ty = Error }
+
 let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
   match e with
   | S.Return (ectx, opt_v) ->
@@ -1989,6 +1992,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
       *)
       translate_forward_end ectx loop_input_values e back_e ctx
   | Loop loop -> translate_loop loop ctx
+  | Error (meta, msg) -> translate_meta meta msg
 
 and translate_panic (ctx : bs_ctx) : texpression =
   (* Here we use the function return type - note that it is ok because
-- 
cgit v1.2.3


From a2a219145587deb0ade9fa7d60171765cd722162 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Wed, 3 Apr 2024 17:36:09 +0200
Subject: added extract_ty_errors and extract_texpression_errors to deal with
 the error case in their respective types

---
 compiler/Extract.ml      | 4 ++--
 compiler/ExtractTypes.ml | 9 ++++++++-
 2 files changed, 10 insertions(+), 3 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index ef5d5dce..af0bf98d 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -298,7 +298,7 @@ let lets_require_wrap_in_do (meta : Meta.meta)
     - match/if scrutinee: [if exp then _ else _]/[match exp | _ -> _]
  *)
 
-let extract_errors (fmt : F.formatter) =
+let extract_texpression_errors (fmt : F.formatter) =
   match !Config.backend with
   | FStar | Coq -> F.pp_print_string fmt "admit"
   | Lean -> F.pp_print_string fmt "sorry"
@@ -330,7 +330,7 @@ let rec extract_texpression (meta : Meta.meta) (ctx : extraction_ctx)
   | Loop _ ->
       (* The loop nodes should have been eliminated in {!PureMicroPasses} *)
       craise __FILE__ __LINE__ meta "Unreachable"
-  | EError (_, _) -> extract_errors fmt
+  | EError (_, _) -> extract_texpression_errors fmt
 
 (* Extract an application *or* a top-level qualif (function extraction has
  * to handle top-level qualifiers, so it seemed more natural to merge the
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 350866e9..1c3657a3 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -433,6 +433,13 @@ let extract_literal_type (_ctx : extraction_ctx) (fmt : F.formatter)
       End
     ]}
  *)
+
+let extract_ty_errors (fmt : F.formatter) : unit =
+  match !Config.backend with
+  | FStar | Coq -> F.pp_print_string fmt "admit"
+  | Lean -> F.pp_print_string fmt "sorry"
+  | HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)"
+
 let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
     (no_params_tys : TypeDeclId.Set.t) (inside : bool) (ty : ty) : unit =
   let extract_rec = extract_ty meta ctx fmt no_params_tys in
@@ -566,7 +573,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
               "Trait types are not supported yet when generating code for HOL4";
             extract_trait_ref meta ctx fmt no_params_tys false trait_ref;
             F.pp_print_string fmt ("." ^ add_brackets type_name))
-  | Error -> craise __FILE__ __LINE__ meta "TODO: Error message?"
+  | Error -> extract_ty_errors fmt
 
 and extract_trait_ref (meta : Meta.meta) (ctx : extraction_ctx)
     (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool)
-- 
cgit v1.2.3


From 78cc58e3076ffd61add6d78b64371b6eb36d6ab2 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Wed, 3 Apr 2024 17:52:10 +0200
Subject: resolved requested changes

---
 compiler/ExtractBase.ml    | 2 +-
 compiler/PrintPure.ml      | 4 +---
 compiler/SymbolicToPure.ml | 4 ++--
 3 files changed, 4 insertions(+), 6 deletions(-)

(limited to 'compiler')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index faca2bde..e399a89c 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1701,7 +1701,7 @@ let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx)
           match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i")
       | TArrow _ -> "f"
       | TTraitType (_, name) -> name_from_type_ident name
-      | Error -> "@Error")
+      | Error -> "x")
 (* TODO : Check*)
 
 (** Generates a type variable basename. *)
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 12d554f2..97ea6048 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -616,9 +616,7 @@ let rec texpression_to_string ?(metadata : Meta.meta option = None)
           let e = meta_s ^ "\n" ^ indent ^ e in
           if inside then "(" ^ e ^ ")" else e
       | MPlace _ -> "(" ^ meta_s ^ " " ^ e ^ ")")
-  | EError (meta, msg) ->
-      if Option.is_none meta then msg
-      else meta_to_string (Option.get meta) ^ " " ^ msg (* TODO formatting *)
+  | EError (_, _) -> "@Error"
 
 and app_to_string ?(meta : Meta.meta option = None) (env : fmt_env)
     (inside : bool) (indent : string) (indent_incr : string) (app : texpression)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 1701891f..53ab1c08 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1963,7 +1963,7 @@ let eval_ctx_to_symbolic_assignments_info (ctx : bs_ctx)
   (* Return the computed information *)
   !info
 
-let translate_meta (meta : Meta.meta option) (msg : string) : texpression =
+let translate_error (meta : Meta.meta option) (msg : string) : texpression =
   { e = EError (meta, msg); ty = Error }
 
 let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
@@ -1992,7 +1992,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
       *)
       translate_forward_end ectx loop_input_values e back_e ctx
   | Loop loop -> translate_loop loop ctx
-  | Error (meta, msg) -> translate_meta meta msg
+  | Error (meta, msg) -> translate_error meta msg
 
 and translate_panic (ctx : bs_ctx) : texpression =
   (* Here we use the function return type - note that it is ok because
-- 
cgit v1.2.3


From cc0b77e4b75990916e331e9ff5c26c912341b13d Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Wed, 3 Apr 2024 17:58:10 +0200
Subject: resolved requested changes

---
 compiler/ExtractBase.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'compiler')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index e399a89c..ba75f580 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1702,7 +1702,6 @@ let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx)
       | TArrow _ -> "f"
       | TTraitType (_, name) -> name_from_type_ident name
       | Error -> "x")
-(* TODO : Check*)
 
 (** Generates a type variable basename. *)
 let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) :
-- 
cgit v1.2.3


From 16ea3ca854a77703487afa8732f247bc26cba695 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 4 Apr 2024 13:23:50 +0200
Subject: Now prints all errors in the error_list

---
 compiler/Errors.ml | 6 ++++++
 compiler/Main.ml   | 8 +++++---
 2 files changed, 11 insertions(+), 3 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Errors.ml b/compiler/Errors.ml
index 30887593..7dfe659a 100644
--- a/compiler/Errors.ml
+++ b/compiler/Errors.ml
@@ -20,6 +20,12 @@ let format_error_message_with_file_line (file : string) (line : int)
   "In file " ^ file ^ ", line " ^ string_of_int line ^ ":\n"
   ^ format_error_message meta msg
 
+let error_list_to_string (error_list : (Meta.meta option * string) list) :
+    string =
+  List.fold_left
+    (fun errors (meta, msg) -> errors ^ "\n" ^ format_error_message meta msg)
+    "" error_list
+
 exception CFailure of (Meta.meta option * string)
 
 let error_list : (Meta.meta option * string) list ref = ref []
diff --git a/compiler/Main.ml b/compiler/Main.ml
index db200f37..9e72a21b 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -274,12 +274,14 @@ let () =
 
          (* Translate the functions *)
          Aeneas.Translate.translate_crate filename dest_dir m
-       with Errors.CFailure (meta, msg) ->
+       with Errors.CFailure (_, _) ->
          (* In theory it shouldn't happen, but there may be uncaught errors -
             note that we let the [Failure] exceptions go through (they are
             send if we use the option [-abort-on-error] *)
-         log#serror (Errors.format_error_message meta msg);
-         exit 1);
+         if not (List.is_empty !Errors.error_list) then (
+           let errors = Errors.error_list_to_string !Errors.error_list in
+           log#serror errors;
+           exit 1));
 
       (* Print total elapsed time *)
       log#linfo
-- 
cgit v1.2.3


From 1f3ce79023d902d0145da38e878d991a6ba29236 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 15:47:54 +0200
Subject: Update the way errors are reported

---
 compiler/Errors.ml |  6 ------
 compiler/Main.ml   | 11 +++++++----
 2 files changed, 7 insertions(+), 10 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Errors.ml b/compiler/Errors.ml
index 7dfe659a..30887593 100644
--- a/compiler/Errors.ml
+++ b/compiler/Errors.ml
@@ -20,12 +20,6 @@ let format_error_message_with_file_line (file : string) (line : int)
   "In file " ^ file ^ ", line " ^ string_of_int line ^ ":\n"
   ^ format_error_message meta msg
 
-let error_list_to_string (error_list : (Meta.meta option * string) list) :
-    string =
-  List.fold_left
-    (fun errors (meta, msg) -> errors ^ "\n" ^ format_error_message meta msg)
-    "" error_list
-
 exception CFailure of (Meta.meta option * string)
 
 let error_list : (Meta.meta option * string) list ref = ref []
diff --git a/compiler/Main.ml b/compiler/Main.ml
index 9e72a21b..416f3a07 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -278,10 +278,13 @@ let () =
          (* In theory it shouldn't happen, but there may be uncaught errors -
             note that we let the [Failure] exceptions go through (they are
             send if we use the option [-abort-on-error] *)
-         if not (List.is_empty !Errors.error_list) then (
-           let errors = Errors.error_list_to_string !Errors.error_list in
-           log#serror errors;
-           exit 1));
+         ());
+
+      if !Errors.error_list <> [] then (
+        List.iter
+          (fun (meta, msg) -> log#serror (Errors.format_error_message meta msg))
+          !Errors.error_list;
+        exit 1);
 
       (* Print total elapsed time *)
       log#linfo
-- 
cgit v1.2.3


From 77208249c717579d1014f27592566069b8cd0eb2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 15:57:12 +0200
Subject: Fix a minor issue

---
 compiler/ExtractBase.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 6130528c..47b613c2 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -259,7 +259,7 @@ let report_name_collision (id_to_string : id -> string)
   let meta_to_string (meta : Meta.meta option) =
     match meta with
     | None -> ""
-    | Some meta -> "\n  " ^ Errors.meta_to_string meta.span
+    | Some meta -> "\n  " ^ Errors.meta_to_string meta
   in
   let id1 = "\n- " ^ id_to_string id1 ^ meta_to_string meta1 in
   let id2 = "\n- " ^ id_to_string id2 ^ meta_to_string meta2 in
-- 
cgit v1.2.3