helm/matita/dist/fill_db.sh

   1 #!/bin/bash
   2 set -e
   3
   4 MYSQL="mysql"
   5 DBHOST="localhost"
   6 DBNAME="matita"
   7 DBUSER="helm"
   8 DBPASS=""
   9
  10 TABLE_CREATOR="../../ocaml/metadata/table_creator/table_creator"
  11
  12 SQL="matita_db.sql"
  13 STDLIB_DATA="matita_stdlib.sql.gz"
  14
  15 grant_sql="GRANT ALL PRIVILEGES ON $DBNAME.* TO $DBUSER@$DBHOST"
  16 create_sql="CREATE DATABASE $DBNAME"
  17 drop_sql="DROP DATABASE $DBNAME"
  18
  19 function appendsql()
  20 {
  21   echo "$1" >> $SQL
  22 }
  23
  24 echo "# SQL statements to create Matita DB" > $SQL
  25 appendsql "$create_sql;"
  26 if [ -z "$DBPASS" ]; then
  27   appendsql "$grant_sql;"
  28 else
  29   appendsql "$grant_sql IDENTIFIED BY '$DBPASS';"
  30 fi
  31 creator_args="table fill index"
  32 for arg in $creator_args; do
  33   for line in `$TABLE_CREATOR $arg all`; do
  34     appendsql $line
  35   done
  36 done
  37
  38 echo "Step 1."
  39 echo "  Dropping old databases, if any."
  40 echo "  You can ignore errors output by this step"
  41 echo "$drop_sql" | $MYSQL -f
  42 echo "Step 2."
  43 echo "  Creating database structure using SQL statements from $SQL."
  44 $MYSQL < $SQL
  45 echo "Step 3."
  46 echo "  Filling database with standard library metadata."
  47 if [ -f "$STDLIB_DATA" ]; then
  48   gunzip -c "$STDLIB_DATA" | $MYSQL
  49 else
  50   echo "  Standard library metadata file $STDLIB_DATA not found, skipping this step."
  51 fi
  52