No batching of warning/errors

src/basic/FStarC.Errors.fst

@@ -320,41 +320,57 @@ let fixup_issue_range (rng:option Range.range) : option Range.range =
   in
   map_opt rng maybe_bound_range
 
-let mk_default_handler print =
-    let issues : ref (list issue) = mk_ref [] in
-    (* This number may be greater than the amount of 'EErrors'
-     * in the list above due to errors that were immediately
-     * printed (if debug_any()) *)
-    let err_count : ref int = mk_ref 0 in
-
-    let add_one (e: issue) =
-        let e = { e with issue_range = fixup_issue_range e.issue_range } in
-        (if e.issue_level = EError then
-           err_count := 1 + !err_count);
-        begin match e.issue_level with
-          | EInfo when print -> print_issue e
-          | _ when print && Debug.any () -> print_issue e
-          | _ -> issues := e :: !issues
-        end;
-        if Options.defensive_abort () && e.issue_number = Some defensive_errno then
-          failwith "Aborting due to --defensive abort";
-        ()
-    in
-    let count_errors () = !err_count in
-    let report () =
-        let unique_issues = BU.remove_dups (fun i0 i1 -> i0=i1) !issues in
-        let sorted_unique_issues = List.sortWith compare_issues unique_issues in
-        if print then List.iter print_issue sorted_unique_issues;
-        sorted_unique_issues
-    in
-    let clear () = issues := []; err_count := 0 in
-    { eh_name = "default handler (print=" ^ string_of_bool print ^ ")";
-      eh_add_one = add_one;
-      eh_count_errors = count_errors;
-      eh_report = report;
-      eh_clear = clear }
-
-let default_handler = mk_default_handler true
+(* This handler prints to the error output immediately. *)
+let mk_default_handler () =
+  let err_count : ref int = mk_ref 0 in
+
+  let add_one (e: issue) =
+      (if e.issue_level = EError then
+         err_count := 1 + !err_count);
+      print_issue e;
+
+      (* We may abort if we are debugging. *)
+      if e.issue_level <> EInfo then begin
+        Options.abort_counter := !Options.abort_counter - 1;
+        if !Options.abort_counter = 0 then
+          failwith "Aborting due to --abort_on"
+      end;
+      if Options.defensive_abort () && e.issue_number = Some defensive_errno then
+        failwith "Aborting due to --defensive abort";
+      ()
+  in
+  let count_errors () = !err_count in
+  let report () = [] in (* we just print them directly *)
+  let clear () = err_count := 0 in
+  { eh_name = "default handler";
+    eh_add_one = add_one;
+    eh_count_errors = count_errors;
+    eh_report = report;
+    eh_clear = clear }
+
+(* This is a single long-living instance of a default handler. *)
+let default_handler = mk_default_handler ()
+
+(* This handle collects all issues, and never prints. It is for
+@@expect_failure and other similar scenarios. *)
+let mk_catch_handler () =
+  let issues : ref (list issue) = mk_ref [] in
+  let err_count : ref int = mk_ref 0 in
+
+  let add_one (e: issue) =
+      (if e.issue_level = EError then
+         err_count := 1 + !err_count);
+      issues := e :: !issues;
+      ()
+  in
+  let count_errors () = !err_count in
+  let report () = !issues in
+  let clear () = issues := []; err_count := 0 in
+  { eh_name = "catch handler";
+    eh_add_one = add_one;
+    eh_count_errors = count_errors;
+    eh_report = report;
+    eh_clear = clear }
 
 let current_handler =
     mk_ref default_handler
@@ -371,12 +387,8 @@ let get_err_count () = (!current_handler).eh_count_errors ()
 
 let wrapped_eh_add_one (h : error_handler) (issue : issue) : unit =
     (* Try to set a good use range if we got an empty/dummy one *)
-    h.eh_add_one issue;
-    if issue.issue_level <> EInfo then begin
-      Options.abort_counter := !Options.abort_counter - 1;
-      if !Options.abort_counter = 0 then
-        failwith "Aborting due to --abort_on"
-    end
+    let issue = { issue with issue_range = fixup_issue_range issue.issue_range } in
+    h.eh_add_one issue
 
 let add_one issue =
     atomically (fun () -> wrapped_eh_add_one (!current_handler) issue)
@@ -643,7 +655,7 @@ let with_ctx_if (b:bool) (s:string) (f : unit -> 'a) : 'a =
 // restores handler back
 //
 let catch_errors_aux (f : unit -> 'a) : list issue & list issue & option 'a =
-  let newh = mk_default_handler false in
+  let newh = mk_catch_handler () in
   let old = !current_handler in
   current_handler := newh;
   let finally_restore () =

src/basic/FStarC.Errors.fsti

@@ -51,8 +51,10 @@ val call_to_erased_errno : int
 
 val update_flags : list (error_flag & string) -> list error_setting
 
+type context_t = list string
+
 (* error code, message, source position, and error context *)
-type error = error_code & error_message & FStarC.Range.range & list string
+type error = error_code & error_message & Range.range & context_t
 
 exception Error   of error
 exception Warning of error
@@ -85,6 +87,8 @@ type error_handler = {
     eh_clear: unit -> unit
 }
 
+val mk_catch_handler () : error_handler
+
 val string_of_issue_level : issue_level -> string
 val issue_level_of_string : string -> issue_level
 val issue_message : issue -> error_message

src/interactive/FStarC.Interactive.Ide.fst

@@ -1213,25 +1213,8 @@ let rec go st : int =
   | Inl st' -> go st'
   | Inr exitcode -> exitcode
 
-let interactive_error_handler = // No printing here — collect everything for future use
-  let issues : ref (list issue) = mk_ref [] in
-  let add_one (e: issue) =
-    let e = { e with issue_range = FStarC.Errors.fixup_issue_range e.issue_range } in
-    issues := e :: !issues
-  in
-  let count_errors () =
-    let issues = Util.remove_dups (fun i0 i1 -> i0=i1) !issues in
-    List.length (List.filter (fun e -> e.issue_level = EError) issues)
-  in
-  let report () =
-    List.sortWith compare_issues (Util.remove_dups (fun i0 i1 -> i0=i1) !issues)
-  in
-  let clear () = issues := [] in
-  { eh_name = "interactive error handler";
-    eh_add_one = add_one;
-    eh_count_errors = count_errors;
-    eh_report = report;
-    eh_clear = clear }
+// No printing here — collect everything for future use
+let interactive_error_handler = Errors.mk_catch_handler ()
 
 let interactive_printer printer =
   { printer_prinfo = (fun s -> forward_message printer "info" (JsonStr s));

src/typechecker/FStarC.TypeChecker.TcTerm.fst

@@ -3865,13 +3865,14 @@ and check_top_level_let env e =
                  g1, e1, univs, TcComm.lcomp_of_comp c1
          in
 
-         (* Check that it doesn't have a top-level effect; warn if it does *)
+         (* Check that it doesn't have a top-level effect; warn if it does.
+            Do not warn in phase1 to avoid double errors.*)
          let e2, c1 =
            let ok, c1 = TcUtil.check_top_level env g1 c1 in //check that it has no effect and a trivial pre-condition
            if ok
            then e2, c1
            else (
-             if not (Options.ml_ish ()) then
+             if not (Options.ml_ish ()) && not env.phase1 then
                Err.warn_top_level_effect (Env.get_range env); // maybe warn
              mk (Tm_meta {tm=e2; meta=Meta_desugared Masked_effect}) e2.pos, c1 //and tag it as masking an effect
            )

tests/error-messages/AQualMismatch.fst.json_output.expected

@@ -1,5 +1,5 @@
+{"msg":["AQualMismatch.f\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"AQualMismatch.fst","start_pos":{"line":3,"col":4},"end_pos":{"line":3,"col":5}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":3,"col":4},"end_pos":{"line":3,"col":5}}},"number":240,"ctx":["While desugaring module AQualMismatch"]}
 >> Got issues: [
 {"msg":["Inconsistent implicit argument annotation on argument x","Got: '#'","Expected: ''"],"level":"Error","range":{"def":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":7},"end_pos":{"line":6,"col":8}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":7},"end_pos":{"line":6,"col":8}}},"number":91,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]}
 >>]
-{"msg":["AQualMismatch.f\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"AQualMismatch.fst","start_pos":{"line":3,"col":4},"end_pos":{"line":3,"col":5}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":3,"col":4},"end_pos":{"line":3,"col":5}}},"number":240,"ctx":["While desugaring module AQualMismatch"]}
 {"msg":["Missing definitions in module AQualMismatch: f"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":0},"end_pos":{"line":6,"col":12}}},"number":240,"ctx":[]}

tests/error-messages/AQualMismatch.fst.output.expected

@@ -1,14 +1,14 @@
+* Warning 240 at AQualMismatch.fst(3,4-3,5):
+  - AQualMismatch.f is declared but no definition was found
+  - Add an 'assume' if this is intentional
+
 >> Got issues: [
 * Error 91 at AQualMismatch.fst(6,7-6,8):
   - Inconsistent implicit argument annotation on argument x
   - Got: '#'
   - Expected: ''
 
 >>]
-* Warning 240 at AQualMismatch.fst(3,4-3,5):
-  - AQualMismatch.f is declared but no definition was found
-  - Add an 'assume' if this is intentional
-
 * Warning 240 at AQualMismatch.fst(6,0-6,12):
   - Missing definitions in module AQualMismatch: f
 

tests/error-messages/ArgsAndQuals.fst.json_output.expected

@@ -1,5 +1,5 @@
+{"msg":["ArgsAndQuals.test1\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":23,"col":4},"end_pos":{"line":23,"col":9}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":23,"col":4},"end_pos":{"line":23,"col":9}}},"number":240,"ctx":["While desugaring module ArgsAndQuals"]}
 >> Got issues: [
 {"msg":["Inconsistent implicit argument annotation on argument uu___","Got: '#'","Expected: '$'"],"level":"Error","range":{"def":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":16},"end_pos":{"line":25,"col":18}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":16},"end_pos":{"line":25,"col":18}}},"number":91,"ctx":["While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]}
 >>]
-{"msg":["ArgsAndQuals.test1\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":23,"col":4},"end_pos":{"line":23,"col":9}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":23,"col":4},"end_pos":{"line":23,"col":9}}},"number":240,"ctx":["While desugaring module ArgsAndQuals"]}
 {"msg":["Missing definitions in module ArgsAndQuals: test1"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":0},"end_pos":{"line":25,"col":29}}},"number":240,"ctx":[]}

tests/error-messages/ArgsAndQuals.fst.output.expected

@@ -1,14 +1,14 @@
+* Warning 240 at ArgsAndQuals.fst(23,4-23,9):
+  - ArgsAndQuals.test1 is declared but no definition was found
+  - Add an 'assume' if this is intentional
+
 >> Got issues: [
 * Error 91 at ArgsAndQuals.fst(25,16-25,18):
   - Inconsistent implicit argument annotation on argument uu___
   - Got: '#'
   - Expected: '$'
 
 >>]
-* Warning 240 at ArgsAndQuals.fst(23,4-23,9):
-  - ArgsAndQuals.test1 is declared but no definition was found
-  - Add an 'assume' if this is intentional
-
 * Warning 240 at ArgsAndQuals.fst(25,0-25,29):
   - Missing definitions in module ArgsAndQuals: test1
 

tests/error-messages/Bug3232b.fst.json_output.expected

@@ -1,5 +1,5 @@
+{"msg":["Bug3232b.f\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"Bug3232b.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}},"use":{"file_name":"Bug3232b.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}}},"number":240,"ctx":["While desugaring module Bug3232b"]}
 >> Got issues: [
 {"msg":["Inconsistent qualifier annotations on\nBug3232b.f","Expected '[inline_for_extraction]'\ngot '[noextract, inline_for_extraction]'","","Only in definition: '[noextract]'"],"level":"Error","range":{"def":{"file_name":"Bug3232b.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}},"use":{"file_name":"Bug3232b.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}}},"number":93,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]}
 >>]
-{"msg":["Bug3232b.f\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"Bug3232b.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}},"use":{"file_name":"Bug3232b.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}}},"number":240,"ctx":["While desugaring module Bug3232b"]}
 {"msg":["Missing definitions in module Bug3232b: f"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"Bug3232b.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}}},"number":240,"ctx":[]}

tests/error-messages/Bug3232b.fst.output.expected

@@ -1,14 +1,14 @@
+* Warning 240 at Bug3232b.fst(4,4-4,5):
+  - Bug3232b.f is declared but no definition was found
+  - Add an 'assume' if this is intentional
+
 >> Got issues: [
 * Error 93 at Bug3232b.fst(8,0-8,12):
   - Inconsistent qualifier annotations on Bug3232b.f
   - Expected '[inline_for_extraction]' got '[noextract, inline_for_extraction]'
   - Only in definition: '[noextract]'
 
 >>]
-* Warning 240 at Bug3232b.fst(4,4-4,5):
-  - Bug3232b.f is declared but no definition was found
-  - Add an 'assume' if this is intentional
-
 * Warning 240 at Bug3232b.fst(8,0-8,12):
   - Missing definitions in module Bug3232b: f
 

tests/error-messages/Bug3232c.fst.json_output.expected

@@ -1,5 +1,5 @@
+{"msg":["Bug3232c.f\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"Bug3232c.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}},"use":{"file_name":"Bug3232c.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}}},"number":240,"ctx":["While desugaring module Bug3232c"]}
 >> Got issues: [
 {"msg":["Inconsistent qualifier annotations on\nBug3232c.f","Expected '[inline_for_extraction, noextract]'\ngot '[noextract]'","Only in declaration: '[inline_for_extraction]'",""],"level":"Error","range":{"def":{"file_name":"Bug3232c.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}},"use":{"file_name":"Bug3232c.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}}},"number":93,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]}
 >>]
-{"msg":["Bug3232c.f\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"Bug3232c.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}},"use":{"file_name":"Bug3232c.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}}},"number":240,"ctx":["While desugaring module Bug3232c"]}
 {"msg":["Missing definitions in module Bug3232c: f"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"Bug3232c.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}}},"number":240,"ctx":[]}

tests/error-messages/Bug3232c.fst.output.expected

@@ -1,14 +1,14 @@
+* Warning 240 at Bug3232c.fst(4,4-4,5):
+  - Bug3232c.f is declared but no definition was found
+  - Add an 'assume' if this is intentional
+
 >> Got issues: [
 * Error 93 at Bug3232c.fst(8,0-8,12):
   - Inconsistent qualifier annotations on Bug3232c.f
   - Expected '[inline_for_extraction, noextract]' got '[noextract]'
   - Only in declaration: '[inline_for_extraction]'
 
 >>]
-* Warning 240 at Bug3232c.fst(4,4-4,5):
-  - Bug3232c.f is declared but no definition was found
-  - Add an 'assume' if this is intentional
-
 * Warning 240 at Bug3232c.fst(8,0-8,12):
   - Missing definitions in module Bug3232c: f
 

tests/error-messages/Bug3232d.fst.json_output.expected

@@ -1,5 +1,5 @@
+{"msg":["Bug3232d.f\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"Bug3232d.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}},"use":{"file_name":"Bug3232d.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}}},"number":240,"ctx":["While desugaring module Bug3232d"]}
 >> Got issues: [
 {"msg":["Inconsistent qualifier annotations on\nBug3232d.f","Expected '[inline_for_extraction]'\ngot '[noextract]'","Only in declaration: '[inline_for_extraction]'","Only in definition: '[noextract]'"],"level":"Error","range":{"def":{"file_name":"Bug3232d.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}},"use":{"file_name":"Bug3232d.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}}},"number":93,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]}
 >>]
-{"msg":["Bug3232d.f\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"Bug3232d.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}},"use":{"file_name":"Bug3232d.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}}},"number":240,"ctx":["While desugaring module Bug3232d"]}
 {"msg":["Missing definitions in module Bug3232d: f"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"Bug3232d.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}}},"number":240,"ctx":[]}

tests/error-messages/Bug3232d.fst.output.expected

@@ -1,3 +1,7 @@
+* Warning 240 at Bug3232d.fst(4,4-4,5):
+  - Bug3232d.f is declared but no definition was found
+  - Add an 'assume' if this is intentional
+
 >> Got issues: [
 * Error 93 at Bug3232d.fst(8,0-8,12):
   - Inconsistent qualifier annotations on Bug3232d.f
@@ -6,10 +10,6 @@
   - Only in definition: '[noextract]'
 
 >>]
-* Warning 240 at Bug3232d.fst(4,4-4,5):
-  - Bug3232d.f is declared but no definition was found
-  - Add an 'assume' if this is intentional
-
 * Warning 240 at Bug3232d.fst(8,0-8,12):
   - Missing definitions in module Bug3232d: f
 

tests/error-messages/DecreasesTypeWarning.fst.json_output.expected

@@ -1,2 +1,2 @@
-{"msg":["In the decreases clause for this function, the SMT solver may not be able to\nprove that the types of\n  x (bound in DecreasesTypeWarning.fst(3,11-3,12))\nand xs (bound in DecreasesTypeWarning.fst(5,7-5,9))\nare equal.","The type of the first term is: Prims.nat","The type of the second term is: Prims.list Prims.nat","If the proof fails, try annotating these with the same type."],"level":"Warning","range":{"def":{"file_name":"DecreasesTypeWarning.fst","start_pos":{"line":3,"col":11},"end_pos":{"line":3,"col":12}},"use":{"file_name":"DecreasesTypeWarning.fst","start_pos":{"line":3,"col":11},"end_pos":{"line":3,"col":12}}},"number":290,"ctx":["While typechecking the top-level declaration `let rec f and g`"]}
 {"msg":["In the decreases clause for this function, the SMT solver may not be able to\nprove that the types of\n  xs (bound in DecreasesTypeWarning.fst(5,7-5,9))\nand x (bound in DecreasesTypeWarning.fst(3,11-3,12))\nare equal.","The type of the first term is: Prims.list Prims.nat","The type of the second term is: Prims.nat","If the proof fails, try annotating these with the same type."],"level":"Warning","range":{"def":{"file_name":"DecreasesTypeWarning.fst","start_pos":{"line":5,"col":7},"end_pos":{"line":5,"col":9}},"use":{"file_name":"DecreasesTypeWarning.fst","start_pos":{"line":5,"col":7},"end_pos":{"line":5,"col":9}}},"number":290,"ctx":["While typechecking the top-level declaration `let rec f and g`"]}
+{"msg":["In the decreases clause for this function, the SMT solver may not be able to\nprove that the types of\n  x (bound in DecreasesTypeWarning.fst(3,11-3,12))\nand xs (bound in DecreasesTypeWarning.fst(5,7-5,9))\nare equal.","The type of the first term is: Prims.nat","The type of the second term is: Prims.list Prims.nat","If the proof fails, try annotating these with the same type."],"level":"Warning","range":{"def":{"file_name":"DecreasesTypeWarning.fst","start_pos":{"line":3,"col":11},"end_pos":{"line":3,"col":12}},"use":{"file_name":"DecreasesTypeWarning.fst","start_pos":{"line":3,"col":11},"end_pos":{"line":3,"col":12}}},"number":290,"ctx":["While typechecking the top-level declaration `let rec f and g`"]}