src/Pure/Tools/phabricator.scala
author wenzelm
Tue, 17 Dec 2019 21:04:55 +0100
changeset 71299 51c19a44cfed
parent 71295 6aadbd650280
child 71300 ca794da3bb1d
permissions -rw-r--r--
support for conduit API;
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
71068
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
     4
Support for Phabricator server, notably for Ubuntu 18.04 LTS.
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
     5
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
     6
See also:
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
     7
  - https://www.phacility.com/phabricator
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
     8
  - https://secure.phabricator.com/book/phabricator
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
     9
*/
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    10
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    11
package isabelle
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    12
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    13
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
    14
import scala.util.matching.Regex
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
    15
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
    16
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    17
object Phabricator
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    18
{
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    19
  /** defaults **/
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    20
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    21
  /* required packages */
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    22
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    23
  val packages: List[String] =
71265
6ca561001244 support for pwgen;
wenzelm
parents: 71135
diff changeset
    24
    Build_Docker.packages ::: Linux.packages :::
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    25
    List(
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    26
      // https://secure.phabricator.com/source/phabricator/browse/master/scripts/install/install_ubuntu.sh 15e6e2adea61
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    27
      "git", "mysql-server", "apache2", "libapache2-mod-php", "php", "php-mysql",
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    28
      "php-gd", "php-curl", "php-apcu", "php-cli", "php-json", "php-mbstring",
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    29
      // more packages
71288
26a40fc962e8 more packages: required for svn;
wenzelm
parents: 71287
diff changeset
    30
      "php-xml", "php-zip", "python-pygments", "ssh", "subversion",
71280
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
    31
      // mercurial build packages
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
    32
      "make", "gcc", "python", "python-dev", "python-docutils", "python-pygments", "python-openssl")
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    33
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    34
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    35
  /* global system resources */
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    36
71068
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
    37
  val www_user = "www-data"
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
    38
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    39
  val daemon_user = "phabricator"
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    40
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
    41
  val sshd_config = Path.explode("/etc/ssh/sshd_config")
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    42
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    43
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    44
  /* installation parameters */
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    45
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    46
  val default_name = "vcs"
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    47
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
    48
  def phabricator_name(name: String = "", ext: String = ""): String =
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
    49
    "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
    50
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
    51
  def isabelle_phabricator_name(name: String = "", ext: String = ""): String =
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
    52
    "isabelle-" + phabricator_name(name = name, ext = ext)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    53
71068
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
    54
  def default_root(name: String): Path =
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
    55
    Path.explode("/var/www") + Path.basic(phabricator_name(name = name))
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    56
71068
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
    57
  def default_repo(name: String): Path = default_root(name) + Path.basic("repo")
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    58
71072
wenzelm
parents: 71071
diff changeset
    59
  val default_mailers: Path = Path.explode("mailers.json")
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
    60
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
    61
  val default_system_port = 22
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
    62
  val alternative_system_port = 222
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
    63
  val default_server_port = 2222
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
    64
71280
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
    65
  val standard_mercurial_source = "https://www.mercurial-scm.org/release/mercurial-5.2.1.tar.gz"
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
    66
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    67
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    68
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    69
  /** global configuration **/
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    70
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
    71
  val global_config = Path.explode("/etc/" + isabelle_phabricator_name(ext = "conf"))
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    72
71122
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
    73
  def global_config_script(
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
    74
    init: String = "",
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
    75
    body: String = "",
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
    76
    exit: String = ""): String =
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
    77
  {
71282
de59dd86760f tuned signature;
wenzelm
parents: 71281
diff changeset
    78
"""#!/bin/bash
71284
49bc17bf4384 more robust: avoid accidental use of stdin;
wenzelm
parents: 71283
diff changeset
    79
""" + (if (init.nonEmpty) "\n" + init else "") + """
49bc17bf4384 more robust: avoid accidental use of stdin;
wenzelm
parents: 71283
diff changeset
    80
{
71122
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
    81
  while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
    82
  do
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
    83
    NAME="$(echo "$REPLY" | cut -d: -f1)"
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
    84
    ROOT="$(echo "$REPLY" | cut -d: -f2)"
71284
49bc17bf4384 more robust: avoid accidental use of stdin;
wenzelm
parents: 71283
diff changeset
    85
    {
49bc17bf4384 more robust: avoid accidental use of stdin;
wenzelm
parents: 71283
diff changeset
    86
""" + Library.prefix_lines("      ", body) + """
49bc17bf4384 more robust: avoid accidental use of stdin;
wenzelm
parents: 71283
diff changeset
    87
    } < /dev/null
49bc17bf4384 more robust: avoid accidental use of stdin;
wenzelm
parents: 71283
diff changeset
    88
  done
49bc17bf4384 more robust: avoid accidental use of stdin;
wenzelm
parents: 71283
diff changeset
    89
} < """ + File.bash_path(global_config) + "\n" +
49bc17bf4384 more robust: avoid accidental use of stdin;
wenzelm
parents: 71283
diff changeset
    90
    (if (exit.nonEmpty) "\n" + exit + "\n" else "")
71122
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
    91
  }
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
    92
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    93
  sealed case class Config(name: String, root: Path)
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
    94
  {
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
    95
    def home: Path = root + Path.explode(phabricator_name())
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
    96
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
    97
    def execute(command: String): Process_Result =
71102
wenzelm
parents: 71101
diff changeset
    98
      Isabelle_System.bash("bin/" + command, cwd = home.file, redirect = true).check
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
    99
  }
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   100
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   101
  def read_config(): List[Config] =
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   102
  {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   103
    if (global_config.is_file) {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   104
      for (entry <- Library.trim_split_lines(File.read(global_config)) if entry.nonEmpty)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   105
      yield {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   106
        space_explode(':', entry) match {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   107
          case List(name, root) => Config(name, Path.explode(root))
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   108
          case _ => error("Malformed config file " + global_config + "\nentry " + quote(entry))
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   109
        }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   110
      }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   111
    }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   112
    else Nil
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   113
  }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   114
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   115
  def write_config(configs: List[Config])
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   116
  {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   117
    File.write(global_config,
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   118
      configs.map(config => config.name + ":" + config.root.implode).mkString("", "\n", "\n"))
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   119
  }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   120
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   121
  def get_config(name: String): Config =
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   122
    read_config().find(config => config.name == name) getOrElse
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   123
      error("Bad Isabelle/Phabricator installation " + quote(name))
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   124
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   125
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   126
71299
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   127
  /** administrative tools **/
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   128
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   129
  /* Isabelle tool wrapper */
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   130
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   131
  val isabelle_tool1 =
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   132
    Isabelle_Tool("phabricator", "invoke command-line tool within Phabricator home directory", args =>
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   133
    {
71101
67c2fed5b0e9 more options;
wenzelm
parents: 71098
diff changeset
   134
      var list = false
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   135
      var name = default_name
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   136
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   137
      val getopts =
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   138
        Getopts("""
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   139
Usage: isabelle phabricator [OPTIONS] COMMAND [ARGS...]
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   140
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   141
  Options are:
71101
67c2fed5b0e9 more options;
wenzelm
parents: 71098
diff changeset
   142
    -l           list available Phabricator installations
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   143
    -n NAME      Phabricator installation name (default: """ + quote(default_name) + """)
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   144
71103
c073c4e79518 more documentation;
wenzelm
parents: 71102
diff changeset
   145
  Invoke a command-line tool within the home directory of the named
c073c4e79518 more documentation;
wenzelm
parents: 71102
diff changeset
   146
  Phabricator installation.
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   147
""",
71101
67c2fed5b0e9 more options;
wenzelm
parents: 71098
diff changeset
   148
          "l" -> (_ => list = true),
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   149
          "n:" -> (arg => name = arg))
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   150
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   151
      val more_args = getopts(args)
71101
67c2fed5b0e9 more options;
wenzelm
parents: 71098
diff changeset
   152
      if (more_args.isEmpty && !list) getopts.usage()
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   153
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   154
      val progress = new Console_Progress
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   155
71101
67c2fed5b0e9 more options;
wenzelm
parents: 71098
diff changeset
   156
      if (list) {
67c2fed5b0e9 more options;
wenzelm
parents: 71098
diff changeset
   157
        for (config <- read_config()) {
71103
c073c4e79518 more documentation;
wenzelm
parents: 71102
diff changeset
   158
          progress.echo("phabricator " + quote(config.name) + " root " + config.root)
71101
67c2fed5b0e9 more options;
wenzelm
parents: 71098
diff changeset
   159
        }
67c2fed5b0e9 more options;
wenzelm
parents: 71098
diff changeset
   160
      }
71276
b4401dfd6544 clarified "isabelle phabricator -l": avoid surprise with non-existent default installation;
wenzelm
parents: 71274
diff changeset
   161
      else {
b4401dfd6544 clarified "isabelle phabricator -l": avoid surprise with non-existent default installation;
wenzelm
parents: 71274
diff changeset
   162
        val config = get_config(name)
b4401dfd6544 clarified "isabelle phabricator -l": avoid surprise with non-existent default installation;
wenzelm
parents: 71274
diff changeset
   163
        val result = progress.bash(Bash.strings(more_args), cwd = config.home.file, echo = true)
b4401dfd6544 clarified "isabelle phabricator -l": avoid surprise with non-existent default installation;
wenzelm
parents: 71274
diff changeset
   164
        if (!result.ok) error("Return code: " + result.rc.toString)
b4401dfd6544 clarified "isabelle phabricator -l": avoid surprise with non-existent default installation;
wenzelm
parents: 71274
diff changeset
   165
      }
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   166
    })
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   167
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   168
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   169
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   170
  /** setup **/
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   171
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   172
  def user_setup(name: String, description: String, ssh_setup: Boolean = false)
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   173
  {
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   174
    if (!Linux.user_exists(name)) {
71054
b64fc38327ae prefer system user setup, e.g. avoid occurrence on login screen;
wenzelm
parents: 71053
diff changeset
   175
      Linux.user_add(name, description = description, system = true, ssh_setup = ssh_setup)
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   176
    }
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   177
    else if (Linux.user_description(name) != description) {
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   178
      error("User " + quote(name) + " already exists --" +
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   179
        " for Phabricator it should have the description:\n  " + quote(description))
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   180
    }
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   181
  }
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   182
71282
de59dd86760f tuned signature;
wenzelm
parents: 71281
diff changeset
   183
  def command_setup(name: String,
de59dd86760f tuned signature;
wenzelm
parents: 71281
diff changeset
   184
    init: String = "",
de59dd86760f tuned signature;
wenzelm
parents: 71281
diff changeset
   185
    body: String = "",
de59dd86760f tuned signature;
wenzelm
parents: 71281
diff changeset
   186
    exit: String = ""): Path =
71270
wenzelm
parents: 71269
diff changeset
   187
  {
wenzelm
parents: 71269
diff changeset
   188
    val command = Path.explode("/usr/local/bin") + Path.basic(name)
71282
de59dd86760f tuned signature;
wenzelm
parents: 71281
diff changeset
   189
    File.write(command, global_config_script(init = init, body = body, exit = exit))
71270
wenzelm
parents: 71269
diff changeset
   190
    Isabelle_System.chmod("755", command)
wenzelm
parents: 71269
diff changeset
   191
    Isabelle_System.chown("root:root", command)
wenzelm
parents: 71269
diff changeset
   192
    command
wenzelm
parents: 71269
diff changeset
   193
  }
wenzelm
parents: 71269
diff changeset
   194
71280
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   195
  def mercurial_setup(mercurial_source: String, progress: Progress = No_Progress)
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   196
  {
71281
5b3a813853bb tuned message;
wenzelm
parents: 71280
diff changeset
   197
    progress.echo("\nMercurial installation from source " + quote(mercurial_source) + " ...")
71280
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   198
    Isabelle_System.with_tmp_dir("mercurial")(tmp_dir =>
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   199
    {
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   200
      val archive =
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   201
        if (Url.is_wellformed(mercurial_source)) {
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   202
          val archive = tmp_dir + Path.basic("mercurial.tar.gz")
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   203
          Bytes.write(archive, Url.read_bytes(Url(mercurial_source)))
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   204
          archive
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   205
        }
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   206
        else Path.explode(mercurial_source)
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   207
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   208
      Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   209
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   210
      File.read_dir(tmp_dir).filter(name => (tmp_dir + Path.basic(name)).is_dir) match {
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   211
        case List(dir) =>
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   212
          val build_dir = tmp_dir + Path.basic(dir)
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   213
          progress.bash("make all && make install", cwd = build_dir.file, echo = true).check
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   214
        case dirs =>
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   215
          error("Bad archive " + archive +
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   216
            (if (dirs.isEmpty) "" else "\nmultiple directory entries " + commas_quote(dirs)))
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   217
      }
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   218
    })
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   219
  }
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   220
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   221
  def phabricator_setup(
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   222
    name: String = default_name,
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   223
    root: String = "",
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   224
    repo: String = "",
71047
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   225
    package_update: Boolean = false,
71280
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   226
    mercurial_source: String = "",
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   227
    progress: Progress = No_Progress)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   228
  {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   229
    /* system environment */
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   230
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   231
    Linux.check_system_root()
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   232
71079
e06852132c1d tuned messages;
wenzelm
parents: 71078
diff changeset
   233
    progress.echo("System packages ...")
e06852132c1d tuned messages;
wenzelm
parents: 71078
diff changeset
   234
71047
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   235
    if (package_update) {
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   236
      Linux.package_update(progress = progress)
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   237
      Linux.check_reboot_required()
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   238
    }
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   239
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   240
    Linux.package_install(packages, progress = progress)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   241
    Linux.check_reboot_required()
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   242
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   243
71280
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   244
    if (mercurial_source.nonEmpty) {
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   245
      for { name <- List("mercurial", "mercurial-common") if Linux.package_installed(name) } {
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   246
        error("Cannot install Mercurial from source:" +
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   247
          "package package " + quote(name) + " already installed")
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   248
      }
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   249
      mercurial_setup(mercurial_source, progress = progress)
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   250
    }
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   251
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   252
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   253
    /* users */
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   254
71125
beb781551a66 more sanity checks;
wenzelm
parents: 71124
diff changeset
   255
    if (name.contains((c: Char) => !(Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c))) ||
71269
7df5c110a43c support database dump;
wenzelm
parents: 71268
diff changeset
   256
        Set("", "ssh", "phd", "dump", daemon_user).contains(name)) {
71125
beb781551a66 more sanity checks;
wenzelm
parents: 71124
diff changeset
   257
      error("Bad installation name: " + quote(name))
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   258
    }
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   259
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   260
    user_setup(daemon_user, "Phabricator Daemon User", ssh_setup = true)
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   261
    user_setup(name, "Phabricator SSH User")
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   262
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   263
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   264
    /* basic installation */
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   265
71079
e06852132c1d tuned messages;
wenzelm
parents: 71078
diff changeset
   266
    progress.echo("\nPhabricator installation ...")
71076
8ac137c65776 tuned messages;
wenzelm
parents: 71075
diff changeset
   267
71068
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
   268
    val root_path = if (root.nonEmpty) Path.explode(root) else default_root(name)
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
   269
    val repo_path = if (repo.nonEmpty) Path.explode(repo) else default_repo(name)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   270
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   271
    val configs = read_config()
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   272
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   273
    for (config <- configs if config.name == name) {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   274
      error("Duplicate Phabricator installation " + quote(name) + " in " + config.root)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   275
    }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   276
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   277
    if (!Isabelle_System.bash("mkdir -p " + File.bash_path(root_path)).ok) {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   278
      error("Failed to create root directory " + root_path)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   279
    }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   280
71116
wenzelm
parents: 71115
diff changeset
   281
    Isabelle_System.chown(Bash.string(www_user) + ":" + Bash.string(www_user), root_path)
wenzelm
parents: 71115
diff changeset
   282
    Isabelle_System.chmod("755", root_path)
wenzelm
parents: 71115
diff changeset
   283
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   284
    progress.bash(cwd = root_path.file, echo = true,
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   285
      script = """
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   286
        set -e
71126
18f87bdbc812 tuned message;
wenzelm
parents: 71125
diff changeset
   287
        echo "Cloning distribution repositories:"
71287
71fd25a7bbe2 more robust setup: avoid blind shot at "the latest" version;
wenzelm
parents: 71285
diff changeset
   288
71283
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   289
        git clone --branch stable https://github.com/phacility/libphutil.git
71287
71fd25a7bbe2 more robust setup: avoid blind shot at "the latest" version;
wenzelm
parents: 71285
diff changeset
   290
        git -C libphutil reset --hard 1750586fdc50a6cd98adba4aa2f5a7649bd91dbe
71fd25a7bbe2 more robust setup: avoid blind shot at "the latest" version;
wenzelm
parents: 71285
diff changeset
   291
71283
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   292
        git clone --branch stable https://github.com/phacility/arcanist.git
71287
71fd25a7bbe2 more robust setup: avoid blind shot at "the latest" version;
wenzelm
parents: 71285
diff changeset
   293
        git -C arcanist reset --hard bac2028421a4be6e34e08764bbbda49e68b3a604
71fd25a7bbe2 more robust setup: avoid blind shot at "the latest" version;
wenzelm
parents: 71285
diff changeset
   294
71283
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   295
        git clone --branch stable https://github.com/phacility/phabricator.git
71287
71fd25a7bbe2 more robust setup: avoid blind shot at "the latest" version;
wenzelm
parents: 71285
diff changeset
   296
        git -C phabricator reset --hard c4b4a53cad7722f031b725f8b41511e9d341d033
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   297
      """).check
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   298
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   299
    val config = Config(name, root_path)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   300
    write_config(configs ::: List(config))
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   301
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   302
    config.execute("config set pygments.enabled true")
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   303
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   304
71050
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   305
    /* local repository directory */
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   306
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   307
    progress.echo("\nRepository hosting setup ...")
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   308
71050
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   309
    if (!Isabelle_System.bash("mkdir -p " + File.bash_path(repo_path)).ok) {
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   310
      error("Failed to create local repository directory " + repo_path)
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   311
    }
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   312
71114
6cfec8029831 clarified signature;
wenzelm
parents: 71112
diff changeset
   313
    Isabelle_System.chown(
6cfec8029831 clarified signature;
wenzelm
parents: 71112
diff changeset
   314
      "-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), repo_path)
6cfec8029831 clarified signature;
wenzelm
parents: 71112
diff changeset
   315
    Isabelle_System.chmod("755", repo_path)
71050
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   316
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   317
    config.execute("config set repository.default-local-path " + File.bash_path(repo_path))
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   318
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   319
71277
74cabc06cf2d proper support for multiple installations;
wenzelm
parents: 71276
diff changeset
   320
    val sudoers_file =
74cabc06cf2d proper support for multiple installations;
wenzelm
parents: 71276
diff changeset
   321
      Path.explode("/etc/sudoers.d") + Path.basic(isabelle_phabricator_name(name = name))
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   322
    File.write(sudoers_file,
71280
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   323
      www_user + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/local/bin/hg, /usr/bin/hg, /usr/bin/ssh, /usr/bin/id\n" +
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   324
      name + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/bin/git-upload-pack, /usr/bin/git-receive-pack, /usr/local/bin/hg, /usr/bin/hg, /usr/bin/svnserve, /usr/bin/ssh, /usr/bin/id\n")
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   325
71115
wenzelm
parents: 71114
diff changeset
   326
    Isabelle_System.chmod("440", sudoers_file)
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   327
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   328
    config.execute("config set diffusion.ssh-user " + Bash.string(config.name))
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   329
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   330
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   331
    /* MySQL setup */
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   332
71079
e06852132c1d tuned messages;
wenzelm
parents: 71078
diff changeset
   333
    progress.echo("\nMySQL setup ...")
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   334
71055
27a998cdc0f4 back to plain name, to have it accepted my mysql;
wenzelm
parents: 71054
diff changeset
   335
    File.write(Path.explode("/etc/mysql/mysql.conf.d/" + phabricator_name(ext = "cnf")),
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   336
"""[mysqld]
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   337
max_allowed_packet = 32M
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   338
innodb_buffer_pool_size = 1600M
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   339
local_infile = 0
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   340
""")
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   341
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   342
    Linux.service_restart("mysql")
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   343
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   344
71266
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   345
    def mysql_conf(R: Regex, which: String): String =
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   346
    {
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   347
      val conf = Path.explode("/etc/mysql/debian.cnf")
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   348
      split_lines(File.read(conf)).collectFirst({ case R(a) => a }) match {
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   349
        case Some(res) => res
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   350
        case None => error("Cannot determine " + which + " from " + conf)
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   351
      }
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   352
    }
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   353
71266
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   354
    val mysql_root_user = mysql_conf("""^user\s*=\s*(\S*)\s*$""".r, "superuser name")
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   355
    val mysql_root_password = mysql_conf("""^password\s*=\s*(\S*)\s*$""".r, "superuser password")
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   356
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   357
    val mysql_name = phabricator_name(name = name).replace("-", "_")
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   358
    val mysql_user_string = SQL.string(mysql_name) + "@'localhost'"
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   359
    val mysql_password = Linux.generate_password()
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   360
71266
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   361
    Isabelle_System.bash("mysql --user=" + Bash.string(mysql_root_user) +
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   362
      " --password=" + Bash.string(mysql_root_password) + " --execute=" +
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   363
      Bash.string(
71274
5212ca49598a more robust;
wenzelm
parents: 71273
diff changeset
   364
        """DROP USER IF EXISTS """ + mysql_user_string + "; " +
5212ca49598a more robust;
wenzelm
parents: 71273
diff changeset
   365
        """CREATE USER """ + mysql_user_string +
71266
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   366
        """ IDENTIFIED BY """ + SQL.string(mysql_password) + """ PASSWORD EXPIRE NEVER; """ +
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   367
        """GRANT ALL ON `""" + (mysql_name + "_%").replace("_", "\\_") +
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   368
        """`.* TO """ + mysql_user_string + ";")).check
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   369
71266
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   370
    config.execute("config set mysql.user " + Bash.string(mysql_name))
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   371
    config.execute("config set mysql.pass " + Bash.string(mysql_password))
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   372
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   373
    config.execute("config set phabricator.cache-namespace " + Bash.string(mysql_name))
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   374
    config.execute("config set storage.default-namespace " + Bash.string(mysql_name))
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   375
    config.execute("config set storage.mysql-engine.max-size 8388608")
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   376
71102
wenzelm
parents: 71101
diff changeset
   377
    progress.bash("bin/storage upgrade --force", cwd = config.home.file, echo = true).check
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   378
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   379
71269
7df5c110a43c support database dump;
wenzelm
parents: 71268
diff changeset
   380
    /* database dump */
7df5c110a43c support database dump;
wenzelm
parents: 71268
diff changeset
   381
7df5c110a43c support database dump;
wenzelm
parents: 71268
diff changeset
   382
    val dump_name = isabelle_phabricator_name(name = "dump")
71282
de59dd86760f tuned signature;
wenzelm
parents: 71281
diff changeset
   383
    command_setup(dump_name, body =
71269
7df5c110a43c support database dump;
wenzelm
parents: 71268
diff changeset
   384
"""mkdir -p "$ROOT/database" && chown root:root "$ROOT/database" && chmod 700 "$ROOT/database"
7df5c110a43c support database dump;
wenzelm
parents: 71268
diff changeset
   385
[ -e "$ROOT/database/dump.sql.gz" ] && mv -f "$ROOT/database/dump.sql.gz" "$ROOT/database/dump-old.sql.gz"
7df5c110a43c support database dump;
wenzelm
parents: 71268
diff changeset
   386
echo "Creating $ROOT/database/dump.sql.gz"
71270
wenzelm
parents: 71269
diff changeset
   387
"$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' """)
71269
7df5c110a43c support database dump;
wenzelm
parents: 71268
diff changeset
   388
7df5c110a43c support database dump;
wenzelm
parents: 71268
diff changeset
   389
71283
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   390
    /* Phabricator upgrade */
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   391
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   392
    command_setup(isabelle_phabricator_name(name = "upgrade"),
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   393
      init =
71285
8cd05f7b3b4a proper default;
wenzelm
parents: 71284
diff changeset
   394
"""BRANCH="${1:-stable}"
71283
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   395
if [ "$BRANCH" != "master" -a "$BRANCH" != "stable" ]
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   396
then
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   397
  echo "Bad branch: \"$BRANCH\""
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   398
  exit 1
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   399
fi
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   400
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   401
systemctl stop isabelle-phabricator-phd
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   402
systemctl stop apache2
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   403
""",
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   404
      body =
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   405
"""echo -e "\nUpgrading phabricator \"$NAME\" root \"$ROOT\" ..."
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   406
for REPO in libphutil arcanist phabricator
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   407
do
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   408
  cd "$ROOT/$REPO"
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   409
  echo -e "\nUpdating \"$REPO\" ..."
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   410
  git checkout "$BRANCH"
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   411
  git pull
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   412
done
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   413
echo -e "\nUpgrading storage ..."
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   414
"$ROOT/phabricator/bin/storage" upgrade --force
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   415
""",
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   416
      exit =
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   417
"""systemctl start apache2
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   418
systemctl start isabelle-phabricator-phd""")
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   419
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   420
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   421
    /* PHP setup */
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   422
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   423
    val php_version =
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   424
      Isabelle_System.bash("""php --run 'echo PHP_MAJOR_VERSION . "." . PHP_MINOR_VERSION;'""")
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   425
        .check.out
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   426
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   427
    val php_conf =
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   428
      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
   429
        Path.explode("apache2/conf.d") +
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   430
        Path.basic(isabelle_phabricator_name(ext = "ini"))
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   431
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   432
    File.write(php_conf,
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   433
      "post_max_size = 32M\n" +
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   434
      "opcache.validate_timestamps = 0\n" +
71129
557703db74c3 tuned PHP setup;
wenzelm
parents: 71128
diff changeset
   435
      "memory_limit = 512M\n" +
557703db74c3 tuned PHP setup;
wenzelm
parents: 71128
diff changeset
   436
      "max_execution_time = 120\n")
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   437
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   438
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   439
    /* Apache setup */
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   440
71079
e06852132c1d tuned messages;
wenzelm
parents: 71078
diff changeset
   441
    progress.echo("Apache setup ...")
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   442
71068
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
   443
    val apache_root = Path.explode("/etc/apache2")
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   444
    val apache_sites = apache_root + Path.explode("sites-available")
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   445
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   446
    if (!apache_sites.is_dir) error("Bad Apache sites directory " + apache_sites)
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   447
71058
6ca9e8377613 proper names for multiple installations;
wenzelm
parents: 71057
diff changeset
   448
    val server_name = phabricator_name(name = name, ext = "lvh.me")  // alias for "localhost" for testing
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   449
    val server_url = "http://" + server_name
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   450
71058
6ca9e8377613 proper names for multiple installations;
wenzelm
parents: 71057
diff changeset
   451
    File.write(apache_sites + Path.basic(isabelle_phabricator_name(name = name, ext = "conf")),
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   452
"""<VirtualHost *:80>
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   453
    ServerName """ + server_name + """
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   454
    ServerAdmin webmaster@localhost
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   455
    DocumentRoot """ + config.home.implode + """/webroot
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   456
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   457
    ErrorLog ${APACHE_LOG_DIR}/error.log
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   458
    RewriteEngine on
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   459
    RewriteRule ^(.*)$  /index.php?__path__=$1  [B,L,QSA]
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   460
</VirtualHost>
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   461
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   462
# vim: syntax=apache ts=4 sw=4 sts=4 sr noet
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   463
""")
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   464
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   465
    Isabelle_System.bash( """
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   466
      set -e
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   467
      a2enmod rewrite
71058
6ca9e8377613 proper names for multiple installations;
wenzelm
parents: 71057
diff changeset
   468
      a2ensite """ + Bash.string(isabelle_phabricator_name(name = name))).check
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   469
71057
2965304143d8 more phabricator setup;
wenzelm
parents: 71056
diff changeset
   470
    config.execute("config set phabricator.base-uri " + Bash.string(server_url))
2965304143d8 more phabricator setup;
wenzelm
parents: 71056
diff changeset
   471
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   472
    Linux.service_restart("apache2")
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   473
71128
f79006c533b0 clarified errors: PHP daemon can fail under odd circumstances;
wenzelm
parents: 71127
diff changeset
   474
    progress.echo("\nWeb configuration via " + server_url)
f79006c533b0 clarified errors: PHP daemon can fail under odd circumstances;
wenzelm
parents: 71127
diff changeset
   475
71053
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   476
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   477
    /* PHP daemon */
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   478
71128
f79006c533b0 clarified errors: PHP daemon can fail under odd circumstances;
wenzelm
parents: 71127
diff changeset
   479
    progress.echo("\nPHP daemon setup ...")
71053
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   480
71273
6b8cbdc9713b more robust;
wenzelm
parents: 71270
diff changeset
   481
    val phd_log_path = Path.explode("/var/tmp/phd")
6b8cbdc9713b more robust;
wenzelm
parents: 71270
diff changeset
   482
    Isabelle_System.mkdirs(phd_log_path)
6b8cbdc9713b more robust;
wenzelm
parents: 71270
diff changeset
   483
    Isabelle_System.chown(
6b8cbdc9713b more robust;
wenzelm
parents: 71270
diff changeset
   484
      "-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), phd_log_path)
6b8cbdc9713b more robust;
wenzelm
parents: 71270
diff changeset
   485
    Isabelle_System.chmod("755", phd_log_path)
6b8cbdc9713b more robust;
wenzelm
parents: 71270
diff changeset
   486
71053
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   487
    config.execute("config set phd.user " + Bash.string(daemon_user))
71112
eed5b6188371 more support for multiple daemons;
wenzelm
parents: 71111
diff changeset
   488
    config.execute("config set phd.log-directory /var/tmp/phd/" +
eed5b6188371 more support for multiple daemons;
wenzelm
parents: 71111
diff changeset
   489
      isabelle_phabricator_name(name = name) + "/log")
71053
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   490
71124
7dbadecdc118 just one isabelle-phabricator-phd service, which manages all processes uniformly (NB: "bin/phd stop" affects all installations);
wenzelm
parents: 71122
diff changeset
   491
    val phd_name = isabelle_phabricator_name(name = "phd")
71127
0ad53b5f2bb1 more robust;
wenzelm
parents: 71126
diff changeset
   492
    Linux.service_shutdown(phd_name)
71282
de59dd86760f tuned signature;
wenzelm
parents: 71281
diff changeset
   493
    val phd_command = command_setup(phd_name, body = """"$ROOT/phabricator/bin/phd" "$@" """)
71128
f79006c533b0 clarified errors: PHP daemon can fail under odd circumstances;
wenzelm
parents: 71127
diff changeset
   494
    try {
f79006c533b0 clarified errors: PHP daemon can fail under odd circumstances;
wenzelm
parents: 71127
diff changeset
   495
      Linux.service_install(phd_name,
71053
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   496
"""[Unit]
71124
7dbadecdc118 just one isabelle-phabricator-phd service, which manages all processes uniformly (NB: "bin/phd stop" affects all installations);
wenzelm
parents: 71122
diff changeset
   497
Description=PHP daemon manager for Isabelle/Phabricator
71053
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   498
After=syslog.target network.target apache2.service mysql.service
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   499
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   500
[Service]
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   501
Type=oneshot
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   502
User=""" + daemon_user + """
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   503
Group=""" + daemon_user + """
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   504
Environment=PATH=/sbin:/usr/sbin:/usr/local/sbin:/usr/local/bin:/usr/bin:/bin
71124
7dbadecdc118 just one isabelle-phabricator-phd service, which manages all processes uniformly (NB: "bin/phd stop" affects all installations);
wenzelm
parents: 71122
diff changeset
   505
ExecStart=""" + phd_command.implode + """ start --force
7dbadecdc118 just one isabelle-phabricator-phd service, which manages all processes uniformly (NB: "bin/phd stop" affects all installations);
wenzelm
parents: 71122
diff changeset
   506
ExecStop=""" + phd_command.implode + """ stop
71053
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   507
RemainAfterExit=yes
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   508
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   509
[Install]
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   510
WantedBy=multi-user.target
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   511
""")
71128
f79006c533b0 clarified errors: PHP daemon can fail under odd circumstances;
wenzelm
parents: 71127
diff changeset
   512
    }
f79006c533b0 clarified errors: PHP daemon can fail under odd circumstances;
wenzelm
parents: 71127
diff changeset
   513
    catch {
f79006c533b0 clarified errors: PHP daemon can fail under odd circumstances;
wenzelm
parents: 71127
diff changeset
   514
      case ERROR(msg) =>
f79006c533b0 clarified errors: PHP daemon can fail under odd circumstances;
wenzelm
parents: 71127
diff changeset
   515
        progress.bash("bin/phd status", cwd = config.home.file, echo = true).check
f79006c533b0 clarified errors: PHP daemon can fail under odd circumstances;
wenzelm
parents: 71127
diff changeset
   516
        error(msg)
f79006c533b0 clarified errors: PHP daemon can fail under odd circumstances;
wenzelm
parents: 71127
diff changeset
   517
    }
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   518
  }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   519
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   520
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   521
  /* Isabelle tool wrapper */
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   522
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   523
  val isabelle_tool2 =
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   524
    Isabelle_Tool("phabricator_setup", "setup Phabricator server on Ubuntu Linux", args =>
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   525
    {
71280
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   526
      var mercurial_source = ""
71047
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   527
      var repo = ""
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   528
      var package_update = false
71078
5bb2235d843d clarified command-line;
wenzelm
parents: 71077
diff changeset
   529
      var name = default_name
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   530
      var root = ""
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   531
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   532
      val getopts =
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   533
        Getopts("""
71078
5bb2235d843d clarified command-line;
wenzelm
parents: 71077
diff changeset
   534
Usage: isabelle phabricator_setup [OPTIONS]
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   535
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   536
  Options are:
71280
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   537
    -M SOURCE    install Mercurial from source: local PATH, or URL, or ":" for
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   538
                 """ + standard_mercurial_source + """
71068
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
   539
    -R DIR       repository directory (default: """ + default_repo("NAME") + """)
71047
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   540
    -U           full update of system packages before installation
71078
5bb2235d843d clarified command-line;
wenzelm
parents: 71077
diff changeset
   541
    -n NAME      Phabricator installation name (default: """ + quote(default_name) + """)
71068
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
   542
    -r DIR       installation root directory (default: """ + default_root("NAME") + """)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   543
71103
c073c4e79518 more documentation;
wenzelm
parents: 71102
diff changeset
   544
  Install Phabricator as LAMP application (Linux, Apache, MySQL, PHP).
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   545
71078
5bb2235d843d clarified command-line;
wenzelm
parents: 71077
diff changeset
   546
  The installation name (default: """ + quote(default_name) + """) is mapped to a regular
5bb2235d843d clarified command-line;
wenzelm
parents: 71077
diff changeset
   547
  Unix user; this is relevant for public SSH access.
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   548
""",
71280
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   549
          "M:" -> (arg => mercurial_source = (if (arg == ":") standard_mercurial_source else arg)),
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   550
          "R:" -> (arg => repo = arg),
71047
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   551
          "U" -> (_ => package_update = true),
71078
5bb2235d843d clarified command-line;
wenzelm
parents: 71077
diff changeset
   552
          "n:" -> (arg => name = arg),
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   553
          "r:" -> (arg => root = arg))
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   554
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   555
      val more_args = getopts(args)
71078
5bb2235d843d clarified command-line;
wenzelm
parents: 71077
diff changeset
   556
      if (more_args.nonEmpty) getopts.usage()
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   557
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   558
      val progress = new Console_Progress
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   559
71268
e2fb60756fb8 proper check of Linux version;
wenzelm
parents: 71266
diff changeset
   560
      val release = Linux.Release()
e2fb60756fb8 proper check of Linux version;
wenzelm
parents: 71266
diff changeset
   561
      if (!release.is_ubuntu_18_04) error("Bad Linux version: Ubuntu 18.04 LTS required")
e2fb60756fb8 proper check of Linux version;
wenzelm
parents: 71266
diff changeset
   562
71078
5bb2235d843d clarified command-line;
wenzelm
parents: 71077
diff changeset
   563
      phabricator_setup(name = name, root = root, repo = repo,
71280
5a2033fc8f3d avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents: 71277
diff changeset
   564
        package_update = package_update, mercurial_source = mercurial_source, progress = progress)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   565
    })
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   566
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   567
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   568
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   569
  /** setup mail **/
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   570
71072
wenzelm
parents: 71071
diff changeset
   571
  val mailers_template: String =
wenzelm
parents: 71071
diff changeset
   572
"""[
wenzelm
parents: 71071
diff changeset
   573
  {
wenzelm
parents: 71071
diff changeset
   574
    "key": "example.org",
wenzelm
parents: 71071
diff changeset
   575
    "type": "smtp",
wenzelm
parents: 71071
diff changeset
   576
    "options": {
wenzelm
parents: 71071
diff changeset
   577
      "host": "mail.example.org",
wenzelm
parents: 71071
diff changeset
   578
      "port": 465,
wenzelm
parents: 71071
diff changeset
   579
      "user": "phabricator@example.org",
wenzelm
parents: 71071
diff changeset
   580
      "password": "********",
wenzelm
parents: 71071
diff changeset
   581
      "protocol": "ssl",
wenzelm
parents: 71071
diff changeset
   582
      "message-id": true
wenzelm
parents: 71071
diff changeset
   583
    }
wenzelm
parents: 71071
diff changeset
   584
  }
wenzelm
parents: 71071
diff changeset
   585
]"""
wenzelm
parents: 71071
diff changeset
   586
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   587
  def phabricator_setup_mail(
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   588
    name: String = default_name,
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   589
    config_file: Option[Path] = None,
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   590
    test_user: String = "",
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   591
    progress: Progress = No_Progress)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   592
  {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   593
    Linux.check_system_root()
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   594
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   595
    val config = get_config(name)
71073
d61fd7aade69 clarified directory;
wenzelm
parents: 71072
diff changeset
   596
    val default_config_file = config.root + default_mailers
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   597
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   598
    val mail_config = config_file getOrElse default_config_file
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   599
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   600
    def setup_mail
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   601
    {
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   602
      progress.echo("Using mail configuration from " + mail_config)
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   603
      config.execute("config set cluster.mailers --stdin < " + File.bash_path(mail_config))
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   604
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   605
      if (test_user.nonEmpty) {
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   606
        progress.echo("Sending test mail to " + quote(test_user))
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   607
        progress.bash(cwd = config.home.file, echo = true,
71102
wenzelm
parents: 71101
diff changeset
   608
          script = """echo "Test from Phabricator ($(date))" | bin/mail send-test --subject "Test" --to """ +
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   609
            Bash.string(test_user)).check
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   610
      }
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   611
    }
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   612
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   613
    if (config_file.isEmpty) {
71070
79b89278b825 clarified permissions;
wenzelm
parents: 71068
diff changeset
   614
      if (!default_config_file.is_file) {
79b89278b825 clarified permissions;
wenzelm
parents: 71068
diff changeset
   615
        File.write(default_config_file, mailers_template)
71114
6cfec8029831 clarified signature;
wenzelm
parents: 71112
diff changeset
   616
        Isabelle_System.chmod("600", default_config_file)
71070
79b89278b825 clarified permissions;
wenzelm
parents: 71068
diff changeset
   617
      }
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   618
      if (File.read(default_config_file) == mailers_template) {
71131
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71129
diff changeset
   619
        progress.echo("Please invoke the tool again, after providing details in\n  " +
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71129
diff changeset
   620
          default_config_file.implode + "\n")
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   621
      }
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   622
      else setup_mail
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   623
    }
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   624
    else setup_mail
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   625
  }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   626
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   627
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   628
  /* Isabelle tool wrapper */
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   629
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   630
  val isabelle_tool3 =
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   631
    Isabelle_Tool("phabricator_setup_mail",
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   632
      "setup mail for one Phabricator installation", args =>
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   633
    {
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   634
      var test_user = ""
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   635
      var name = default_name
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   636
      var config_file: Option[Path] = None
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   637
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   638
      val getopts =
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   639
        Getopts("""
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   640
Usage: isabelle phabricator_setup_mail [OPTIONS]
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   641
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   642
  Options are:
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   643
    -T USER      send test mail to Phabricator user
71103
c073c4e79518 more documentation;
wenzelm
parents: 71102
diff changeset
   644
    -f FILE      config file (default: """ + default_mailers + """ within Phabricator root)
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   645
    -n NAME      Phabricator installation name (default: """ + quote(default_name) + """)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   646
71077
41b6ca223500 tuned messages;
wenzelm
parents: 71076
diff changeset
   647
  Provide mail configuration for existing Phabricator installation.
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   648
""",
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   649
          "T:" -> (arg => test_user = arg),
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   650
          "f:" -> (arg => config_file = Some(Path.explode(arg))),
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   651
          "n:" -> (arg => name = arg))
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   652
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   653
      val more_args = getopts(args)
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   654
      if (more_args.nonEmpty) getopts.usage()
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   655
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   656
      val progress = new Console_Progress
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   657
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   658
      phabricator_setup_mail(name = name, config_file = config_file,
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   659
        test_user = test_user, progress = progress)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   660
    })
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   661
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   662
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   663
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   664
  /** setup ssh **/
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   665
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   666
  /* sshd config */
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   667
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   668
  private val Port = """^\s*Port\s+(\d+)\s*$""".r
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   669
  private val No_Port = """^#\s*Port\b.*$""".r
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   670
  private val Any_Port = """^#?\s*Port\b.*$""".r
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   671
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   672
  def conf_ssh_port(port: Int): String =
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   673
    if (port == 22) "#Port 22" else "Port " + port
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   674
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   675
  def read_ssh_port(conf: Path): Int =
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   676
  {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   677
    val lines = split_lines(File.read(conf))
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   678
    val ports =
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   679
      lines.flatMap({
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   680
        case Port(Value.Int(p)) => Some(p)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   681
        case No_Port() => Some(22)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   682
        case _ => None
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   683
      })
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   684
    ports match {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   685
      case List(port) => port
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   686
      case Nil => error("Missing Port specification in " + conf)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   687
      case _ => error("Multiple Port specifications in " + conf)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   688
    }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   689
  }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   690
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   691
  def write_ssh_port(conf: Path, port: Int): Boolean =
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   692
  {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   693
    val old_port = read_ssh_port(conf)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   694
    if (old_port == port) false
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   695
    else {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   696
      val lines = split_lines(File.read(conf))
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   697
      val lines1 = lines.map({ case Any_Port() => conf_ssh_port(port) case line => line })
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   698
      File.write(conf, cat_lines(lines1))
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   699
      true
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   700
    }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   701
  }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   702
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   703
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   704
  /* phabricator_setup_ssh */
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   705
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   706
  def phabricator_setup_ssh(
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   707
    server_port: Int = default_server_port,
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   708
    system_port: Int = default_system_port,
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   709
    progress: Progress = No_Progress)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   710
  {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   711
    Linux.check_system_root()
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   712
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   713
    val configs = read_config()
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   714
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   715
    if (server_port == system_port) {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   716
      error("Port for Phabricator sshd coincides with system port: " + system_port)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   717
    }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   718
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   719
    val sshd_conf_system = Path.explode("/etc/ssh/sshd_config")
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   720
    val sshd_conf_server = sshd_conf_system.ext(isabelle_phabricator_name())
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   721
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   722
    val ssh_name = isabelle_phabricator_name(name = "ssh")
71111
cd166c3904dd more robust: system ssh service is required for Phabricator ssh service;
wenzelm
parents: 71109
diff changeset
   723
    Linux.service_shutdown(ssh_name)
cd166c3904dd more robust: system ssh service is required for Phabricator ssh service;
wenzelm
parents: 71109
diff changeset
   724
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   725
    val old_system_port = read_ssh_port(sshd_conf_system)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   726
    if (old_system_port != system_port) {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   727
      progress.echo("Reconfigurig system ssh service")
71111
cd166c3904dd more robust: system ssh service is required for Phabricator ssh service;
wenzelm
parents: 71109
diff changeset
   728
      Linux.service_shutdown("ssh")
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   729
      write_ssh_port(sshd_conf_system, system_port)
71111
cd166c3904dd more robust: system ssh service is required for Phabricator ssh service;
wenzelm
parents: 71109
diff changeset
   730
      Linux.service_start("ssh")
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   731
    }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   732
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   733
    progress.echo("Configuring " + ssh_name + " service")
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   734
71282
de59dd86760f tuned signature;
wenzelm
parents: 71281
diff changeset
   735
    val ssh_command = command_setup(ssh_name, body =
71122
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
   736
"""if [ "$1" = "$NAME" ]
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
   737
then
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
   738
  exec "$ROOT/phabricator/bin/ssh-auth" "$@"
71270
wenzelm
parents: 71269
diff changeset
   739
fi""", exit = "exit 1")
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   740
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   741
    File.write(sshd_conf_server,
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   742
"""# OpenBSD Secure Shell server for Isabelle/Phabricator
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   743
AuthorizedKeysCommand """ + ssh_command.implode + """
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   744
AuthorizedKeysCommandUser """ + daemon_user + """
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   745
AuthorizedKeysFile none
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   746
AllowUsers """ + configs.map(_.name).mkString(" ") + """
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   747
Port """ + server_port + """
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   748
Protocol 2
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   749
PermitRootLogin no
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   750
AllowAgentForwarding no
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   751
AllowTcpForwarding no
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   752
PrintMotd no
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   753
PrintLastLog no
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   754
PasswordAuthentication no
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   755
ChallengeResponseAuthentication no
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   756
PidFile /var/run/""" + ssh_name + """.pid
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   757
""")
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   758
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   759
    Linux.service_install(ssh_name,
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   760
"""[Unit]
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   761
Description=OpenBSD Secure Shell server for Isabelle/Phabricator
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   762
After=network.target auditd.service
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   763
ConditionPathExists=!/etc/ssh/sshd_not_to_be_run
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   764
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   765
[Service]
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   766
EnvironmentFile=-/etc/default/ssh
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   767
ExecStartPre=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   768
ExecStart=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -D $SSHD_OPTS
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   769
ExecReload=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   770
ExecReload=/bin/kill -HUP $MAINPID
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   771
KillMode=process
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   772
Restart=on-failure
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   773
RestartPreventExitStatus=255
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   774
Type=notify
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   775
RuntimeDirectory=sshd-phabricator
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   776
RuntimeDirectoryMode=0755
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   777
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   778
[Install]
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   779
WantedBy=multi-user.target
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   780
Alias=""" + ssh_name + """.service
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   781
""")
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   782
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   783
    for (config <- configs) {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   784
      progress.echo("phabricator " + quote(config.name) + " port " +  server_port)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   785
      config.execute("config set diffusion.ssh-port " + Bash.string(server_port.toString))
71292
8b745b4d71b5 more rebust setup for Subversion -- assuming that diffusion.ssh-port is only set in phabricator/conf/local/local.json, not in the database;
wenzelm
parents: 71288
diff changeset
   786
      if (server_port == 22) config.execute("config delete diffusion.ssh-port")
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   787
    }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   788
  }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   789
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   790
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   791
  /* Isabelle tool wrapper */
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   792
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   793
  val isabelle_tool4 =
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   794
    Isabelle_Tool("phabricator_setup_ssh",
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   795
      "setup ssh service for all Phabricator installations", args =>
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   796
    {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   797
      var server_port = default_server_port
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   798
      var system_port = default_system_port
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   799
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   800
      val getopts =
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   801
        Getopts("""
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   802
Usage: isabelle phabricator_setup_ssh [OPTIONS]
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   803
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   804
  Options are:
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   805
    -p PORT      sshd port for Phabricator servers (default: """ + default_server_port + """)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   806
    -q PORT      sshd port for the operating system (default: """ + default_system_port + """)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   807
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   808
  Configure ssh service for all Phabricator installations: a separate sshd
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   809
  is run in addition to the one of the operating system, and ports need to
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   810
  be distinct.
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   811
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   812
  A particular Phabricator installation is addressed by using its
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   813
  name as the ssh user; the actual Phabricator user is determined via
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   814
  stored ssh keys.
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   815
""",
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   816
          "p:" -> (arg => server_port = Value.Int.parse(arg)),
71295
6aadbd650280 eliminated pointless option -T: it merely tests ssh config of root, which is not required later;
wenzelm
parents: 71292
diff changeset
   817
          "q:" -> (arg => system_port = Value.Int.parse(arg)))
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   818
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   819
      val more_args = getopts(args)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   820
      if (more_args.nonEmpty) getopts.usage()
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   821
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   822
      val progress = new Console_Progress
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   823
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   824
      phabricator_setup_ssh(
71295
6aadbd650280 eliminated pointless option -T: it merely tests ssh config of root, which is not required later;
wenzelm
parents: 71292
diff changeset
   825
        server_port = server_port, system_port = system_port, progress = progress)
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   826
    })
71299
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   827
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   828
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   829
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   830
  /** conduit API **/
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   831
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   832
  object Conduit
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   833
  {
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   834
    def apply(ssh_host: String, ssh_user: String, ssh_port: Int = 22): Conduit =
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   835
      new Conduit(ssh_host, ssh_user, ssh_port)
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   836
  }
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   837
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   838
  final class Conduit private(ssh_host: String, ssh_user: String, ssh_port: Int)
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   839
  {
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   840
    /* connection */
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   841
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   842
    require(ssh_host.nonEmpty && ssh_port >= 0)
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   843
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   844
    private def ssh_user_prefix: String = if (ssh_user.isEmpty) "" else ssh_user + "@"
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   845
    private def ssh_port_suffix: String = if (ssh_port == 22) "" else ":" + ssh_port
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   846
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   847
    override def toString: String = ssh_user_prefix + ssh_host + ssh_port_suffix
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   848
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   849
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   850
    /* execute methods */
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   851
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   852
    def execute(
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   853
      method: String,
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   854
      args: List[String] = Nil,
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   855
      input: JSON.T = JSON.Object.empty): JSON.T =
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   856
    {
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   857
      Isabelle_System.with_tmp_file("input", "json")(input_file =>
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   858
      {
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   859
        File.write(input_file, JSON.Format(JSON.Object("params" -> JSON.Format(input))))
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   860
        val result =
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   861
          Isabelle_System.bash(
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   862
            "ssh -p " + ssh_port + " " + Bash.string(ssh_user_prefix + ssh_host) +
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   863
            " conduit " + Bash.strings(method :: args) + " < " + File.bash_path(input_file)).check
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   864
        JSON.parse(result.out, strict = false)
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   865
      })
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   866
    }
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   867
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   868
    def execute_result(
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   869
      method: String,
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   870
      args: List[String] = Nil,
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   871
      input: JSON.T = JSON.Object.empty): API.Result =
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   872
    {
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   873
      API.make_result(execute(method, args = args, input = input))
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   874
    }
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   875
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   876
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   877
    /* concrete methods */
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   878
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   879
    def ping(): String = execute_result("conduit.ping").get_string
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   880
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   881
    lazy val user_phid: String = execute_result("user.whoami").get_value(JSON.string(_, "phid"))
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   882
    lazy val user_name: String = execute_result("user.whoami").get_value(JSON.string(_, "userName"))
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   883
  }
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   884
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   885
  object API
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   886
  {
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   887
    /* result with optional error */
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   888
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   889
    object Error_Code extends Enumeration
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   890
    {
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   891
      val bad_diff = Value("ERR-BAD-DIFF")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   892
      val bad_document = Value("ERR-BAD-DOCUMENT")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   893
      val bad_file = Value("ERR-BAD-FILE")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   894
      val bad_phid = Value("ERR-BAD-PHID")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   895
      val bad_revision = Value("ERR-BAD-REVISION")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   896
      val bad_task = Value("ERR-BAD-TASK")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   897
      val bad_token = Value("ERR-BAD-TOKEN")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   898
      val bad_version = Value("ERR-BAD-VERSION")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   899
      val conduit_call = Value("ERR-CONDUIT-CALL")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   900
      val conduit_core = Value("ERR-CONDUIT-CORE")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   901
      val invalid_auth = Value("ERR-INVALID-AUTH")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   902
      val invalid_certificate = Value("ERR-INVALID-CERTIFICATE")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   903
      val invalid_engine_ = Value("ERR-INVALID_ENGINE")  // FIXME !?
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   904
      val invalid_engine = Value("ERR-INVALID-ENGINE")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   905
      val invalid_parameter = Value("ERR-INVALID-PARAMETER")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   906
      val invalid_session = Value("ERR-INVALID-SESSION")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   907
      val invalid_token = Value("ERR-INVALID-TOKEN")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   908
      val invalid_usage = Value("ERR-INVALID-USAGE")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   909
      val invalid_user = Value("ERR-INVALID-USER")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   910
      val need_diff = Value("ERR-NEED-DIFF")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   911
      val need_file = Value("ERR-NEED-FILE")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   912
      val no_certificate = Value("ERR-NO-CERTIFICATE")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   913
      val no_content = Value("ERR-NO-CONTENT")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   914
      val no_effect = Value("ERR-NO-EFFECT")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   915
      val no_paste = Value("ERR-NO-PASTE")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   916
      val not_found = Value("ERR-NOT-FOUND")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   917
      val not_pusher = Value("ERR-NOT-PUSHER")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   918
      val oauth_access = Value("ERR-OAUTH-ACCESS")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   919
      val permissions = Value("ERR-PERMISSIONS")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   920
      val rate_limit = Value("ERR-RATE-LIMIT")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   921
      val unknown_client = Value("ERR-UNKNOWN-CLIENT")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   922
      val unknown_repository = Value("ERR-UNKNOWN-REPOSITORY")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   923
      val unknown_type = Value("ERR-UNKNOWN-TYPE")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   924
      val unknown_vcs_type = Value("ERR-UNKNOWN-VCS-TYPE")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   925
      val unsupported_vcs = Value("ERR-UNSUPPORTED-VCS")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   926
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   927
      val unknown_error = Value("ERR-UNKNOWN-ERROR")
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   928
    }
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   929
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   930
    sealed case class Result(
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   931
      result: JSON.T,
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   932
      error_code: Option[Error_Code.Value],
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   933
      error_info: String)
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   934
    {
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   935
      def ok: Boolean = error_code.isEmpty && error_info.isEmpty
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   936
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   937
      def get: JSON.T =
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   938
        if (error_info.nonEmpty) error(error_info)
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   939
        else if (error_code.nonEmpty) error(error_code.get.toString)
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   940
        else result
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   941
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   942
      def get_value[A](unapply: JSON.T => Option[A]): A =
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   943
        unapply(get) getOrElse error("Bad JSON result: " + JSON.Format(result))
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   944
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   945
      def get_string: String = get_value(JSON.Value.String.unapply)
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   946
    }
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   947
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   948
    def make_error_code(str: String): Error_Code.Value =
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   949
      try { Error_Code.withName(str) }
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   950
      catch { case _: java.util.NoSuchElementException => Error_Code.unknown_error }
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   951
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   952
    def make_result(json: JSON.T): Result =
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   953
      Result(
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   954
        JSON.value(json, "result").getOrElse(JSON.Object.empty),
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   955
        JSON.string(json, "error_code").map(make_error_code),
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   956
        JSON.string(json, "error_info").getOrElse(""))
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   957
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   958
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   959
    /* repository operations */
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   960
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   961
    object VCS extends Enumeration
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   962
    {
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   963
      val hg, git, svn = Value
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   964
    }
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   965
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   966
    def edit(typ: String, value: JSON.T): JSON.Object.T =
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   967
      JSON.Object("type" -> typ, "value" -> value)
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   968
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   969
    def edits(typ: String, value: Option[JSON.T]): List[JSON.Object.T] =
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   970
      List(edit(typ, value))
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   971
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   972
    def opt_edits(typ: String, value: Option[JSON.T]): List[JSON.Object.T] =
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   973
      value.map(edit(typ, _)).toList
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   974
  }
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   975
}