From ceb977d9f052e99b0e473c5484578eaaf307a4f6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 15 Nov 2005 17:59:56 +0000 Subject: [PATCH] New directory for bad tests with checks on the error message. --- helm/matita/tests/bad_tests/.depend | 4 + helm/matita/tests/bad_tests/Makefile | 57 ++++++++++ helm/matita/tests/bad_tests/auto.log | 107 +++++++++++++++++++ helm/matita/tests/{ => bad_tests}/auto.ma | 0 helm/matita/tests/bad_tests/baseuri.log | 5 + helm/matita/tests/{ => bad_tests}/baseuri.ma | 0 6 files changed, 173 insertions(+) create mode 100644 helm/matita/tests/bad_tests/.depend create mode 100644 helm/matita/tests/bad_tests/Makefile create mode 100644 helm/matita/tests/bad_tests/auto.log rename helm/matita/tests/{ => bad_tests}/auto.ma (100%) create mode 100644 helm/matita/tests/bad_tests/baseuri.log rename helm/matita/tests/{ => bad_tests}/baseuri.ma (100%) 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/auto.ma b/helm/matita/tests/bad_tests/auto.ma similarity index 100% rename from helm/matita/tests/auto.ma rename to helm/matita/tests/bad_tests/auto.ma 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/baseuri.ma b/helm/matita/tests/bad_tests/baseuri.ma similarity index 100% rename from helm/matita/tests/baseuri.ma rename to helm/matita/tests/bad_tests/baseuri.ma -- 2.39.2