ocaml 3.09 transition

[helm.git] / helm / metadata / Makefile

diff --git a/helm/metadata/Makefile b/helm/metadata/Makefile
index a651c5864e2f90e7d3099cd56cde278f67a727a0..1485dfdbfef49b9e97b2e7803d791dc8ef2709ec 100644 (file)
--- 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,14 @@ 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)
+       cat sql/drop_mowgli_tables.mysql.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)