New directory for bad tests with checks on the error message.

diff --git a/helm/matita/tests/auto.ma b/helm/matita/tests/auto.ma
deleted file mode 100755 (executable)
index 5c6c043..0000000
--- a/helm/matita/tests/auto.ma
+++ /dev/null
@@ -1,27 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/tests/auto/".
-include "coq.ma".
-
-alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
-alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
-alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
-alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
-alias symbol "minus" (instance 0) = "Coq's natural minus".
-alias symbol "plus" (instance 0) = "Coq's natural plus".
-alias symbol "times" (instance 0) = "Coq's natural times".
-theorem a : \forall x,y:nat. x*x+(S y) = O - x.
-intros.
-auto depth = 3.

diff --git a/helm/matita/tests/bad_tests/.depend b/helm/matita/tests/bad_tests/.depend
new file mode 100644 (file)
index 0000000..79b43d4
--- /dev/null
+++ b/helm/matita/tests/bad_tests/.depend
@@ -0,0 +1,4 @@
+/home/sacerdot/.matita/xml/matita/tests/auto.moo: auto.ma /home/sacerdot/miohelm/matita/coq.moo
+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

diff --git a/helm/matita/tests/bad_tests/Makefile b/helm/matita/tests/bad_tests/Makefile
new file mode 100644 (file)
index 0000000..6ce0b0d
--- /dev/null
+++ b/helm/matita/tests/bad_tests/Makefile
@@ -0,0 +1,57 @@
+SRC=$(wildcard *.ma)
+
+MATITA_FLAGS =
+NODB=false
+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
+VERBOSEMATITAC=../../matitac $(MATITA_FLAGS)
+VERBOSEMATITACOPT=../../matitac.opt $(MATITA_FLAGS)
+
+MATITACLEAN=../../matitaclean $(MATITA_FLAGS)
+MATITACLEANOPT=../../matitaclean.opt $(MATITA_FLAGS)
+
+MATITADEP=../../matitadep $(MATITA_FLAGS)
+MATITADEPOPT=../../matitadep.opt $(MATITA_FLAGS)
+
+DEPEND_NAME=.depend
+
+H=@
+
+all: $(SRC:%.ma=%.mo)
+
+opt:
+       $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' all
+
+verbose:
+       $(H)$(MAKE) MATITAC='$(VERBOSEMATITAC)' MATITACLEAN='$(MATITACLEAN)' MATITADEP='$(MATITADEP)' all
+
+%.opt:
+       $(H)$(MAKE) MATITAC='$(MATITACOPT)' MATITACLEAN='$(MATITACLEANOPT)' MATITADEP='$(MATITADEPOPT)' $(@:%.opt=%)
+
+clean:
+       $(H)$(MATITACLEAN) $(SRC)
+
+cleanall:
+       $(H)rm -f $(SRC:%.ma=%.moo)
+       $(MATITACLEAN) all
+
+depend:
+       rm -f $(DEPEND_NAME)
+       $(MAKE) $(DEPEND_NAME)
+.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
+
+$(DEPEND_NAME): $(SRC)
+       $(H)$(MATITADEP) $(SRC) > $@ || rm -f $@
+
+#include $(DEPEND_NAME)
+include .depend

diff --git a/helm/matita/tests/bad_tests/auto.log b/helm/matita/tests/bad_tests/auto.log
new file mode 100644 (file)
index 0000000..1e1fc77
--- /dev/null
+++ b/helm/matita/tests/bad_tests/auto.log
@@ -0,0 +1,107 @@
+\e[0;32mInfo:  \e[0mexecution of auto.ma started:
+\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/tests/auto/"''
+\e[0;34mDebug: \e[0mExecuting: ``include coq.ma''
+\e[0;34mDebug: \e[0mExecuting: ``alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xp ...''
+\e[0;34mDebug: \e[0mExecuting: ``alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xp ...''
+\e[0;34mDebug: \e[0mExecuting: ``alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind# ...''
+\e[0;34mDebug: \e[0mExecuting: ``alias symbol "eq" (instance 0) = "Coq's leibnitz's ...''
+\e[0;34mDebug: \e[0mExecuting: ``alias symbol "minus" (instance 0) = "Coq's natural ...''
+\e[0;34mDebug: \e[0mExecuting: ``alias symbol "plus" (instance 0) = "Coq's natural  ...''
+\e[0;34mDebug: \e[0mExecuting: ``alias symbol "times" (instance 0) = "Coq's natural ...''
+\e[0;34mDebug: \e[0mExecuting: ``Theorem a: @[\forall ((x): (@[nat])).(\forall ((y) ...''
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Datatypes/nat.ind
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/eq.ind
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/minus.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/plus.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/mult.con
+\e[0;31mError: \e[0mBad name: a
+\e[0;34mDebug: \e[0mExecuting: ``intro.''
+\e[0;34mDebug: \e[0mExecuting: ``auto.''
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/trans_eq.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/z.var
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/f_equal3.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/f_equal2.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/f_equal.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/B.var
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/f.var
+WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/add_sub_square_identity.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/mult_n_Sm.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/TreeAutomata/semantics/conservation_0_0.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/MATHS/Z/Nat_complements/technical_lemma.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/ARITH/Chinese/Nat_complements/technical_lemma.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/plus_minus.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/minus_plus_simpl_l_reverse.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/minus_plus.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/minus_minus.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_plus_distr_r.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_plus_distr_l.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_plus_distr_r.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/mult_plus_distr2.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/minus_n_n.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/minus_n_O.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/minus_minus_lem1.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Cachan/SMC/mu/Splus_nm.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/plus_n_Sm.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/plus_Sn_m.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_Snm_nSm.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/TreeAutomata/bases/S_plus_l.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/Qpositive/mult_reg_l.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_reg_l.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_permute_2_in_4.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_permute.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_comm.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_assoc_reverse.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_assoc.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/eq_plus_reg_r.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/eq_plus_reg_l.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/plus_eq.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/plus_permute2.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/minus_eq_decompose.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/Qpositive/minus_decompose.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/minus_eq.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/eq_add_S.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/expand_mult2.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_n_2.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/ring/ArithRing/S_to_plus_one.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/ZArith/BinInt/ZL0.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/S_plus.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/plus_n_SO.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/plus_n_O.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_0_r.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_0_l.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Marseille/GC/lib_arith/lib_plus/plus_O_O.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/plus_eqO.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/plus_O_O.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Bertrand/Misc/plus_eqO.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/DEMOS/Demo_AutoRewrite/g0.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/DEMOS/Demo_AutoRewrite/McCarthy/g.var
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/mult_SO.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Bertrand/Misc/mult_SO.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/DEMOS/Demo_AutoRewrite/Ack1.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/DEMOS/Demo_AutoRewrite/Ackermann/Ack.var
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_1_r.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_1_l.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/mult2_recompose.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_n_1.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/mult_n_O.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_0_r.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_0_l.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_comm.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_assoc_reverse.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_assoc.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/square_recompose.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_sym.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_permut.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_assoc_l.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/eq_mult_reg_r.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/eq_mult_reg_l.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/mult_eq.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/mult_sym.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/mult_permute.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Float/Faux/minus_inv_lt_aux.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_minus_distr_r.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/mult_minus_distr_l.con
+\e[0;31mError: \e[0mTactic error: No Applicable theorem

diff --git a/helm/matita/tests/bad_tests/auto.ma b/helm/matita/tests/bad_tests/auto.ma
new file mode 100755 (executable)
index 0000000..5c6c043
--- /dev/null
+++ b/helm/matita/tests/bad_tests/auto.ma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/tests/auto/".
+include "coq.ma".
+
+alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
+alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
+alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
+alias symbol "minus" (instance 0) = "Coq's natural minus".
+alias symbol "plus" (instance 0) = "Coq's natural plus".
+alias symbol "times" (instance 0) = "Coq's natural times".
+theorem a : \forall x,y:nat. x*x+(S y) = O - x.
+intros.
+auto depth = 3.

diff --git a/helm/matita/tests/bad_tests/baseuri.log b/helm/matita/tests/bad_tests/baseuri.log
new file mode 100644 (file)
index 0000000..c0c2004
--- /dev/null
+++ b/helm/matita/tests/bad_tests/baseuri.log
@@ -0,0 +1,5 @@
+\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;31mError: \e[0mError: Redefinition of 'baseuri' is forbidden.

diff --git a/helm/matita/tests/bad_tests/baseuri.ma b/helm/matita/tests/bad_tests/baseuri.ma
new file mode 100644 (file)
index 0000000..0e06223
--- /dev/null
+++ b/helm/matita/tests/bad_tests/baseuri.ma
@@ -0,0 +1,16 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/tests/baseuri/".
+set "baseuri" "cic:/matita/tests/baseuri/".

diff --git a/helm/matita/tests/baseuri.ma b/helm/matita/tests/baseuri.ma
deleted file mode 100644 (file)
index 0e06223..0000000
--- a/helm/matita/tests/baseuri.ma
+++ /dev/null
@@ -1,16 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/tests/baseuri/".
-set "baseuri" "cic:/matita/tests/baseuri/".