]> matita.cs.unibo.it Git - helm.git/blob - metadata/Makefile
made executable again
[helm.git] / metadata / Makefile
1 FILLDB=fill_db.sql
2 INDUCTIVETYPES=inductive_types.txt
3 CONSTANTSANDVARIABLES=constants_and_variables.txt
4 ALLOBJECTS=all_objects.txt
5 GETTERURL=http://mowgli.cs.unibo.it:58081
6
7 all:
8         @echo "try one of:"
9         @echo "  make indexes"
10         @echo "  make drop_tables"
11         @echo "  make create_tables"
12         @echo "  make $(FILLDB)"
13         @echo "  make fill_db"
14
15 $(FILLDB):
16         rm -f $(FILLDB)
17         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
18         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
19
20 indexes:
21         wget "$(GETTERURL)/getalluris?format=txt" -O - | grep -v "\\.body$$" | grep -v "\\.types$$" | grep -v "\\.proof_tree$$" | sort > $(ALLOBJECTS)
22         cat $(ALLOBJECTS) | grep "\\.ind$$" > $(INDUCTIVETYPES)
23         cat $(ALLOBJECTS) | grep -v "\\.ind$$" > $(CONSTANTSANDVARIABLES)
24
25 drop_tables:
26         cat sql/drop_mowgli_tables.sql | mysql -pbjIcRpru -u helmadmin mowgli
27
28 create_tables:
29         cat sql/create_mowgli_tables.sql | mysql -pbjIcRpru -u helmadmin mowgli
30
31 fill_db:
32         cat $(FILLDB) | mysql -pbjIcRpru -u helmadmin mowgli
33
34 .PHONY: all create_tables drop_tables fill_db indexes $(FILLDB)