From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 4 Feb 2004 13:45:03 +0000 (+0000)
Subject: Improved regression testing reporting.
X-Git-Tag: V_0_2_3~73
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e02c6e8e53e94e0bc7e2556fcd67645f46b039fc;p=helm.git

Improved regression testing reporting.
---

diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile
index 0f3318ab2..c1aa8c60f 100644
--- a/helm/gTopLevel/Makefile
+++ b/helm/gTopLevel/Makefile
@@ -88,9 +88,9 @@ cleantest:
 tests/%.cic.test: tests/%.cic regtest
 	time ./regtest -gen $<
 test:
-	time ./regtest $(INTESTS)
+	./regtest $(INTESTS) 2> /dev/null
 envtest:
-	time ./regtest -dump $(INTESTS)
+	./regtest -dump $(INTESTS) 2> /dev/null
 
 ifneq ($(MAKECMDGOALS), depend)
    include .depend   
diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml
index 3a601e0c3..ecccf4579 100644
--- a/helm/gTopLevel/regtest.ml
+++ b/helm/gTopLevel/regtest.ml
@@ -29,8 +29,8 @@ let argc = Array.length Sys.argv
 
 let rawsep = "###"
 let sep = Pcre.regexp (sprintf "^%s" rawsep)
-let msg_prefix = "*** REGTEST *** "
-let print_msg s = prerr_endline (msg_prefix ^ s)
+let print s = print_string s
+let print_endline s = print_endline s
 
 type state = Term | EMetasenv | ETerm | EType | EReduced
 
@@ -112,35 +112,35 @@ let parse_regtest =
 let as_expected expected found = (* ignores "term" field *)
   let outcome = ref true in
   if expected.eterm <> found.eterm then begin
-    print_msg "Term mismatch";
-    print_msg "  expected:";
-    print_msg ("  " ^ expected.eterm);
-    print_msg "  found:";
-    print_msg ("  " ^ found.eterm);
+    print_endline "Term mismatch";
+    print_endline "  expected:";
+    print_endline ("  " ^ expected.eterm);
+    print_endline "  found:";
+    print_endline ("  " ^ found.eterm);
     outcome := false;
   end;
   if expected.emetasenv <> found.emetasenv then begin
-    print_msg "Metasenv mismatch";
-    print_msg "  expected:";
-    print_msg ("  " ^ expected.emetasenv);
-    print_msg "  found:";
-    print_msg ("  " ^ found.emetasenv);
+    print_endline "Metasenv mismatch";
+    print_endline "  expected:";
+    print_endline ("  " ^ expected.emetasenv);
+    print_endline "  found:";
+    print_endline ("  " ^ found.emetasenv);
     outcome := false;
   end;
   if expected.etype <> found.etype then begin
-    print_msg "Type mismatch";
-    print_msg "  expected:";
-    print_msg ("  " ^ expected.etype);
-    print_msg "  found:";
-    print_msg ("  " ^ found.etype);
+    print_endline "Type mismatch";
+    print_endline "  expected:";
+    print_endline ("  " ^ expected.etype);
+    print_endline "  found:";
+    print_endline ("  " ^ found.etype);
     outcome := false;
   end;
   if expected.ereduced <> found.ereduced then begin
-    print_msg "Reduced term mismatch";
-    print_msg "  expected:";
-    print_msg ("  " ^ expected.ereduced);
-    print_msg "  found:";
-    print_msg ("  " ^ found.ereduced);
+    print_endline "Reduced term mismatch";
+    print_endline "  expected:";
+    print_endline ("  " ^ expected.ereduced);
+    print_endline "  found:";
+    print_endline ("  " ^ found.ereduced);
     outcome := false;
   end;
   !outcome
@@ -201,12 +201,12 @@ let main generate dump fnames =
  if generate then
   begin
    (* gen mode *)
-   print_msg "[ Gen mode ]";
+   print_endline "[ Gen mode ]";
    List.iter
     (function fname ->
       let test_fname = fname ^ ".test" in
       let env_fname = fname ^ ".env" in
-      print_msg (sprintf "Generating regtest %s -> %s\n ..."
+      print_endline (sprintf "Generating regtest %s -> %s\n ..."
         fname test_fname);
       let raw_term = (parse_regtest fname).term in
       let result = test_this raw_term in
@@ -216,28 +216,34 @@ let main generate dump fnames =
   end else
    begin
     (* regtest mode *)
-    print_msg "[ Regtest mode ]";
+    print_endline "[ Regtest mode ]";
     let (ok, nok) = (ref 0, ref []) in
     List.iter
      (function fname ->
        let env_fname = fname ^ ".env" in
        let test_fname = fname ^ ".test" in
        restore_environment env_fname ;
-       prerr_endline ("# " ^ fname);
-       try
-         let expected = parse_regtest test_fname in
-         let actual = test_this expected.term in
-         if dump then dump_environment env_fname ;
-         if as_expected expected actual then
-           incr ok
-         else
-           nok := fname :: !nok;
-       with e -> nok := fname :: !nok
+       let time = Unix.gettimeofday () in
+       print ("Processing " ^ fname ^":\t") ;
+       let is_ok = 
+        try
+          let expected = parse_regtest test_fname in
+          let actual = test_this expected.term in
+          if dump then dump_environment env_fname ;
+          if as_expected expected actual then
+           (incr ok ; true)
+          else
+           (nok := fname :: !nok ; false)
+        with e -> (nok := fname :: !nok ; false)
+       in
+        let timediff = Unix.gettimeofday () -. time in
+         print (sprintf "done in %f seconds\t" timediff) ;
+         print_endline (if is_ok then "[   OK   ]" else "[ FAILED ]")
      ) fnames ;
-    print_msg "Regtest completed:";
-    print_msg (sprintf "Succeeded: %d" !ok);
-    print_msg (sprintf "Failed: %d" (List.length !nok));
-    List.iter (fun fname -> print_msg (sprintf "  %s failed :-(" fname))
+    print_endline "*** Summary ***";
+    print_endline (sprintf "Succeeded: %d" !ok);
+    print_endline (sprintf "Failed: %d" (List.length !nok));
+    List.iter (fun fname -> print_endline (sprintf "  %s failed :-(" fname))
       (List.rev !nok)
   end
 ;;