first draft of db filling script

diff --git a/helm/matita/dist/fill_db.sh b/helm/matita/dist/fill_db.sh
new file mode 100755 (executable)
index 0000000..e4e9843
--- /dev/null
+++ b/helm/matita/dist/fill_db.sh
@@ -0,0 +1,52 @@
+#!/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 "# SQL statements to create Matita DB" > $SQL
+appendsql "$create_sql;"
+if [ -z "$DBPASS" ]; then
+  appendsql "$grant_sql;"
+else
+  appendsql "$grant_sql IDENTIFIED BY '$DBPASS';"
+fi
+creator_args="table fill index"
+for arg in $creator_args; do
+  for line in `$TABLE_CREATOR $arg all`; do
+    appendsql $line
+  done
+done
+
+echo "Step 1."
+echo " Dropping old databases, if any."
+echo " You can ignore errors output by this step"
+echo "$drop_sql" | $MYSQL -f
+echo "Step 2."
+echo "  Creating database structure using SQL statements from $SQL."
+$MYSQL < $SQL
+echo "Step 3."
+echo "  Filling database with standard library metadata."
+if [ -f "$STDLIB_DATA" ]; then
+  gunzip -c "$STDLIB_DATA" | $MYSQL
+else
+  echo "  Standard library metadata file $STDLIB_DATA not found, skipping this step."
+fi
+