New framework for regression of bad tests.

Now do_test.sh should always return OK if everything is "correct"
(i.e. if good tests are OK and bad tests FAIL with the expected output)

diff --git a/helm/matita/contribs/LAMBDA-TYPES/Makefile b/helm/matita/contribs/LAMBDA-TYPES/Makefile
index fc2e0ce8438c3c038c9db5486cf76ac3bb2908d0..c12b0fb43fc2328504fc16b1d0a15cdb13515ea9 100644 (file)
--- a/helm/matita/contribs/LAMBDA-TYPES/Makefile
+++ b/helm/matita/contribs/LAMBDA-TYPES/Makefile
@@ -6,8 +6,8 @@ ifeq ($(NODB),true)
        MATITA_FLAGS += -nodb
 endif
 
-MATITAC=../../scripts/do_tests.sh $(DO_TESTS_OPTS) "../../matitac $(MATITA_FLAGS)" "../../matitaclean $(MATITA_FLAGS)" /dev/null
-MATITACOPT=../../scripts/do_tests.sh $(DO_TESTS_OPTS) "../../matitac.opt $(MATITA_FLAGS)" "../../matitaclean.opt $(MATITA_FLAGS)" /dev/null
+MATITAC=../../scripts/do_tests.sh $(DO_TESTS_OPTS) "../../matitac $(MATITA_FLAGS)" "../../matitaclean $(MATITA_FLAGS)" /dev/null OK
+MATITACOPT=../../scripts/do_tests.sh $(DO_TESTS_OPTS) "../../matitac.opt $(MATITA_FLAGS)" "../../matitaclean.opt $(MATITA_FLAGS)" /dev/null OK
 VERBOSEMATITAC=../../matitac $(MATITA_FLAGS)
 VERBOSEMATITACOPT=../../matitac.opt $(MATITA_FLAGS)
 

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/Makefile b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/Makefile
index fc2e0ce8438c3c038c9db5486cf76ac3bb2908d0..c12b0fb43fc2328504fc16b1d0a15cdb13515ea9 100644 (file)
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/Makefile
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/Makefile
@@ -6,8 +6,8 @@ ifeq ($(NODB),true)
        MATITA_FLAGS += -nodb
 endif
 
-MATITAC=../../scripts/do_tests.sh $(DO_TESTS_OPTS) "../../matitac $(MATITA_FLAGS)" "../../matitaclean $(MATITA_FLAGS)" /dev/null
-MATITACOPT=../../scripts/do_tests.sh $(DO_TESTS_OPTS) "../../matitac.opt $(MATITA_FLAGS)" "../../matitaclean.opt $(MATITA_FLAGS)" /dev/null
+MATITAC=../../scripts/do_tests.sh $(DO_TESTS_OPTS) "../../matitac $(MATITA_FLAGS)" "../../matitaclean $(MATITA_FLAGS)" /dev/null OK
+MATITACOPT=../../scripts/do_tests.sh $(DO_TESTS_OPTS) "../../matitac.opt $(MATITA_FLAGS)" "../../matitaclean.opt $(MATITA_FLAGS)" /dev/null OK
 VERBOSEMATITAC=../../matitac $(MATITA_FLAGS)
 VERBOSEMATITACOPT=../../matitac.opt $(MATITA_FLAGS)
 

diff --git a/helm/matita/library/Makefile b/helm/matita/library/Makefile
index 607e57f41db8ee5a6ce9b57a32f0309f3ff44795..e13b3e8a48d6c05fb5e07f19043e285192c24309 100644 (file)
--- a/helm/matita/library/Makefile
+++ b/helm/matita/library/Makefile
@@ -6,8 +6,8 @@ ifeq ($(NODB),true)
        MATITA_FLAGS += -nodb
 endif
 
-MATITAC=../scripts/do_tests.sh $(DO_TESTS_OPTS) "../matitac $(MATITA_FLAGS)" "../matitaclean $(MATITA_FLAGS)" /dev/null
-MATITACOPT=../scripts/do_tests.sh $(DO_TESTS_OPTS) "../matitac.opt $(MATITA_FLAGS)" "../matitaclean.opt $(MATITA_FLAGS)" /dev/null
+MATITAC=../scripts/do_tests.sh $(DO_TESTS_OPTS) "../matitac $(MATITA_FLAGS)" "../matitaclean $(MATITA_FLAGS)" /dev/null OK
+MATITACOPT=../scripts/do_tests.sh $(DO_TESTS_OPTS) "../matitac.opt $(MATITA_FLAGS)" "../matitaclean.opt $(MATITA_FLAGS)" /dev/null OK
 VERBOSEMATITAC=../matitac $(MATITA_FLAGS)
 VERBOSEMATITACOPT=../matitac.opt $(MATITA_FLAGS)
 

diff --git a/helm/matita/library/list/sort.ma b/helm/matita/library/list/sort.ma
index 1cc127759f0b37f8778491389718224a0215a85f..ffd1e21872cd85c53c38fd3c9c518bc3a381a211 100644 (file)
--- a/helm/matita/library/list/sort.ma
+++ b/helm/matita/library/list/sort.ma
@@ -48,6 +48,26 @@ let rec insert (A:Set) (le: A → A → bool) x (l: list A) on l ≝
        | false ⇒ he::(insert A le x l')
        ]
   ].
+(*
+theorem insert_ind:
+ ∀A:Set. ∀le: A → A → bool. ∀x:A.
+  ∀P: list A → Prop.
+   ∀l:list A. P (insert A le x l).
+ intros (A le x P H l).
+ apply (
+ let rec insert_ind (l: list A) ≝
+  match l in list return λl.P (insert A le x l) with
+   [ nil ⇒ (? : P [x])
+   | (cons he l') ⇒
+       match le x he return λb.P (match b with [ true ⇒ x::he::l' | false ⇒ he::(insert A le x l') ]) with
+        [ true ⇒ (H2 : P (x::he::l'))
+        | false ⇒ (? : P (he::(insert A le x l')))
+        ]
+   ]
+ in
+  insert_ind l).
+qed.
+*)
 
 let rec insertionsort (A:Set) (le: A → A → bool) (l: list A) on l ≝
  match l with
@@ -56,7 +76,7 @@ let rec insertionsort (A:Set) (le: A → A → bool) (l: list A) on l ≝
       let l'' ≝ insertionsort A le l' in
        insert A le he l''
   ].
-  
+
 lemma ordered_injective:
   ∀ A:Set. ∀ le:A → A → bool.
   ∀ l:list A.
@@ -90,6 +110,65 @@ lemma ordered_injective:
   ].
 qed.
 
+(*
+lemma insert_sorted:
+  \forall A:Set. \forall le:A\to A\to bool.
+  (\forall a,b:A. le a b = false \to le b a = true) \to
+  \forall l:list A. \forall x:A.
+    ordered A le l = true \to ordered A le (insert A le x l) = true.
+ intros (A le H l x K).
+ letin P ≝ (\lambda ll. ordered A le ll = true).
+ fold simplify (P (insert A le x l)).
+ apply (
+  let rec insert_ind (l: list A) \def
+  match l in list return λli. l = li → P (insert A le x li) with
+   [ nil ⇒ (? : l = [] → P [x])
+   | (cons he l') ⇒
+       match le x he
+       return
+        λb. le x he = b → l = he::l' → P (match b with 
+             [ true ⇒ x::he::l'
+             | false ⇒ he::(insert A le x l') ])
+       with
+        [ true ⇒ (? : le x he = true → l = he::l' → P (x::he::l'))
+        | false ⇒
+            (? : \forall lrec. P (insert A le x lrec) \to
+                  le x he = false → l = he::l' → P (he::(insert A le x l')))
+            l' (insert_ind l')
+        ]
+       (refl_eq ? (le x he))
+   ] (refl_eq ? l) in insert_ind l);
+  
+  intros; simplify;
+  [ rewrite > H1;
+    apply andb_elim; simplify;
+    generalize in match K; clear K;
+    rewrite > H2; intro;
+    apply H3
+  | 
+  | reflexivity
+  ]. 
+    
+    
+    
+
+  
+  
+  [ rewrite > H1; simplify;
+    generalize in match (ordered_injective A le l K);
+    rewrite > H2; simplify; intro; change with (ordered A le l' = true).
+    elim l'; simplify;
+     [ reflexivity 
+     | 
+          
+    
+  rewrite > H1; simplify.
+    elim l'; [ reflexivity | simplify; 
+  | simplify.
+  | reflexivity.
+  ].
+*)
+
 lemma insert_sorted:
   \forall A:Set. \forall le:A\to A\to bool.
   (\forall a,b:A. le a b = false \to le b a = true) \to
@@ -105,7 +184,8 @@ lemma insert_sorted:
          apply andb_elim;
          rewrite > H3;
          assumption;
-       | generalize in match H2;
+       | change with (le x s = false → ordered ? le (s::insert A le x l1) = true);
+         generalize in match H2;
          clear H1; clear H2;
          generalize in match s;
          clear s;
@@ -114,6 +194,8 @@ lemma insert_sorted:
            rewrite > (H x a H2);
            reflexivity;
          | simplify in \vdash (? ? (? ? ? %) ?);
+            change with (ordered A le (a::(insert A le x (s::l2))) = true);
+            simplify;
             apply (bool_elim ? (le x s));
             [ intros;
               simplify;
@@ -161,22 +243,4 @@ theorem insertionsort_sorted:
   | apply (insert_sorted A le le_tot (insertionsort A le l1) s);
     assumption;
   ]
-qed.
-
-(*
-theorem insertionsort_correct:
-  ∀A:Set.
-  ∀le:A → A → bool.∀eq:A → A → bool.
-  (∀a,b:A. le a b = false → le b a = true) \to
-  ∀l,l':list A.
-  l' = insertionsort A le l
-  \to ordered A le l' = true
-    ∧ ((\forall x:A. mem A eq x l = true \to mem A eq x l' = true)
-        ∧ (\forall x:A. mem A eq x l = true \to mem A eq x l' = true)).
-  intros;
-  split;
-  [ rewrite > H1; 
-    apply (insertionsort_sorted A le eq H);
-  | split;
-    [ TO BE CONTINUED ...
-*)
+qed.
\ No newline at end of file

diff --git a/helm/matita/scripts/do_tests.sh b/helm/matita/scripts/do_tests.sh
index 5e8b0d583bda5f1cd31f768fc61f609089fc38e7..e8e4ddda4e9cc19e1b9dbcc8418f0a22e5b989c8 100755 (executable)
--- a/helm/matita/scripts/do_tests.sh
+++ b/helm/matita/scripts/do_tests.sh
@@ -19,23 +19,29 @@ CLEANER=$1
 shift
 LOGFILE=$1
 shift
+EXPECTED=$1
+shift
 TODO="$@"
 
-if [ -z "$COMPILER" -o -z "$CLEANER" -o -z "$LOGFILE" -o -z "$TODO" ]; then
+if [ -z "$COMPILER" -o -z "$CLEANER" -o -z "$LOGFILE" -o -z "$EXPECTED" -o -z "$TODO" ]; then
   echo
   echo "usage: "
-  echo "  do_tests.sh [-no-color] [-twice] ./compiler ./cleaner logfile tests.ma ..."
+  echo "  do_tests.sh [-no-color] [-twice] ./compiler ./cleaner logfile expected_result test.ma ..."
   echo
   echo "options:  "
   echo "  -no-color Do not use vt100 colors"
   echo "  -twice    Run each test twice but show only the second run times"
   echo
+  echo "If expected_result is OK the result will be OK if the test compiles."
+  echo "Otherwise if expected_result is FAIL the result will be OK if the test"
+  echo "does not compile and the generated output is equal to test.log."
   echo "The value of the DO_TESTS_EXTRA evironment variable"
   echo "will be appended to each line."
   exit 1
 fi
 
-TMP=.__temp.txt
+LOG=.__log
+DIFF=.__diff
 
 export TIMEFORMAT="%2lR %2lU %2lS"
 for T in $TODO; do
@@ -45,12 +51,26 @@ for T in $TODO; do
     $COMPILER $T 1>/dev/null 2>/dev/null
   fi
   $CLEANER $T 1>/dev/null 2>/dev/null
-  TIMES=`(time $COMPILER $T >> $LOGFILE 2>&1) 2>&1`
+  TIMES=`(time $COMPILER $T > $LOG 2>&1) 2>&1`
   RC=$?;
+  cat $LOG >> $LOGFILE
+  touch $DIFF
+  if [ $EXPECTED = "FAIL" ]; then
+   if [ $RC = 0 ]; then
+     echo "The test was successful but it should have failed!" > $DIFF
+     RC=1;
+   else
+     diff $LOG `basename $T .ma`.log > $DIFF
+     RC=$?
+     rm -f $LOG
+   fi
+  fi
   if [ $RC = 0 ]; then
     printf "$OK\t$TIMES\t$DO_TESTS_EXTRA\n"
   else
     printf "$FAIL\t$TIMES\t$DO_TESTS_EXTRA\n";
-    exit $RC
+    cat $DIFF
   fi
+  rm -f $DIFF
+  exit $RC
 done

diff --git a/helm/matita/tests/Makefile b/helm/matita/tests/Makefile
index d9ce39b18096fb18118926ce88f54181da1dc91c..33d4589296c18262a2292fa6bae2f4c395ebed52 100644 (file)
--- a/helm/matita/tests/Makefile
+++ b/helm/matita/tests/Makefile
@@ -6,8 +6,8 @@ ifeq ($(NODB),true)
        MATITA_FLAGS += -nodb
 endif
 
-MATITAC=../scripts/do_tests.sh $(DO_TESTS_OPTS) "../matitac $(MATITA_FLAGS)" "../matitaclean $(MATITA_FLAGS)" /dev/null
-MATITACOPT=../scripts/do_tests.sh $(DO_TESTS_OPTS) "../matitac.opt $(MATITA_FLAGS)" "../matitaclean.opt $(MATITA_FLAGS)" /dev/null
+MATITAC=../scripts/do_tests.sh $(DO_TESTS_OPTS) "../matitac $(MATITA_FLAGS)" "../matitaclean $(MATITA_FLAGS)" /dev/null OK
+MATITACOPT=../scripts/do_tests.sh $(DO_TESTS_OPTS) "../matitac.opt $(MATITA_FLAGS)" "../matitaclean.opt $(MATITA_FLAGS)" /dev/null OK
 VERBOSEMATITAC=../matitac $(MATITA_FLAGS)
 VERBOSEMATITACOPT=../matitac.opt $(MATITA_FLAGS)
 

diff --git a/helm/matita/tests/bad_tests/.depend b/helm/matita/tests/bad_tests/.depend
index 79b43d4b7a4c4d0a7168ab1e0368c332e1ab022d..8f040e5c7d70770fa68196d7dc40f4b6c3f62f67 100644 (file)
--- a/helm/matita/tests/bad_tests/.depend
+++ b/helm/matita/tests/bad_tests/.depend
@@ -2,3 +2,5 @@
 auto.mo: /home/sacerdot/.matita/xml/matita/tests/auto.moo
 /home/sacerdot/.matita/xml/matita/tests/baseuri.moo: baseuri.ma
 baseuri.mo: /home/sacerdot/.matita/xml/matita/tests/baseuri.moo
+/home/sacerdot/.matita/xml/matita/tests/test2.moo: test2.ma /home/sacerdot/miohelm/matita/coq.moo
+test2.mo: /home/sacerdot/.matita/xml/matita/tests/test2.moo

diff --git a/helm/matita/tests/bad_tests/Makefile b/helm/matita/tests/bad_tests/Makefile
index 6ce0b0d62fa605069660bae071733c841952614c..8f7a83fd599e7793f2d859b6fb9cec29220a5233 100644 (file)
--- a/helm/matita/tests/bad_tests/Makefile
+++ b/helm/matita/tests/bad_tests/Makefile
@@ -6,8 +6,8 @@ ifeq ($(NODB),true)
        MATITA_FLAGS += -nodb
 endif
 
-MATITAC=../../scripts/do_tests.sh $(DO_TESTS_OPTS) "../../matitac $(MATITA_FLAGS) -noprofile" "../../matitaclean $(MATITA_FLAGS)" log
-MATITACOPT=../../scripts/do_tests.sh $(DO_TESTS_OPTS) "../../matitac.opt $(MATITA_FLAGS) -noprofile" "../../matitaclean.opt $(MATITA_FLAGS)" log
+MATITAC=../../scripts/do_tests.sh $(DO_TESTS_OPTS) "../../matitac $(MATITA_FLAGS) -noprofile" "../../matitaclean $(MATITA_FLAGS)" /dev/null FAIL
+MATITACOPT=../../scripts/do_tests.sh $(DO_TESTS_OPTS) "../../matitac.opt $(MATITA_FLAGS) -noprofile" "../../matitaclean.opt $(MATITA_FLAGS)" /dev/null FAIL
 VERBOSEMATITAC=../../matitac $(MATITA_FLAGS)
 VERBOSEMATITACOPT=../../matitac.opt $(MATITA_FLAGS)
 
@@ -45,10 +45,7 @@ depend:
 .PHONY: depend
 
 %.moo:
-       $(H)($(MATITAC) $< && echo "ERROR: THIS SHOULD FAIL!") || \
-         ((diff `basename $< .ma`.log log > diff || \
-            (echo "ERROR: WRONG OUTPUT"; cat diff)) && rm -f log diff) || \
-            rm -f log diff
+       $(H)$(MATITAC) $<
 
 $(DEPEND_NAME): $(SRC)
        $(H)$(MATITADEP) $(SRC) > $@ || rm -f $@

diff --git a/helm/matita/tests/bad_tests/baseuri.log b/helm/matita/tests/bad_tests/baseuri.log
index c0c2004bc2440db996c8b2b0f601b9b140798b3c..9185479df94fa7d86d21d96c61ddddc502bf8694 100644 (file)
--- a/helm/matita/tests/bad_tests/baseuri.log
+++ b/helm/matita/tests/bad_tests/baseuri.log
@@ -1,5 +1,4 @@
 \e[0;32mInfo:  \e[0mexecution of baseuri.ma started:
-ciao
-\e[0;34mDfffebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/tests/baseuri/"''
+\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/tests/baseuri/"''
 \e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/tests/baseuri/"''
 \e[0;31mError: \e[0mError: Redefinition of 'baseuri' is forbidden.