# HG changeset patch
# User wenzelm
# Date 1573489960 -3600
# Node ID 20c1b9516d271396dc972280ab814383fcc68fa5
# Parent  da378866f580b20613a97c505f0d279d9d9e6f68
documentation on Phabricator server administration;

diff -r da378866f580 -r 20c1b9516d27 src/Doc/ROOT
--- a/src/Doc/ROOT	Mon Nov 11 17:00:07 2019 +0100
+++ b/src/Doc/ROOT	Mon Nov 11 17:32:40 2019 +0100
@@ -387,6 +387,7 @@
     Presentation
     Server
     Scala
+    Phabricator
     Misc
   document_files (in "..")
     "prepare_document"
diff -r da378866f580 -r 20c1b9516d27 src/Doc/System/Phabricator.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/System/Phabricator.thy	Mon Nov 11 17:32:40 2019 +0100
@@ -0,0 +1,159 @@
+(*:maxLineLen=78:*)
+
+theory Phabricator
+imports Base
+begin
+
+chapter \<open>Phabricator server administration\<close>
+
+text \<open>
+  Phabricator\<^footnote>\<open>\<^url>\<open>https://www.phacility.com/phabricator\<close>\<close> is an open-source
+  product to support the development process of complex software projects
+  (open or closed ones). The official slogan is:
+
+  \begin{quote}
+    Discuss. Plan. Code. Review. Test. \\
+    Every application your project needs, all in one tool.
+  \end{quote}
+
+  Ongoing changes and discussions about changes are maintained uniformly
+  within a MySQL database. There are standard connections to major version
+  control systems: \<^bold>\<open>Subversion\<close>, \<^bold>\<open>Mercurial\<close>, \<^bold>\<open>Git\<close>. So Phabricator offers
+  a counter-model to trends of monoculture and centralized version control,
+  especially due to Microsoft's Github and Atlassian's Bitbucket.
+
+  The small company behind Phabricator provides paid plans for support and
+  hosting of servers, but it is relatively easy to do \<^emph>\<open>independent
+  self-hosting\<close> on a standard LAMP server (Linux, Apache, MySQL, PHP). This
+  merely requires a virtual Ubuntu server on the net, which can be rented
+  rather cheaply from local hosting providers (there is no need to follow big
+  cloud corporations). So it is feasible to remain the master of your virtual
+  home, following the slogan ``own all your data''. In many respects,
+  Phabricator is similar to the well-known
+  Nextcloud\<^footnote>\<open>\<^url>\<open>https://nextcloud.com\<close>\<close> product, concerning both the
+  technology and sociology.
+
+  \<^medskip>
+  The following Phabricator instances may serve as examples:
+
+    \<^item> Phabricator development \<^url>\<open>https://secure.phabricator.com\<close>
+    \<^item> Wikimedia development \<^url>\<open>https://phabricator.wikimedia.org\<close>
+    \<^item> Mercurial development \<^url>\<open>https://phab.mercurial-scm.org\<close>
+    \<^item> Isabelle development \<^url>\<open>https://isabelle-dev.sketis.net\<close>
+
+  \<^medskip> Initial Phabricator server configuration requires many details to be done
+  right. Isabelle provides some command-line tools to help with it, but
+  afterwards Isabelle support is optional: it is possible to run and maintain
+  the server, without requiring a full Isabelle distribution again.
+\<close>
+
+
+section \<open>Quick start\<close>
+
+text \<open>
+  The starting point is a fresh installation of \<^bold>\<open>Ubuntu 18.04 LTS\<close>: that
+  particular version is required due to subtle dependencies on system
+  configuration and add-on packages.
+
+  For production use, a proper \<^emph>\<open>Virtual Server\<close> or \<^emph>\<open>Root Server\<close> product
+  from a hosting provider will be required, including an Internet Domain Name
+  (a pseudo sub-domain in the style of Apache is sufficient).
+
+  Initial experimentation also works on a local host, e.g.\ via
+  VirtualBox\<^footnote>\<open>\<^url>\<open>https://www.virtualbox.org\<close>\<close>. The public server behind
+  \<^verbatim>\<open>lvh.me\<close> provides arbitrary subdomains as an alias to \<^verbatim>\<open>localhost\<close>, which
+  will be used for the default installation below.
+
+  All administrative commands need to be run as \<^verbatim>\<open>root\<close> user (e.g.\ via
+  \<^verbatim>\<open>sudo\<close>).
+\<close>
+
+
+subsection \<open>Initial setup\<close>
+
+text \<open>
+  Isabelle can managed multiple named installations Phabricator installations:
+  this allows to separate administrative responsibilities, e.g.\ different
+  approaches to user management for different projects. Subsequently we always
+  use the implicit default name ``\<^verbatim>\<open>vcs\<close>'': it will appear in file and
+  directory locations, internal database names and URLs.
+
+  The initial setup (with full Linux package upgrade) works as follows:
+
+  @{verbatim [display] \<open>  isabelle phabricator_setup -U\<close>}
+
+  After installing many packages and cloning the Phabricator distribution, the
+  final output of the tool should be the URL for further manual configuration
+  (using a local web browser). Here the key points are:
+
+    \<^item> An initial user account that will get administrator rights. There is no
+    need to create a separate \<^verbatim>\<open>admin\<close> account. Instead, a regular user that
+    will take over this responsibility can be used here. Subsequently we
+    assume that user \<^verbatim>\<open>makarius\<close> becomes the initial administrator.
+
+    \<^item> An \<^emph>\<open>Auth Provider\<close> to manage user names and passwords. None is provided
+    by default, and Phabricator points out this omission prominently in its
+    overview of \<^emph>\<open>Setup Issues\<close>: following these hints quickly leads to the
+    place where a regular \<^emph>\<open>Username/Password\<close> provider can be added.
+
+  Note that Phabricator allows to delegate the responsibility of
+  authentication to big corporations like Google and Facebook, but these can
+  be easily avoided. Genuine self-hosting means to manage users directly,
+  without outsourcing of authentication.
+
+  \<^medskip>
+  With the Auth Provider available, the administrator can now set a proper
+  password. This works e.g.\ by initiating a local password reset procedure:
+
+  @{verbatim [display] \<open>  isabelle phabricator ./bin/auth recover makarius\<close>}
+
+  The printed URL gives access to a password dialog in the web browser.
+
+  Further users will be able to provide a password more directly, because the
+  Auth Provider is now active.
+
+  \<^medskip>
+  The pending request in Phabricator Setup Issues to lock the configuration
+  can be fulfilled as follows:
+
+  @{verbatim [display] \<open>  isabelle phabricator ./bin/auth lock\<close>}
+\<close>
+
+
+subsection \<open>Mailer configuration\<close>
+
+text \<open>
+  The next important thing is messaging: Phabricator needs to be able to
+  communicate with users. There are many variations on \<^emph>\<open>Mailer
+  Configuration\<close>, but a conventional SMTP server connection with a dedicated
+  \<^verbatim>\<open>phabricator\<close> user is sufficient. Note that there is no need to run a mail
+  server on the self-hosted Linux machine: regular web-hosting packages
+  usually allow to create new mail accounts easily. (As a last resort it is
+  possible to use a service like Gmail, but that would again introduce
+  unnecessary dependency on Google.)
+
+  \<^medskip>
+  Mailer configuration requires a few command-line invocations as follows:
+
+  @{verbatim [display] \<open>  isabelle phabricator_setup_mail\<close>}
+
+  \<^noindent> Now edit the generated JSON file to provide the mail account details. Then
+  add and test it with Phabricator like this (to let Phabricator send a
+  message to the administrator from above):
+
+  @{verbatim [display] \<open>  isabelle phabricator_setup_mail -T makarius\<close>}
+
+  The mail configuration process can be refined and repeated until it really
+  works: host name, port number, protocol etc.\ all need to be correct. The
+  \<^verbatim>\<open>key\<close> field in the JSON file identifies the name of the configuration; it
+  will be overwritten each time, when taking over the parameters via
+  \<^verbatim>\<open>isabelle phabricator_setup_mail\<close>.
+
+  \<^medskip>
+  For information, the resulting mailer configuration can be queried like
+  this:
+
+  @{verbatim [display] \<open>  isabelle phabricator ./bin/config get cluster.mailers\<close>}
+\<close>
+
+end
diff -r da378866f580 -r 20c1b9516d27 src/Doc/System/document/root.tex
--- a/src/Doc/System/document/root.tex	Mon Nov 11 17:00:07 2019 +0100
+++ b/src/Doc/System/document/root.tex	Mon Nov 11 17:32:40 2019 +0100
@@ -35,6 +35,7 @@
 \input{Presentation.tex}
 \input{Server.tex}
 \input{Scala.tex}
+\input{Phabricator.tex}
 \input{Misc.tex}
 
 \begingroup