X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmetadata%2FMakefile;fp=helm%2Fmetadata%2FMakefile;h=0000000000000000000000000000000000000000;hb=1696761e4b8576e8ed81caa905fd108717019226;hp=a651c5864e2f90e7d3099cd56cde278f67a727a0;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;p=helm.git

diff --git a/helm/metadata/Makefile b/helm/metadata/Makefile
deleted file mode 100644
index a651c5864..000000000
--- a/helm/metadata/Makefile
+++ /dev/null
@@ -1,34 +0,0 @@
-FILLDB=fill_db.sql
-INDUCTIVETYPES=inductive_types.txt
-CONSTANTSANDVARIABLES=constants_and_variables.txt
-ALLOBJECTS=all_objects.txt
-GETTERURL=http://mowgli.cs.unibo.it:58081
-
-all:
-	@echo "try one of:"
-	@echo "  make indexes"
-	@echo "  make drop_tables"
-	@echo "  make create_tables"
-	@echo "  make $(FILLDB)"
-	@echo "  make fill_db"
-
-$(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
-
-indexes:
-	wget "$(GETTERURL)/getalluris?format=txt" -O - | grep -v "\\.body$$" | grep -v "\\.types$$" | grep -v "\\.proof_tree$$" | sort > $(ALLOBJECTS)
-	cat $(ALLOBJECTS) | grep "\\.ind$$" > $(INDUCTIVETYPES)
-	cat $(ALLOBJECTS) | grep -v "\\.ind$$" > $(CONSTANTSANDVARIABLES)
-
-drop_tables:
-	cat sql/drop_mowgli_tables.sql | mysql -pbjIcRpru -u helmadmin mowgli
-
-create_tables:
-	cat sql/create_mowgli_tables.sql | mysql -pbjIcRpru -u helmadmin mowgli
-
-fill_db:
-	cat $(FILLDB) | mysql -pbjIcRpru -u helmadmin mowgli
-
-.PHONY: all create_tables drop_tables fill_db indexes $(FILLDB)