From: Claudio Sacerdoti Coen Date: Tue, 15 Nov 2005 17:59:56 +0000 (+0000) Subject: New directory for bad tests with checks on the error message. X-Git-Tag: V_0_7_2_3~72 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=ceb977d9f052e99b0e473c5484578eaaf307a4f6 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 index 5c6c04358..000000000 --- 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 index 000000000..79b43d4b7 --- /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 index 000000000..6ce0b0d62 --- /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 index 000000000..1e1fc77ae --- /dev/null +++ b/helm/matita/tests/bad_tests/auto.log @@ -0,0 +1,107 @@ +Info: execution of auto.ma started: +Debug: Executing: ``set "baseuri" "cic:/matita/tests/auto/"'' +Debug: Executing: ``include coq.ma'' +Debug: Executing: ``alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xp ...'' +Debug: Executing: ``alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xp ...'' +Debug: Executing: ``alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind# ...'' +Debug: Executing: ``alias symbol "eq" (instance 0) = "Coq's leibnitz's ...'' +Debug: Executing: ``alias symbol "minus" (instance 0) = "Coq's natural ...'' +Debug: Executing: ``alias symbol "plus" (instance 0) = "Coq's natural ...'' +Debug: Executing: ``alias symbol "times" (instance 0) = "Coq's natural ...'' +Debug: Executing: ``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 +Error: Bad name: a +Debug: Executing: ``intro.'' +Debug: Executing: ``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 +Error: Tactic 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 index 000000000..5c6c04358 --- /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 index 000000000..c0c2004bc --- /dev/null +++ b/helm/matita/tests/bad_tests/baseuri.log @@ -0,0 +1,5 @@ +Info: execution of baseuri.ma started: +ciao +Dfffebug: Executing: ``set "baseuri" "cic:/matita/tests/baseuri/"'' +Debug: Executing: ``set "baseuri" "cic:/matita/tests/baseuri/"'' +Error: Error: 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 index 000000000..0e06223fa --- /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 index 0e06223fa..000000000 --- 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/".