From 4cde46f31cb4e9e74d7872d638680d593d294eff Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 14 Nov 2005 13:12:59 +0000
Subject: [PATCH] first draft of db filling script

---
 helm/matita/dist/fill_db.sh | 52 +++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)
 create mode 100755 helm/matita/dist/fill_db.sh

diff --git a/helm/matita/dist/fill_db.sh b/helm/matita/dist/fill_db.sh
new file mode 100755
index 000000000..e4e984308
--- /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
+
-- 
2.39.2