src/Pure/Tools/phabricator.scala
author wenzelm
Wed, 13 Nov 2019 17:33:59 +0100
changeset 71109 8c1c717a830b
parent 71103 c073c4e79518
child 71111 cd166c3904dd
permissions -rw-r--r--
configure SSH hosting via "isabelle phabricator_setup_ssh"; tuned message;
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] =
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    24
    Build_Docker.packages :::
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
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    30
      "php-zip", "python-pygments", "ssh")
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    31
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    32
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    33
  /* global system resources */
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    34
71068
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
    35
  val www_user = "www-data"
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
    36
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    37
  val daemon_user = "phabricator"
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    38
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
    39
  val sshd_config = Path.explode("/etc/ssh/sshd_config")
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    40
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    41
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    42
  /* installation parameters */
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
    43
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    44
  val default_name = "vcs"
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    45
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
    46
  def phabricator_name(name: String = "", ext: String = ""): String =
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
    47
    "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
    48
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
    49
  def isabelle_phabricator_name(name: String = "", ext: String = ""): String =
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
    50
    "isabelle-" + phabricator_name(name = name, ext = ext)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    51
71068
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
    52
  def default_root(name: String): Path =
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
    53
    Path.explode("/var/www") + Path.basic(phabricator_name(name = name))
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    54
71068
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
    55
  def default_repo(name: String): Path = default_root(name) + Path.basic("repo")
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    56
71072
wenzelm
parents: 71071
diff changeset
    57
  val default_mailers: Path = Path.explode("mailers.json")
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
    58
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
    59
  val default_system_port = 22
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
    60
  val alternative_system_port = 222
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
    61
  val default_server_port = 2222
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
    62
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    63
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    64
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    65
  /** global configuration **/
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    66
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
    67
  val global_config = Path.explode("/etc/" + isabelle_phabricator_name(ext = "conf"))
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    68
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    69
  sealed case class Config(name: String, root: Path)
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
    70
  {
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
    71
    def home: Path = root + Path.explode(phabricator_name())
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
    72
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
    73
    def execute(command: String): Process_Result =
71102
wenzelm
parents: 71101
diff changeset
    74
      Isabelle_System.bash("bin/" + command, cwd = home.file, redirect = true).check
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
    75
  }
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    76
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    77
  def read_config(): List[Config] =
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    78
  {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    79
    if (global_config.is_file) {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    80
      for (entry <- Library.trim_split_lines(File.read(global_config)) if entry.nonEmpty)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    81
      yield {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    82
        space_explode(':', entry) match {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    83
          case List(name, root) => Config(name, Path.explode(root))
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    84
          case _ => error("Malformed config file " + global_config + "\nentry " + quote(entry))
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    85
        }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    86
      }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    87
    }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    88
    else Nil
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    89
  }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    90
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    91
  def write_config(configs: List[Config])
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    92
  {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    93
    File.write(global_config,
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    94
      configs.map(config => config.name + ":" + config.root.implode).mkString("", "\n", "\n"))
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    95
  }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    96
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    97
  def get_config(name: String): Config =
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    98
    read_config().find(config => config.name == name) getOrElse
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    99
      error("Bad Isabelle/Phabricator installation " + quote(name))
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   100
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   101
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   102
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   103
  /** command-line tools **/
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   104
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   105
  /* Isabelle tool wrapper */
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   106
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   107
  val isabelle_tool1 =
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   108
    Isabelle_Tool("phabricator", "invoke command-line tool within Phabricator home directory", args =>
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   109
    {
71101
67c2fed5b0e9 more options;
wenzelm
parents: 71098
diff changeset
   110
      var list = false
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   111
      var name = default_name
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   112
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   113
      val getopts =
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   114
        Getopts("""
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   115
Usage: isabelle phabricator [OPTIONS] COMMAND [ARGS...]
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   116
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   117
  Options are:
71101
67c2fed5b0e9 more options;
wenzelm
parents: 71098
diff changeset
   118
    -l           list available Phabricator installations
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   119
    -n NAME      Phabricator installation name (default: """ + quote(default_name) + """)
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   120
71103
c073c4e79518 more documentation;
wenzelm
parents: 71102
diff changeset
   121
  Invoke a command-line tool within the home directory of the named
c073c4e79518 more documentation;
wenzelm
parents: 71102
diff changeset
   122
  Phabricator installation.
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   123
""",
71101
67c2fed5b0e9 more options;
wenzelm
parents: 71098
diff changeset
   124
          "l" -> (_ => list = true),
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   125
          "n:" -> (arg => name = arg))
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   126
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   127
      val more_args = getopts(args)
71101
67c2fed5b0e9 more options;
wenzelm
parents: 71098
diff changeset
   128
      if (more_args.isEmpty && !list) getopts.usage()
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   129
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   130
      val progress = new Console_Progress
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   131
71101
67c2fed5b0e9 more options;
wenzelm
parents: 71098
diff changeset
   132
      if (list) {
67c2fed5b0e9 more options;
wenzelm
parents: 71098
diff changeset
   133
        for (config <- read_config()) {
71103
c073c4e79518 more documentation;
wenzelm
parents: 71102
diff changeset
   134
          progress.echo("phabricator " + quote(config.name) + " root " + config.root)
71101
67c2fed5b0e9 more options;
wenzelm
parents: 71098
diff changeset
   135
        }
67c2fed5b0e9 more options;
wenzelm
parents: 71098
diff changeset
   136
      }
67c2fed5b0e9 more options;
wenzelm
parents: 71098
diff changeset
   137
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   138
      val config = get_config(name)
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   139
71098
da378866f580 tuned message;
wenzelm
parents: 71097
diff changeset
   140
      val result = progress.bash(Bash.strings(more_args), cwd = config.home.file, echo = true)
da378866f580 tuned message;
wenzelm
parents: 71097
diff changeset
   141
      if (!result.ok) error("Return code: " + result.rc.toString)
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   142
    })
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   143
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   144
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   145
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   146
  /** setup **/
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   147
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   148
  def user_setup(name: String, description: String, ssh_setup: Boolean = false)
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   149
  {
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   150
    if (!Linux.user_exists(name)) {
71054
b64fc38327ae prefer system user setup, e.g. avoid occurrence on login screen;
wenzelm
parents: 71053
diff changeset
   151
      Linux.user_add(name, description = description, system = true, ssh_setup = ssh_setup)
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   152
    }
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   153
    else if (Linux.user_description(name) != description) {
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   154
      error("User " + quote(name) + " already exists --" +
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   155
        " for Phabricator it should have the description:\n  " + quote(description))
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   156
    }
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   157
  }
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   158
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   159
  def phabricator_setup(
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   160
    name: String = default_name,
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   161
    root: String = "",
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   162
    repo: String = "",
71047
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   163
    package_update: Boolean = false,
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   164
    progress: Progress = No_Progress)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   165
  {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   166
    /* system environment */
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   167
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   168
    Linux.check_system_root()
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   169
71079
e06852132c1d tuned messages;
wenzelm
parents: 71078
diff changeset
   170
    progress.echo("System packages ...")
e06852132c1d tuned messages;
wenzelm
parents: 71078
diff changeset
   171
71047
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   172
    if (package_update) {
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   173
      Linux.package_update(progress = progress)
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   174
      Linux.check_reboot_required()
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   175
    }
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   176
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   177
    Linux.package_install(packages, progress = progress)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   178
    Linux.check_reboot_required()
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   179
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   180
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   181
    /* users */
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   182
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   183
    if (name == daemon_user) {
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   184
      error("Clash of installation name with daemon user " + quote(daemon_user))
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   185
    }
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   186
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   187
    user_setup(daemon_user, "Phabricator Daemon User", ssh_setup = true)
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   188
    user_setup(name, "Phabricator SSH User")
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   189
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   190
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   191
    /* basic installation */
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   192
71079
e06852132c1d tuned messages;
wenzelm
parents: 71078
diff changeset
   193
    progress.echo("\nPhabricator installation ...")
71076
8ac137c65776 tuned messages;
wenzelm
parents: 71075
diff changeset
   194
71068
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
   195
    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
   196
    val repo_path = if (repo.nonEmpty) Path.explode(repo) else default_repo(name)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   197
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   198
    val configs = read_config()
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   199
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   200
    for (config <- configs if config.name == name) {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   201
      error("Duplicate Phabricator installation " + quote(name) + " in " + config.root)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   202
    }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   203
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   204
    if (!Isabelle_System.bash("mkdir -p " + File.bash_path(root_path)).ok) {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   205
      error("Failed to create root directory " + root_path)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   206
    }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   207
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   208
    progress.bash(cwd = root_path.file, echo = true,
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   209
      script = """
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   210
        set -e
71050
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   211
        chown """ + Bash.string(www_user) + ":" + Bash.string(www_user) + """ .
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   212
        chmod 755 .
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   213
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   214
        git clone https://github.com/phacility/libphutil.git
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   215
        git clone https://github.com/phacility/arcanist.git
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   216
        git clone https://github.com/phacility/phabricator.git
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   217
      """).check
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   218
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   219
    val config = Config(name, root_path)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   220
    write_config(configs ::: List(config))
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   221
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   222
    config.execute("config set pygments.enabled true")
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   223
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   224
71050
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   225
    /* local repository directory */
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   226
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   227
    progress.echo("\nRepository hosting setup ...")
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   228
71050
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   229
    if (!Isabelle_System.bash("mkdir -p " + File.bash_path(repo_path)).ok) {
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   230
      error("Failed to create local repository directory " + repo_path)
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   231
    }
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   232
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   233
    Isabelle_System.bash(cwd = repo_path.file,
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   234
      script = """
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   235
        set -e
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   236
        chown -R """ + Bash.string(daemon_user) + ":" + Bash.string(daemon_user) + """ .
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   237
        chmod 755 .
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   238
      """).check
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   239
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   240
    config.execute("config set repository.default-local-path " + File.bash_path(repo_path))
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   241
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   242
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   243
    val sudoers_file = Path.explode("/etc/sudoers.d") + Path.basic(isabelle_phabricator_name())
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   244
    File.write(sudoers_file,
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   245
      www_user + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/bin/hg, /usr/bin/ssh, /usr/bin/id\n" +
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   246
      name + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/bin/git-upload-pack, /usr/bin/git-receive-pack, /usr/bin/hg, /usr/bin/svnserve, /usr/bin/ssh, /usr/bin/id\n")
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   247
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   248
    Isabelle_System.bash("chmod 0440 " + File.bash_path(sudoers_file)).check
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   249
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   250
    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
   251
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   252
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   253
    /* MySQL setup */
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   254
71079
e06852132c1d tuned messages;
wenzelm
parents: 71078
diff changeset
   255
    progress.echo("\nMySQL setup ...")
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   256
71055
27a998cdc0f4 back to plain name, to have it accepted my mysql;
wenzelm
parents: 71054
diff changeset
   257
    File.write(Path.explode("/etc/mysql/mysql.conf.d/" + phabricator_name(ext = "cnf")),
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   258
"""[mysqld]
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   259
max_allowed_packet = 32M
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   260
innodb_buffer_pool_size = 1600M
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   261
local_infile = 0
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   262
""")
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   263
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   264
    Linux.service_restart("mysql")
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   265
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   266
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   267
    def mysql_conf(R: Regex): Option[String] =
71068
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
   268
      split_lines(File.read(Path.explode("/etc/mysql/debian.cnf"))).collectFirst({ case R(a) => a })
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   269
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   270
    for (user <- mysql_conf("""^user\s*=\s*(\S*)\s*$""".r)) {
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   271
      config.execute("config set mysql.user " + Bash.string(user))
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   272
    }
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   273
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   274
    for (pass <- mysql_conf("""^password\s*=\s*(\S*)\s*$""".r)) {
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   275
      config.execute("config set mysql.pass " + Bash.string(pass))
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   276
    }
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   277
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   278
    config.execute("config set storage.default-namespace " +
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   279
      Bash.string(phabricator_name(name = name).replace("-", "_")))
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   280
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   281
    config.execute("config set storage.mysql-engine.max-size 8388608")
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   282
71102
wenzelm
parents: 71101
diff changeset
   283
    progress.bash("bin/storage upgrade --force", cwd = config.home.file, echo = true).check
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   284
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   285
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   286
    /* PHP setup */
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   287
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   288
    val php_version =
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   289
      Isabelle_System.bash("""php --run 'echo PHP_MAJOR_VERSION . "." . PHP_MINOR_VERSION;'""")
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   290
        .check.out
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   291
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   292
    val php_conf =
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   293
      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
   294
        Path.explode("apache2/conf.d") +
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   295
        Path.basic(isabelle_phabricator_name(ext = "ini"))
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   296
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   297
    File.write(php_conf,
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   298
      "post_max_size = 32M\n" +
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   299
      "opcache.validate_timestamps = 0\n" +
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   300
      "memory_limit = 512M\n")
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   301
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   302
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   303
    /* Apache setup */
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   304
71079
e06852132c1d tuned messages;
wenzelm
parents: 71078
diff changeset
   305
    progress.echo("Apache setup ...")
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   306
71068
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
   307
    val apache_root = Path.explode("/etc/apache2")
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   308
    val apache_sites = apache_root + Path.explode("sites-available")
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   309
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   310
    if (!apache_sites.is_dir) error("Bad Apache sites directory " + apache_sites)
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   311
71058
6ca9e8377613 proper names for multiple installations;
wenzelm
parents: 71057
diff changeset
   312
    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
   313
    val server_url = "http://" + server_name
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   314
71058
6ca9e8377613 proper names for multiple installations;
wenzelm
parents: 71057
diff changeset
   315
    File.write(apache_sites + Path.basic(isabelle_phabricator_name(name = name, ext = "conf")),
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   316
"""<VirtualHost *:80>
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   317
    ServerName """ + server_name + """
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   318
    ServerAdmin webmaster@localhost
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   319
    DocumentRoot """ + config.home.implode + """/webroot
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   320
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   321
    ErrorLog ${APACHE_LOG_DIR}/error.log
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   322
    RewriteEngine on
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   323
    RewriteRule ^(.*)$  /index.php?__path__=$1  [B,L,QSA]
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   324
</VirtualHost>
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   325
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   326
# vim: syntax=apache ts=4 sw=4 sts=4 sr noet
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   327
""")
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   328
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   329
    Isabelle_System.bash( """
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   330
      set -e
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   331
      a2enmod rewrite
71058
6ca9e8377613 proper names for multiple installations;
wenzelm
parents: 71057
diff changeset
   332
      a2ensite """ + Bash.string(isabelle_phabricator_name(name = name))).check
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   333
71057
2965304143d8 more phabricator setup;
wenzelm
parents: 71056
diff changeset
   334
    config.execute("config set phabricator.base-uri " + Bash.string(server_url))
2965304143d8 more phabricator setup;
wenzelm
parents: 71056
diff changeset
   335
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   336
    Linux.service_restart("apache2")
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   337
71053
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   338
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   339
    /* PHP daemon */
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   340
71079
e06852132c1d tuned messages;
wenzelm
parents: 71078
diff changeset
   341
    progress.echo("PHP daemon setup ...")
71053
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   342
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   343
    config.execute("config set phd.user " + Bash.string(daemon_user))
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   344
71056
ee3c43eb79ae proper service name (again): it is specific to each installation;
wenzelm
parents: 71055
diff changeset
   345
    Linux.service_install(isabelle_phabricator_name(name = name),
71053
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   346
"""[Unit]
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   347
Description=PHP daemon for Isabelle/Phabricator """ + quote(name) + """
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   348
After=syslog.target network.target apache2.service mysql.service
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   349
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   350
[Service]
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   351
Type=oneshot
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   352
User=""" + daemon_user + """
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   353
Group=""" + daemon_user + """
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   354
Environment=PATH=/sbin:/usr/sbin:/usr/local/sbin:/usr/local/bin:/usr/bin:/bin
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   355
ExecStart=""" + config.home.implode + """/bin/phd start
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   356
ExecStop=""" + config.home.implode + """/bin/phd stop
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   357
RemainAfterExit=yes
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   358
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   359
[Install]
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   360
WantedBy=multi-user.target
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   361
""")
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   362
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   363
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   364
    progress.echo("\nDONE\nWeb configuration via " + server_url)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   365
  }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   366
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   367
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   368
  /* Isabelle tool wrapper */
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   369
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   370
  val isabelle_tool2 =
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   371
    Isabelle_Tool("phabricator_setup", "setup Phabricator server on Ubuntu Linux", args =>
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   372
    {
71047
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   373
      var repo = ""
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   374
      var package_update = false
71078
5bb2235d843d clarified command-line;
wenzelm
parents: 71077
diff changeset
   375
      var name = default_name
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   376
      var root = ""
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   377
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   378
      val getopts =
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   379
        Getopts("""
71078
5bb2235d843d clarified command-line;
wenzelm
parents: 71077
diff changeset
   380
Usage: isabelle phabricator_setup [OPTIONS]
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   381
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   382
  Options are:
71068
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
   383
    -R DIR       repository directory (default: """ + default_repo("NAME") + """)
71047
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   384
    -U           full update of system packages before installation
71078
5bb2235d843d clarified command-line;
wenzelm
parents: 71077
diff changeset
   385
    -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
   386
    -r DIR       installation root directory (default: """ + default_root("NAME") + """)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   387
71103
c073c4e79518 more documentation;
wenzelm
parents: 71102
diff changeset
   388
  Install Phabricator as LAMP application (Linux, Apache, MySQL, PHP).
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   389
71078
5bb2235d843d clarified command-line;
wenzelm
parents: 71077
diff changeset
   390
  The installation name (default: """ + quote(default_name) + """) is mapped to a regular
5bb2235d843d clarified command-line;
wenzelm
parents: 71077
diff changeset
   391
  Unix user; this is relevant for public SSH access.
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   392
""",
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   393
          "R:" -> (arg => repo = arg),
71047
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   394
          "U" -> (_ => package_update = true),
71078
5bb2235d843d clarified command-line;
wenzelm
parents: 71077
diff changeset
   395
          "n:" -> (arg => name = arg),
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   396
          "r:" -> (arg => root = arg))
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   397
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   398
      val more_args = getopts(args)
71078
5bb2235d843d clarified command-line;
wenzelm
parents: 71077
diff changeset
   399
      if (more_args.nonEmpty) getopts.usage()
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   400
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   401
      val progress = new Console_Progress
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   402
71078
5bb2235d843d clarified command-line;
wenzelm
parents: 71077
diff changeset
   403
      phabricator_setup(name = name, root = root, repo = repo,
71047
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   404
        package_update = package_update, progress = progress)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   405
    })
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   406
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   407
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   408
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   409
  /** setup mail **/
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   410
71072
wenzelm
parents: 71071
diff changeset
   411
  val mailers_template: String =
wenzelm
parents: 71071
diff changeset
   412
"""[
wenzelm
parents: 71071
diff changeset
   413
  {
wenzelm
parents: 71071
diff changeset
   414
    "key": "example.org",
wenzelm
parents: 71071
diff changeset
   415
    "type": "smtp",
wenzelm
parents: 71071
diff changeset
   416
    "options": {
wenzelm
parents: 71071
diff changeset
   417
      "host": "mail.example.org",
wenzelm
parents: 71071
diff changeset
   418
      "port": 465,
wenzelm
parents: 71071
diff changeset
   419
      "user": "phabricator@example.org",
wenzelm
parents: 71071
diff changeset
   420
      "password": "********",
wenzelm
parents: 71071
diff changeset
   421
      "protocol": "ssl",
wenzelm
parents: 71071
diff changeset
   422
      "message-id": true
wenzelm
parents: 71071
diff changeset
   423
    }
wenzelm
parents: 71071
diff changeset
   424
  }
wenzelm
parents: 71071
diff changeset
   425
]"""
wenzelm
parents: 71071
diff changeset
   426
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   427
  def phabricator_setup_mail(
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   428
    name: String = default_name,
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   429
    config_file: Option[Path] = None,
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   430
    test_user: String = "",
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   431
    progress: Progress = No_Progress)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   432
  {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   433
    Linux.check_system_root()
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   434
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   435
    val config = get_config(name)
71073
d61fd7aade69 clarified directory;
wenzelm
parents: 71072
diff changeset
   436
    val default_config_file = config.root + default_mailers
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   437
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   438
    val mail_config = config_file getOrElse default_config_file
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   439
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   440
    def setup_mail
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   441
    {
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   442
      progress.echo("Using mail configuration from " + mail_config)
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   443
      config.execute("config set cluster.mailers --stdin < " + File.bash_path(mail_config))
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   444
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   445
      if (test_user.nonEmpty) {
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   446
        progress.echo("Sending test mail to " + quote(test_user))
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   447
        progress.bash(cwd = config.home.file, echo = true,
71102
wenzelm
parents: 71101
diff changeset
   448
          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
   449
            Bash.string(test_user)).check
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   450
      }
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   451
    }
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   452
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   453
    if (config_file.isEmpty) {
71070
79b89278b825 clarified permissions;
wenzelm
parents: 71068
diff changeset
   454
      if (!default_config_file.is_file) {
79b89278b825 clarified permissions;
wenzelm
parents: 71068
diff changeset
   455
        File.write(default_config_file, mailers_template)
79b89278b825 clarified permissions;
wenzelm
parents: 71068
diff changeset
   456
        Isabelle_System.bash("chmod 600 " + File.bash_path(default_config_file)).check
79b89278b825 clarified permissions;
wenzelm
parents: 71068
diff changeset
   457
      }
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   458
      if (File.read(default_config_file) == mailers_template) {
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   459
        progress.echo(
71077
41b6ca223500 tuned messages;
wenzelm
parents: 71076
diff changeset
   460
"""
41b6ca223500 tuned messages;
wenzelm
parents: 71076
diff changeset
   461
Please invoke the tool again, after providing details in
41b6ca223500 tuned messages;
wenzelm
parents: 71076
diff changeset
   462
  """ + default_config_file.implode + """
41b6ca223500 tuned messages;
wenzelm
parents: 71076
diff changeset
   463
41b6ca223500 tuned messages;
wenzelm
parents: 71076
diff changeset
   464
See also section "Mailer: SMTP" in
41b6ca223500 tuned messages;
wenzelm
parents: 71076
diff changeset
   465
  https://secure.phabricator.com/book/phabricator/article/configuring_outbound_email
41b6ca223500 tuned messages;
wenzelm
parents: 71076
diff changeset
   466
""")
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   467
      }
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   468
      else setup_mail
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   469
    }
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   470
    else setup_mail
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   471
  }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   472
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   473
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   474
  /* Isabelle tool wrapper */
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   475
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   476
  val isabelle_tool3 =
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   477
    Isabelle_Tool("phabricator_setup_mail",
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   478
      "setup mail for one Phabricator installation", args =>
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   479
    {
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   480
      var test_user = ""
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   481
      var name = default_name
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   482
      var config_file: Option[Path] = None
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   483
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   484
      val getopts =
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   485
        Getopts("""
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   486
Usage: isabelle phabricator_setup_mail [OPTIONS]
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   487
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   488
  Options are:
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   489
    -T USER      send test mail to Phabricator user
71103
c073c4e79518 more documentation;
wenzelm
parents: 71102
diff changeset
   490
    -f FILE      config file (default: """ + default_mailers + """ within Phabricator root)
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   491
    -n NAME      Phabricator installation name (default: """ + quote(default_name) + """)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   492
71077
41b6ca223500 tuned messages;
wenzelm
parents: 71076
diff changeset
   493
  Provide mail configuration for existing Phabricator installation.
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   494
""",
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   495
          "T:" -> (arg => test_user = arg),
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   496
          "f:" -> (arg => config_file = Some(Path.explode(arg))),
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   497
          "n:" -> (arg => name = arg))
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   498
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   499
      val more_args = getopts(args)
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   500
      if (more_args.nonEmpty) getopts.usage()
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   501
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   502
      val progress = new Console_Progress
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   503
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   504
      phabricator_setup_mail(name = name, config_file = config_file,
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   505
        test_user = test_user, progress = progress)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   506
    })
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   507
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   508
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   509
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   510
  /** setup ssh **/
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   511
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   512
  /* sshd config */
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   513
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   514
  private val Port = """^\s*Port\s+(\d+)\s*$""".r
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   515
  private val No_Port = """^#\s*Port\b.*$""".r
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   516
  private val Any_Port = """^#?\s*Port\b.*$""".r
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   517
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   518
  def conf_ssh_port(port: Int): String =
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   519
    if (port == 22) "#Port 22" else "Port " + port
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   520
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   521
  def read_ssh_port(conf: Path): Int =
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   522
  {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   523
    val lines = split_lines(File.read(conf))
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   524
    val ports =
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   525
      lines.flatMap({
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   526
        case Port(Value.Int(p)) => Some(p)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   527
        case No_Port() => Some(22)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   528
        case _ => None
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   529
      })
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   530
    ports match {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   531
      case List(port) => port
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   532
      case Nil => error("Missing Port specification in " + conf)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   533
      case _ => error("Multiple Port specifications in " + conf)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   534
    }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   535
  }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   536
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   537
  def write_ssh_port(conf: Path, port: Int): Boolean =
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   538
  {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   539
    val old_port = read_ssh_port(conf)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   540
    if (old_port == port) false
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   541
    else {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   542
      val lines = split_lines(File.read(conf))
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   543
      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
   544
      File.write(conf, cat_lines(lines1))
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   545
      true
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   546
    }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   547
  }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   548
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   549
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   550
  /* phabricator_setup_ssh */
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   551
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   552
  def phabricator_setup_ssh(
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   553
    server_port: Int = default_server_port,
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   554
    system_port: Int = default_system_port,
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   555
    test_server: Boolean = false,
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   556
    progress: Progress = No_Progress)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   557
  {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   558
    Linux.check_system_root()
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   559
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   560
    val configs = read_config()
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   561
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   562
    if (server_port == system_port) {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   563
      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
   564
    }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   565
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   566
    val sshd_conf_system = Path.explode("/etc/ssh/sshd_config")
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   567
    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
   568
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   569
    val ssh_name = isabelle_phabricator_name(name = "ssh")
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   570
    val ssh_command = Path.explode("/usr/local/bin") + Path.basic(ssh_name)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   571
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   572
    val old_system_port = read_ssh_port(sshd_conf_system)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   573
    if (old_system_port != system_port) {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   574
      progress.echo("Reconfigurig system ssh service")
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   575
      Linux.service_stop("ssh")
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   576
      write_ssh_port(sshd_conf_system, system_port)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   577
    }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   578
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   579
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   580
    progress.echo("Configuring " + ssh_name + " service")
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   581
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   582
    File.write(ssh_command,
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   583
"""#!/bin/bash
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   584
{
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   585
  while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   586
  do
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   587
    NAME="$(echo "$REPLY" | cut -d: -f1)"
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   588
    ROOT="$(echo "$REPLY" | cut -d: -f2)"
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   589
    if [ "$1" = "$NAME" ]
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   590
    then
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   591
      exec "$ROOT/phabricator/bin/ssh-auth" "$@"
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   592
    fi
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   593
  done
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   594
  exit 1
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   595
} < /etc/isabelle-phabricator.conf
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   596
""")
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   597
    Isabelle_System.bash("chmod 755 " + File.bash_path(ssh_command)).check
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   598
    Isabelle_System.bash("chown root:root " + File.bash_path(ssh_command)).check
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   599
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   600
    File.write(sshd_conf_server,
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   601
"""# OpenBSD Secure Shell server for Isabelle/Phabricator
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   602
AuthorizedKeysCommand """ + ssh_command.implode + """
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   603
AuthorizedKeysCommandUser """ + daemon_user + """
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   604
AuthorizedKeysFile none
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   605
AllowUsers """ + configs.map(_.name).mkString(" ") + """
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   606
Port """ + server_port + """
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   607
Protocol 2
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   608
PermitRootLogin no
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   609
AllowAgentForwarding no
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   610
AllowTcpForwarding no
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   611
PrintMotd no
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   612
PrintLastLog no
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   613
PasswordAuthentication no
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   614
ChallengeResponseAuthentication no
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   615
PidFile /var/run/""" + ssh_name + """.pid
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   616
""")
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   617
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   618
    Linux.service_install(ssh_name,
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   619
"""[Unit]
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   620
Description=OpenBSD Secure Shell server for Isabelle/Phabricator
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   621
After=network.target auditd.service
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   622
ConditionPathExists=!/etc/ssh/sshd_not_to_be_run
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   623
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   624
[Service]
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   625
EnvironmentFile=-/etc/default/ssh
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   626
ExecStartPre=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   627
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
   628
ExecReload=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   629
ExecReload=/bin/kill -HUP $MAINPID
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   630
KillMode=process
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   631
Restart=on-failure
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   632
RestartPreventExitStatus=255
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   633
Type=notify
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   634
RuntimeDirectory=sshd-phabricator
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   635
RuntimeDirectoryMode=0755
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   636
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   637
[Install]
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   638
WantedBy=multi-user.target
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   639
Alias=""" + ssh_name + """.service
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   640
""")
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   641
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   642
    for (config <- configs) {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   643
      progress.echo("phabricator " + quote(config.name) + " port " +  server_port)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   644
      config.execute("config set diffusion.ssh-port " + Bash.string(server_port.toString))
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   645
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   646
      if (test_server) {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   647
        progress.bash(
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   648
          """unset DISPLAY
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   649
          echo "{}" | ssh -p """ + Bash.string(server_port.toString) +
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   650
          " -o StrictHostKeyChecking=false " +
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   651
          Bash.string(config.name) + """@localhost conduit conduit.ping""").print
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   652
      }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   653
    }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   654
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   655
    if (old_system_port != system_port) {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   656
      progress.echo("Restarting system ssh service")
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   657
      Linux.service_start("ssh")
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   658
    }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   659
  }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   660
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
  /* Isabelle tool wrapper */
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
  val isabelle_tool4 =
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   665
    Isabelle_Tool("phabricator_setup_ssh",
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   666
      "setup ssh service for all Phabricator installations", args =>
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
      var server_port = default_server_port
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   669
      var system_port = default_system_port
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   670
      var test_server = false
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
      val getopts =
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   673
        Getopts("""
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   674
Usage: isabelle phabricator_setup_ssh [OPTIONS]
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   675
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   676
  Options are:
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   677
    -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
   678
    -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
   679
    -T           test the ssh service for each Phabricator installation
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   680
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   681
  Configure ssh service for all Phabricator installations: a separate sshd
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   682
  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
   683
  be distinct.
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   684
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   685
  A particular Phabricator installation is addressed by using its
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   686
  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
   687
  stored ssh keys.
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
          "p:" -> (arg => server_port = Value.Int.parse(arg)),
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   690
          "q:" -> (arg => system_port = Value.Int.parse(arg)),
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   691
          "T" -> (_ => test_server = true))
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 more_args = getopts(args)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   694
      if (more_args.nonEmpty) getopts.usage()
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   695
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   696
      val progress = new Console_Progress
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   697
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   698
      phabricator_setup_ssh(
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   699
        server_port = server_port, system_port = system_port, test_server = test_server,
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   700
        progress = progress)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   701
    })
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   702
}