From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 24 Feb 2004 10:15:36 +0000 (+0000)
Subject: - Targets reorganized
X-Git-Tag: v0_0_4~95
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9fa929210e8c97e4dd5905298d4f178ecb479147;p=helm.git

- Targets reorganized
- new targets
---

diff --git a/helm/metadata/.cvsignore b/helm/metadata/.cvsignore
new file mode 100644
index 000000000..2cde8a0b2
--- /dev/null
+++ b/helm/metadata/.cvsignore
@@ -0,0 +1,6 @@
+all_objects.txt
+constants_and_variables.txt
+fill_db.sql
+inductive_types.txt
+log
+tmp
diff --git a/helm/metadata/Makefile b/helm/metadata/Makefile
index 3b6b9b08e..a651c5864 100644
--- a/helm/metadata/Makefile
+++ b/helm/metadata/Makefile
@@ -1,9 +1,26 @@
 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 tipi_induttivi.txt` ; do (cd tmp ; wget -t 1 -O downloaded.xml.gz "http://mowgli.cs.unibo.it:58081/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 costanti_e_variabili.txt` ; do (cd tmp ; wget -t 1 -O downloaded.xml.gz "http://mowgli.cs.unibo.it:58081/getxml?format=gz&uri=$$i" ; wget -t 1 -O downloaded_body.xml.gz "http://mowgli.cs.unibo.it:58081/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
+	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
@@ -14,4 +31,4 @@ create_tables:
 fill_db:
 	cat $(FILLDB) | mysql -pbjIcRpru -u helmadmin mowgli
 
-.PHONY: all create_tables drop_tables fill_db
+.PHONY: all create_tables drop_tables fill_db indexes $(FILLDB)