src/Doc/System/Phabricator.thy
author wenzelm
Fri, 27 Dec 2019 16:02:23 +0100
changeset 71556 3c4c171344f4
parent 71538 2217c731d228
child 71571 597059a44d6f
permissions -rw-r--r--
more examples;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
     1
(*:maxLineLen=78:*)
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
     2
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
     3
theory Phabricator
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
     4
imports Base
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
     5
begin
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
     6
71531
0256ce61f405 more documentation;
wenzelm
parents: 71505
diff changeset
     7
chapter \<open>Phabricator server setup \label{ch:phabricator}\<close>
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
     8
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
     9
text \<open>
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    10
  Phabricator\<^footnote>\<open>\<^url>\<open>https://www.phacility.com/phabricator\<close>\<close> is an open-source
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    11
  product to support the development process of complex software projects
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    12
  (open or closed ones). The official slogan is:
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    13
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    14
  \begin{quote}
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    15
    Discuss. Plan. Code. Review. Test. \\
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    16
    Every application your project needs, all in one tool.
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    17
  \end{quote}
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    18
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    19
  Ongoing changes and discussions about changes are maintained uniformly
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    20
  within a MySQL database. There are standard connections to major version
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    21
  control systems: \<^bold>\<open>Subversion\<close>, \<^bold>\<open>Mercurial\<close>, \<^bold>\<open>Git\<close>. So Phabricator offers
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    22
  a counter-model to trends of monoculture and centralized version control,
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    23
  especially due to Microsoft's Github and Atlassian's Bitbucket.
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    24
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    25
  The small company behind Phabricator provides paid plans for support and
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
    26
  hosting of servers, but it is easy to do \<^emph>\<open>independent self-hosting\<close> on a
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
    27
  standard LAMP server (Linux, Apache, MySQL, PHP). This merely requires a
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
    28
  virtual machine on the Net, which can be rented cheaply from local hosting
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
    29
  providers --- there is no need to follow big cloud corporations. So it is
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
    30
  feasible to remain the master of your virtual home, following the slogan
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
    31
  ``own all your data''. In many respects, Phabricator is similar to the
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
    32
  well-known Nextcloud\<^footnote>\<open>\<^url>\<open>https://nextcloud.org\<close>\<close> product, concerning both
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
    33
  the technology and sociology.
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    34
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    35
  \<^medskip>
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    36
  The following Phabricator instances may serve as examples:
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    37
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    38
    \<^item> Phabricator development \<^url>\<open>https://secure.phabricator.com\<close>
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    39
    \<^item> Wikimedia development \<^url>\<open>https://phabricator.wikimedia.org\<close>
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
    40
    \<^item> Blender development \<^url>\<open>https://developer.blender.org\<close>
71556
3c4c171344f4 more examples;
wenzelm
parents: 71538
diff changeset
    41
    \<^item> LLVM development \<^url>\<open>https://reviews.llvm.org\<close>
3c4c171344f4 more examples;
wenzelm
parents: 71538
diff changeset
    42
    \<^item> Mozilla development \<^url>\<open>https://phabricator.services.mozilla.com\<close>
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    43
    \<^item> Mercurial development \<^url>\<open>https://phab.mercurial-scm.org\<close>
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    44
    \<^item> Isabelle development \<^url>\<open>https://isabelle-dev.sketis.net\<close>
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    45
71505
71ea54e851ad tuned documentation;
wenzelm
parents: 71504
diff changeset
    46
  \<^medskip>
71ea54e851ad tuned documentation;
wenzelm
parents: 71504
diff changeset
    47
  Initial Phabricator configuration requires many details to be done right.
71ea54e851ad tuned documentation;
wenzelm
parents: 71504
diff changeset
    48
  Isabelle provides some command-line tools to help with the setup, and
71ea54e851ad tuned documentation;
wenzelm
parents: 71504
diff changeset
    49
  afterwards Isabelle support is optional: it is possible to run and maintain
71ea54e851ad tuned documentation;
wenzelm
parents: 71504
diff changeset
    50
  the server, without requiring the somewhat bulky Isabelle distribution
71ea54e851ad tuned documentation;
wenzelm
parents: 71504
diff changeset
    51
  again.
71531
0256ce61f405 more documentation;
wenzelm
parents: 71505
diff changeset
    52
0256ce61f405 more documentation;
wenzelm
parents: 71505
diff changeset
    53
  \<^medskip>
0256ce61f405 more documentation;
wenzelm
parents: 71505
diff changeset
    54
  Assuming an existing Phabricator installation, the command-line tool @{tool
0256ce61f405 more documentation;
wenzelm
parents: 71505
diff changeset
    55
  hg_setup} (\secref{sec:hg-setup}) helps to create new repositories or to
0256ce61f405 more documentation;
wenzelm
parents: 71505
diff changeset
    56
  migrate old ones. In particular, this avoids the lengthy sequence of clicks
0256ce61f405 more documentation;
wenzelm
parents: 71505
diff changeset
    57
  in Phabricator to make a new private repository with hosting on the server.
0256ce61f405 more documentation;
wenzelm
parents: 71505
diff changeset
    58
  (Phabricator is a software project management platform, where initial
0256ce61f405 more documentation;
wenzelm
parents: 71505
diff changeset
    59
  repository setup happens rarely in practice.)
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    60
\<close>
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    61
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    62
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    63
section \<open>Quick start\<close>
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    64
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    65
text \<open>
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
    66
  The starting point is a fresh installation of \<^bold>\<open>Ubuntu 18.04
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
    67
  LTS\<close>\<^footnote>\<open>\<^url>\<open>https://ubuntu.com/download\<close>\<close>: this version is mandatory due to
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
    68
  subtle dependencies on system packages and configuration that is assumed by
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
    69
  the Isabelle setup tool.
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    70
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    71
  For production use, a proper \<^emph>\<open>Virtual Server\<close> or \<^emph>\<open>Root Server\<close> product
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    72
  from a hosting provider will be required, including an Internet Domain Name
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
    73
  (\secref{sec:phabricator-domain}).
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    74
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    75
  Initial experimentation also works on a local host, e.g.\ via
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
    76
  VirtualBox\<^footnote>\<open>\<^url>\<open>https://www.virtualbox.org\<close>\<close>. The public domain \<^verbatim>\<open>lvh.me\<close> is
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
    77
  used by default: it maps arbitrary subdomains to \<^verbatim>\<open>localhost\<close>.
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    78
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    79
  All administrative commands need to be run as \<^verbatim>\<open>root\<close> user (e.g.\ via
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
    80
  \<^verbatim>\<open>sudo\<close>). Note that Isabelle refers to user-specific configuration in the
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
    81
  user home directory via @{setting ISABELLE_HOME_USER}
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
    82
  (\secref{sec:settings}); that may be different or absent for the root user
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
    83
  and thus cause confusion.
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    84
\<close>
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    85
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    86
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    87
subsection \<open>Initial setup\<close>
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    88
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    89
text \<open>
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
    90
  Isabelle can manage multiple named Phabricator installations: this allows to
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
    91
  separate administrative responsibilities, e.g.\ different approaches to user
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
    92
  management for different projects. Subsequently we always use the default
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
    93
  name ``\<^verbatim>\<open>vcs\<close>'': the name will appear in file and directory locations,
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
    94
  internal database names and URLs.
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    95
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
    96
  The initial setup works as follows (with full Linux package upgrade):
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    97
71489
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: 71488
diff changeset
    98
  @{verbatim [display] \<open>  isabelle phabricator_setup -U -M:\<close>}
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
    99
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   100
  After installing many packages, cloning the Phabricator distribution,
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   101
  initializing the MySQL database and Apache, the tool prints an URL for
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   102
  further configuration. Now the following needs to be provided by the web
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   103
  interface.
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   104
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   105
    \<^item> An initial user that will get administrator rights. There is no need to
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   106
    create a special \<^verbatim>\<open>admin\<close> account. Instead, a regular user that will take
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   107
    over this responsibility can be used here. Subsequently we assume that
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   108
    user \<^verbatim>\<open>makarius\<close> becomes the initial administrator.
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   109
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   110
    \<^item> An \<^emph>\<open>Auth Provider\<close> to manage user names and passwords. None is provided
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   111
    by default, and Phabricator points out this omission prominently in its
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   112
    overview of \<^emph>\<open>Setup Issues\<close>: following these hints quickly leads to the
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   113
    place where a regular \<^emph>\<open>Username/Password\<close> provider can be added.
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   114
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   115
    Alternatively, Phabricator can delegate the responsibility of
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   116
    authentication to big corporations like Google and Facebook, but these can
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   117
    be easily ignored. Genuine self-hosting means to manage users directly,
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   118
    without outsourcing of authentication.
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   119
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   120
    \<^item> A proper password for the administrator can now be set, e.g.\ by the
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   121
    following command:
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   122
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   123
    @{verbatim [display] \<open>  isabelle phabricator bin/auth recover makarius\<close>}
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   124
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   125
    The printed URL gives access to a login and password dialog in the web
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   126
    interface.
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   127
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   128
    Any further users will be able to provide a password directly, because the
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   129
    Auth Provider is already active.
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   130
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   131
    \<^item> The list of Phabricator \<^bold>\<open>Setup Issues\<close> should be studied with some
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   132
    care, to make sure that no serious problems are remaining. For example,
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   133
    the request to lock the configuration can be fulfilled as follows:
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   134
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   135
    @{verbatim [display] \<open>  isabelle phabricator bin/auth lock\<close>}
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   136
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   137
    \<^medskip> A few other Setup Issues might be relevant as well, e.g.\ the timezone
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   138
    of the server. Some more exotic points can be ignored: Phabricator
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   139
    provides careful explanations about what it thinks could be wrong, while
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   140
    leaving some room for interpretation.
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   141
\<close>
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   142
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   143
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   144
subsection \<open>Mailer configuration\<close>
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   145
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   146
text \<open>
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   147
  The next important thing is messaging: Phabricator needs to be able to
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   148
  communicate with users on its own account, e.g.\ to reset passwords. The
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   149
  documentation has many variations on \<^emph>\<open>Configuring Outbound
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   150
  Email\<close>\<^footnote>\<open>\<^url>\<open>https://secure.phabricator.com/book/phabricator/article/configuring_outbound_email\<close>\<close>,
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   151
  but a conventional SMTP server with a dedicated \<^verbatim>\<open>phabricator\<close> user is
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   152
  sufficient. There is no need to run a separate mail server on the
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   153
  self-hosted Linux machine: hosting providers often include such a service
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   154
  for free, e.g.\ as part of a web-hosting package. As a last resort it is
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   155
  also possible to use a corporate service like Gmail, but such dependency
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   156
  dilutes the whole effort of self-hosting.
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   157
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   158
  \<^medskip>
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   159
  Mailer configuration requires a few command-line invocations as follows:
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   160
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   161
  @{verbatim [display] \<open>  isabelle phabricator_setup_mail\<close>}
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   162
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   163
  \<^noindent> This generates a JSON template file for the the mail account details.
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   164
  After editing that, the subsequent command will add and test it with
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   165
  Phabricator:
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   166
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   167
  @{verbatim [display] \<open>  isabelle phabricator_setup_mail -T makarius\<close>}
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   168
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   169
  This tells Phabricator to send a message to the administrator created
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   170
  before; the output informs about success or errors.
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   171
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   172
  The mail configuration process can be refined and repeated until it works
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   173
  properly: host name, port number, protocol etc.\ all need to be correct. The
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   174
  \<^verbatim>\<open>key\<close> field in the JSON file identifies the name of the configuration that
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   175
  will be overwritten each time, when taking over the parameters via
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   176
  \<^verbatim>\<open>isabelle phabricator_setup_mail\<close>.
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   177
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   178
  \<^medskip>
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   179
  The effective mail configuration can be queried like this:
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   180
71302
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   181
  @{verbatim [display] \<open>  isabelle phabricator bin/config get cluster.mailers\<close>}
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   182
\<close>
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   183
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   184
71330
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   185
subsection \<open>SSH configuration\<close>
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   186
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   187
text \<open>
71532
7c27a379190f tuned documentation;
wenzelm
parents: 71531
diff changeset
   188
  SSH configuration is important to access hosted repositories with public-key
7c27a379190f tuned documentation;
wenzelm
parents: 71531
diff changeset
   189
  authentication. It is done by a separate tool, because it affects the
7c27a379190f tuned documentation;
wenzelm
parents: 71531
diff changeset
   190
  operating-system and all installations of Phabricator simultaneously.
71330
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   191
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   192
  The subsequent configuration is convenient (and ambitious): it takes away
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   193
  the standard port 22 from the operating system and assigns it to
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   194
  Isabelle/Phabricator.
71330
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   195
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   196
  @{verbatim [display] \<open>  isabelle phabricator_setup_ssh -p 22 -q 222\<close>}
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   197
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   198
  Afterwards, remote login to the server host needs to use that alternative
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   199
  port 222. If there is a problem connecting again, the administrator can
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   200
  usually access a remote console via some web interface of the virtual server
71476
wenzelm
parents: 71331
diff changeset
   201
  provider.
71330
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   202
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   203
  \<^medskip>
71476
wenzelm
parents: 71331
diff changeset
   204
  The following alternative is more modest: it uses port 2222 for Phabricator,
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   205
  and retains port 22 for the operating system.
71330
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   206
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   207
  @{verbatim [display] \<open>  isabelle phabricator_setup_ssh -p 2222 -q 22\<close>}
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   208
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   209
  \<^medskip>
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   210
  The tool can be invoked multiple times with different parameters; ports are
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   211
  changed back and forth each time and services restarted.
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   212
\<close>
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   213
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   214
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   215
subsection \<open>Public domain name and HTTPS configuration \label{sec:phabricator-domain}\<close>
71487
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   216
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   217
text \<open>
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   218
  So far the Phabricator server has been accessible only on \<^verbatim>\<open>localhost\<close> (via
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   219
  the alias \<^verbatim>\<open>lvh.me\<close>). Proper configuration of a public Internet domain name
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   220
  (with HTTPS certificate from \<^emph>\<open>Let's Encrypt\<close>) works as follows.
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   221
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   222
    \<^item> Register a subdomain (e.g.\ \<^verbatim>\<open>vcs.example.org\<close>) as an alias for the IP
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   223
    address of the underlying Linux host. This usually works by some web
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   224
    interface of the hosting provider to edit DNS entries; it might require
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   225
    some time for updated DNS records to become publicly available.
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   226
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   227
    \<^item> Edit the Phabricator website configuration file in
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   228
    \<^path>\<open>/etc/apache2/sites-available/\<close> to specify \<^verbatim>\<open>ServerName\<close> and
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   229
    \<^verbatim>\<open>ServerAdmin\<close> like this: @{verbatim [display] \<open>  ServerName vcs.example.org
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   230
  ServerAdmin webmaster@example.org\<close>}
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   231
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   232
    Then reload (or restart) Apache like this:
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   233
    @{verbatim [display] \<open>  systemctl reload apache2\<close>}
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   234
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   235
    \<^item> Install \<^verbatim>\<open>certbot\<close> from \<^url>\<open>https://certbot.eff.org\<close> following the
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   236
    description for Apache and Ubuntu 18.04 on
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   237
    \<^url>\<open>https://certbot.eff.org/lets-encrypt/ubuntubionic-apache\<close>. Run
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   238
    \<^verbatim>\<open>certbot\<close> interactively and let it operate on the domain
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   239
    \<^verbatim>\<open>vcs.example.org\<close>.
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   240
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   241
    \<^item> Inform Phabricator about its new domain name like this:
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   242
    @{verbatim [display] \<open>  isabelle phabricator bin/config set \
71487
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   243
    phabricator.base-uri https://vcs.example.org\<close>}
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   244
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   245
    \<^item> Visit the website \<^verbatim>\<open>https://vcs.example.org\<close> and configure Phabricator
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   246
    as described before. The following options are particularly relevant for a
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   247
    public website:
71487
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   248
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   249
      \<^item> \<^emph>\<open>Auth Provider / Username/Password\<close>: disable \<^emph>\<open>Allow Registration\<close> to
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   250
      avoid uncontrolled registrants; users can still be invited via email
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   251
      instead.
71487
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   252
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   253
      \<^item> Enable \<^verbatim>\<open>policy.allow-public\<close> to allow read-only access to resources,
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   254
      without requiring user registration.
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   255
\<close>
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   256
197aa6b57a83 more documentation;
wenzelm
parents: 71485
diff changeset
   257
71505
71ea54e851ad tuned documentation;
wenzelm
parents: 71504
diff changeset
   258
section \<open>Global data storage and backups \label{sec:phabricator-backup}\<close>
71480
58aa62b8c6d3 more documentation;
wenzelm
parents: 71476
diff changeset
   259
58aa62b8c6d3 more documentation;
wenzelm
parents: 71476
diff changeset
   260
text \<open>
58aa62b8c6d3 more documentation;
wenzelm
parents: 71476
diff changeset
   261
  The global state of a Phabricator installation consists of two main parts:
58aa62b8c6d3 more documentation;
wenzelm
parents: 71476
diff changeset
   262
58aa62b8c6d3 more documentation;
wenzelm
parents: 71476
diff changeset
   263
    \<^enum> The \<^emph>\<open>root directory\<close> according to
58aa62b8c6d3 more documentation;
wenzelm
parents: 71476
diff changeset
   264
    \<^path>\<open>/etc/isabelle-phabricator.conf\<close> or \<^verbatim>\<open>isabelle phabricator -l\<close>: it
58aa62b8c6d3 more documentation;
wenzelm
parents: 71476
diff changeset
   265
    contains the main PHP program suite with administrative tools, and some
58aa62b8c6d3 more documentation;
wenzelm
parents: 71476
diff changeset
   266
    configuration files. The default setup also puts hosted repositories here
58aa62b8c6d3 more documentation;
wenzelm
parents: 71476
diff changeset
   267
    (subdirectory \<^verbatim>\<open>repo\<close>).
58aa62b8c6d3 more documentation;
wenzelm
parents: 71476
diff changeset
   268
58aa62b8c6d3 more documentation;
wenzelm
parents: 71476
diff changeset
   269
    \<^enum> Multiple \<^emph>\<open>MySQL databases\<close> with a common prefix derived from the
58aa62b8c6d3 more documentation;
wenzelm
parents: 71476
diff changeset
   270
    installation name --- the same name is used as database user name.
58aa62b8c6d3 more documentation;
wenzelm
parents: 71476
diff changeset
   271
71538
2217c731d228 tuned documentation;
wenzelm
parents: 71532
diff changeset
   272
  The root user may invoke \<^verbatim>\<open>/usr/local/bin/isabelle-phabricator-dump\<close> to
2217c731d228 tuned documentation;
wenzelm
parents: 71532
diff changeset
   273
  create a complete database dump within the root directory. Afterwards it is
2217c731d228 tuned documentation;
wenzelm
parents: 71532
diff changeset
   274
  sufficient to make a conventional \<^bold>\<open>file-system backup\<close> of everything. To
71480
58aa62b8c6d3 more documentation;
wenzelm
parents: 71476
diff changeset
   275
  restore the database state, see the explanations on \<^verbatim>\<open>mysqldump\<close> in
71538
2217c731d228 tuned documentation;
wenzelm
parents: 71532
diff changeset
   276
  \<^url>\<open>https://secure.phabricator.com/book/phabricator/article/configuring_backups\<close>;
2217c731d228 tuned documentation;
wenzelm
parents: 71532
diff changeset
   277
  some background information is in
2217c731d228 tuned documentation;
wenzelm
parents: 71532
diff changeset
   278
  \<^url>\<open>https://secure.phabricator.com/book/phabflavor/article/so_many_databases\<close>.
71488
2e873da296ae more documentation;
wenzelm
parents: 71487
diff changeset
   279
2e873da296ae more documentation;
wenzelm
parents: 71487
diff changeset
   280
  \<^medskip> The following command-line tools are particularly interesting for advanced
2e873da296ae more documentation;
wenzelm
parents: 71487
diff changeset
   281
  database maintenance (within the Phabricator root directory):
2e873da296ae more documentation;
wenzelm
parents: 71487
diff changeset
   282
  @{verbatim [display] \<open>  phabricator/bin/storage help dump
2e873da296ae more documentation;
wenzelm
parents: 71487
diff changeset
   283
  phabricator/bin/storage help shell
2e873da296ae more documentation;
wenzelm
parents: 71487
diff changeset
   284
  phabricator/bin/storage help destroy
2e873da296ae more documentation;
wenzelm
parents: 71487
diff changeset
   285
  phabricator/bin/storage help renamespace\<close>}
2e873da296ae more documentation;
wenzelm
parents: 71487
diff changeset
   286
2e873da296ae more documentation;
wenzelm
parents: 71487
diff changeset
   287
  For example, copying a database snapshot from one installation to another
2e873da296ae more documentation;
wenzelm
parents: 71487
diff changeset
   288
  works as follows. Run on the first installation root directory:
2e873da296ae more documentation;
wenzelm
parents: 71487
diff changeset
   289
2e873da296ae more documentation;
wenzelm
parents: 71487
diff changeset
   290
  @{verbatim [display] \<open>  phabricator/bin/storage dump > dump1.sql
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   291
  phabricator/bin/storage renamespace --from phabricator_vcs \
71488
2e873da296ae more documentation;
wenzelm
parents: 71487
diff changeset
   292
    --to phabricator_xyz --input dump1.sql --output dump2.sql\<close>}
2e873da296ae more documentation;
wenzelm
parents: 71487
diff changeset
   293
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   294
  Them run on the second installation root directory:
71488
2e873da296ae more documentation;
wenzelm
parents: 71487
diff changeset
   295
  @{verbatim [display] \<open>  phabricator/bin/storage destroy
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   296
  phabricator/bin/storage shell < .../dump2.sql\<close>}
71488
2e873da296ae more documentation;
wenzelm
parents: 71487
diff changeset
   297
2e873da296ae more documentation;
wenzelm
parents: 71487
diff changeset
   298
  Local configuration in \<^verbatim>\<open>phabricator/config/local/\<close> and hosted repositories
2e873da296ae more documentation;
wenzelm
parents: 71487
diff changeset
   299
  need to be treated separately within the file-system. For the latter
2e873da296ae more documentation;
wenzelm
parents: 71487
diff changeset
   300
  see also these tools:
2e873da296ae more documentation;
wenzelm
parents: 71487
diff changeset
   301
  @{verbatim [display] \<open>  phabricator/bin/repository help list-paths
2e873da296ae more documentation;
wenzelm
parents: 71487
diff changeset
   302
  phabricator/bin/repository help move-paths\<close>}
71480
58aa62b8c6d3 more documentation;
wenzelm
parents: 71476
diff changeset
   303
\<close>
58aa62b8c6d3 more documentation;
wenzelm
parents: 71476
diff changeset
   304
58aa62b8c6d3 more documentation;
wenzelm
parents: 71476
diff changeset
   305
71495
058edb8f232c more documentation;
wenzelm
parents: 71489
diff changeset
   306
section \<open>Upgrading Phabricator installations\<close>
058edb8f232c more documentation;
wenzelm
parents: 71489
diff changeset
   307
058edb8f232c more documentation;
wenzelm
parents: 71489
diff changeset
   308
text \<open>
058edb8f232c more documentation;
wenzelm
parents: 71489
diff changeset
   309
  The Phabricator developers publish a new version approx.\ every 1--4 weeks:
058edb8f232c more documentation;
wenzelm
parents: 71489
diff changeset
   310
  see also \<^url>\<open>https://secure.phabricator.com/w/changelog\<close>. There is no need to
058edb8f232c more documentation;
wenzelm
parents: 71489
diff changeset
   311
  follow such frequent updates on the spot, but it is a good idea to upgrade
71505
71ea54e851ad tuned documentation;
wenzelm
parents: 71504
diff changeset
   312
  occasionally --- after dump and/or backup (\secref{sec:phabricator-backup}).
71495
058edb8f232c more documentation;
wenzelm
parents: 71489
diff changeset
   313
058edb8f232c more documentation;
wenzelm
parents: 71489
diff changeset
   314
  The Isabelle/Phabricator setup provides a convenience tool to upgrade all
058edb8f232c more documentation;
wenzelm
parents: 71489
diff changeset
   315
  installations uniformly:
058edb8f232c more documentation;
wenzelm
parents: 71489
diff changeset
   316
  @{verbatim [display] \<open>  /usr/local/bin/isabelle-phabricator-upgrade\<close>}
058edb8f232c more documentation;
wenzelm
parents: 71489
diff changeset
   317
058edb8f232c more documentation;
wenzelm
parents: 71489
diff changeset
   318
  This refers to the \<^verbatim>\<open>stable\<close> branch of the distribution repositories by
058edb8f232c more documentation;
wenzelm
parents: 71489
diff changeset
   319
  default. Alternatively, it also possible to use the \<^verbatim>\<open>master\<close> like this:
058edb8f232c more documentation;
wenzelm
parents: 71489
diff changeset
   320
  @{verbatim [display] \<open>  /usr/local/bin/isabelle-phabricator-upgrade master\<close>}
71505
71ea54e851ad tuned documentation;
wenzelm
parents: 71504
diff changeset
   321
71ea54e851ad tuned documentation;
wenzelm
parents: 71504
diff changeset
   322
  \<^medskip>
71ea54e851ad tuned documentation;
wenzelm
parents: 71504
diff changeset
   323
  See
71ea54e851ad tuned documentation;
wenzelm
parents: 71504
diff changeset
   324
  \<^url>\<open>https://secure.phabricator.com/book/phabricator/article/upgrading\<close> for
71ea54e851ad tuned documentation;
wenzelm
parents: 71504
diff changeset
   325
  further explanations on Phabricator upgrade.
71495
058edb8f232c more documentation;
wenzelm
parents: 71489
diff changeset
   326
\<close>
058edb8f232c more documentation;
wenzelm
parents: 71489
diff changeset
   327
058edb8f232c more documentation;
wenzelm
parents: 71489
diff changeset
   328
71302
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   329
section \<open>Reference of command-line tools\<close>
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   330
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   331
text \<open>
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   332
  The subsequent command-line tools usually require root user privileges on
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   333
  the underlying Linux system (e.g.\ via \<^verbatim>\<open>sudo bash\<close> to open a subshell, or
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   334
  directly via \<^verbatim>\<open>sudo isabelle phabricator ...\<close>).
71302
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   335
\<close>
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   336
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   337
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   338
subsection \<open>\<^verbatim>\<open>isabelle phabricator\<close>\<close>
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   339
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   340
text \<open>
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   341
  The @{tool_def phabricator} tool invokes a GNU bash command-line within the
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   342
  Phabricator home directory:
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   343
  @{verbatim [display]
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   344
\<open>Usage: isabelle phabricator [OPTIONS] COMMAND [ARGS...]
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   345
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   346
  Options are:
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   347
    -l           list available Phabricator installations
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   348
    -n NAME      Phabricator installation name (default: "vcs")
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   349
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   350
  Invoke a command-line tool within the home directory of the named
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   351
  Phabricator installation.\<close>}
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   352
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   353
  Isabelle/Phabricator installations are registered in the global
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   354
  configuration file \<^path>\<open>/etc/isabelle-phabricator.conf\<close>, with name and
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   355
  root directory separated by colon (no extra whitespace). The home directory
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   356
  is the subdirectory \<^verbatim>\<open>phabricator\<close> within the root.
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   357
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   358
  \<^medskip> Option \<^verbatim>\<open>-l\<close> lists the available Phabricator installations with name and
71485
b4401dfd6544 clarified "isabelle phabricator -l": avoid surprise with non-existent default installation;
wenzelm
parents: 71480
diff changeset
   359
  root directory --- without invoking a command.
71302
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   360
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   361
  Option \<^verbatim>\<open>-n\<close> selects the explicitly named Phabricator installation.
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   362
\<close>
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   363
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   364
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   365
subsubsection \<open>Examples\<close>
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   366
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   367
text \<open>
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   368
  Print the home directory of the Phabricator installation:
71330
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   369
  @{verbatim [display] \<open>  isabelle phabricator pwd\<close>}
71302
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   370
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   371
  Print some Phabricator configuration information:
71330
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   372
  @{verbatim [display] \<open>  isabelle phabricator bin/config get phabricator.base-uri\<close>}
71302
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   373
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   374
  The latter conforms to typical command templates seen in the original
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   375
  Phabricator documentation:
71330
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   376
  @{verbatim [display] \<open>  phabricator/ $ ./bin/config get phabricator.base-uri\<close>}
71302
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   377
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   378
  Here the user is meant to navigate to the Phabricator home manually, in
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   379
  contrast to \<^verbatim>\<open>isabelle phabricator\<close> doing it automatically thanks to the
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   380
  global configuration \<^path>\<open>/etc/isabelle-phabricator.conf\<close>.
71302
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   381
\<close>
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   382
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   383
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   384
subsection \<open>\<^verbatim>\<open>isabelle phabricator_setup\<close>\<close>
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   385
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   386
text \<open>
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   387
  The @{tool_def phabricator_setup} tool installs a fresh Phabricator instance
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   388
  on Ubuntu 18.04 LTS:
71302
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   389
  @{verbatim [display] \<open>Usage: isabelle phabricator_setup [OPTIONS]
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   390
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   391
  Options are:
71489
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: 71488
diff changeset
   392
    -M SOURCE    install Mercurial from source: local PATH, or URL, or ":"
71302
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   393
    -R DIR       repository directory (default: "/var/www/phabricator-NAME/repo")
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   394
    -U           full update of system packages before installation
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   395
    -n NAME      Phabricator installation name (default: "vcs")
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   396
    -r DIR       installation root directory (default: "/var/www/phabricator-NAME")
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   397
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   398
  Install Phabricator as LAMP application (Linux, Apache, MySQL, PHP).
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   399
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   400
  The installation name (default: "vcs") is mapped to a regular
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   401
  Unix user; this is relevant for public SSH access.\<close>}
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   402
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   403
  Installation requires Linux root permissions. All required packages are
71302
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   404
  installed automatically beforehand, this includes the Apache web server and
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   405
  the MySQL database engine.
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   406
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   407
  Global configuration in \<^verbatim>\<open>/etc\<close> or a few other directories like \<^verbatim>\<open>/var/www\<close>
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   408
  uses name prefixes like \<^verbatim>\<open>isabelle-phabricator\<close> or \<^verbatim>\<open>phabricator\<close>. Local
71302
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   409
  configuration for a particular installation uses more specific names derived
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   410
  from \<^verbatim>\<open>phabricator-\<close>\<open>NAME\<close>, e.g.\ \<^verbatim>\<open>/var/www/phabricator-vcs\<close> for the
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   411
  default.
71302
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   412
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   413
  Knowing the naming conventions, it is possible to purge a Linux installation
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   414
  from Isabelle/Phabricator with some effort, but there is no automated
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   415
  procedure for de-installation. In the worst case, it might be better to
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   416
  re-install the virtual machine from a clean image.
71302
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   417
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   418
  \<^medskip>
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   419
  Option \<^verbatim>\<open>-U\<close> ensures a full update of system packages, before installing
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   420
  further packages required by Phabricator. This might require a reboot.
71302
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   421
71489
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: 71488
diff changeset
   422
  Option \<^verbatim>\<open>-M:\<close> installs a standard Mercurial release from source: this works
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: 71488
diff changeset
   423
  better than the package provided by Ubuntu 18.04. Alternatively, an explicit
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: 71488
diff changeset
   424
  file path or URL the source archive (\<^verbatim>\<open>.tar.gz\<close>) may be here. This option is
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: 71488
diff changeset
   425
  recommended for production use, but it requires to \<^emph>\<open>uninstall\<close> existing
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: 71488
diff changeset
   426
  Mercurial packages provided by the operating system.
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: 71488
diff changeset
   427
71302
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   428
  Option \<^verbatim>\<open>-n\<close> provides an alternative installation name. The default name
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   429
  \<^verbatim>\<open>vcs\<close> means ``version control system''. The name appears in the URL for SSH
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   430
  access, and thus has some relevance to end-users. The initial server URL
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   431
  also uses the same suffix, but that can (and should) be changed later via
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   432
  regular Apache configuration.
71302
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   433
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   434
  Option \<^verbatim>\<open>-r\<close> specifies an alternative installation root directory: it needs
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   435
  to be accessible for the Apache web server.
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   436
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   437
  Option \<^verbatim>\<open>-R\<close> specifies an alternative directory for repositories that are
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   438
  hosted by Phabricator. Provided that it is accessible for the Apache web
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   439
  server, the directory can be reused for the \<^verbatim>\<open>hgweb\<close> view by Mercurial.\<^footnote>\<open>See
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   440
  also the documentation
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   441
  \<^url>\<open>https://www.mercurial-scm.org/wiki/PublishingRepositories\<close> and the
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   442
  example \<^url>\<open>https://isabelle.sketis.net/repos\<close>.\<close>
71302
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   443
\<close>
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   444
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   445
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   446
subsection \<open>\<^verbatim>\<open>isabelle phabricator_setup_mail\<close>\<close>
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   447
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   448
text \<open>
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   449
  The @{tool_def phabricator_setup_mail} tool provides mail configuration for
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   450
  an existing Phabricator installation:
71302
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   451
  @{verbatim [display] \<open>Usage: isabelle phabricator_setup_mail [OPTIONS]
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   452
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   453
  Options are:
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   454
    -T USER      send test mail to Phabricator user
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   455
    -f FILE      config file (default: "mailers.json" within
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   456
                 Phabricator root)
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   457
    -n NAME      Phabricator installation name (default: "vcs")
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   458
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   459
  Provide mail configuration for existing Phabricator installation.\<close>}
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   460
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   461
  Proper mail configuration is vital for Phabricator, but the details can be
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   462
  tricky. A common approach is to re-use an existing SMTP mail service, as is
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   463
  often included in regular web hosting packages. It is sufficient to create
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   464
  one mail account for multiple Phabricator installations, but the
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   465
  configuration needs to be set for each installation.
71302
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   466
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   467
  The first invocation of \<^verbatim>\<open>isabelle phabricator_setup_mail\<close> without options
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   468
  creates a JSON template file. Its \<^verbatim>\<open>key\<close> entry should be changed to
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   469
  something sensible to identify the configuration, e.g.\ the Internet Domain
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   470
  Name of the mail address. The \<^verbatim>\<open>options\<close> specify the SMTP server address and
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   471
  account information.
71302
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   472
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   473
  Another invocation of \<^verbatim>\<open>isabelle phabricator_setup_mail\<close> with updated JSON
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   474
  file will change the underlying Phabricator installation. This can be done
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   475
  repeatedly, until everything works as expected.
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   476
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   477
  Option \<^verbatim>\<open>-T\<close> invokes a standard Phabricator test procedure for the mail
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   478
  configuration. The argument needs to be a valid Phabricator user: the mail
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   479
  address is derived from the user profile.
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   480
c073c4e79518 more documentation;
wenzelm
parents: 71298
diff changeset
   481
  Option \<^verbatim>\<open>-f\<close> refers to an existing JSON configuration file, e.g.\ from a
71329
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   482
  previous successful Phabricator installation: sharing mailers setup with the
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   483
  same mail address is fine for outgoing mails; incoming mails are optional
1579a9160c7f misc tuning and clarification;
wenzelm
parents: 71304
diff changeset
   484
  and not configured here.
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   485
\<close>
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   486
71330
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   487
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   488
subsection \<open>\<^verbatim>\<open>isabelle phabricator_setup_ssh\<close>\<close>
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   489
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   490
text \<open>
71499
8d21cba3bad4 tuned documentation;
wenzelm
parents: 71495
diff changeset
   491
  The @{tool_def phabricator_setup_ssh} tool configures a special SSH service
71330
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   492
  for all Phabricator installations:
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   493
  @{verbatim [display] \<open>Usage: isabelle phabricator_setup_ssh [OPTIONS]
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   494
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   495
  Options are:
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   496
    -p PORT      sshd port for Phabricator servers (default: 2222)
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   497
    -q PORT      sshd port for the operating system (default: 22)
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   498
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   499
  Configure ssh service for all Phabricator installations: a separate sshd
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   500
  is run in addition to the one of the operating system, and ports need to
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   501
  be distinct.
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   502
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   503
  A particular Phabricator installation is addressed by using its
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   504
  name as the ssh user; the actual Phabricator user is determined via
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   505
  stored ssh keys.\<close>}
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   506
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   507
  This is optional, but very useful. It allows to refer to hosted repositories
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   508
  via ssh with the usual public-key authentication. It also allows to
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   509
  communicate with a Phabricator server via the JSON API of
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   510
  \<^emph>\<open>Conduit\<close>\<^footnote>\<open>\<^url>\<open>https://secure.phabricator.com/book/phabricator/article/conduit\<close>\<close>.
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   511
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   512
  \<^medskip> The Phabricator SSH server distinguishes installations by their name,
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   513
  e.g.\ \<^verbatim>\<open>vcs\<close> as SSH user name. The public key that is used for
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   514
  authentication identifies the user within Phabricator: there is a web
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   515
  interface to provide that as part of the user profile.
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   516
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   517
  The operating system already has an SSH server (by default on port 22) that
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   518
  remains important for remote administration of the machine.
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   519
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   520
  \<^medskip>
71501
8b745b4d71b5 more rebust setup for Subversion -- assuming that diffusion.ssh-port is only set in phabricator/conf/local/local.json, not in the database;
wenzelm
parents: 71499
diff changeset
   521
  Options \<^verbatim>\<open>-p\<close> and \<^verbatim>\<open>-q\<close> allow to change the port assignment for both
8b745b4d71b5 more rebust setup for Subversion -- assuming that diffusion.ssh-port is only set in phabricator/conf/local/local.json, not in the database;
wenzelm
parents: 71499
diff changeset
   522
  servers. A common scheme is \<^verbatim>\<open>-p 22 -q 222\<close> to leave the standard port to
71330
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   523
  Phabricator, to simplify the ssh URL that users will see for remote
71501
8b745b4d71b5 more rebust setup for Subversion -- assuming that diffusion.ssh-port is only set in phabricator/conf/local/local.json, not in the database;
wenzelm
parents: 71499
diff changeset
   524
  repository clones.\<^footnote>\<open>For the rare case of hosting Subversion repositories,
8b745b4d71b5 more rebust setup for Subversion -- assuming that diffusion.ssh-port is only set in phabricator/conf/local/local.json, not in the database;
wenzelm
parents: 71499
diff changeset
   525
  port 22 is de-facto required. Otherwise Phabricator presents malformed
8b745b4d71b5 more rebust setup for Subversion -- assuming that diffusion.ssh-port is only set in phabricator/conf/local/local.json, not in the database;
wenzelm
parents: 71499
diff changeset
   526
  \<^verbatim>\<open>svn+ssh\<close> URLs with port specification.\<close>
71330
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   527
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   528
  Redirecting the operating system sshd to port 222 requires some care: it
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   529
  requires to adjust the remote login procedure, e.g.\ in \<^verbatim>\<open>$HOME/.ssh/config\<close>
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   530
  to add a \<^verbatim>\<open>Port\<close> specification for the server machine.
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   531
\<close>
e5984c853f77 more documentation;
wenzelm
parents: 71329
diff changeset
   532
71298
20c1b9516d27 documentation on Phabricator server administration;
wenzelm
parents:
diff changeset
   533
end