src/Pure/Tools/phabricator.scala
author wenzelm
Sat, 04 Jan 2025 20:59:41 +0100
changeset 81719 6fbda9453c1b
parent 81717 114449035ec6
child 81720 12ecf11f8eab
permissions -rw-r--r--
some support for Ubuntu 24.04;
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
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
     4
Support for Phorge / Phabricator server, notably for Ubuntu 20.04 or 22.04 LTS.
71068
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:
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
     7
  - https://phorge.it
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
     8
  - https://we.phorge.it/book/phorge
70967
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
71330
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
    14
import scala.collection.mutable
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
    15
import scala.util.matching.Regex
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
    16
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
    17
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
    18
object Phabricator {
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    19
  /** defaults **/
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
    20
79520
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    21
  /* system packages */
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    22
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    23
  val packages_ubuntu_20_04: List[String] =
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    24
    Docker_Build.packages :::
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    25
    List(
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    26
      // https://secure.phabricator.com/source/phabricator/browse/master/scripts/install/install_ubuntu.sh 15e6e2adea61
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    27
      "git", "mysql-server", "php", "php-mysql", "php-gd", "php-curl", "php-apcu", "php-cli",
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    28
      "php-json", "php-mbstring",
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    29
      // more packages
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    30
      "php-xml", "php-zip", "python3-pygments", "ssh", "subversion", "python-pygments",
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    31
      // mercurial build packages
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    32
      "make", "gcc", "python", "python2-dev", "python-docutils", "python-openssl")
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    33
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    34
  val packages_ubuntu_22_04: List[String] =
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    35
    Docker_Build.packages :::
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    36
    List(
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    37
      // https://secure.phabricator.com/source/phabricator/browse/master/scripts/install/install_ubuntu.sh 15e6e2adea61
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    38
      "git", "mysql-server", "php", "php-mysql", "php-gd", "php-curl", "php-apcu", "php-cli",
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    39
      "php-json", "php-mbstring",
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    40
      // more packages
79521
db2b5c04075d proper packages for mercurial_setup on Ubuntu 22.04: building from source provides hgweb modules, and also provides a defined version (6.1.1 is also provided by Ubuntu 22.04);
wenzelm
parents: 79520
diff changeset
    41
      "php-xml", "php-zip", "python3-pygments", "ssh", "subversion",
db2b5c04075d proper packages for mercurial_setup on Ubuntu 22.04: building from source provides hgweb modules, and also provides a defined version (6.1.1 is also provided by Ubuntu 22.04);
wenzelm
parents: 79520
diff changeset
    42
      // mercurial build packages
db2b5c04075d proper packages for mercurial_setup on Ubuntu 22.04: building from source provides hgweb modules, and also provides a defined version (6.1.1 is also provided by Ubuntu 22.04);
wenzelm
parents: 79520
diff changeset
    43
      "make", "gcc", "python3", "python3-dev", "python3-docutils")
79520
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    44
81719
6fbda9453c1b some support for Ubuntu 24.04;
wenzelm
parents: 81717
diff changeset
    45
  val packages_ubuntu_24_04: List[String] =
6fbda9453c1b some support for Ubuntu 24.04;
wenzelm
parents: 81717
diff changeset
    46
    Docker_Build.packages :::
6fbda9453c1b some support for Ubuntu 24.04;
wenzelm
parents: 81717
diff changeset
    47
    List(
6fbda9453c1b some support for Ubuntu 24.04;
wenzelm
parents: 81717
diff changeset
    48
      // https://secure.phabricator.com/source/phabricator/browse/master/scripts/install/install_ubuntu.sh 15e6e2adea61
6fbda9453c1b some support for Ubuntu 24.04;
wenzelm
parents: 81717
diff changeset
    49
      "git", "mysql-server", "php", "php-mysql", "php-gd", "php-curl", "php-apcu", "php-cli",
6fbda9453c1b some support for Ubuntu 24.04;
wenzelm
parents: 81717
diff changeset
    50
      "php-json", "php-mbstring",
6fbda9453c1b some support for Ubuntu 24.04;
wenzelm
parents: 81717
diff changeset
    51
      // more packages
6fbda9453c1b some support for Ubuntu 24.04;
wenzelm
parents: 81717
diff changeset
    52
      "php-xml", "php-zip", "python3-pygments", "ssh", "subversion",
6fbda9453c1b some support for Ubuntu 24.04;
wenzelm
parents: 81717
diff changeset
    53
      // mercurial build packages
6fbda9453c1b some support for Ubuntu 24.04;
wenzelm
parents: 81717
diff changeset
    54
      "make", "gcc", "gettext", "python3", "python3-dev", "python3-docutils", "python3-setuptools")
6fbda9453c1b some support for Ubuntu 24.04;
wenzelm
parents: 81717
diff changeset
    55
79520
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    56
  def packages(webserver: Webserver): List[String] = {
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    57
    val release = Linux.Release()
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    58
    val pkgs =
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    59
      if (release.is_ubuntu_20_04) packages_ubuntu_20_04
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    60
      else if (release.is_ubuntu_22_04) packages_ubuntu_22_04
81719
6fbda9453c1b some support for Ubuntu 24.04;
wenzelm
parents: 81717
diff changeset
    61
      else if (release.is_ubuntu_24_04) packages_ubuntu_24_04
6fbda9453c1b some support for Ubuntu 24.04;
wenzelm
parents: 81717
diff changeset
    62
      else error("Bad Linux version: expected Ubuntu 20.04 or 22.04 or 24.04 LTS")
79520
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    63
    pkgs ::: webserver.packages()
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    64
  }
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    65
627bb49a1111 tuned source structure;
wenzelm
parents: 79519
diff changeset
    66
79512
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
    67
  /* webservers */
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
    68
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
    69
  sealed abstract class Webserver {
79523
f1287f1894a0 clarified webserver names;
wenzelm
parents: 79522
diff changeset
    70
    override def toString: String = user_name
f1287f1894a0 clarified webserver names;
wenzelm
parents: 79522
diff changeset
    71
    def user_name: String
f1287f1894a0 clarified webserver names;
wenzelm
parents: 79522
diff changeset
    72
    def system_name: String
79522
08ef19aacced proper Apache.php_name;
wenzelm
parents: 79521
diff changeset
    73
    def php_name: String = system_name
79512
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
    74
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
    75
    def packages(): List[String]
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
    76
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
    77
    def system_path: Path = Path.basic(system_name)
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
    78
    def root_dir: Path = Path.explode("/etc") + system_path
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
    79
    def sites_dir: Path = root_dir + Path.explode("sites-available")
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
    80
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
    81
    def restart(): Unit = Linux.service_restart(system_name)
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
    82
79513
292605271dcf proper php-fpm configuration for nginx;
wenzelm
parents: 79512
diff changeset
    83
    def php_init(): Unit =
79515
fa581264522e clarified modules;
wenzelm
parents: 79513
diff changeset
    84
      File.write(Linux.php_conf_dir(php_name) + Path.basic(isabelle_phabricator_name(ext = "ini")),
79513
292605271dcf proper php-fpm configuration for nginx;
wenzelm
parents: 79512
diff changeset
    85
        "post_max_size = 32M\n" +
292605271dcf proper php-fpm configuration for nginx;
wenzelm
parents: 79512
diff changeset
    86
        "opcache.validate_timestamps = 0\n" +
292605271dcf proper php-fpm configuration for nginx;
wenzelm
parents: 79512
diff changeset
    87
        "memory_limit = 512M\n" +
292605271dcf proper php-fpm configuration for nginx;
wenzelm
parents: 79512
diff changeset
    88
        "max_execution_time = 120\n")
79512
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
    89
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
    90
    def site_name(name: String): String = isabelle_phabricator_name(name = name)
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
    91
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
    92
    def site_conf(name: String): Path =
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
    93
      sites_dir + Path.basic(isabelle_phabricator_name(name = name, ext = "conf"))
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
    94
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
    95
    def site_init(name: String, server_name: String, webroot: String): Unit
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
    96
  }
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
    97
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
    98
  object Apache extends Webserver {
79523
f1287f1894a0 clarified webserver names;
wenzelm
parents: 79522
diff changeset
    99
    override val user_name = "Apache"
79512
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   100
    override def system_name = "apache2"
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   101
    override def packages(): List[String] = List("apache2", "libapache2-mod-php")
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   102
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   103
    override def site_init(name: String, server_name: String, webroot: String): Unit = {
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   104
      File.write(site_conf(name),
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   105
"""<VirtualHost *:80>
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   106
    ServerName """ + server_name + """
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   107
    ServerAdmin webmaster@localhost
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   108
    DocumentRoot """ + webroot + """
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   109
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   110
    ErrorLog ${APACHE_LOG_DIR}/error.log
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   111
    CustomLog ${APACHE_LOG_DIR}/access.log combined
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   112
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   113
    RewriteEngine on
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   114
    RewriteRule ^(.*)$  /index.php?__path__=$1  [B,L,QSA]
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   115
</VirtualHost>
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   116
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   117
# vim: syntax=apache ts=4 sw=4 sts=4 sr noet
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   118
""")
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   119
      Isabelle_System.bash("""
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   120
        set -e
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   121
        a2enmod rewrite
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   122
        a2ensite """ + Bash.string(site_name(name))).check
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   123
    }
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   124
  }
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   125
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   126
  object Nginx extends Webserver {
79523
f1287f1894a0 clarified webserver names;
wenzelm
parents: 79522
diff changeset
   127
    override val user_name = "Nginx"
f1287f1894a0 clarified webserver names;
wenzelm
parents: 79522
diff changeset
   128
    override val system_name = "nginx"
79513
292605271dcf proper php-fpm configuration for nginx;
wenzelm
parents: 79512
diff changeset
   129
    override val php_name = "fpm"
79512
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   130
    override def packages(): List[String] = List("nginx", "php-fpm")
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   131
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   132
    override def site_init(name: String, server_name: String, webroot: String): Unit = {
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   133
      File.write(site_conf(name),
79517
0856026e2c88 tuned whitespace in generated file;
wenzelm
parents: 79516
diff changeset
   134
"""server {
79518
ad27859952cb more robust nginx configuration, notably for "certbot --nginx -d DOMAIN";
wenzelm
parents: 79517
diff changeset
   135
  listen 80;
ad27859952cb more robust nginx configuration, notably for "certbot --nginx -d DOMAIN";
wenzelm
parents: 79517
diff changeset
   136
  listen [::]:80;
ad27859952cb more robust nginx configuration, notably for "certbot --nginx -d DOMAIN";
wenzelm
parents: 79517
diff changeset
   137
79512
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   138
  server_name """ + server_name + """;
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   139
  root """ + webroot + """;
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   140
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   141
  location / {
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   142
    index index.php;
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   143
    rewrite ^/(.*)$ /index.php?__path__=/$1 last;
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   144
  }
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   145
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   146
  location ~ \.php$ {
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   147
    include snippets/fastcgi-php.conf;
79515
fa581264522e clarified modules;
wenzelm
parents: 79513
diff changeset
   148
    fastcgi_pass unix:/var/run/php/php""" + Linux.php_version() + """-fpm.sock;
79512
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   149
  }
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   150
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   151
  location /index.php {
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   152
    fastcgi_index  index.php;
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   153
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   154
    #required if PHP was built with --enable-force-cgi-redirect
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   155
    fastcgi_param  REDIRECT_STATUS    200;
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   156
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   157
    #variables to make the $_SERVER populate in PHP
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   158
    fastcgi_param  SCRIPT_FILENAME    $document_root$fastcgi_script_name;
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   159
    fastcgi_param  QUERY_STRING       $query_string;
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   160
    fastcgi_param  REQUEST_METHOD     $request_method;
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   161
    fastcgi_param  CONTENT_TYPE       $content_type;
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   162
    fastcgi_param  CONTENT_LENGTH     $content_length;
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   163
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   164
    fastcgi_param  SCRIPT_NAME        $fastcgi_script_name;
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   165
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   166
    fastcgi_param  GATEWAY_INTERFACE  CGI/1.1;
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   167
    fastcgi_param  SERVER_SOFTWARE    nginx/$nginx_version;
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   168
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   169
    fastcgi_param  REMOTE_ADDR        $remote_addr;
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   170
  }
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   171
}
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   172
""")
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   173
      Isabelle_System.bash(
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   174
        "ln -sf " + File.bash_path(site_conf(name)) + " /etc/nginx/sites-enabled/.").check
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   175
    }
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   176
  }
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   177
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   178
  val all_webservers: List[Webserver] = List(Apache, Nginx)
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   179
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   180
  def get_webserver(name: String): Webserver =
79523
f1287f1894a0 clarified webserver names;
wenzelm
parents: 79522
diff changeset
   181
    all_webservers.find(w => w.user_name == name) getOrElse
79512
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   182
      error("Bad webserver " + quote(name))
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   183
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   184
  val default_webserver: Webserver = Apache
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   185
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   186
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   187
  /* global system resources */
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   188
71068
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
   189
  val www_user = "www-data"
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
   190
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   191
  val daemon_user = "phabricator"
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   192
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71550
diff changeset
   193
  val sshd_config: Path = Path.explode("/etc/ssh/sshd_config")
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   194
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   195
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   196
  /* installation parameters */
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   197
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   198
  val default_name = "vcs"
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   199
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   200
  def phabricator_name(name: String = "", ext: String = ""): String =
77368
wenzelm
parents: 76540
diff changeset
   201
    "phabricator" + if_proper(name, "-" + name) + if_proper(ext, "." + ext)
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   202
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   203
  def isabelle_phabricator_name(name: String = "", ext: String = ""): String =
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   204
    "isabelle-" + phabricator_name(name = name, ext = ext)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   205
71068
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
   206
  def default_root(name: String): Path =
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
   207
    Path.explode("/var/www") + Path.basic(phabricator_name(name = name))
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   208
71068
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
   209
  def default_repo(name: String): Path = default_root(name) + Path.basic("repo")
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   210
71072
wenzelm
parents: 71071
diff changeset
   211
  val default_mailers: Path = Path.explode("mailers.json")
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   212
76129
5979f73b9db1 clarified signature: separate unrelated modules;
wenzelm
parents: 76104
diff changeset
   213
  val default_system_port: Int = 22
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   214
  val alternative_system_port = 222
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   215
  val default_server_port = 2222
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   216
79524
a0174eeca5ce more robust: avoid crash on non-Linux systems;
wenzelm
parents: 79523
diff changeset
   217
  def standard_mercurial_source: String = {
79521
db2b5c04075d proper packages for mercurial_setup on Ubuntu 22.04: building from source provides hgweb modules, and also provides a defined version (6.1.1 is also provided by Ubuntu 22.04);
wenzelm
parents: 79520
diff changeset
   218
    val release = Linux.Release()
db2b5c04075d proper packages for mercurial_setup on Ubuntu 22.04: building from source provides hgweb modules, and also provides a defined version (6.1.1 is also provided by Ubuntu 22.04);
wenzelm
parents: 79520
diff changeset
   219
    if (release.is_ubuntu_20_04) "https://www.mercurial-scm.org/release/mercurial-3.9.2.tar.gz"
81719
6fbda9453c1b some support for Ubuntu 24.04;
wenzelm
parents: 81717
diff changeset
   220
    else if (release.is_ubuntu_22_04) "https://www.mercurial-scm.org/release/mercurial-6.1.4.tar.gz"
6fbda9453c1b some support for Ubuntu 24.04;
wenzelm
parents: 81717
diff changeset
   221
    else "https://www.mercurial-scm.org/release/mercurial-6.8.2.tar.gz"
79521
db2b5c04075d proper packages for mercurial_setup on Ubuntu 22.04: building from source provides hgweb modules, and also provides a defined version (6.1.1 is also provided by Ubuntu 22.04);
wenzelm
parents: 79520
diff changeset
   222
  }
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
   223
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   224
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   225
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   226
  /** global configuration **/
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   227
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71550
diff changeset
   228
  val global_config: Path = Path.explode("/etc/" + isabelle_phabricator_name(ext = "conf"))
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   229
71122
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
   230
  def global_config_script(
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
   231
    init: String = "",
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
   232
    body: String = "",
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   233
    exit: String = ""): String = {
71282
de59dd86760f tuned signature;
wenzelm
parents: 71281
diff changeset
   234
"""#!/bin/bash
77369
wenzelm
parents: 77368
diff changeset
   235
""" + if_proper(init, "\n" + init) + """
71284
49bc17bf4384 more robust: avoid accidental use of stdin;
wenzelm
parents: 71283
diff changeset
   236
{
71122
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
   237
  while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
   238
  do
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
   239
    NAME="$(echo "$REPLY" | cut -d: -f1)"
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
   240
    ROOT="$(echo "$REPLY" | cut -d: -f2)"
71284
49bc17bf4384 more robust: avoid accidental use of stdin;
wenzelm
parents: 71283
diff changeset
   241
    {
73736
a8ff6e4ee661 tuned signature;
wenzelm
parents: 73566
diff changeset
   242
""" + Library.indent_lines(6, body) + """
71284
49bc17bf4384 more robust: avoid accidental use of stdin;
wenzelm
parents: 71283
diff changeset
   243
    } < /dev/null
49bc17bf4384 more robust: avoid accidental use of stdin;
wenzelm
parents: 71283
diff changeset
   244
  done
49bc17bf4384 more robust: avoid accidental use of stdin;
wenzelm
parents: 71283
diff changeset
   245
} < """ + File.bash_path(global_config) + "\n" +
77369
wenzelm
parents: 77368
diff changeset
   246
    if_proper(exit, "\n" + exit + "\n")
71122
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
   247
  }
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
   248
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   249
  sealed case class Config(name: String, root: Path) {
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   250
    def home: Path = root + Path.explode(phabricator_name())
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   251
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   252
    def execute(command: String): Process_Result =
80224
db92e0b6a11a clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
wenzelm
parents: 79525
diff changeset
   253
      Isabelle_System.bash("bin/" + command, cwd = home, redirect = true).check
79512
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   254
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   255
    def webroot: String = home.implode + "/webroot"
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   256
  }
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   257
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   258
  def read_config(): List[Config] = {
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   259
    if (global_config.is_file) {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   260
      for (entry <- Library.trim_split_lines(File.read(global_config)) if entry.nonEmpty)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   261
      yield {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   262
        space_explode(':', entry) match {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   263
          case List(name, root) => Config(name, Path.explode(root))
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   264
          case _ => error("Malformed config file " + global_config + "\nentry " + quote(entry))
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   265
        }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   266
      }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   267
    }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   268
    else Nil
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   269
  }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   270
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   271
  def write_config(configs: List[Config]): Unit = {
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   272
    File.write(global_config,
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   273
      configs.map(config => config.name + ":" + config.root.implode).mkString("", "\n", "\n"))
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   274
  }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   275
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   276
  def get_config(name: String): Config =
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   277
    read_config().find(config => config.name == name) getOrElse
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   278
      error("Bad Isabelle/Phorge installation " + quote(name))
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   279
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   280
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   281
71299
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   282
  /** administrative tools **/
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   283
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   284
  /* Isabelle tool wrapper */
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   285
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   286
  val isabelle_tool1 =
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   287
    Isabelle_Tool("phabricator", "invoke command-line tool within Phorge home directory",
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   288
      Scala_Project.here,
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   289
      { args =>
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   290
        var list = false
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   291
        var name = default_name
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   292
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   293
        val getopts = Getopts("""
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   294
Usage: isabelle phabricator [OPTIONS] COMMAND [ARGS...]
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   295
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   296
  Options are:
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   297
    -l           list available Phorge installations
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   298
    -n NAME      Phorge installation name (default: """ + quote(default_name) + """)
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   299
71103
c073c4e79518 more documentation;
wenzelm
parents: 71102
diff changeset
   300
  Invoke a command-line tool within the home directory of the named
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   301
  Phorge installation.
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   302
""",
71101
67c2fed5b0e9 more options;
wenzelm
parents: 71098
diff changeset
   303
          "l" -> (_ => list = true),
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   304
          "n:" -> (arg => name = arg))
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   305
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   306
        val more_args = getopts(args)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   307
        if (more_args.isEmpty && !list) getopts.usage()
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   308
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   309
        val progress = new Console_Progress
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   310
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   311
        if (list) {
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   312
          for (config <- read_config()) {
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   313
            progress.echo("phabricator " + quote(config.name) + " root " + config.root)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   314
          }
71101
67c2fed5b0e9 more options;
wenzelm
parents: 71098
diff changeset
   315
        }
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   316
        else {
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   317
          val config = get_config(name)
80224
db92e0b6a11a clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
wenzelm
parents: 79525
diff changeset
   318
          val result = progress.bash(Bash.strings(more_args), cwd = config.home, echo = true)
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   319
          if (!result.ok) error(result.print_return_code)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   320
        }
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   321
      })
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   322
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   323
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   324
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   325
  /** setup **/
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   326
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   327
  def user_setup(name: String, description: String, ssh_setup: Boolean = false): Unit = {
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   328
    if (!Linux.user_exists(name)) {
71054
b64fc38327ae prefer system user setup, e.g. avoid occurrence on login screen;
wenzelm
parents: 71053
diff changeset
   329
      Linux.user_add(name, description = description, system = true, ssh_setup = ssh_setup)
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   330
    }
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   331
    else if (Linux.user_description(name) != description) {
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   332
      error("User " + quote(name) + " already exists --" +
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   333
        " for Phorge it should have the description:\n  " + quote(description))
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   334
    }
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   335
  }
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   336
71282
de59dd86760f tuned signature;
wenzelm
parents: 71281
diff changeset
   337
  def command_setup(name: String,
de59dd86760f tuned signature;
wenzelm
parents: 71281
diff changeset
   338
    init: String = "",
de59dd86760f tuned signature;
wenzelm
parents: 71281
diff changeset
   339
    body: String = "",
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   340
    exit: String = ""
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   341
  ): Path = {
71270
wenzelm
parents: 71269
diff changeset
   342
    val command = Path.explode("/usr/local/bin") + Path.basic(name)
71282
de59dd86760f tuned signature;
wenzelm
parents: 71281
diff changeset
   343
    File.write(command, global_config_script(init = init, body = body, exit = exit))
71270
wenzelm
parents: 71269
diff changeset
   344
    Isabelle_System.chmod("755", command)
wenzelm
parents: 71269
diff changeset
   345
    Isabelle_System.chown("root:root", command)
wenzelm
parents: 71269
diff changeset
   346
    command
wenzelm
parents: 71269
diff changeset
   347
  }
wenzelm
parents: 71269
diff changeset
   348
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   349
  def mercurial_setup(mercurial_source: String, progress: Progress = new Progress): Unit = {
71281
5b3a813853bb tuned message;
wenzelm
parents: 71280
diff changeset
   350
    progress.echo("\nMercurial installation from source " + quote(mercurial_source) + " ...")
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   351
    Isabelle_System.with_tmp_dir("mercurial") { tmp_dir =>
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
   352
      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
   353
        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
   354
          val archive = tmp_dir + Path.basic("mercurial.tar.gz")
73566
4e6b31ed7197 clarified signature: avoid tmp file;
wenzelm
parents: 73534
diff changeset
   355
          Isabelle_System.download_file(mercurial_source, archive)
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
   356
          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
   357
        }
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
   358
        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
   359
76540
83de6e9ae983 clarified signature: prefer Scala functions instead of shell scripts;
wenzelm
parents: 76529
diff changeset
   360
      Isabelle_System.extract(archive, tmp_dir)
76529
ded37aade88e clarified signature;
wenzelm
parents: 76173
diff changeset
   361
      val build_dir = File.get_dir(tmp_dir, title = 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
   362
80224
db92e0b6a11a clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
wenzelm
parents: 79525
diff changeset
   363
      progress.bash("make all && make install", cwd = build_dir, echo = true).check
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   364
    }
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
   365
  }
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
   366
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   367
  def phabricator_setup(
71422
5d5be87330b5 allow to override repository versions at runtime;
wenzelm
parents: 71421
diff changeset
   368
    options: Options,
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   369
    name: String = default_name,
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   370
    root: String = "",
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   371
    repo: String = "",
79512
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   372
    webserver: Webserver = default_webserver,
71047
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   373
    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
   374
    mercurial_source: String = "",
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   375
    progress: Progress = new Progress
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   376
  ): Unit = {
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   377
    /* system environment */
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   378
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   379
    Linux.check_system_root()
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   380
71079
e06852132c1d tuned messages;
wenzelm
parents: 71078
diff changeset
   381
    progress.echo("System packages ...")
e06852132c1d tuned messages;
wenzelm
parents: 71078
diff changeset
   382
71047
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   383
    if (package_update) {
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   384
      Linux.package_update(progress = progress)
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   385
      Linux.check_reboot_required()
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   386
    }
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   387
79512
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   388
    Linux.package_install(packages(webserver), progress = progress)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   389
    Linux.check_reboot_required()
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   390
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   391
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
   392
    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
   393
      for { name <- List("mercurial", "mercurial-common") if Linux.package_installed(name) } {
71326
d85258458623 tuned message;
wenzelm
parents: 71314
diff changeset
   394
        error("Cannot install Mercurial from source:\n" +
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
   395
          "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
   396
      }
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
   397
      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
   398
    }
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
   399
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
   400
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   401
    /* users */
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   402
72520
581d9d74e1e4 tuned --- make IntelliJ IDEA happy;
wenzelm
parents: 72494
diff changeset
   403
    if (name.exists((c: Char) => !(Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c))) ||
71269
7df5c110a43c support database dump;
wenzelm
parents: 71268
diff changeset
   404
        Set("", "ssh", "phd", "dump", daemon_user).contains(name)) {
71125
beb781551a66 more sanity checks;
wenzelm
parents: 71124
diff changeset
   405
      error("Bad installation name: " + quote(name))
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   406
    }
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   407
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   408
    user_setup(daemon_user, "Phorge Daemon User", ssh_setup = true)
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   409
    user_setup(name, "Phorge SSH User")
71049
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   410
f4b9dd5ab0cc more phabricator setup;
wenzelm
parents: 71047
diff changeset
   411
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   412
    /* basic installation */
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   413
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   414
    progress.echo("\nPhorge installation ...")
71076
8ac137c65776 tuned messages;
wenzelm
parents: 71075
diff changeset
   415
71068
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
   416
    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
   417
    val repo_path = if (repo.nonEmpty) Path.explode(repo) else default_repo(name)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   418
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   419
    val configs = read_config()
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   420
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   421
    for (config <- configs if config.name == name) {
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   422
      error("Duplicate Phorge installation " + quote(name) + " in " + config.root)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   423
    }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   424
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   425
    if (!Isabelle_System.bash("mkdir -p " + File.bash_path(root_path)).ok) {
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   426
      error("Failed to create root directory " + root_path)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   427
    }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   428
71116
wenzelm
parents: 71115
diff changeset
   429
    Isabelle_System.chown(Bash.string(www_user) + ":" + Bash.string(www_user), root_path)
wenzelm
parents: 71115
diff changeset
   430
    Isabelle_System.chmod("755", root_path)
wenzelm
parents: 71115
diff changeset
   431
80224
db92e0b6a11a clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
wenzelm
parents: 79525
diff changeset
   432
    progress.bash(cwd = root_path, echo = true,
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   433
      script = """
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   434
        set -e
71126
18f87bdbc812 tuned message;
wenzelm
parents: 71125
diff changeset
   435
        echo "Cloning distribution repositories:"
71287
71fd25a7bbe2 more robust setup: avoid blind shot at "the latest" version;
wenzelm
parents: 71285
diff changeset
   436
79487
47272fac86d8 support Phabricator on Ubuntu 22.04 LTS with PHP 8.1, using community form we.phorge.it version "2023 week 49";
wenzelm
parents: 79482
diff changeset
   437
        git clone --branch stable https://we.phorge.it/source/arcanist.git
71422
5d5be87330b5 allow to override repository versions at runtime;
wenzelm
parents: 71421
diff changeset
   438
        git -C arcanist reset --hard """ +
5d5be87330b5 allow to override repository versions at runtime;
wenzelm
parents: 71421
diff changeset
   439
          Bash.string(options.string("phabricator_version_arcanist")) + """
71287
71fd25a7bbe2 more robust setup: avoid blind shot at "the latest" version;
wenzelm
parents: 71285
diff changeset
   440
79487
47272fac86d8 support Phabricator on Ubuntu 22.04 LTS with PHP 8.1, using community form we.phorge.it version "2023 week 49";
wenzelm
parents: 79482
diff changeset
   441
        git clone --branch stable https://we.phorge.it/source/phorge.git phabricator
71422
5d5be87330b5 allow to override repository versions at runtime;
wenzelm
parents: 71421
diff changeset
   442
        git -C phabricator reset --hard """ +
5d5be87330b5 allow to override repository versions at runtime;
wenzelm
parents: 71421
diff changeset
   443
          Bash.string(options.string("phabricator_version_phabricator")) + """
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   444
      """).check
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   445
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   446
    val config = Config(name, root_path)
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   447
    write_config(configs ::: List(config))
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   448
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   449
    config.execute("config set pygments.enabled true")
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   450
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   451
71050
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   452
    /* local repository directory */
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   453
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   454
    progress.echo("\nRepository hosting setup ...")
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   455
71050
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   456
    if (!Isabelle_System.bash("mkdir -p " + File.bash_path(repo_path)).ok) {
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   457
      error("Failed to create local repository directory " + repo_path)
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   458
    }
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   459
71114
6cfec8029831 clarified signature;
wenzelm
parents: 71112
diff changeset
   460
    Isabelle_System.chown(
6cfec8029831 clarified signature;
wenzelm
parents: 71112
diff changeset
   461
      "-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), repo_path)
6cfec8029831 clarified signature;
wenzelm
parents: 71112
diff changeset
   462
    Isabelle_System.chmod("755", repo_path)
71050
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   463
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   464
    config.execute("config set repository.default-local-path " + File.bash_path(repo_path))
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   465
8198ceef0301 more phabricator setup;
wenzelm
parents: 71049
diff changeset
   466
71277
74cabc06cf2d proper support for multiple installations;
wenzelm
parents: 71276
diff changeset
   467
    val sudoers_file =
74cabc06cf2d proper support for multiple installations;
wenzelm
parents: 71276
diff changeset
   468
      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
   469
    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
   470
      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
   471
      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
   472
71115
wenzelm
parents: 71114
diff changeset
   473
    Isabelle_System.chmod("440", sudoers_file)
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   474
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   475
    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
   476
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   477
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   478
    /* MySQL setup */
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   479
71079
e06852132c1d tuned messages;
wenzelm
parents: 71078
diff changeset
   480
    progress.echo("\nMySQL setup ...")
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   481
71055
27a998cdc0f4 back to plain name, to have it accepted my mysql;
wenzelm
parents: 71054
diff changeset
   482
    File.write(Path.explode("/etc/mysql/mysql.conf.d/" + phabricator_name(ext = "cnf")),
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   483
"""[mysqld]
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   484
max_allowed_packet = 32M
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   485
innodb_buffer_pool_size = 1600M
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   486
local_infile = 0
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   487
""")
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   488
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   489
    Linux.service_restart("mysql")
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   490
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   491
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   492
    def mysql_conf(R: Regex, which: String): String = {
71266
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   493
      val conf = Path.explode("/etc/mysql/debian.cnf")
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   494
      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
   495
        case Some(res) => res
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   496
        case None => error("Cannot determine " + which + " from " + conf)
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   497
      }
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   498
    }
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   499
71266
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   500
    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
   501
    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
   502
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   503
    val mysql_name = phabricator_name(name = name).replace("-", "_")
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   504
    val mysql_user_string = SQL.string(mysql_name) + "@'localhost'"
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   505
    val mysql_password = Linux.generate_password()
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   506
71266
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   507
    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
   508
      " --password=" + Bash.string(mysql_root_password) + " --execute=" +
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   509
      Bash.string(
71274
5212ca49598a more robust;
wenzelm
parents: 71273
diff changeset
   510
        """DROP USER IF EXISTS """ + mysql_user_string + "; " +
5212ca49598a more robust;
wenzelm
parents: 71273
diff changeset
   511
        """CREATE USER """ + mysql_user_string +
71266
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   512
        """ IDENTIFIED BY """ + SQL.string(mysql_password) + """ PASSWORD EXPIRE NEVER; """ +
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   513
        """GRANT ALL ON `""" + (mysql_name + "_%").replace("_", "\\_") +
80450
4355857e13a6 tuned output;
wenzelm
parents: 80224
diff changeset
   514
        """`.* TO """ + mysql_user_string + "; " +
72522
6e27af808c17 more privileges for the sake of mysqldump (avoid workaround --no-tablespaces);
wenzelm
parents: 72521
diff changeset
   515
        """GRANT PROCESS ON *.* TO """ + mysql_user_string + ";")).check
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   516
71266
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   517
    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
   518
    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
   519
8451c86ffa85 proper mysql user setup: avoid superuser powers in production;
wenzelm
parents: 71265
diff changeset
   520
    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
   521
    config.execute("config set storage.default-namespace " + Bash.string(mysql_name))
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   522
    config.execute("config set storage.mysql-engine.max-size 8388608")
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   523
80224
db92e0b6a11a clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
wenzelm
parents: 79525
diff changeset
   524
    progress.bash("bin/storage upgrade --force", cwd = config.home, echo = true).check
70969
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   525
a48112873f81 MySQL setup;
wenzelm
parents: 70968
diff changeset
   526
71269
7df5c110a43c support database dump;
wenzelm
parents: 71268
diff changeset
   527
    /* database dump */
7df5c110a43c support database dump;
wenzelm
parents: 71268
diff changeset
   528
7df5c110a43c support database dump;
wenzelm
parents: 71268
diff changeset
   529
    val dump_name = isabelle_phabricator_name(name = "dump")
71282
de59dd86760f tuned signature;
wenzelm
parents: 71281
diff changeset
   530
    command_setup(dump_name, body =
71269
7df5c110a43c support database dump;
wenzelm
parents: 71268
diff changeset
   531
"""mkdir -p "$ROOT/database" && chown root:root "$ROOT/database" && chmod 700 "$ROOT/database"
7df5c110a43c support database dump;
wenzelm
parents: 71268
diff changeset
   532
[ -e "$ROOT/database/dump.sql.gz" ] && mv -f "$ROOT/database/dump.sql.gz" "$ROOT/database/dump-old.sql.gz"
71328
4642a81f5913 tuned messages;
wenzelm
parents: 71326
diff changeset
   533
echo -n "Creating $ROOT/database/dump.sql.gz ..."
4642a81f5913 tuned messages;
wenzelm
parents: 71326
diff changeset
   534
"$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'
4642a81f5913 tuned messages;
wenzelm
parents: 71326
diff changeset
   535
echo " $(ls -hs "$ROOT/database/dump.sql.gz" | cut -d" " -f1)" """)
71269
7df5c110a43c support database dump;
wenzelm
parents: 71268
diff changeset
   536
7df5c110a43c support database dump;
wenzelm
parents: 71268
diff changeset
   537
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   538
    /* Phorge upgrade */
71283
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   539
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   540
    command_setup(isabelle_phabricator_name(name = "upgrade"),
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   541
      init =
71285
8cd05f7b3b4a proper default;
wenzelm
parents: 71284
diff changeset
   542
"""BRANCH="${1:-stable}"
71283
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   543
if [ "$BRANCH" != "master" -a "$BRANCH" != "stable" ]
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   544
then
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   545
  echo "Bad branch: \"$BRANCH\""
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   546
  exit 1
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   547
fi
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   548
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   549
systemctl stop isabelle-phabricator-phd
79516
wenzelm
parents: 79515
diff changeset
   550
systemctl stop """ + webserver.system_name,
71283
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   551
      body =
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   552
"""echo -e "\nUpgrading phabricator \"$NAME\" root \"$ROOT\" ..."
71845
b8d7b623e274 follow Phabricator update 2020 Week 19;
wenzelm
parents: 71747
diff changeset
   553
for REPO in arcanist phabricator
71283
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   554
do
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   555
  cd "$ROOT/$REPO"
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   556
  echo -e "\nUpdating \"$REPO\" ..."
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   557
  git checkout "$BRANCH"
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   558
  git pull
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   559
done
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   560
echo -e "\nUpgrading storage ..."
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   561
"$ROOT/phabricator/bin/storage" upgrade --force
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   562
""",
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   563
      exit =
79516
wenzelm
parents: 79515
diff changeset
   564
"""systemctl start """ + webserver.system_name + """
71283
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   565
systemctl start isabelle-phabricator-phd""")
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   566
cfcc1a2233ca support for Phabricator upgrade;
wenzelm
parents: 71282
diff changeset
   567
79512
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   568
    /* webserver setup */
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   569
79523
f1287f1894a0 clarified webserver names;
wenzelm
parents: 79522
diff changeset
   570
    progress.echo(webserver.user_name + " setup ...")
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   571
79512
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   572
    val sites_dir = webserver.sites_dir
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   573
    if (!sites_dir.is_dir) error("Bad " + webserver + " sites directory " + sites_dir)
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   574
79482
a49db426ffd4 refer to "localhost" as pro-forma domain;
wenzelm
parents: 78602
diff changeset
   575
    val server_name = phabricator_name(name = name, ext = "localhost")  // alias for "localhost" for testing
71052
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   576
    val server_url = "http://" + server_name
6bf53035baf0 clarified name prefixes: global config always uses "isabelle-phabricator";
wenzelm
parents: 71051
diff changeset
   577
79512
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   578
    webserver.php_init()
71439
760e19aa9b09 afford more logging (following defaults on Ubuntu);
wenzelm
parents: 71422
diff changeset
   579
79512
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   580
    webserver.site_init(name, server_name, config.webroot)
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71050
diff changeset
   581
71057
2965304143d8 more phabricator setup;
wenzelm
parents: 71056
diff changeset
   582
    config.execute("config set phabricator.base-uri " + Bash.string(server_url))
2965304143d8 more phabricator setup;
wenzelm
parents: 71056
diff changeset
   583
79512
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   584
    webserver.restart()
70968
46847076477c Apache setup;
wenzelm
parents: 70967
diff changeset
   585
71328
4642a81f5913 tuned messages;
wenzelm
parents: 71326
diff changeset
   586
    progress.echo("\nFurther manual configuration via " + server_url)
71128
f79006c533b0 clarified errors: PHP daemon can fail under odd circumstances;
wenzelm
parents: 71127
diff changeset
   587
71053
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   588
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   589
    /* PHP daemon */
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   590
71128
f79006c533b0 clarified errors: PHP daemon can fail under odd circumstances;
wenzelm
parents: 71127
diff changeset
   591
    progress.echo("\nPHP daemon setup ...")
71053
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   592
72376
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
   593
    val phd_log_path = Isabelle_System.make_directory(Path.explode("/var/tmp/phd"))
71273
6b8cbdc9713b more robust;
wenzelm
parents: 71270
diff changeset
   594
    Isabelle_System.chown(
6b8cbdc9713b more robust;
wenzelm
parents: 71270
diff changeset
   595
      "-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), phd_log_path)
6b8cbdc9713b more robust;
wenzelm
parents: 71270
diff changeset
   596
    Isabelle_System.chmod("755", phd_log_path)
6b8cbdc9713b more robust;
wenzelm
parents: 71270
diff changeset
   597
71053
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   598
    config.execute("config set phd.user " + Bash.string(daemon_user))
71112
eed5b6188371 more support for multiple daemons;
wenzelm
parents: 71111
diff changeset
   599
    config.execute("config set phd.log-directory /var/tmp/phd/" +
eed5b6188371 more support for multiple daemons;
wenzelm
parents: 71111
diff changeset
   600
      isabelle_phabricator_name(name = name) + "/log")
71053
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   601
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
   602
    val phd_name = isabelle_phabricator_name(name = "phd")
71127
0ad53b5f2bb1 more robust;
wenzelm
parents: 71126
diff changeset
   603
    Linux.service_shutdown(phd_name)
71282
de59dd86760f tuned signature;
wenzelm
parents: 71281
diff changeset
   604
    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
   605
    try {
f79006c533b0 clarified errors: PHP daemon can fail under odd circumstances;
wenzelm
parents: 71127
diff changeset
   606
      Linux.service_install(phd_name,
71053
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   607
"""[Unit]
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   608
Description=PHP daemon manager for Isabelle/Phorge
79512
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   609
After=syslog.target network.target """ + webserver.system_name + """.service mysql.service
71053
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   610
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   611
[Service]
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   612
Type=oneshot
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   613
User=""" + daemon_user + """
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   614
Group=""" + daemon_user + """
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   615
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
   616
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
   617
ExecStop=""" + phd_command.implode + """ stop
71053
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   618
RemainAfterExit=yes
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   619
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   620
[Install]
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   621
WantedBy=multi-user.target
ba14aa0b5a5d more robust: install PHP daemon after Apache;
wenzelm
parents: 71052
diff changeset
   622
""")
71128
f79006c533b0 clarified errors: PHP daemon can fail under odd circumstances;
wenzelm
parents: 71127
diff changeset
   623
    }
f79006c533b0 clarified errors: PHP daemon can fail under odd circumstances;
wenzelm
parents: 71127
diff changeset
   624
    catch {
f79006c533b0 clarified errors: PHP daemon can fail under odd circumstances;
wenzelm
parents: 71127
diff changeset
   625
      case ERROR(msg) =>
80224
db92e0b6a11a clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
wenzelm
parents: 79525
diff changeset
   626
        progress.bash("bin/phd status", cwd = config.home, echo = true).check
71128
f79006c533b0 clarified errors: PHP daemon can fail under odd circumstances;
wenzelm
parents: 71127
diff changeset
   627
        error(msg)
f79006c533b0 clarified errors: PHP daemon can fail under odd circumstances;
wenzelm
parents: 71127
diff changeset
   628
    }
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   629
  }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   630
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   631
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   632
  /* Isabelle tool wrapper */
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   633
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   634
  val isabelle_tool2 =
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   635
    Isabelle_Tool("phabricator_setup", "setup Phorge server on Ubuntu Linux",
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   636
      Scala_Project.here,
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   637
      { args =>
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   638
        var mercurial_source = ""
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   639
        var repo = ""
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   640
        var package_update = false
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   641
        var name = default_name
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   642
        var options = Options.init()
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   643
        var root = ""
79512
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   644
        var webserver = default_webserver
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   645
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   646
        val getopts = Getopts("""
71078
5bb2235d843d clarified command-line;
wenzelm
parents: 71077
diff changeset
   647
Usage: isabelle phabricator_setup [OPTIONS]
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   648
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   649
  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
   650
    -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
   651
                 """ + standard_mercurial_source + """
71068
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
   652
    -R DIR       repository directory (default: """ + default_repo("NAME") + """)
71047
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   653
    -U           full update of system packages before installation
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   654
    -n NAME      Phorge installation name (default: """ + quote(default_name) + """)
71422
5d5be87330b5 allow to override repository versions at runtime;
wenzelm
parents: 71421
diff changeset
   655
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
71068
510b89906d86 discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
wenzelm
parents: 71066
diff changeset
   656
    -r DIR       installation root directory (default: """ + default_root("NAME") + """)
79512
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   657
    -w NAME      webserver name (""" +
79523
f1287f1894a0 clarified webserver names;
wenzelm
parents: 79522
diff changeset
   658
          all_webservers.map(w => quote(w.user_name)).mkString (" or ") +
f1287f1894a0 clarified webserver names;
wenzelm
parents: 79522
diff changeset
   659
          ", default: " + quote(default_webserver.user_name) + """)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   660
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   661
  Install Phorge as Linux service, based on webserver + PHP + MySQL.
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   662
71078
5bb2235d843d clarified command-line;
wenzelm
parents: 71077
diff changeset
   663
  The installation name (default: """ + quote(default_name) + """) is mapped to a regular
5bb2235d843d clarified command-line;
wenzelm
parents: 71077
diff changeset
   664
  Unix user; this is relevant for public SSH access.
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   665
""",
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
   666
          "M:" -> (arg => mercurial_source = (if (arg == ":") standard_mercurial_source else arg)),
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   667
          "R:" -> (arg => repo = arg),
71047
87c132cf5860 more options;
wenzelm
parents: 70970
diff changeset
   668
          "U" -> (_ => package_update = true),
71078
5bb2235d843d clarified command-line;
wenzelm
parents: 71077
diff changeset
   669
          "n:" -> (arg => name = arg),
71422
5d5be87330b5 allow to override repository versions at runtime;
wenzelm
parents: 71421
diff changeset
   670
          "o:" -> (arg => options = options + arg),
79512
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   671
          "r:" -> (arg => root = arg),
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   672
          "w:" -> (arg => webserver = get_webserver(arg)))
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   673
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   674
        val more_args = getopts(args)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   675
        if (more_args.nonEmpty) getopts.usage()
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   676
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   677
        val progress = new Console_Progress
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   678
79512
bf91c1aec34b support multiple webservers: Apache or Nginx;
wenzelm
parents: 79496
diff changeset
   679
        phabricator_setup(options, name = name, root = root, repo = repo, webserver = webserver,
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   680
          package_update = package_update, mercurial_source = mercurial_source, progress = progress)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   681
      })
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   682
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   683
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   684
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   685
  /** setup mail **/
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   686
71072
wenzelm
parents: 71071
diff changeset
   687
  val mailers_template: String =
75659
9bd92ac9328f more robust Scala 3 indentation, for the sake of IntelliJ IDEA;
wenzelm
parents: 75394
diff changeset
   688
    """[
71072
wenzelm
parents: 71071
diff changeset
   689
  {
wenzelm
parents: 71071
diff changeset
   690
    "key": "example.org",
wenzelm
parents: 71071
diff changeset
   691
    "type": "smtp",
wenzelm
parents: 71071
diff changeset
   692
    "options": {
wenzelm
parents: 71071
diff changeset
   693
      "host": "mail.example.org",
wenzelm
parents: 71071
diff changeset
   694
      "port": 465,
wenzelm
parents: 71071
diff changeset
   695
      "user": "phabricator@example.org",
wenzelm
parents: 71071
diff changeset
   696
      "password": "********",
wenzelm
parents: 71071
diff changeset
   697
      "protocol": "ssl",
wenzelm
parents: 71071
diff changeset
   698
      "message-id": true
wenzelm
parents: 71071
diff changeset
   699
    }
wenzelm
parents: 71071
diff changeset
   700
  }
wenzelm
parents: 71071
diff changeset
   701
]"""
wenzelm
parents: 71071
diff changeset
   702
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   703
  def phabricator_setup_mail(
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   704
    name: String = default_name,
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   705
    config_file: Option[Path] = None,
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   706
    test_user: String = "",
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   707
    progress: Progress = new Progress
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   708
  ): Unit = {
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   709
    Linux.check_system_root()
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   710
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   711
    val config = get_config(name)
71073
d61fd7aade69 clarified directory;
wenzelm
parents: 71072
diff changeset
   712
    val default_config_file = config.root + default_mailers
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   713
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   714
    val mail_config = config_file getOrElse default_config_file
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   715
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   716
    def setup_mail: Unit = {
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   717
      progress.echo("Using mail configuration from " + mail_config)
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   718
      config.execute("config set cluster.mailers --stdin < " + File.bash_path(mail_config))
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   719
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   720
      if (test_user.nonEmpty) {
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   721
        progress.echo("Sending test mail to " + quote(test_user))
80224
db92e0b6a11a clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
wenzelm
parents: 79525
diff changeset
   722
        progress.bash(cwd = config.home, echo = true,
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   723
          script = """echo "Test from Phorge ($(date))" | bin/mail send-test --subject "Test" --to """ +
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   724
            Bash.string(test_user)).check
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   725
      }
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   726
    }
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   727
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   728
    if (config_file.isEmpty) {
71070
79b89278b825 clarified permissions;
wenzelm
parents: 71068
diff changeset
   729
      if (!default_config_file.is_file) {
79b89278b825 clarified permissions;
wenzelm
parents: 71068
diff changeset
   730
        File.write(default_config_file, mailers_template)
71114
6cfec8029831 clarified signature;
wenzelm
parents: 71112
diff changeset
   731
        Isabelle_System.chmod("600", default_config_file)
71070
79b89278b825 clarified permissions;
wenzelm
parents: 71068
diff changeset
   732
      }
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   733
      if (File.read(default_config_file) == mailers_template) {
71131
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71129
diff changeset
   734
        progress.echo("Please invoke the tool again, after providing details in\n  " +
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71129
diff changeset
   735
          default_config_file.implode + "\n")
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   736
      }
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   737
      else setup_mail
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   738
    }
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   739
    else setup_mail
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   740
  }
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   741
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   742
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   743
  /* Isabelle tool wrapper */
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   744
71097
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71079
diff changeset
   745
  val isabelle_tool3 =
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   746
    Isabelle_Tool("phabricator_setup_mail", "setup mail for one Phorge installation",
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   747
      Scala_Project.here,
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   748
      { args =>
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   749
        var test_user = ""
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   750
        var name = default_name
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   751
        var config_file: Option[Path] = None
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   752
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   753
        val getopts = Getopts("""
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   754
Usage: isabelle phabricator_setup_mail [OPTIONS]
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   755
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   756
  Options are:
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   757
    -T USER      send test mail to Phorge user
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   758
    -f FILE      config file (default: """ + default_mailers + """ within Phorge root)
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   759
    -n NAME      Phorge installation name (default: """ + quote(default_name) + """)
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   760
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   761
  Provide mail configuration for existing Phorge installation.
71066
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   762
""",
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   763
          "T:" -> (arg => test_user = arg),
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   764
          "f:" -> (arg => config_file = Some(Path.explode(arg))),
114db2b5a5f8 support for Phabricator mail configuration;
wenzelm
parents: 71058
diff changeset
   765
          "n:" -> (arg => name = arg))
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   766
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   767
        val more_args = getopts(args)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   768
        if (more_args.nonEmpty) getopts.usage()
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   769
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   770
        val progress = new Console_Progress
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
   771
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   772
        phabricator_setup_mail(name = name, config_file = config_file,
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   773
          test_user = test_user, progress = progress)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   774
      })
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   775
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   776
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
  /** setup ssh **/
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   779
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   780
  /* sshd config */
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
  private val Port = """^\s*Port\s+(\d+)\s*$""".r
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   783
  private val No_Port = """^#\s*Port\b.*$""".r
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   784
  private val Any_Port = """^#?\s*Port\b.*$""".r
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   785
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   786
  def conf_ssh_port(port: Int): String =
76129
5979f73b9db1 clarified signature: separate unrelated modules;
wenzelm
parents: 76104
diff changeset
   787
    if (port == default_system_port) "#Port " + default_system_port else "Port " + port
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   788
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   789
  def read_ssh_port(conf: Path): Int = {
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   790
    val lines = split_lines(File.read(conf))
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   791
    val ports =
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   792
      lines.flatMap({
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   793
        case Port(Value.Int(p)) => Some(p)
76129
5979f73b9db1 clarified signature: separate unrelated modules;
wenzelm
parents: 76104
diff changeset
   794
        case No_Port() => Some(default_system_port)
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   795
        case _ => None
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
    ports match {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   798
      case List(port) => port
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   799
      case Nil => error("Missing Port specification in " + conf)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   800
      case _ => error("Multiple Port specifications in " + conf)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   801
    }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   802
  }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   803
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   804
  def write_ssh_port(conf: Path, port: Int): Boolean = {
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   805
    val old_port = read_ssh_port(conf)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   806
    if (old_port == port) false
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   807
    else {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   808
      val lines = split_lines(File.read(conf))
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   809
      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
   810
      File.write(conf, cat_lines(lines1))
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   811
      true
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   812
    }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   813
  }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   814
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
  /* phabricator_setup_ssh */
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   817
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   818
  def phabricator_setup_ssh(
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   819
    server_port: Int = default_server_port,
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   820
    system_port: Int = default_system_port,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   821
    progress: Progress = new Progress
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   822
  ): Unit = {
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   823
    Linux.check_system_root()
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   824
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   825
    val configs = read_config()
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   826
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   827
    if (server_port == system_port) {
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   828
      error("Port for Phorge sshd coincides with system port: " + system_port)
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   829
    }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   830
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   831
    val sshd_conf_system = Path.explode("/etc/ssh/sshd_config")
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   832
    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
   833
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   834
    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
   835
    Linux.service_shutdown(ssh_name)
cd166c3904dd more robust: system ssh service is required for Phabricator ssh service;
wenzelm
parents: 71109
diff changeset
   836
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   837
    val old_system_port = read_ssh_port(sshd_conf_system)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   838
    if (old_system_port != system_port) {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   839
      progress.echo("Reconfigurig system ssh service")
71111
cd166c3904dd more robust: system ssh service is required for Phabricator ssh service;
wenzelm
parents: 71109
diff changeset
   840
      Linux.service_shutdown("ssh")
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   841
      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
   842
      Linux.service_start("ssh")
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   843
    }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   844
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   845
    progress.echo("Configuring " + ssh_name + " service")
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   846
71282
de59dd86760f tuned signature;
wenzelm
parents: 71281
diff changeset
   847
    val ssh_command = command_setup(ssh_name, body =
71122
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
   848
"""if [ "$1" = "$NAME" ]
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
   849
then
730090397e0d clarified signature;
wenzelm
parents: 71116
diff changeset
   850
  exec "$ROOT/phabricator/bin/ssh-auth" "$@"
71270
wenzelm
parents: 71269
diff changeset
   851
fi""", exit = "exit 1")
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   852
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   853
    File.write(sshd_conf_server,
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   854
"""# OpenBSD Secure Shell server for Isabelle/Phorge
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   855
AuthorizedKeysCommand """ + ssh_command.implode + """
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   856
AuthorizedKeysCommandUser """ + daemon_user + """
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   857
AuthorizedKeysFile none
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   858
AllowUsers """ + configs.map(_.name).mkString(" ") + """
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   859
Port """ + server_port + """
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   860
Protocol 2
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   861
PermitRootLogin no
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   862
AllowAgentForwarding no
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   863
AllowTcpForwarding no
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   864
PrintMotd no
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   865
PrintLastLog no
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   866
PasswordAuthentication no
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   867
ChallengeResponseAuthentication no
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   868
PidFile /var/run/""" + ssh_name + """.pid
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   869
""")
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   870
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   871
    Linux.service_install(ssh_name,
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   872
"""[Unit]
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   873
Description=OpenBSD Secure Shell server for Isabelle/Phorge
79519
557f00504bb6 more robust systemd configuration;
wenzelm
parents: 79518
diff changeset
   874
After=network.target auditd.service isabelle-phabricator-phd.service
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   875
ConditionPathExists=!/etc/ssh/sshd_not_to_be_run
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   876
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   877
[Service]
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   878
EnvironmentFile=-/etc/default/ssh
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   879
ExecStartPre=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   880
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
   881
ExecReload=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   882
ExecReload=/bin/kill -HUP $MAINPID
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   883
KillMode=process
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   884
Restart=on-failure
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   885
RestartPreventExitStatus=255
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   886
Type=notify
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   887
RuntimeDirectory=sshd-phabricator
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   888
RuntimeDirectoryMode=0755
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   889
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   890
[Install]
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   891
WantedBy=multi-user.target
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   892
Alias=""" + ssh_name + """.service
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   893
""")
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   894
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   895
    for (config <- configs) {
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   896
      progress.echo("phabricator " + quote(config.name) + " port " +  server_port)
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   897
      config.execute("config set diffusion.ssh-port " + Bash.string(server_port.toString))
76129
5979f73b9db1 clarified signature: separate unrelated modules;
wenzelm
parents: 76104
diff changeset
   898
      if (server_port == default_system_port) config.execute("config delete diffusion.ssh-port")
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   899
    }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   900
  }
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   901
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   902
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   903
  /* Isabelle tool wrapper */
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   904
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   905
  val isabelle_tool4 =
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   906
    Isabelle_Tool("phabricator_setup_ssh", "setup ssh service for all Phorge installations",
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   907
      Scala_Project.here,
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   908
      { args =>
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   909
        var server_port = default_server_port
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   910
        var system_port = default_system_port
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   911
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   912
        val getopts = Getopts("""
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   913
Usage: isabelle phabricator_setup_ssh [OPTIONS]
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   914
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   915
  Options are:
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   916
    -p PORT      sshd port for Phorge servers (default: """ + default_server_port + """)
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   917
    -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
   918
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   919
  Configure ssh service for all Phorge installations: a separate sshd
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   920
  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
   921
  be distinct.
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   922
81717
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   923
  A particular Phorge installation is addressed by using its
114449035ec6 update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
wenzelm
parents: 80450
diff changeset
   924
  name as the ssh user; the actual Phorge user is determined via
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   925
  stored ssh keys.
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   926
""",
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   927
          "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
   928
          "q:" -> (arg => system_port = Value.Int.parse(arg)))
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   929
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   930
        val more_args = getopts(args)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   931
        if (more_args.nonEmpty) getopts.usage()
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   932
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   933
        val progress = new Console_Progress
71109
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71103
diff changeset
   934
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   935
        phabricator_setup_ssh(
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   936
          server_port = server_port, system_port = system_port, progress = progress)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   937
      })
71299
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   938
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   939
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   940
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   941
  /** conduit API **/
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
   942
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   943
  object API {
71332
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
   944
    /* user information */
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
   945
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
   946
    sealed case class User(
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
   947
      id: Long,
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
   948
      phid: String,
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
   949
      name: String,
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
   950
      real_name: String,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   951
      roles: List[String]
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   952
    ) {
71332
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
   953
      def is_valid: Boolean =
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
   954
        roles.contains("verified") &&
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
   955
        roles.contains("approved") &&
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
   956
        roles.contains("activated")
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
   957
      def is_admin: Boolean = roles.contains("admin")
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
   958
      def is_regular: Boolean = !(roles.contains("bot") || roles.contains("list"))
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
   959
    }
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
   960
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
   961
71314
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   962
    /* repository information */
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   963
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   964
    sealed case class Repository(
78602
92b6958e8787 clarified signature: prefer enum types;
wenzelm
parents: 77567
diff changeset
   965
      vcs: VCS,
71314
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   966
      id: Long,
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   967
      phid: String,
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   968
      name: String,
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   969
      callsign: String,
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   970
      short_name: String,
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   971
      importing: Boolean,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   972
      ssh_url: String
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   973
    ) {
71314
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   974
      def is_hg: Boolean = vcs == VCS.hg
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   975
    }
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   976
78602
92b6958e8787 clarified signature: prefer enum types;
wenzelm
parents: 77567
diff changeset
   977
    enum VCS { case hg, git, svn }
92b6958e8787 clarified signature: prefer enum types;
wenzelm
parents: 77567
diff changeset
   978
92b6958e8787 clarified signature: prefer enum types;
wenzelm
parents: 77567
diff changeset
   979
    def read_vcs(s: String): VCS =
92b6958e8787 clarified signature: prefer enum types;
wenzelm
parents: 77567
diff changeset
   980
      try { VCS.valueOf(s) }
92b6958e8787 clarified signature: prefer enum types;
wenzelm
parents: 77567
diff changeset
   981
      catch { case _: IllegalArgumentException => error("Unknown vcs type " + quote(s)) }
71314
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   982
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   983
    def edits(typ: String, value: JSON.T): List[JSON.Object.T] =
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   984
      List(JSON.Object("type" -> typ, "value" -> value))
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   985
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   986
    def opt_edits(typ: String, value: Option[JSON.T]): List[JSON.Object.T] =
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   987
      value.toList.flatMap(edits(typ, _))
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   988
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   989
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   990
    /* result with optional error */
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   991
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
   992
    sealed case class Result(result: JSON.T, error: Option[String]) {
71314
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   993
      def ok: Boolean = error.isEmpty
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   994
      def get: JSON.T = if (ok) result else Exn.error(error.get)
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   995
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   996
      def get_value[A](unapply: JSON.T => Option[A]): A =
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   997
        unapply(get) getOrElse Exn.error("Bad JSON result: " + JSON.Format(result))
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   998
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
   999
      def get_string: String = get_value(JSON.Value.String.unapply)
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
  1000
    }
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
  1001
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1002
    def make_result(json: JSON.T): Result = {
71314
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
  1003
      val result = JSON.value(json, "result").getOrElse(JSON.Object.empty)
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
  1004
      val error_info = JSON.string(json, "error_info")
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
  1005
      val error_code = JSON.string(json, "error_code")
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
  1006
      Result(result, error_info orElse error_code)
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
  1007
    }
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
  1008
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
  1009
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
  1010
    /* context for operations */
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
  1011
76173
5298a498738c clarified default, following 8b695e59db3f;
wenzelm
parents: 76172
diff changeset
  1012
    def apply(server: String, port: Int = 0): API = new API(server, port)
71299
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
  1013
  }
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
  1014
76172
81241a1d3d99 tuned signature;
wenzelm
parents: 76171
diff changeset
  1015
  final class API private(server: String, port: Int) {
71299
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
  1016
    /* connection */
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
  1017
76172
81241a1d3d99 tuned signature;
wenzelm
parents: 76171
diff changeset
  1018
    private def port_suffix: String = if (port > 0) ":" + port else ""
81241a1d3d99 tuned signature;
wenzelm
parents: 76171
diff changeset
  1019
    override def toString: String = server + port_suffix
81241a1d3d99 tuned signature;
wenzelm
parents: 76171
diff changeset
  1020
    def hg_url: String = "ssh://" + server + port_suffix
71299
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
  1021
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
  1022
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
  1023
    /* execute methods */
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
  1024
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1025
    def execute_raw(method: String, params: JSON.T = JSON.Object.empty): JSON.T = {
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1026
      Isabelle_System.with_tmp_file("params", "json") { params_file =>
71300
ca794da3bb1d tuned signature;
wenzelm
parents: 71299
diff changeset
  1027
        File.write(params_file, JSON.Format(JSON.Object("params" -> JSON.Format(params))))
71299
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
  1028
        val result =
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
  1029
          Isabelle_System.bash(
76172
81241a1d3d99 tuned signature;
wenzelm
parents: 76171
diff changeset
  1030
            SSH.client_command(port = port) + " -- " + Bash.string(server) +
71300
ca794da3bb1d tuned signature;
wenzelm
parents: 71299
diff changeset
  1031
            " conduit " + Bash.string(method) + " < " + File.bash_path(params_file)).check
71299
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
  1032
        JSON.parse(result.out, strict = false)
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
  1033
      }
71299
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
  1034
    }
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
  1035
71300
ca794da3bb1d tuned signature;
wenzelm
parents: 71299
diff changeset
  1036
    def execute(method: String, params: JSON.T = JSON.Object.empty): API.Result =
ca794da3bb1d tuned signature;
wenzelm
parents: 71299
diff changeset
  1037
      API.make_result(execute_raw(method, params = params))
71299
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
  1038
71330
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1039
    def execute_search[A](
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1040
      method: String,
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1041
      params: JSON.Object.T,
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1042
      unapply: JSON.T => Option[A]
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1043
    ): List[A] = {
71330
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1044
      val results = new mutable.ListBuffer[A]
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1045
      var after = ""
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1046
75382
81673c441ce3 tuned: eliminted do-while for the sake of scala3;
wenzelm
parents: 74944
diff changeset
  1047
      var cont = true
81673c441ce3 tuned: eliminted do-while for the sake of scala3;
wenzelm
parents: 74944
diff changeset
  1048
      while (cont) {
71330
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1049
        val result =
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1050
          execute(method, params = params ++ JSON.optional("after" -> proper_string(after)))
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1051
        results ++= result.get_value(JSON.list(_, "data", unapply))
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1052
        after = result.get_value(JSON.value(_, "cursor", JSON.string0(_, "after")))
75382
81673c441ce3 tuned: eliminted do-while for the sake of scala3;
wenzelm
parents: 74944
diff changeset
  1053
        cont = after.nonEmpty
81673c441ce3 tuned: eliminted do-while for the sake of scala3;
wenzelm
parents: 74944
diff changeset
  1054
      }
71330
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1055
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1056
      results.toList
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1057
    }
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1058
71332
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1059
    def ping(): String = execute("conduit.ping").get_string
71299
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
  1060
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
  1061
71332
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1062
    /* users */
71299
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
  1063
71300
ca794da3bb1d tuned signature;
wenzelm
parents: 71299
diff changeset
  1064
    lazy val user_phid: String = execute("user.whoami").get_value(JSON.string(_, "phid"))
ca794da3bb1d tuned signature;
wenzelm
parents: 71299
diff changeset
  1065
    lazy val user_name: String = execute("user.whoami").get_value(JSON.string(_, "userName"))
71301
3fdd0b93fa4b clarified signature;
wenzelm
parents: 71300
diff changeset
  1066
71332
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1067
    def get_users(
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1068
      all: Boolean = false,
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1069
      phid: String = "",
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1070
      name: String = ""
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1071
    ): List[API.User] = {
71332
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1072
      val constraints: JSON.Object.T =
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1073
        (for { (key, value) <- List("phids" -> phid, "usernames" -> name) if value.nonEmpty }
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1074
          yield (key, List(value))).toMap
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1075
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1076
      execute_search("user.search",
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1077
          JSON.Object("queryKey" -> (if (all) "all" else "active"), "constraints" -> constraints),
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1078
            data => JSON.value(data, "fields", fields =>
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1079
              for {
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1080
                id <- JSON.long(data, "id")
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1081
                phid <- JSON.string(data, "phid")
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1082
                name <- JSON.string(fields, "username")
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1083
                real_name <- JSON.string0(fields, "realName")
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1084
                roles <- JSON.strings(fields, "roles")
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1085
              } yield API.User(id, phid, name, real_name, roles)))
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1086
    }
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1087
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1088
    def the_user(phid: String): API.User =
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1089
      get_users(phid = phid) match {
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1090
        case List(user) => user
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1091
        case _ => error("Bad user PHID " + quote(phid))
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1092
      }
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1093
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1094
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1095
    /* repositories */
277ee690cb14 clarified signature -- more operations;
wenzelm
parents: 71331
diff changeset
  1096
71306
113779776ee4 more repository information;
wenzelm
parents: 71303
diff changeset
  1097
    def get_repositories(
71331
79232f138382 clarified signature;
wenzelm
parents: 71330
diff changeset
  1098
      all: Boolean = false,
79232f138382 clarified signature;
wenzelm
parents: 71330
diff changeset
  1099
      phid: String = "",
79232f138382 clarified signature;
wenzelm
parents: 71330
diff changeset
  1100
      callsign: String = "",
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1101
      short_name: String = ""
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1102
    ): List[API.Repository] = {
71306
113779776ee4 more repository information;
wenzelm
parents: 71303
diff changeset
  1103
      val constraints: JSON.Object.T =
113779776ee4 more repository information;
wenzelm
parents: 71303
diff changeset
  1104
        (for {
113779776ee4 more repository information;
wenzelm
parents: 71303
diff changeset
  1105
          (key, value) <- List("phids" -> phid, "callsigns" -> callsign, "shortNames" -> short_name)
113779776ee4 more repository information;
wenzelm
parents: 71303
diff changeset
  1106
          if value.nonEmpty
113779776ee4 more repository information;
wenzelm
parents: 71303
diff changeset
  1107
        } yield (key, List(value))).toMap
113779776ee4 more repository information;
wenzelm
parents: 71303
diff changeset
  1108
71330
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1109
      execute_search("diffusion.repository.search",
71331
79232f138382 clarified signature;
wenzelm
parents: 71330
diff changeset
  1110
          JSON.Object("queryKey" -> (if (all) "all" else "active"), "constraints" -> constraints),
71330
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1111
            data => JSON.value(data, "fields", fields =>
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1112
              for {
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1113
                vcs_name <- JSON.string(fields, "vcs")
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1114
                id <- JSON.long(data, "id")
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1115
                phid <- JSON.string(data, "phid")
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1116
                name <- JSON.string(fields, "name")
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1117
                callsign <- JSON.string0(fields, "callsign")
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1118
                short_name <- JSON.string0(fields, "shortName")
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1119
                importing <- JSON.bool(fields, "isImporting")
71306
113779776ee4 more repository information;
wenzelm
parents: 71303
diff changeset
  1120
              }
71330
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1121
              yield {
78602
92b6958e8787 clarified signature: prefer enum types;
wenzelm
parents: 77567
diff changeset
  1122
                val vcs = API.read_vcs(vcs_name)
71330
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1123
                val url_path =
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1124
                  if (short_name.isEmpty) "/diffusion/" + id else "/source/" + short_name
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1125
                val ssh_url =
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1126
                  vcs match {
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1127
                    case API.VCS.hg => hg_url + url_path
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1128
                    case API.VCS.git => hg_url + url_path + ".git"
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1129
                    case API.VCS.svn => ""
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1130
                  }
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1131
                API.Repository(vcs, id, phid, name, callsign, short_name, importing, ssh_url)
836fde6f9d7e proper search with multiple "pages" of results;
wenzelm
parents: 71328
diff changeset
  1132
              }))
71306
113779776ee4 more repository information;
wenzelm
parents: 71303
diff changeset
  1133
    }
71309
wenzelm
parents: 71308
diff changeset
  1134
71311
e169a04e4d3b clarified signature;
wenzelm
parents: 71310
diff changeset
  1135
    def the_repository(phid: String): API.Repository =
e169a04e4d3b clarified signature;
wenzelm
parents: 71310
diff changeset
  1136
      get_repositories(phid = phid) match {
e169a04e4d3b clarified signature;
wenzelm
parents: 71310
diff changeset
  1137
        case List(repo) => repo
71314
5b68cc73f8b1 clarified signature;
wenzelm
parents: 71311
diff changeset
  1138
        case _ => error("Bad repository PHID " + quote(phid))
71311
e169a04e4d3b clarified signature;
wenzelm
parents: 71310
diff changeset
  1139
      }
e169a04e4d3b clarified signature;
wenzelm
parents: 71310
diff changeset
  1140
71309
wenzelm
parents: 71308
diff changeset
  1141
    def create_repository(
wenzelm
parents: 71308
diff changeset
  1142
      name: String,
wenzelm
parents: 71308
diff changeset
  1143
      callsign: String = "",    // unique name, UPPERCASE
wenzelm
parents: 71308
diff changeset
  1144
      short_name: String = "",  // unique name
wenzelm
parents: 71308
diff changeset
  1145
      description: String = "",
wenzelm
parents: 71308
diff changeset
  1146
      public: Boolean = false,
78602
92b6958e8787 clarified signature: prefer enum types;
wenzelm
parents: 77567
diff changeset
  1147
      vcs: API.VCS = API.VCS.hg
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
  1148
    ): API.Repository = {
73120
c3589f2dff31 more informative errors: simplify diagnosis of spurious failures reported by users;
wenzelm
parents: 72763
diff changeset
  1149
      require(name.nonEmpty, "bad repository name")
71309
wenzelm
parents: 71308
diff changeset
  1150
wenzelm
parents: 71308
diff changeset
  1151
      val transactions =
wenzelm
parents: 71308
diff changeset
  1152
        API.edits("vcs", vcs.toString) :::
wenzelm
parents: 71308
diff changeset
  1153
        API.edits("name", name) :::
wenzelm
parents: 71308
diff changeset
  1154
        API.opt_edits("callsign", proper_string(callsign)) :::
wenzelm
parents: 71308
diff changeset
  1155
        API.opt_edits("shortName", proper_string(short_name)) :::
wenzelm
parents: 71308
diff changeset
  1156
        API.opt_edits("description", proper_string(description)) :::
wenzelm
parents: 71308
diff changeset
  1157
        (if (public) Nil
wenzelm
parents: 71308
diff changeset
  1158
         else API.edits("view", user_phid) ::: API.edits("policy.push", user_phid)) :::
wenzelm
parents: 71308
diff changeset
  1159
        API.edits("status", "active")
wenzelm
parents: 71308
diff changeset
  1160
71310
fd644fb7871b clarified signature;
wenzelm
parents: 71309
diff changeset
  1161
      val phid =
71309
wenzelm
parents: 71308
diff changeset
  1162
        execute("diffusion.repository.edit", params = JSON.Object("transactions" -> transactions))
wenzelm
parents: 71308
diff changeset
  1163
          .get_value(JSON.value(_, "object", JSON.string(_, "phid")))
wenzelm
parents: 71308
diff changeset
  1164
71310
fd644fb7871b clarified signature;
wenzelm
parents: 71309
diff changeset
  1165
      execute("diffusion.looksoon", params = JSON.Object("repositories" -> List(phid))).get
71309
wenzelm
parents: 71308
diff changeset
  1166
71311
e169a04e4d3b clarified signature;
wenzelm
parents: 71310
diff changeset
  1167
      the_repository(phid)
71309
wenzelm
parents: 71308
diff changeset
  1168
    }
71299
51c19a44cfed support for conduit API;
wenzelm
parents: 71295
diff changeset
  1169
  }
70967
79736ffe77c3 some support for Phabricator server;
wenzelm
parents:
diff changeset
  1170
}