# HG changeset patch
# User wenzelm
# Date 1576070958 -3600
# Node ID 7df5c110a43c0ea6c2e9637fd67be26a68d9672b
# Parent  e2fb60756fb80aa1d24c6a579da9d3b4d46b45e7
support database dump;

diff -r e2fb60756fb8 -r 7df5c110a43c src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Tue Dec 10 21:05:07 2019 +0100
+++ b/src/Pure/Tools/phabricator.scala	Wed Dec 11 14:29:18 2019 +0100
@@ -201,7 +201,7 @@
     /* users */
 
     if (name.contains((c: Char) => !(Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c))) ||
-        Set("", "ssh", "phd", daemon_user).contains(name)) {
+        Set("", "ssh", "phd", "dump", daemon_user).contains(name)) {
       error("Bad installation name: " + quote(name))
     }
 
@@ -317,6 +317,21 @@
     progress.bash("bin/storage upgrade --force", cwd = config.home.file, echo = true).check
 
 
+    /* database dump */
+
+    val dump_name = isabelle_phabricator_name(name = "dump")
+    val dump_command = Path.explode("/usr/local/bin") + Path.basic(dump_name)
+
+    File.write(dump_command,
+      global_config_script(header = true, body =
+"""mkdir -p "$ROOT/database" && chown root:root "$ROOT/database" && chmod 700 "$ROOT/database"
+[ -e "$ROOT/database/dump.sql.gz" ] && mv -f "$ROOT/database/dump.sql.gz" "$ROOT/database/dump-old.sql.gz"
+echo "Creating $ROOT/database/dump.sql.gz"
+"$ROOT/phabricator/bin/storage" dump --compress --output "$ROOT/database/dump.sql.gz" 2>&1 | fgrep -v '[Warning] Using a password on the command line interface can be insecure' """))
+    Isabelle_System.chmod("755", dump_command)
+    Isabelle_System.chown("root:root", dump_command)
+
+
     /* PHP setup */
 
     val php_version =