X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fdist%2Ffill_db.sh;fp=helm%2Fmatita%2Fdist%2Ffill_db.sh;h=1ae28d336944f77a77e3b9b7123f264599d9d6ea;hb=792b5d29ebae8f917043d9dd226692919b5d6ca1;hp=0000000000000000000000000000000000000000;hpb=a14a8c7637fd0b95e9d4deccb20c6abc98e8f953;p=helm.git

diff --git a/helm/matita/dist/fill_db.sh b/helm/matita/dist/fill_db.sh
new file mode 100755
index 000000000..1ae28d336
--- /dev/null
+++ b/helm/matita/dist/fill_db.sh
@@ -0,0 +1,53 @@
+#!/bin/bash
+set -e
+
+MYSQL="mysql"
+DBHOST="localhost"
+DBNAME="matita"
+DBUSER="helm"
+DBPASS=""
+
+TABLE_CREATOR="../../ocaml/metadata/table_creator/table_creator"
+
+SQL="matita_db.sql"
+STDLIB_DATA="matita_stdlib.sql.gz"
+
+grant_sql="GRANT ALL PRIVILEGES ON $DBNAME.* TO $DBUSER@$DBHOST"
+create_sql="CREATE DATABASE $DBNAME"
+drop_sql="DROP DATABASE $DBNAME"
+
+function appendsql()
+{
+  echo "$1" >> $SQL
+}
+
+echo "Step 0."
+echo "  Dropping old databases, if any."
+echo "  You can ignore errors output by this step"
+echo "$drop_sql" | $MYSQL -f
+echo "Step 1."
+echo "  Creating database and users."
+echo "# SQL statements to create Matita DB and users" > $SQL
+appendsql "$create_sql;"
+if [ -z "$DBPASS" ]; then
+  appendsql "$grant_sql;"
+else
+  appendsql "$grant_sql IDENTIFIED BY '$DBPASS';"
+fi
+$MYSQL < $SQL
+echo "Step 2."
+echo "  Creating database structure."
+echo "# SQL statements to create Matita DB structure" > $SQL
+creator_args="table fill index"
+for arg in $creator_args; do
+  appendsql "`$TABLE_CREATOR $arg all`"
+done
+$MYSQL $DBNAME < $SQL
+echo "Step 3."
+echo "  Filling database with standard library metadata."
+if [ -f "$STDLIB_DATA" ]; then
+  gunzip -c "$STDLIB_DATA" | $MYSQL $DBNAME
+else
+  echo "  Standard library metadata file $STDLIB_DATA not found, skipping this step."
+fi
+