src/Pure/Tools/phabricator.scala
author wenzelm
Tue, 05 Nov 2019 22:00:29 +0100
changeset 71054 b64fc38327ae
parent 71053 ba14aa0b5a5d
child 71055 27a998cdc0f4
permissions -rw-r--r--
prefer system user setup, e.g. avoid occurrence on login screen;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/phabricator.scala
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
     3
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
     4
Support for Phabricator server. See also:
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
     5
  - https://www.phacility.com/phabricator
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
     6
  - https://secure.phabricator.com/book/phabricator
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
     7
*/
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
     8
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
     9
package isabelle
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    10
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    11
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
    12
import scala.util.matching.Regex
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
    13
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
    14
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    15
object Phabricator
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    16
{
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    17
  /** defaults **/
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    18
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    19
  /* required packages */
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    20
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    21
  val packages: List[String] =
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    22
    Build_Docker.packages :::
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    23
    List(
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    24
      // https://secure.phabricator.com/source/phabricator/browse/master/scripts/install/install_ubuntu.sh 15e6e2adea61
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    25
      "git", "mysql-server", "apache2", "libapache2-mod-php", "php", "php-mysql",
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    26
      "php-gd", "php-curl", "php-apcu", "php-cli", "php-json", "php-mbstring",
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    27
      // more packages
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    28
      "php-zip", "python-pygments", "ssh")
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    29
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    30
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    31
  /* global system resources */
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    32
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    33
  val daemon_user = "phabricator"
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    34
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    35
  val ssh_standard = 22
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    36
  val ssh_alternative1 = 222
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    37
  val ssh_alternative2 = 2222
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    38
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    39
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    40
  /* installation parameters */
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    41
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    42
  val default_name = "vcs"
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    43
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
    44
  def phabricator_name(name: String = "", ext: String = ""): String =
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
    45
    "phabricator" + (if (name.isEmpty) "" else "-" + name) + (if (ext.isEmpty) "" else "." + ext)
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
    46
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
    47
  def isabelle_phabricator_name(name: String = "", ext: String = ""): String =
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
    48
    "isabelle-" + phabricator_name(name = name, ext = ext)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    49
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    50
  def default_root(options: Options, name: String): Path =
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
    51
    Path.explode(options.string("phabricator_www_root")) +
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
    52
    Path.basic(phabricator_name(name = name))
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    53
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    54
  def default_repo(options: Options, name: String): Path =
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    55
    default_root(options, name) + Path.basic("repo")
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    56
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    57
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    58
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    59
  /** global configuration **/
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    60
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
    61
  val global_config = Path.explode("/etc/" + isabelle_phabricator_name(ext = "conf"))
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    62
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    63
  sealed case class Config(name: String, root: Path)
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
    64
  {
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
    65
    def home: Path = root + Path.explode(phabricator_name())
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
    66
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
    67
    def execute(command: String): Process_Result =
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
    68
      Isabelle_System.bash("./bin/" + command, cwd = home.file).check
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
    69
  }
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    70
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    71
  def read_config(): List[Config] =
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    72
  {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    73
    if (global_config.is_file) {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    74
      for (entry <- Library.trim_split_lines(File.read(global_config)) if entry.nonEmpty)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    75
      yield {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    76
        space_explode(':', entry) match {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    77
          case List(name, root) => Config(name, Path.explode(root))
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    78
          case _ => error("Malformed config file " + global_config + "\nentry " + quote(entry))
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    79
        }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    80
      }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    81
    }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    82
    else Nil
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    83
  }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    84
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    85
  def write_config(configs: List[Config])
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    86
  {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    87
    File.write(global_config,
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    88
      configs.map(config => config.name + ":" + config.root.implode).mkString("", "\n", "\n"))
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    89
  }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    90
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    91
  def get_config(name: String): Config =
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    92
    read_config().find(config => config.name == name) getOrElse
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    93
      error("Bad Isabelle/Phabricator installation " + quote(name))
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    94
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    95
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    96
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    97
  /** setup **/
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    98
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    99
  def user_setup(name: String, description: String, ssh_setup: Boolean = false)
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   100
  {
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   101
    if (!Linux.user_exists(name)) {
71054
b64fc38327ae prefer system user setup, e.g. avoid occurrence on login screen;
wenzelm
parents: 71053
diff changeset
   102
      Linux.user_add(name, description = description, system = true, ssh_setup = ssh_setup)
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   103
    }
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   104
    else if (Linux.user_description(name) != description) {
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   105
      error("User " + quote(name) + " already exists --" +
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   106
        " for Phabricator it should have the description:\n  " + quote(description))
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   107
    }
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   108
  }
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   109
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   110
  def phabricator_setup(
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   111
    options: Options,
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   112
    name: String = default_name,
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   113
    root: String = "",
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   114
    repo: String = "",
71047
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   115
    package_update: Boolean = false,
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   116
    progress: Progress = No_Progress)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   117
  {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   118
    /* system environment */
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   119
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   120
    Linux.check_system_root()
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   121
71047
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   122
    if (package_update) {
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   123
      Linux.package_update(progress = progress)
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   124
      Linux.check_reboot_required()
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   125
    }
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   126
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   127
    Linux.package_install(packages, progress = progress)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   128
    Linux.check_reboot_required()
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   129
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   130
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   131
    /* users */
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   132
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   133
    if (name == daemon_user) {
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   134
      error("Clash of installation name with daemon user " + quote(daemon_user))
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   135
    }
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   136
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   137
    user_setup(daemon_user, "Phabricator Daemon User", ssh_setup = true)
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   138
    user_setup(name, "Phabricator SSH User")
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   139
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   140
    val www_user = options.string("phabricator_www_user")
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   141
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   142
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   143
    /* basic installation */
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   144
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   145
    val root_path = if (root.nonEmpty) Path.explode(root) else default_root(options, name)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   146
    val repo_path = if (repo.nonEmpty) Path.explode(repo) else default_repo(options, name)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   147
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   148
    val configs = read_config()
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   149
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   150
    for (config <- configs if config.name == name) {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   151
      error("Duplicate Phabricator installation " + quote(name) + " in " + config.root)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   152
    }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   153
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   154
    if (!Isabelle_System.bash("mkdir -p " + File.bash_path(root_path)).ok) {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   155
      error("Failed to create root directory " + root_path)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   156
    }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   157
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   158
    progress.bash(cwd = root_path.file, echo = true,
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   159
      script = """
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   160
        set -e
71050
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   161
        chown """ + Bash.string(www_user) + ":" + Bash.string(www_user) + """ .
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   162
        chmod 755 .
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   163
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   164
        git clone https://github.com/phacility/libphutil.git
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   165
        git clone https://github.com/phacility/arcanist.git
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   166
        git clone https://github.com/phacility/phabricator.git
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   167
      """).check
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   168
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   169
    val config = Config(name, root_path)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   170
    write_config(configs ::: List(config))
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   171
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   172
    config.execute("config set pygments.enabled true")
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   173
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   174
71050
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   175
    /* local repository directory */
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   176
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   177
    if (!Isabelle_System.bash("mkdir -p " + File.bash_path(repo_path)).ok) {
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   178
      error("Failed to create local repository directory " + repo_path)
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   179
    }
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   180
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   181
    Isabelle_System.bash(cwd = repo_path.file,
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   182
      script = """
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   183
        set -e
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   184
        chown -R """ + Bash.string(daemon_user) + ":" + Bash.string(daemon_user) + """ .
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   185
        chmod 755 .
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   186
      """).check
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   187
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   188
    config.execute("config set repository.default-local-path " + File.bash_path(repo_path))
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   189
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   190
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   191
    /* MySQL setup */
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   192
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   193
    progress.echo("MySQL setup...")
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   194
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   195
    File.write(Path.explode("/etc/mysql/mysql.conf.d/" + isabelle_phabricator_name(ext = "cnf")),
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   196
"""[mysqld]
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   197
max_allowed_packet = 32M
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   198
innodb_buffer_pool_size = 1600M
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   199
local_infile = 0
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   200
""")
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   201
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   202
    Linux.service_restart("mysql")
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   203
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   204
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   205
    def mysql_conf(R: Regex): Option[String] =
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   206
      split_lines(File.read(Path.explode(options.string("phabricator_mysql_config")))).
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   207
        collectFirst({ case R(a) => a })
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   208
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   209
    for (user <- mysql_conf("""^user\s*=\s*(\S*)\s*$""".r)) {
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   210
      config.execute("config set mysql.user " + Bash.string(user))
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   211
    }
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   212
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   213
    for (pass <- mysql_conf("""^password\s*=\s*(\S*)\s*$""".r)) {
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   214
      config.execute("config set mysql.pass " + Bash.string(pass))
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   215
    }
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   216
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   217
    config.execute("config set storage.default-namespace " +
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   218
      Bash.string(phabricator_name(name = name).replace("-", "_")))
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   219
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   220
    config.execute("config set storage.mysql-engine.max-size 8388608")
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   221
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   222
    config.execute("storage upgrade --force")
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   223
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   224
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   225
    /* SSH hosting */
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   226
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   227
    progress.echo("SSH hosting setup...")
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   228
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   229
    val ssh_port = ssh_alternative2
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   230
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   231
    config.execute("config set diffusion.ssh-user " + Bash.string(name))
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   232
    config.execute("config set diffusion.ssh-port " + ssh_port)
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   233
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   234
    val sudoers_file = Path.explode("/etc/sudoers.d") + Path.basic(isabelle_phabricator_name())
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   235
    File.write(sudoers_file,
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   236
      www_user + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/bin/hg, /usr/bin/ssh, /usr/bin/id\n" +
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   237
      name + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/bin/git-upload-pack, /usr/bin/git-receive-pack, /usr/bin/hg, /usr/bin/svnserve, /usr/bin/ssh, /usr/bin/id\n")
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   238
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   239
    Isabelle_System.bash("chmod 0440 " + File.bash_path(sudoers_file)).check
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   240
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   241
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   242
    /* PHP setup */
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   243
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   244
    val php_version =
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   245
      Isabelle_System.bash("""php --run 'echo PHP_MAJOR_VERSION . "." . PHP_MINOR_VERSION;'""")
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   246
        .check.out
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   247
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   248
    val php_conf =
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   249
      Path.explode("/etc/php") + Path.basic(php_version) +  // educated guess
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   250
        Path.explode("apache2/conf.d") +
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   251
        Path.basic(isabelle_phabricator_name(ext = "ini"))
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   252
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   253
    File.write(php_conf,
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   254
      "post_max_size = 32M\n" +
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   255
      "opcache.validate_timestamps = 0\n" +
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   256
      "memory_limit = 512M\n")
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   257
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   258
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   259
    /* Apache setup */
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   260
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   261
    progress.echo("Apache setup...")
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   262
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   263
    val apache_root = Path.explode(options.string("phabricator_apache_root"))
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   264
    val apache_sites = apache_root + Path.explode("sites-available")
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   265
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   266
    if (!apache_sites.is_dir) error("Bad Apache sites directory " + apache_sites)
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   267
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   268
    val server_name = phabricator_name(ext = "lvh.me")  // alias for "localhost" for testing
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   269
    val server_url = "http://" + server_name
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   270
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   271
    File.write(apache_sites + Path.basic(isabelle_phabricator_name(ext = "conf")),
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   272
"""<VirtualHost *:80>
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   273
    ServerName """ + server_name + """
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   274
    ServerAdmin webmaster@localhost
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   275
    DocumentRoot """ + config.home.implode + """/webroot
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   276
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   277
    ErrorLog ${APACHE_LOG_DIR}/error.log
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   278
    RewriteEngine on
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   279
    RewriteRule ^(.*)$  /index.php?__path__=$1  [B,L,QSA]
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   280
</VirtualHost>
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   281
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   282
# vim: syntax=apache ts=4 sw=4 sts=4 sr noet
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   283
""")
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   284
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   285
    Isabelle_System.bash( """
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   286
      set -e
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   287
      a2enmod rewrite
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   288
      a2ensite """ + Bash.string(isabelle_phabricator_name())).check
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   289
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   290
    Linux.service_restart("apache2")
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   291
71053
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   292
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   293
    /* PHP daemon */
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   294
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   295
    progress.echo("PHP daemon setup...")
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   296
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   297
    config.execute("config set phd.user " + Bash.string(daemon_user))
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   298
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   299
    Linux.service_install(isabelle_phabricator_name(),
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   300
"""[Unit]
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   301
Description=PHP daemon for Isabelle/Phabricator """ + quote(name) + """
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   302
After=syslog.target network.target apache2.service mysql.service
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   303
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   304
[Service]
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   305
Type=oneshot
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   306
User=""" + daemon_user + """
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   307
Group=""" + daemon_user + """
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   308
Environment=PATH=/sbin:/usr/sbin:/usr/local/sbin:/usr/local/bin:/usr/bin:/bin
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   309
ExecStart=""" + config.home.implode + """/bin/phd start
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   310
ExecStop=""" + config.home.implode + """/bin/phd stop
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   311
RemainAfterExit=yes
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   312
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   313
[Install]
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   314
WantedBy=multi-user.target
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   315
""")
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   316
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   317
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   318
    progress.echo("\nDONE\nWeb configuration via " + server_url)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   319
  }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   320
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   321
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   322
  /* Isabelle tool wrapper */
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   323
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   324
  val isabelle_tool1 =
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   325
    Isabelle_Tool("phabricator_setup", "setup Phabricator server on Ubuntu Linux", args =>
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   326
    {
71047
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   327
      var repo = ""
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   328
      var package_update = false
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   329
      var options = Options.init()
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   330
      var root = ""
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   331
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   332
      val getopts =
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   333
        Getopts("""
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   334
Usage: isabelle phabricator_setup [OPTIONS] [NAME]
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   335
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   336
  Options are:
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   337
    -R DIR       repository directory (default: """ + default_repo(options, "NAME") + """)
71047
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   338
    -U           full update of system packages before installation
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   339
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   340
    -r DIR       installation root directory (default: """ + default_root(options, "NAME") + """)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   341
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   342
  Install Phabricator as Ubuntu LAMP application (Linux, Apache, MySQL, PHP).
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   343
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   344
  Slogan: "Discuss. Plan. Code. Review. Test.
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   345
  Every application your project needs, all in one tool."
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   346
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   347
  The installation NAME (default: """ + quote(default_name) + """) is mapped to
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   348
  a regular Unix user and used for public SSH access.
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   349
""",
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   350
          "R:" -> (arg => repo = arg),
71047
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   351
          "U" -> (_ => package_update = true),
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   352
          "o:" -> (arg => options = options + arg),
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   353
          "r:" -> (arg => root = arg))
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   354
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   355
      val more_args = getopts(args)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   356
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   357
      val name =
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   358
        more_args match {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   359
          case Nil => default_name
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   360
          case List(name) => name
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   361
          case _ => getopts.usage()
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   362
        }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   363
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   364
      val progress = new Console_Progress
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   365
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   366
      phabricator_setup(options, name, root = root, repo = repo,
71047
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   367
        package_update = package_update, progress = progress)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   368
    })
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   369
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   370
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   371
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   372
  /** update **/
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   373
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   374
  def phabricator_update(name: String, progress: Progress = No_Progress)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   375
  {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   376
    Linux.check_system_root()
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   377
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   378
    ???
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   379
  }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   380
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   381
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   382
  /* Isabelle tool wrapper */
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   383
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   384
  val isabelle_tool2 =
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   385
    Isabelle_Tool("phabricator_update", "update Phabricator server installation", args =>
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   386
    {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   387
      val getopts =
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   388
        Getopts("""
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   389
Usage: isabelle phabricator_update [NAME]
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   390
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   391
  Update Phabricator installation, with lookup of NAME (default + """ + quote(default_name) + """)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   392
  in """ + global_config + "\n")
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   393
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   394
      val more_args = getopts(args)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   395
      val name =
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   396
        more_args match {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   397
          case Nil => default_name
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   398
          case List(name) => name
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   399
          case _ => getopts.usage()
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   400
        }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   401
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   402
      val progress = new Console_Progress
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   403
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   404
      phabricator_update(name, progress = progress)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   405
    })
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   406
}