helm/software/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 "Step 0."
  25 echo "  Dropping old databases, if any."
  26 echo "  You can ignore errors output by this step"
  27 echo "$drop_sql" | $MYSQL -f
  28 echo "Step 1."
  29 echo "  Creating database and users."
  30 echo "# SQL statements to create Matita DB and users" > $SQL
  31 appendsql "$create_sql;"
  32 if [ -z "$DBPASS" ]; then
  33   appendsql "$grant_sql;"
  34 else
  35   appendsql "$grant_sql IDENTIFIED BY '$DBPASS';"
  36 fi
  37 $MYSQL < $SQL
  38 echo "Step 2."
  39 echo "  Creating database structure."
  40 echo "# SQL statements to create Matita DB structure" > $SQL
  41 creator_args="table fill index"
  42 for arg in $creator_args; do
  43   appendsql "`$TABLE_CREATOR $arg all`"
  44 done
  45 $MYSQL $DBNAME < $SQL
  46 echo "Step 3."
  47 echo "  Filling database with standard library metadata."
  48 if [ -f "$STDLIB_DATA" ]; then
  49   gunzip -c "$STDLIB_DATA" | $MYSQL $DBNAME
  50 else
  51   echo "  Standard library metadata file $STDLIB_DATA not found, skipping this step."
  52 fi
  53