From: Stefano Zacchiroli Date: Tue, 9 Nov 2004 08:15:43 +0000 (+0000) Subject: added filling of no_concl_hyp X-Git-Tag: v_0_6_4_1~14 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=257516df1ad90ec279f7a29510384f19b5d15341;p=helm.git added filling of no_concl_hyp --- diff --git a/helm/metadata/Makefile b/helm/metadata/Makefile index a651c5864..88b01fdc5 100644 --- a/helm/metadata/Makefile +++ b/helm/metadata/Makefile @@ -3,6 +3,8 @@ INDUCTIVETYPES=inductive_types.txt CONSTANTSANDVARIABLES=constants_and_variables.txt ALLOBJECTS=all_objects.txt GETTERURL=http://mowgli.cs.unibo.it:58081 +DBCOMM=mysql -pbjIcRpru -u helmadmin mowgli +#DBCOMM=psql -q -U helm mowgli2 all: @echo "try one of:" @@ -16,6 +18,8 @@ $(FILLDB): rm -f $(FILLDB) time for i in `cat $(INDUCTIVETYPES)` ; do (cd tmp ; wget -t 1 -O downloaded.xml.gz "$(GETTERURL)/getxml?format=gz&uri=$$i") ; zcat tmp/downloaded.xml.gz > tmp/inductive_type.xml ; extractor/meta_ind $$i "tmp/inductive_type.xml" >> $(FILLDB) ; rm -f tmp/downloaded.xml.gz tmp/inductive_type.xml; done > log 2>&1 time for i in `cat $(CONSTANTSANDVARIABLES)` ; do (cd tmp ; wget -t 1 -O downloaded.xml.gz "$(GETTERURL)/getxml?format=gz&uri=$$i" ; wget -t 1 -O downloaded_body.xml.gz "$(GETTERURL)/getxml?format=gz&uri=$$i.body"); zcat tmp/downloaded.xml.gz > tmp/type.xml ; zcat tmp/downloaded_body.xml.gz > tmp/body.xml ; extractor/meta $$i "tmp/body.xml" "tmp/type.xml" >> $(FILLDB) ; rm -f tmp/downloaded.xml.gz tmp/downloaded_body.xml.gz tmp/type.xml tmp/body.xml ; done > log 2>&1 + cat sql/fill_inconcl_aux.sql >> $@ + cat sql/fill_no_concl_hyp.sql >> $@ indexes: wget "$(GETTERURL)/getalluris?format=txt" -O - | grep -v "\\.body$$" | grep -v "\\.types$$" | grep -v "\\.proof_tree$$" | sort > $(ALLOBJECTS) @@ -23,12 +27,13 @@ indexes: cat $(ALLOBJECTS) | grep -v "\\.ind$$" > $(CONSTANTSANDVARIABLES) drop_tables: - cat sql/drop_mowgli_tables.sql | mysql -pbjIcRpru -u helmadmin mowgli + cat sql/drop_mowgli_tables.sql | $(DBCOMM) create_tables: - cat sql/create_mowgli_tables.sql | mysql -pbjIcRpru -u helmadmin mowgli + #cat sql/create_mowgli_tables.sql | $(DBCOMM) + cat sql/create_mowgli_tables.mysql.sql | $(DBCOMM) fill_db: - cat $(FILLDB) | mysql -pbjIcRpru -u helmadmin mowgli + cat $(FILLDB) | $(DBCOMM) .PHONY: all create_tables drop_tables fill_db indexes $(FILLDB)