CWStopOnFailure

Author: monadius

README.md

@@ -35,6 +35,11 @@ Run `make .merlin` to create the `.merlin` file.
 
    Note that the `term` should be in parentheses.
 
+- `CWStopOnFailure 0/1`
+
+   This command controls whether Coq execution should be stopped after a failed test (`1`) or not (`0`).
+   The default behavior is to stop after the first failed test.
+
 - `CWGroup string`
 
    Begins a group of tests (outputs `<DESCRIBE::>`).

cw_example/SolutionTest.v

@@ -2,15 +2,17 @@ Require Solution.
 Require Import Preloaded.
 From CW Require Import Loader.
 
+CWStopOnFailure 0.
+
 CWGroup "Tests for Solution.solution".
   CWTest "Type test".
     (* The expected type should be in parentheses *)
-    Fail CWAssert "Should fail" Solution.solution : (1 + 1 = 2).
+    CWAssert "Should fail" Solution.solution : (1 + 1 = 2).
     CWAssert Solution.solution : (1 + 1 = 3).
   (* CWEndTest is optional before CWTest or CWEndGroup *)
   CWEndTest.
   CWTest "Assumptions test".
-    CWAssert "Testing solution" Solution.solution Assumes test_axiom.
+    CWAssert "Testing solution" Solution.solution Assumes. (*test_axiom.*)
   CWTest "Type test 2".
     Definition expected := 1 + 1 = 3.
     CWAssert Solution.solution : expected.

cw_example_extraction/SolutionTest.v

@@ -10,6 +10,8 @@ Extract Inductive nat => "int"
 Extract Constant plus => "( + )".
 Extract Constant mult => "( * )".
 
+(* CWStopOnFailure 0. *)
+
 CWGroup "Group".
 
 CWTest "Successful Extraction Test".

src/coq_cw.ml

@@ -11,15 +11,15 @@ let format_msg =
 let display tag msg =
   Feedback.msg_notice (str (Printf.sprintf "\n<%s::>%s\n" tag (format_msg msg)))
 
-let passed = display "PASSED"
-
-let failed = display "FAILED"
+let stop_on_failure_flag = ref true
 
 type group = {
   tag : string;
   start_time : float
 }
 
+let stop_on_failure v = stop_on_failure_flag := v <> 0
+
 let mk_group tag t = { tag = tag; start_time = t }
 
 let group_stack = Summary.ref ~name:"open_groups" ([] : group list)
@@ -49,6 +49,15 @@ let rec end_all_groups () =
   | [] -> ()
   | {tag = tag} :: gs -> end_group tag; end_all_groups ()
 
+let passed = display "PASSED"
+
+let failed msg = 
+  display "FAILED" msg;
+  if !stop_on_failure_flag then begin
+    end_all_groups ();
+    CErrors.user_err (str msg)
+  end
+
 let locate r =
   try
     let gr = Smartlocate.locate_global_with_alias r in
@@ -67,9 +76,8 @@ let test_type ?(msg = "Type Test") r c_ty =
     let p_actual = Printer.pr_econstr_env env sigma actual_ty in
     let p_expected = Printer.pr_econstr_env env sigma expected_ty in
     failed (Printf.sprintf "%s\nActual type = %s\nExpected type = %s"
-              msg (string_of_ppcmds p_actual) (string_of_ppcmds p_expected));
-    end_all_groups ();
-    CErrors.user_err (str "Incorrect Type: " ++ Printer.pr_econstr_env env sigma tm)
+              msg (string_of_ppcmds p_actual) (string_of_ppcmds p_expected))
+    (* CErrors.user_err (str "Incorrect Type: " ++ Printer.pr_econstr_env env sigma tm) *)
 
 (* Based on the PrintAssumptions code from vernac/vernacentries.ml *)
 let assumptions r =
@@ -106,9 +114,8 @@ let test_axioms ?(msg = "Axiom Test") c_ref ax_refs =
     | Printer.Axiom (ax, _) ->
       if Printer.ContextObjectSet.mem t ax_set then ()
       else begin
-        failed msg;
-        end_all_groups ();
-        CErrors.user_err (str "Prohibited Axiom: " ++ pr_axiom env sigma ax ty)
+        let p_axiom = pr_axiom env sigma ax ty in
+        failed (Printf.sprintf "%s\nProhibited Axiom: %s" msg (string_of_ppcmds p_axiom))
       end
     | _ -> ()
   in
@@ -123,9 +130,7 @@ let test_file_size ?(fname = solution_file) size =
       passed (Format.sprintf "Size %d < %d" stats.Unix.st_size size)
     else begin
       let msg = Format.sprintf "Size %d >= %d" stats.Unix.st_size size in 
-      failed msg;
-      end_all_groups ();
-      CErrors.user_err (str msg)
+      failed msg
     end
   with Unix.Unix_error _ -> CErrors.user_err (str ("Bad file name: " ^ fname))
 
@@ -140,22 +145,15 @@ let test_file_regex ?(fname = solution_file) match_flag regex =
                 with Not_found -> false in
   if matched = match_flag then
     passed "OK"
-  else begin
-    failed "Bad match";
-    end_all_groups ();
-    CErrors.user_err (str "Bad match")
-  end
+  else
+    failed "Bad match"
 
-let run_system_command ?err_msg args =
+let run_system_command ?(err_msg = "Failed") args =
   let cmd = String.concat " " args in
   Printf.printf "Running: %s" cmd;
-  match Unix.system cmd with
-  | Unix.WEXITED 0 -> ()
-  | _ ->
-    let msg = match err_msg with None -> "Failed" | Some msg -> msg in
-    failed msg;
-    end_all_groups ();
-    CErrors.user_err (str msg)
+  match Unix.system (cmd ^ " 2>&1") with
+  | Unix.WEXITED 0 -> true
+  | _ -> (failed err_msg; false)
 
 let write_file fname str =
   let oc = open_out fname in
@@ -165,7 +163,7 @@ let write_file fname str =
 (** Compiles and runs the given OCaml source files *)
 let compile_and_run files ?(options = "") driver_code =
   write_file driver_file driver_code;
-  run_system_command ~err_msg:"Compilation failed" ([ocaml_compiler; options] @ files @ [driver_file]);
-  passed "OK";
-  run_system_command ["./a.out"];
-  passed "OK"
+  if run_system_command ~err_msg:"Compilation failed" ([ocaml_compiler; options] @ files @ [driver_file]) then begin
+    passed "OK";
+    if run_system_command ["./a.out"] then passed "OK"
+  end

src/coq_cw.mli

@@ -8,6 +8,8 @@ val test_file_regex : ?fname:string -> bool -> string -> unit
 
 val compile_and_run : string list -> ?options:string -> string -> unit
 
+val stop_on_failure : int -> unit
+
 val begin_group : string -> string -> unit
 
 val end_group : string -> unit

src/g_coq_cw.ml4

@@ -14,6 +14,12 @@ VERNAC COMMAND EXTEND CWAssertAssumptions CLASSIFIED AS QUERY
     ]
 END
 
+VERNAC COMMAND EXTEND CWStopOnFailure CLASSIFIED AS SIDEFF
+| [ "CWStopOnFailure" int(flag)] -> [
+        Coq_cw.stop_on_failure flag
+    ]
+END
+
 VERNAC COMMAND EXTEND CWGroup CLASSIFIED AS SIDEFF
 | [ "CWGroup" string(msg)] -> [ 
         Coq_cw.begin_group "DESCRIBE" msg