From 1276d3c7b85f4edc049a5d68a6120816fe64c806 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 16 Nov 2005 11:10:17 +0000 Subject: [PATCH] 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) --- helm/matita/contribs/LAMBDA-TYPES/Makefile | 4 +- .../contribs/PREDICATIVE-TOPOLOGY/Makefile | 4 +- helm/matita/library/Makefile | 4 +- helm/matita/library/list/sort.ma | 106 ++++++++++++++---- helm/matita/scripts/do_tests.sh | 30 ++++- helm/matita/tests/Makefile | 4 +- helm/matita/tests/bad_tests/.depend | 2 + helm/matita/tests/bad_tests/Makefile | 9 +- helm/matita/tests/bad_tests/baseuri.log | 3 +- 9 files changed, 124 insertions(+), 42 deletions(-) diff --git a/helm/matita/contribs/LAMBDA-TYPES/Makefile b/helm/matita/contribs/LAMBDA-TYPES/Makefile index fc2e0ce84..c12b0fb43 100644 --- 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 fc2e0ce84..c12b0fb43 100644 --- 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 607e57f41..e13b3e8a4 100644 --- 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 1cc127759..ffd1e2187 100644 --- 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 5e8b0d583..e8e4ddda4 100755 --- 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 d9ce39b18..33d458929 100644 --- 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 79b43d4b7..8f040e5c7 100644 --- 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 6ce0b0d62..8f7a83fd5 100644 --- 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 c0c2004bc..9185479df 100644 --- a/helm/matita/tests/bad_tests/baseuri.log +++ b/helm/matita/tests/bad_tests/baseuri.log @@ -1,5 +1,4 @@ Info: execution of baseuri.ma started: -ciao -Dfffebug: Executing: ``set "baseuri" "cic:/matita/tests/baseuri/"'' +Debug: Executing: ``set "baseuri" "cic:/matita/tests/baseuri/"'' Debug: Executing: ``set "baseuri" "cic:/matita/tests/baseuri/"'' Error: Error: Redefinition of 'baseuri' is forbidden. -- 2.39.2