helm/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)