diff --git a/src/Doc/System/Phabricator.thy b/src/Doc/System/Phabricator.thy
--- a/src/Doc/System/Phabricator.thy
+++ b/src/Doc/System/Phabricator.thy
@@ -1,533 +1,535 @@
 (*:maxLineLen=78:*)
 
 theory Phabricator
 imports Base
 begin
 
 chapter \<open>Phabricator server setup \label{ch:phabricator}\<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 easy to do \<^emph>\<open>independent self-hosting\<close> on a
   standard LAMP server (Linux, Apache, MySQL, PHP). This merely requires a
   virtual machine on the Net, which can be rented 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.org\<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> Blender development \<^url>\<open>https://developer.blender.org\<close>
     \<^item> LLVM development \<^url>\<open>https://reviews.llvm.org\<close>
     \<^item> Mozilla development \<^url>\<open>https://phabricator.services.mozilla.com\<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 configuration requires many details to be done right.
   Isabelle provides some command-line tools to help with the setup, and
   afterwards Isabelle support is optional: it is possible to run and maintain
   the server, without requiring the somewhat bulky Isabelle distribution
   again.
 
   \<^medskip>
   Assuming an existing Phabricator installation, the command-line tool @{tool
   hg_setup} (\secref{sec:hg-setup}) helps to create new repositories or to
   migrate old ones. In particular, this avoids the lengthy sequence of clicks
   in Phabricator to make a new private repository with hosting on the server.
   (Phabricator is a software project management platform, where initial
   repository setup happens rarely in practice.)
 \<close>
 
 
 section \<open>Quick start\<close>
 
 text \<open>
   The starting point is a fresh installation of \<^bold>\<open>Ubuntu 18.04
   LTS\<close>\<^footnote>\<open>\<^url>\<open>https://ubuntu.com/download\<close>\<close>: this version is mandatory due to
   subtle dependencies on system packages and configuration that is assumed by
   the Isabelle setup tool.
 
   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
   (\secref{sec:phabricator-domain}).
 
   Initial experimentation also works on a local host, e.g.\ via
   VirtualBox\<^footnote>\<open>\<^url>\<open>https://www.virtualbox.org\<close>\<close>. The public domain \<^verbatim>\<open>lvh.me\<close> is
   used by default: it maps arbitrary subdomains to \<^verbatim>\<open>localhost\<close>.
 
   All administrative commands need to be run as \<^verbatim>\<open>root\<close> user (e.g.\ via
   \<^verbatim>\<open>sudo\<close>). Note that Isabelle refers to user-specific configuration in the
   user home directory via @{setting ISABELLE_HOME_USER}
   (\secref{sec:settings}); that may be different or absent for the root user
   and thus cause confusion.
 \<close>
 
 
 subsection \<open>Initial setup\<close>
 
 text \<open>
   Isabelle can manage multiple named Phabricator installations: this allows to
   separate administrative responsibilities, e.g.\ different approaches to user
   management for different projects. Subsequently we always use the default
   name ``\<^verbatim>\<open>vcs\<close>'': the name will appear in file and directory locations,
   internal database names and URLs.
 
   The initial setup works as follows (with full Linux package upgrade):
 
   @{verbatim [display] \<open>  isabelle phabricator_setup -U -M:\<close>}
 
   After installing many packages, cloning the Phabricator distribution,
   initializing the MySQL database and Apache, the tool prints an URL for
   further configuration. Now the following needs to be provided by the web
   interface.
 
     \<^item> An initial user that will get administrator rights. There is no need to
     create a special \<^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.
 
     Alternatively, Phabricator can delegate the responsibility of
     authentication to big corporations like Google and Facebook, but these can
     be easily ignored. Genuine self-hosting means to manage users directly,
     without outsourcing of authentication.
 
     \<^item> A proper password for the administrator can now be set, e.g.\ by the
     following command:
 
     @{verbatim [display] \<open>  isabelle phabricator bin/auth recover makarius\<close>}
 
     The printed URL gives access to a login and password dialog in the web
     interface.
 
     Any further users will be able to provide a password directly, because the
     Auth Provider is already active.
 
     \<^item> The list of Phabricator \<^bold>\<open>Setup Issues\<close> should be studied with some
     care, to make sure that no serious problems are remaining. For example,
     the request to lock the configuration can be fulfilled as follows:
 
     @{verbatim [display] \<open>  isabelle phabricator bin/auth lock\<close>}
 
     \<^medskip> A few other Setup Issues might be relevant as well, e.g.\ the timezone
     of the server. Some more exotic points can be ignored: Phabricator
     provides careful explanations about what it thinks could be wrong, while
     leaving some room for interpretation.
 \<close>
 
 
 subsection \<open>Mailer configuration\<close>
 
 text \<open>
   The next important thing is messaging: Phabricator needs to be able to
   communicate with users on its own account, e.g.\ to reset passwords. The
   documentation has many variations on \<^emph>\<open>Configuring Outbound
   Email\<close>\<^footnote>\<open>\<^url>\<open>https://secure.phabricator.com/book/phabricator/article/configuring_outbound_email\<close>\<close>,
   but a conventional SMTP server with a dedicated \<^verbatim>\<open>phabricator\<close> user is
   sufficient. There is no need to run a separate mail server on the
   self-hosted Linux machine: hosting providers often include such a service
   for free, e.g.\ as part of a web-hosting package. As a last resort it is
   also possible to use a corporate service like Gmail, but such dependency
   dilutes the whole effort of self-hosting.
 
   \<^medskip>
   Mailer configuration requires a few command-line invocations as follows:
 
   @{verbatim [display] \<open>  isabelle phabricator_setup_mail\<close>}
 
   \<^noindent> This generates a JSON template file for the the mail account details.
   After editing that, the subsequent command will add and test it with
   Phabricator:
 
   @{verbatim [display] \<open>  isabelle phabricator_setup_mail -T makarius\<close>}
 
   This tells Phabricator to send a message to the administrator created
   before; the output informs about success or errors.
 
   The mail configuration process can be refined and repeated until it works
   properly: 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 that
   will be overwritten each time, when taking over the parameters via
   \<^verbatim>\<open>isabelle phabricator_setup_mail\<close>.
 
   \<^medskip>
   The effective mail configuration can be queried like this:
 
   @{verbatim [display] \<open>  isabelle phabricator bin/config get cluster.mailers\<close>}
 \<close>
 
 
 subsection \<open>SSH configuration\<close>
 
 text \<open>
   SSH configuration is important to access hosted repositories with public-key
   authentication. It is done by a separate tool, because it affects the
   operating-system and all installations of Phabricator simultaneously.
 
   The subsequent configuration is convenient (and ambitious): it takes away
   the standard port 22 from the operating system and assigns it to
   Isabelle/Phabricator.
 
   @{verbatim [display] \<open>  isabelle phabricator_setup_ssh -p 22 -q 222\<close>}
 
   Afterwards, remote login to the server host needs to use that alternative
   port 222. If there is a problem connecting again, the administrator can
   usually access a remote console via some web interface of the virtual server
   provider.
 
   \<^medskip>
   The following alternative is more modest: it uses port 2222 for Phabricator,
   and retains port 22 for the operating system.
 
   @{verbatim [display] \<open>  isabelle phabricator_setup_ssh -p 2222 -q 22\<close>}
 
   \<^medskip>
   The tool can be invoked multiple times with different parameters; ports are
   changed back and forth each time and services restarted.
 \<close>
 
 
 subsection \<open>Public domain name and HTTPS configuration \label{sec:phabricator-domain}\<close>
 
 text \<open>
   So far the Phabricator server has been accessible only on \<^verbatim>\<open>localhost\<close> (via
   the alias \<^verbatim>\<open>lvh.me\<close>). Proper configuration of a public Internet domain name
   (with HTTPS certificate from \<^emph>\<open>Let's Encrypt\<close>) works as follows.
 
     \<^item> Register a subdomain (e.g.\ \<^verbatim>\<open>vcs.example.org\<close>) as an alias for the IP
     address of the underlying Linux host. This usually works by some web
     interface of the hosting provider to edit DNS entries; it might require
     some time for updated DNS records to become publicly available.
 
     \<^item> Edit the Phabricator website configuration file in
     \<^path>\<open>/etc/apache2/sites-available/\<close> to specify \<^verbatim>\<open>ServerName\<close> and
     \<^verbatim>\<open>ServerAdmin\<close> like this: @{verbatim [display] \<open>  ServerName vcs.example.org
   ServerAdmin webmaster@example.org\<close>}
 
     Then reload (or restart) Apache like this:
     @{verbatim [display] \<open>  systemctl reload apache2\<close>}
 
     \<^item> Install \<^verbatim>\<open>certbot\<close> from \<^url>\<open>https://certbot.eff.org\<close> following the
     description for Apache and Ubuntu 18.04 on
     \<^url>\<open>https://certbot.eff.org/lets-encrypt/ubuntubionic-apache\<close>. Run
     \<^verbatim>\<open>certbot\<close> interactively and let it operate on the domain
     \<^verbatim>\<open>vcs.example.org\<close>.
 
     \<^item> Inform Phabricator about its new domain name like this:
     @{verbatim [display] \<open>  isabelle phabricator bin/config set \
     phabricator.base-uri https://vcs.example.org\<close>}
 
     \<^item> Visit the website \<^verbatim>\<open>https://vcs.example.org\<close> and configure Phabricator
     as described before. The following options are particularly relevant for a
     public website:
 
       \<^item> \<^emph>\<open>Auth Provider / Username/Password\<close>: disable \<^emph>\<open>Allow Registration\<close> to
       avoid uncontrolled registrants; users can still be invited via email
       instead.
 
       \<^item> Enable \<^verbatim>\<open>policy.allow-public\<close> to allow read-only access to resources,
       without requiring user registration.
 \<close>
 
 
 section \<open>Global data storage and backups \label{sec:phabricator-backup}\<close>
 
 text \<open>
   The global state of a Phabricator installation consists of two main parts:
 
     \<^enum> The \<^emph>\<open>root directory\<close> according to
     \<^path>\<open>/etc/isabelle-phabricator.conf\<close> or \<^verbatim>\<open>isabelle phabricator -l\<close>: it
     contains the main PHP program suite with administrative tools, and some
     configuration files. The default setup also puts hosted repositories here
     (subdirectory \<^verbatim>\<open>repo\<close>).
 
     \<^enum> Multiple \<^emph>\<open>MySQL databases\<close> with a common prefix derived from the
     installation name --- the same name is used as database user name.
 
   The root user may invoke \<^verbatim>\<open>/usr/local/bin/isabelle-phabricator-dump\<close> to
   create a complete database dump within the root directory. Afterwards it is
   sufficient to make a conventional \<^bold>\<open>file-system backup\<close> of everything. To
   restore the database state, see the explanations on \<^verbatim>\<open>mysqldump\<close> in
   \<^url>\<open>https://secure.phabricator.com/book/phabricator/article/configuring_backups\<close>;
   some background information is in
   \<^url>\<open>https://secure.phabricator.com/book/phabflavor/article/so_many_databases\<close>.
 
   \<^medskip> The following command-line tools are particularly interesting for advanced
   database maintenance (within the Phabricator root directory):
   @{verbatim [display] \<open>  phabricator/bin/storage help dump
   phabricator/bin/storage help shell
   phabricator/bin/storage help destroy
   phabricator/bin/storage help renamespace\<close>}
 
   For example, copying a database snapshot from one installation to another
   works as follows. Run on the first installation root directory:
 
   @{verbatim [display] \<open>  phabricator/bin/storage dump > dump1.sql
   phabricator/bin/storage renamespace --from phabricator_vcs \
     --to phabricator_xyz --input dump1.sql --output dump2.sql\<close>}
 
   Them run on the second installation root directory:
   @{verbatim [display] \<open>  phabricator/bin/storage destroy
   phabricator/bin/storage shell < .../dump2.sql\<close>}
 
   Local configuration in \<^verbatim>\<open>phabricator/config/local/\<close> and hosted repositories
   need to be treated separately within the file-system. For the latter
   see also these tools:
   @{verbatim [display] \<open>  phabricator/bin/repository help list-paths
   phabricator/bin/repository help move-paths\<close>}
 \<close>
 
 
 section \<open>Upgrading Phabricator installations\<close>
 
 text \<open>
   The Phabricator developers publish a new version approx.\ every 1--4 weeks:
   see also \<^url>\<open>https://secure.phabricator.com/w/changelog\<close>. There is no need to
   follow such frequent updates on the spot, but it is a good idea to upgrade
   occasionally --- after dump and/or backup (\secref{sec:phabricator-backup}).
 
   The Isabelle/Phabricator setup provides a convenience tool to upgrade all
   installations uniformly:
   @{verbatim [display] \<open>  /usr/local/bin/isabelle-phabricator-upgrade\<close>}
 
   This refers to the \<^verbatim>\<open>stable\<close> branch of the distribution repositories by
   default. Alternatively, it also possible to use the \<^verbatim>\<open>master\<close> like this:
   @{verbatim [display] \<open>  /usr/local/bin/isabelle-phabricator-upgrade master\<close>}
 
   \<^medskip>
   See
   \<^url>\<open>https://secure.phabricator.com/book/phabricator/article/upgrading\<close> for
   further explanations on Phabricator upgrade.
 \<close>
 
 
 section \<open>Reference of command-line tools\<close>
 
 text \<open>
   The subsequent command-line tools usually require root user privileges on
   the underlying Linux system (e.g.\ via \<^verbatim>\<open>sudo bash\<close> to open a subshell, or
   directly via \<^verbatim>\<open>sudo isabelle phabricator ...\<close>).
 \<close>
 
 
 subsection \<open>\<^verbatim>\<open>isabelle phabricator\<close>\<close>
 
 text \<open>
   The @{tool_def phabricator} tool invokes a GNU bash command-line within the
   Phabricator home directory:
   @{verbatim [display]
 \<open>Usage: isabelle phabricator [OPTIONS] COMMAND [ARGS...]
 
   Options are:
     -l           list available Phabricator installations
     -n NAME      Phabricator installation name (default: "vcs")
 
   Invoke a command-line tool within the home directory of the named
   Phabricator installation.\<close>}
 
   Isabelle/Phabricator installations are registered in the global
   configuration file \<^path>\<open>/etc/isabelle-phabricator.conf\<close>, with name and
   root directory separated by colon (no extra whitespace). The home directory
   is the subdirectory \<^verbatim>\<open>phabricator\<close> within the root.
 
   \<^medskip> Option \<^verbatim>\<open>-l\<close> lists the available Phabricator installations with name and
   root directory --- without invoking a command.
 
   Option \<^verbatim>\<open>-n\<close> selects the explicitly named Phabricator installation.
 \<close>
 
 
 subsubsection \<open>Examples\<close>
 
 text \<open>
   Print the home directory of the Phabricator installation:
   @{verbatim [display] \<open>  isabelle phabricator pwd\<close>}
 
   Print some Phabricator configuration information:
   @{verbatim [display] \<open>  isabelle phabricator bin/config get phabricator.base-uri\<close>}
 
   The latter conforms to typical command templates seen in the original
   Phabricator documentation:
   @{verbatim [display] \<open>  phabricator/ $ ./bin/config get phabricator.base-uri\<close>}
 
   Here the user is meant to navigate to the Phabricator home manually, in
   contrast to \<^verbatim>\<open>isabelle phabricator\<close> doing it automatically thanks to the
   global configuration \<^path>\<open>/etc/isabelle-phabricator.conf\<close>.
 \<close>
 
 
 subsection \<open>\<^verbatim>\<open>isabelle phabricator_setup\<close>\<close>
 
 text \<open>
   The @{tool_def phabricator_setup} tool installs a fresh Phabricator instance
   on Ubuntu 18.04 LTS:
   @{verbatim [display] \<open>Usage: isabelle phabricator_setup [OPTIONS]
 
   Options are:
     -M SOURCE    install Mercurial from source: local PATH, or URL, or ":"
     -R DIR       repository directory (default: "/var/www/phabricator-NAME/repo")
     -U           full update of system packages before installation
     -n NAME      Phabricator installation name (default: "vcs")
     -r DIR       installation root directory (default: "/var/www/phabricator-NAME")
 
   Install Phabricator as LAMP application (Linux, Apache, MySQL, PHP).
 
   The installation name (default: "vcs") is mapped to a regular
   Unix user; this is relevant for public SSH access.\<close>}
 
   Installation requires Linux root permissions. All required packages are
   installed automatically beforehand, this includes the Apache web server and
   the MySQL database engine.
 
   Global configuration in \<^verbatim>\<open>/etc\<close> or a few other directories like \<^verbatim>\<open>/var/www\<close>
   uses name prefixes like \<^verbatim>\<open>isabelle-phabricator\<close> or \<^verbatim>\<open>phabricator\<close>. Local
   configuration for a particular installation uses more specific names derived
   from \<^verbatim>\<open>phabricator-\<close>\<open>NAME\<close>, e.g.\ \<^verbatim>\<open>/var/www/phabricator-vcs\<close> for the
   default.
 
   Knowing the naming conventions, it is possible to purge a Linux installation
   from Isabelle/Phabricator with some effort, but there is no automated
   procedure for de-installation. In the worst case, it might be better to
   re-install the virtual machine from a clean image.
 
   \<^medskip>
   Option \<^verbatim>\<open>-U\<close> ensures a full update of system packages, before installing
   further packages required by Phabricator. This might require a reboot.
 
-  Option \<^verbatim>\<open>-M:\<close> installs a standard Mercurial release from source: this works
-  better than the package provided by Ubuntu 18.04. Alternatively, an explicit
-  file path or URL the source archive (\<^verbatim>\<open>.tar.gz\<close>) may be here. This option is
+  Option \<^verbatim>\<open>-M:\<close> installs a standard Mercurial release from source --- the one
+  that is used by the Phabricator hosting service
+  \<^url>\<open>https://admin.phacility.com\<close>. This avoids various problems with the
+  package provided by Ubuntu 18.04. Alternatively, an explicit file path or
+  URL the source archive (\<^verbatim>\<open>.tar.gz\<close>) may be given here. This option is
   recommended for production use, but it requires to \<^emph>\<open>uninstall\<close> existing
   Mercurial packages provided by the operating system.
 
   Option \<^verbatim>\<open>-n\<close> provides an alternative installation name. The default name
   \<^verbatim>\<open>vcs\<close> means ``version control system''. The name appears in the URL for SSH
   access, and thus has some relevance to end-users. The initial server URL
   also uses the same suffix, but that can (and should) be changed later via
   regular Apache configuration.
 
   Option \<^verbatim>\<open>-r\<close> specifies an alternative installation root directory: it needs
   to be accessible for the Apache web server.
 
   Option \<^verbatim>\<open>-R\<close> specifies an alternative directory for repositories that are
   hosted by Phabricator. Provided that it is accessible for the Apache web
   server, the directory can be reused for the \<^verbatim>\<open>hgweb\<close> view by Mercurial.\<^footnote>\<open>See
   also the documentation
   \<^url>\<open>https://www.mercurial-scm.org/wiki/PublishingRepositories\<close> and the
   example \<^url>\<open>https://isabelle.sketis.net/repos\<close>.\<close>
 \<close>
 
 
 subsection \<open>\<^verbatim>\<open>isabelle phabricator_setup_mail\<close>\<close>
 
 text \<open>
   The @{tool_def phabricator_setup_mail} tool provides mail configuration for
   an existing Phabricator installation:
   @{verbatim [display] \<open>Usage: isabelle phabricator_setup_mail [OPTIONS]
 
   Options are:
     -T USER      send test mail to Phabricator user
     -f FILE      config file (default: "mailers.json" within
                  Phabricator root)
     -n NAME      Phabricator installation name (default: "vcs")
 
   Provide mail configuration for existing Phabricator installation.\<close>}
 
   Proper mail configuration is vital for Phabricator, but the details can be
   tricky. A common approach is to re-use an existing SMTP mail service, as is
   often included in regular web hosting packages. It is sufficient to create
   one mail account for multiple Phabricator installations, but the
   configuration needs to be set for each installation.
 
   The first invocation of \<^verbatim>\<open>isabelle phabricator_setup_mail\<close> without options
   creates a JSON template file. Its \<^verbatim>\<open>key\<close> entry should be changed to
   something sensible to identify the configuration, e.g.\ the Internet Domain
   Name of the mail address. The \<^verbatim>\<open>options\<close> specify the SMTP server address and
   account information.
 
   Another invocation of \<^verbatim>\<open>isabelle phabricator_setup_mail\<close> with updated JSON
   file will change the underlying Phabricator installation. This can be done
   repeatedly, until everything works as expected.
 
   Option \<^verbatim>\<open>-T\<close> invokes a standard Phabricator test procedure for the mail
   configuration. The argument needs to be a valid Phabricator user: the mail
   address is derived from the user profile.
 
   Option \<^verbatim>\<open>-f\<close> refers to an existing JSON configuration file, e.g.\ from a
   previous successful Phabricator installation: sharing mailers setup with the
   same mail address is fine for outgoing mails; incoming mails are optional
   and not configured here.
 \<close>
 
 
 subsection \<open>\<^verbatim>\<open>isabelle phabricator_setup_ssh\<close>\<close>
 
 text \<open>
   The @{tool_def phabricator_setup_ssh} tool configures a special SSH service
   for all Phabricator installations:
   @{verbatim [display] \<open>Usage: isabelle phabricator_setup_ssh [OPTIONS]
 
   Options are:
     -p PORT      sshd port for Phabricator servers (default: 2222)
     -q PORT      sshd port for the operating system (default: 22)
 
   Configure ssh service for all Phabricator installations: a separate sshd
   is run in addition to the one of the operating system, and ports need to
   be distinct.
 
   A particular Phabricator installation is addressed by using its
   name as the ssh user; the actual Phabricator user is determined via
   stored ssh keys.\<close>}
 
   This is optional, but very useful. It allows to refer to hosted repositories
   via ssh with the usual public-key authentication. It also allows to
   communicate with a Phabricator server via the JSON API of
   \<^emph>\<open>Conduit\<close>\<^footnote>\<open>\<^url>\<open>https://secure.phabricator.com/book/phabricator/article/conduit\<close>\<close>.
 
   \<^medskip> The Phabricator SSH server distinguishes installations by their name,
   e.g.\ \<^verbatim>\<open>vcs\<close> as SSH user name. The public key that is used for
   authentication identifies the user within Phabricator: there is a web
   interface to provide that as part of the user profile.
 
   The operating system already has an SSH server (by default on port 22) that
   remains important for remote administration of the machine.
 
   \<^medskip>
   Options \<^verbatim>\<open>-p\<close> and \<^verbatim>\<open>-q\<close> allow to change the port assignment for both
   servers. A common scheme is \<^verbatim>\<open>-p 22 -q 222\<close> to leave the standard port to
   Phabricator, to simplify the ssh URL that users will see for remote
   repository clones.\<^footnote>\<open>For the rare case of hosting Subversion repositories,
   port 22 is de-facto required. Otherwise Phabricator presents malformed
   \<^verbatim>\<open>svn+ssh\<close> URLs with port specification.\<close>
 
   Redirecting the operating system sshd to port 222 requires some care: it
   requires to adjust the remote login procedure, e.g.\ in \<^verbatim>\<open>$HOME/.ssh/config\<close>
   to add a \<^verbatim>\<open>Port\<close> specification for the server machine.
 \<close>
 
 end
diff --git a/src/Pure/Tools/phabricator.scala b/src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala
+++ b/src/Pure/Tools/phabricator.scala
@@ -1,1070 +1,1070 @@
 /*  Title:      Pure/Tools/phabricator.scala
     Author:     Makarius
 
 Support for Phabricator server, notably for Ubuntu 18.04 LTS.
 
 See also:
   - https://www.phacility.com/phabricator
   - https://secure.phabricator.com/book/phabricator
 */
 
 package isabelle
 
 
 import scala.collection.mutable
 import scala.util.matching.Regex
 
 
 object Phabricator
 {
   /** defaults **/
 
   /* required packages */
 
   val packages: List[String] =
     Build_Docker.packages ::: Linux.packages :::
     List(
       // https://secure.phabricator.com/source/phabricator/browse/master/scripts/install/install_ubuntu.sh 15e6e2adea61
       "git", "mysql-server", "apache2", "libapache2-mod-php", "php", "php-mysql",
       "php-gd", "php-curl", "php-apcu", "php-cli", "php-json", "php-mbstring",
       // more packages
       "php-xml", "php-zip", "python-pygments", "ssh", "subversion",
       // mercurial build packages
       "make", "gcc", "python", "python-dev", "python-docutils", "python-pygments", "python-openssl")
 
 
   /* global system resources */
 
   val www_user = "www-data"
 
   val daemon_user = "phabricator"
 
   val sshd_config = Path.explode("/etc/ssh/sshd_config")
 
 
   /* installation parameters */
 
   val default_name = "vcs"
 
   def phabricator_name(name: String = "", ext: String = ""): String =
     "phabricator" + (if (name.isEmpty) "" else "-" + name) + (if (ext.isEmpty) "" else "." + ext)
 
   def isabelle_phabricator_name(name: String = "", ext: String = ""): String =
     "isabelle-" + phabricator_name(name = name, ext = ext)
 
   def default_root(name: String): Path =
     Path.explode("/var/www") + Path.basic(phabricator_name(name = name))
 
   def default_repo(name: String): Path = default_root(name) + Path.basic("repo")
 
   val default_mailers: Path = Path.explode("mailers.json")
 
   val default_system_port = 22
   val alternative_system_port = 222
   val default_server_port = 2222
 
-  val standard_mercurial_source = "https://www.mercurial-scm.org/release/mercurial-5.2.1.tar.gz"
+  val standard_mercurial_source = "https://www.mercurial-scm.org/release/mercurial-2.8.2.tar.gz"
 
 
 
   /** global configuration **/
 
   val global_config = Path.explode("/etc/" + isabelle_phabricator_name(ext = "conf"))
 
   def global_config_script(
     init: String = "",
     body: String = "",
     exit: String = ""): String =
   {
 """#!/bin/bash
 """ + (if (init.nonEmpty) "\n" + init else "") + """
 {
   while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
   do
     NAME="$(echo "$REPLY" | cut -d: -f1)"
     ROOT="$(echo "$REPLY" | cut -d: -f2)"
     {
 """ + Library.prefix_lines("      ", body) + """
     } < /dev/null
   done
 } < """ + File.bash_path(global_config) + "\n" +
     (if (exit.nonEmpty) "\n" + exit + "\n" else "")
   }
 
   sealed case class Config(name: String, root: Path)
   {
     def home: Path = root + Path.explode(phabricator_name())
 
     def execute(command: String): Process_Result =
       Isabelle_System.bash("bin/" + command, cwd = home.file, redirect = true).check
   }
 
   def read_config(): List[Config] =
   {
     if (global_config.is_file) {
       for (entry <- Library.trim_split_lines(File.read(global_config)) if entry.nonEmpty)
       yield {
         space_explode(':', entry) match {
           case List(name, root) => Config(name, Path.explode(root))
           case _ => error("Malformed config file " + global_config + "\nentry " + quote(entry))
         }
       }
     }
     else Nil
   }
 
   def write_config(configs: List[Config])
   {
     File.write(global_config,
       configs.map(config => config.name + ":" + config.root.implode).mkString("", "\n", "\n"))
   }
 
   def get_config(name: String): Config =
     read_config().find(config => config.name == name) getOrElse
       error("Bad Isabelle/Phabricator installation " + quote(name))
 
 
 
   /** administrative tools **/
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool1 =
     Isabelle_Tool("phabricator", "invoke command-line tool within Phabricator home directory", args =>
     {
       var list = false
       var name = default_name
 
       val getopts =
         Getopts("""
 Usage: isabelle phabricator [OPTIONS] COMMAND [ARGS...]
 
   Options are:
     -l           list available Phabricator installations
     -n NAME      Phabricator installation name (default: """ + quote(default_name) + """)
 
   Invoke a command-line tool within the home directory of the named
   Phabricator installation.
 """,
           "l" -> (_ => list = true),
           "n:" -> (arg => name = arg))
 
       val more_args = getopts(args)
       if (more_args.isEmpty && !list) getopts.usage()
 
       val progress = new Console_Progress
 
       if (list) {
         for (config <- read_config()) {
           progress.echo("phabricator " + quote(config.name) + " root " + config.root)
         }
       }
       else {
         val config = get_config(name)
         val result = progress.bash(Bash.strings(more_args), cwd = config.home.file, echo = true)
         if (!result.ok) error("Return code: " + result.rc.toString)
       }
     })
 
 
 
   /** setup **/
 
   def user_setup(name: String, description: String, ssh_setup: Boolean = false)
   {
     if (!Linux.user_exists(name)) {
       Linux.user_add(name, description = description, system = true, ssh_setup = ssh_setup)
     }
     else if (Linux.user_description(name) != description) {
       error("User " + quote(name) + " already exists --" +
         " for Phabricator it should have the description:\n  " + quote(description))
     }
   }
 
   def command_setup(name: String,
     init: String = "",
     body: String = "",
     exit: String = ""): Path =
   {
     val command = Path.explode("/usr/local/bin") + Path.basic(name)
     File.write(command, global_config_script(init = init, body = body, exit = exit))
     Isabelle_System.chmod("755", command)
     Isabelle_System.chown("root:root", command)
     command
   }
 
   def mercurial_setup(mercurial_source: String, progress: Progress = No_Progress)
   {
     progress.echo("\nMercurial installation from source " + quote(mercurial_source) + " ...")
     Isabelle_System.with_tmp_dir("mercurial")(tmp_dir =>
     {
       val archive =
         if (Url.is_wellformed(mercurial_source)) {
           val archive = tmp_dir + Path.basic("mercurial.tar.gz")
           Bytes.write(archive, Url.read_bytes(Url(mercurial_source)))
           archive
         }
         else Path.explode(mercurial_source)
 
       Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
 
       File.read_dir(tmp_dir).filter(name => (tmp_dir + Path.basic(name)).is_dir) match {
         case List(dir) =>
           val build_dir = tmp_dir + Path.basic(dir)
           progress.bash("make all && make install", cwd = build_dir.file, echo = true).check
         case dirs =>
           error("Bad archive " + archive +
             (if (dirs.isEmpty) "" else "\nmultiple directory entries " + commas_quote(dirs)))
       }
     })
   }
 
   def phabricator_setup(
     name: String = default_name,
     root: String = "",
     repo: String = "",
     package_update: Boolean = false,
     mercurial_source: String = "",
     progress: Progress = No_Progress)
   {
     /* system environment */
 
     Linux.check_system_root()
 
     progress.echo("System packages ...")
 
     if (package_update) {
       Linux.package_update(progress = progress)
       Linux.check_reboot_required()
     }
 
     Linux.package_install(packages, progress = progress)
     Linux.check_reboot_required()
 
 
     if (mercurial_source.nonEmpty) {
       for { name <- List("mercurial", "mercurial-common") if Linux.package_installed(name) } {
         error("Cannot install Mercurial from source:\n" +
           "package package " + quote(name) + " already installed")
       }
       mercurial_setup(mercurial_source, progress = progress)
     }
 
 
     /* users */
 
     if (name.contains((c: Char) => !(Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c))) ||
         Set("", "ssh", "phd", "dump", daemon_user).contains(name)) {
       error("Bad installation name: " + quote(name))
     }
 
     user_setup(daemon_user, "Phabricator Daemon User", ssh_setup = true)
     user_setup(name, "Phabricator SSH User")
 
 
     /* basic installation */
 
     progress.echo("\nPhabricator installation ...")
 
     val root_path = if (root.nonEmpty) Path.explode(root) else default_root(name)
     val repo_path = if (repo.nonEmpty) Path.explode(repo) else default_repo(name)
 
     val configs = read_config()
 
     for (config <- configs if config.name == name) {
       error("Duplicate Phabricator installation " + quote(name) + " in " + config.root)
     }
 
     if (!Isabelle_System.bash("mkdir -p " + File.bash_path(root_path)).ok) {
       error("Failed to create root directory " + root_path)
     }
 
     Isabelle_System.chown(Bash.string(www_user) + ":" + Bash.string(www_user), root_path)
     Isabelle_System.chmod("755", root_path)
 
     progress.bash(cwd = root_path.file, echo = true,
       script = """
         set -e
         echo "Cloning distribution repositories:"
 
         git clone --branch stable https://github.com/phacility/libphutil.git
         git -C libphutil reset --hard 1750586fdc50a6cd98adba4aa2f5a7649bd91dbe
 
         git clone --branch stable https://github.com/phacility/arcanist.git
         git -C arcanist reset --hard bac2028421a4be6e34e08764bbbda49e68b3a604
 
         git clone --branch stable https://github.com/phacility/phabricator.git
         git -C phabricator reset --hard c4b4a53cad7722f031b725f8b41511e9d341d033
       """).check
 
     val config = Config(name, root_path)
     write_config(configs ::: List(config))
 
     config.execute("config set pygments.enabled true")
 
 
     /* local repository directory */
 
     progress.echo("\nRepository hosting setup ...")
 
     if (!Isabelle_System.bash("mkdir -p " + File.bash_path(repo_path)).ok) {
       error("Failed to create local repository directory " + repo_path)
     }
 
     Isabelle_System.chown(
       "-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), repo_path)
     Isabelle_System.chmod("755", repo_path)
 
     config.execute("config set repository.default-local-path " + File.bash_path(repo_path))
 
 
     val sudoers_file =
       Path.explode("/etc/sudoers.d") + Path.basic(isabelle_phabricator_name(name = name))
     File.write(sudoers_file,
       www_user + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/local/bin/hg, /usr/bin/hg, /usr/bin/ssh, /usr/bin/id\n" +
       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")
 
     Isabelle_System.chmod("440", sudoers_file)
 
     config.execute("config set diffusion.ssh-user " + Bash.string(config.name))
 
 
     /* MySQL setup */
 
     progress.echo("\nMySQL setup ...")
 
     File.write(Path.explode("/etc/mysql/mysql.conf.d/" + phabricator_name(ext = "cnf")),
 """[mysqld]
 max_allowed_packet = 32M
 innodb_buffer_pool_size = 1600M
 local_infile = 0
 """)
 
     Linux.service_restart("mysql")
 
 
     def mysql_conf(R: Regex, which: String): String =
     {
       val conf = Path.explode("/etc/mysql/debian.cnf")
       split_lines(File.read(conf)).collectFirst({ case R(a) => a }) match {
         case Some(res) => res
         case None => error("Cannot determine " + which + " from " + conf)
       }
     }
 
     val mysql_root_user = mysql_conf("""^user\s*=\s*(\S*)\s*$""".r, "superuser name")
     val mysql_root_password = mysql_conf("""^password\s*=\s*(\S*)\s*$""".r, "superuser password")
 
     val mysql_name = phabricator_name(name = name).replace("-", "_")
     val mysql_user_string = SQL.string(mysql_name) + "@'localhost'"
     val mysql_password = Linux.generate_password()
 
     Isabelle_System.bash("mysql --user=" + Bash.string(mysql_root_user) +
       " --password=" + Bash.string(mysql_root_password) + " --execute=" +
       Bash.string(
         """DROP USER IF EXISTS """ + mysql_user_string + "; " +
         """CREATE USER """ + mysql_user_string +
         """ IDENTIFIED BY """ + SQL.string(mysql_password) + """ PASSWORD EXPIRE NEVER; """ +
         """GRANT ALL ON `""" + (mysql_name + "_%").replace("_", "\\_") +
         """`.* TO """ + mysql_user_string + ";")).check
 
     config.execute("config set mysql.user " + Bash.string(mysql_name))
     config.execute("config set mysql.pass " + Bash.string(mysql_password))
 
     config.execute("config set phabricator.cache-namespace " + Bash.string(mysql_name))
     config.execute("config set storage.default-namespace " + Bash.string(mysql_name))
     config.execute("config set storage.mysql-engine.max-size 8388608")
 
     progress.bash("bin/storage upgrade --force", cwd = config.home.file, echo = true).check
 
 
     /* database dump */
 
     val dump_name = isabelle_phabricator_name(name = "dump")
     command_setup(dump_name, body =
 """mkdir -p "$ROOT/database" && chown root:root "$ROOT/database" && chmod 700 "$ROOT/database"
 [ -e "$ROOT/database/dump.sql.gz" ] && mv -f "$ROOT/database/dump.sql.gz" "$ROOT/database/dump-old.sql.gz"
 echo -n "Creating $ROOT/database/dump.sql.gz ..."
 "$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'
 echo " $(ls -hs "$ROOT/database/dump.sql.gz" | cut -d" " -f1)" """)
 
 
     /* Phabricator upgrade */
 
     command_setup(isabelle_phabricator_name(name = "upgrade"),
       init =
 """BRANCH="${1:-stable}"
 if [ "$BRANCH" != "master" -a "$BRANCH" != "stable" ]
 then
   echo "Bad branch: \"$BRANCH\""
   exit 1
 fi
 
 systemctl stop isabelle-phabricator-phd
 systemctl stop apache2
 """,
       body =
 """echo -e "\nUpgrading phabricator \"$NAME\" root \"$ROOT\" ..."
 for REPO in libphutil arcanist phabricator
 do
   cd "$ROOT/$REPO"
   echo -e "\nUpdating \"$REPO\" ..."
   git checkout "$BRANCH"
   git pull
 done
 echo -e "\nUpgrading storage ..."
 "$ROOT/phabricator/bin/storage" upgrade --force
 """,
       exit =
 """systemctl start apache2
 systemctl start isabelle-phabricator-phd""")
 
 
     /* PHP setup */
 
     val php_version =
       Isabelle_System.bash("""php --run 'echo PHP_MAJOR_VERSION . "." . PHP_MINOR_VERSION;'""")
         .check.out
 
     val php_conf =
       Path.explode("/etc/php") + Path.basic(php_version) +  // educated guess
         Path.explode("apache2/conf.d") +
         Path.basic(isabelle_phabricator_name(ext = "ini"))
 
     File.write(php_conf,
       "post_max_size = 32M\n" +
       "opcache.validate_timestamps = 0\n" +
       "memory_limit = 512M\n" +
       "max_execution_time = 120\n")
 
 
     /* Apache setup */
 
     progress.echo("Apache setup ...")
 
     val apache_root = Path.explode("/etc/apache2")
     val apache_sites = apache_root + Path.explode("sites-available")
 
     if (!apache_sites.is_dir) error("Bad Apache sites directory " + apache_sites)
 
     val server_name = phabricator_name(name = name, ext = "lvh.me")  // alias for "localhost" for testing
     val server_url = "http://" + server_name
 
     File.write(apache_sites + Path.basic(isabelle_phabricator_name(name = name, ext = "conf")),
 """<VirtualHost *:80>
     ServerName """ + server_name + """
     ServerAdmin webmaster@localhost
     DocumentRoot """ + config.home.implode + """/webroot
 
     ErrorLog ${APACHE_LOG_DIR}/error.log
     RewriteEngine on
     RewriteRule ^(.*)$  /index.php?__path__=$1  [B,L,QSA]
 </VirtualHost>
 
 # vim: syntax=apache ts=4 sw=4 sts=4 sr noet
 """)
 
     Isabelle_System.bash( """
       set -e
       a2enmod rewrite
       a2ensite """ + Bash.string(isabelle_phabricator_name(name = name))).check
 
     config.execute("config set phabricator.base-uri " + Bash.string(server_url))
 
     Linux.service_restart("apache2")
 
     progress.echo("\nFurther manual configuration via " + server_url)
 
 
     /* PHP daemon */
 
     progress.echo("\nPHP daemon setup ...")
 
     val phd_log_path = Path.explode("/var/tmp/phd")
     Isabelle_System.mkdirs(phd_log_path)
     Isabelle_System.chown(
       "-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), phd_log_path)
     Isabelle_System.chmod("755", phd_log_path)
 
     config.execute("config set phd.user " + Bash.string(daemon_user))
     config.execute("config set phd.log-directory /var/tmp/phd/" +
       isabelle_phabricator_name(name = name) + "/log")
 
     val phd_name = isabelle_phabricator_name(name = "phd")
     Linux.service_shutdown(phd_name)
     val phd_command = command_setup(phd_name, body = """"$ROOT/phabricator/bin/phd" "$@" """)
     try {
       Linux.service_install(phd_name,
 """[Unit]
 Description=PHP daemon manager for Isabelle/Phabricator
 After=syslog.target network.target apache2.service mysql.service
 
 [Service]
 Type=oneshot
 User=""" + daemon_user + """
 Group=""" + daemon_user + """
 Environment=PATH=/sbin:/usr/sbin:/usr/local/sbin:/usr/local/bin:/usr/bin:/bin
 ExecStart=""" + phd_command.implode + """ start --force
 ExecStop=""" + phd_command.implode + """ stop
 RemainAfterExit=yes
 
 [Install]
 WantedBy=multi-user.target
 """)
     }
     catch {
       case ERROR(msg) =>
         progress.bash("bin/phd status", cwd = config.home.file, echo = true).check
         error(msg)
     }
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool2 =
     Isabelle_Tool("phabricator_setup", "setup Phabricator server on Ubuntu Linux", args =>
     {
       var mercurial_source = ""
       var repo = ""
       var package_update = false
       var name = default_name
       var root = ""
 
       val getopts =
         Getopts("""
 Usage: isabelle phabricator_setup [OPTIONS]
 
   Options are:
     -M SOURCE    install Mercurial from source: local PATH, or URL, or ":" for
                  """ + standard_mercurial_source + """
     -R DIR       repository directory (default: """ + default_repo("NAME") + """)
     -U           full update of system packages before installation
     -n NAME      Phabricator installation name (default: """ + quote(default_name) + """)
     -r DIR       installation root directory (default: """ + default_root("NAME") + """)
 
   Install Phabricator as LAMP application (Linux, Apache, MySQL, PHP).
 
   The installation name (default: """ + quote(default_name) + """) is mapped to a regular
   Unix user; this is relevant for public SSH access.
 """,
           "M:" -> (arg => mercurial_source = (if (arg == ":") standard_mercurial_source else arg)),
           "R:" -> (arg => repo = arg),
           "U" -> (_ => package_update = true),
           "n:" -> (arg => name = arg),
           "r:" -> (arg => root = arg))
 
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
       val progress = new Console_Progress
 
       val release = Linux.Release()
       if (!release.is_ubuntu_18_04) error("Bad Linux version: Ubuntu 18.04 LTS required")
 
       phabricator_setup(name = name, root = root, repo = repo,
         package_update = package_update, mercurial_source = mercurial_source, progress = progress)
     })
 
 
 
   /** setup mail **/
 
   val mailers_template: String =
 """[
   {
     "key": "example.org",
     "type": "smtp",
     "options": {
       "host": "mail.example.org",
       "port": 465,
       "user": "phabricator@example.org",
       "password": "********",
       "protocol": "ssl",
       "message-id": true
     }
   }
 ]"""
 
   def phabricator_setup_mail(
     name: String = default_name,
     config_file: Option[Path] = None,
     test_user: String = "",
     progress: Progress = No_Progress)
   {
     Linux.check_system_root()
 
     val config = get_config(name)
     val default_config_file = config.root + default_mailers
 
     val mail_config = config_file getOrElse default_config_file
 
     def setup_mail
     {
       progress.echo("Using mail configuration from " + mail_config)
       config.execute("config set cluster.mailers --stdin < " + File.bash_path(mail_config))
 
       if (test_user.nonEmpty) {
         progress.echo("Sending test mail to " + quote(test_user))
         progress.bash(cwd = config.home.file, echo = true,
           script = """echo "Test from Phabricator ($(date))" | bin/mail send-test --subject "Test" --to """ +
             Bash.string(test_user)).check
       }
     }
 
     if (config_file.isEmpty) {
       if (!default_config_file.is_file) {
         File.write(default_config_file, mailers_template)
         Isabelle_System.chmod("600", default_config_file)
       }
       if (File.read(default_config_file) == mailers_template) {
         progress.echo("Please invoke the tool again, after providing details in\n  " +
           default_config_file.implode + "\n")
       }
       else setup_mail
     }
     else setup_mail
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool3 =
     Isabelle_Tool("phabricator_setup_mail",
       "setup mail for one Phabricator installation", args =>
     {
       var test_user = ""
       var name = default_name
       var config_file: Option[Path] = None
 
       val getopts =
         Getopts("""
 Usage: isabelle phabricator_setup_mail [OPTIONS]
 
   Options are:
     -T USER      send test mail to Phabricator user
     -f FILE      config file (default: """ + default_mailers + """ within Phabricator root)
     -n NAME      Phabricator installation name (default: """ + quote(default_name) + """)
 
   Provide mail configuration for existing Phabricator installation.
 """,
           "T:" -> (arg => test_user = arg),
           "f:" -> (arg => config_file = Some(Path.explode(arg))),
           "n:" -> (arg => name = arg))
 
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
       val progress = new Console_Progress
 
       phabricator_setup_mail(name = name, config_file = config_file,
         test_user = test_user, progress = progress)
     })
 
 
 
   /** setup ssh **/
 
   /* sshd config */
 
   private val Port = """^\s*Port\s+(\d+)\s*$""".r
   private val No_Port = """^#\s*Port\b.*$""".r
   private val Any_Port = """^#?\s*Port\b.*$""".r
 
   def conf_ssh_port(port: Int): String =
     if (port == 22) "#Port 22" else "Port " + port
 
   def read_ssh_port(conf: Path): Int =
   {
     val lines = split_lines(File.read(conf))
     val ports =
       lines.flatMap({
         case Port(Value.Int(p)) => Some(p)
         case No_Port() => Some(22)
         case _ => None
       })
     ports match {
       case List(port) => port
       case Nil => error("Missing Port specification in " + conf)
       case _ => error("Multiple Port specifications in " + conf)
     }
   }
 
   def write_ssh_port(conf: Path, port: Int): Boolean =
   {
     val old_port = read_ssh_port(conf)
     if (old_port == port) false
     else {
       val lines = split_lines(File.read(conf))
       val lines1 = lines.map({ case Any_Port() => conf_ssh_port(port) case line => line })
       File.write(conf, cat_lines(lines1))
       true
     }
   }
 
 
   /* phabricator_setup_ssh */
 
   def phabricator_setup_ssh(
     server_port: Int = default_server_port,
     system_port: Int = default_system_port,
     progress: Progress = No_Progress)
   {
     Linux.check_system_root()
 
     val configs = read_config()
 
     if (server_port == system_port) {
       error("Port for Phabricator sshd coincides with system port: " + system_port)
     }
 
     val sshd_conf_system = Path.explode("/etc/ssh/sshd_config")
     val sshd_conf_server = sshd_conf_system.ext(isabelle_phabricator_name())
 
     val ssh_name = isabelle_phabricator_name(name = "ssh")
     Linux.service_shutdown(ssh_name)
 
     val old_system_port = read_ssh_port(sshd_conf_system)
     if (old_system_port != system_port) {
       progress.echo("Reconfigurig system ssh service")
       Linux.service_shutdown("ssh")
       write_ssh_port(sshd_conf_system, system_port)
       Linux.service_start("ssh")
     }
 
     progress.echo("Configuring " + ssh_name + " service")
 
     val ssh_command = command_setup(ssh_name, body =
 """if [ "$1" = "$NAME" ]
 then
   exec "$ROOT/phabricator/bin/ssh-auth" "$@"
 fi""", exit = "exit 1")
 
     File.write(sshd_conf_server,
 """# OpenBSD Secure Shell server for Isabelle/Phabricator
 AuthorizedKeysCommand """ + ssh_command.implode + """
 AuthorizedKeysCommandUser """ + daemon_user + """
 AuthorizedKeysFile none
 AllowUsers """ + configs.map(_.name).mkString(" ") + """
 Port """ + server_port + """
 Protocol 2
 PermitRootLogin no
 AllowAgentForwarding no
 AllowTcpForwarding no
 PrintMotd no
 PrintLastLog no
 PasswordAuthentication no
 ChallengeResponseAuthentication no
 PidFile /var/run/""" + ssh_name + """.pid
 """)
 
     Linux.service_install(ssh_name,
 """[Unit]
 Description=OpenBSD Secure Shell server for Isabelle/Phabricator
 After=network.target auditd.service
 ConditionPathExists=!/etc/ssh/sshd_not_to_be_run
 
 [Service]
 EnvironmentFile=-/etc/default/ssh
 ExecStartPre=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t
 ExecStart=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -D $SSHD_OPTS
 ExecReload=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t
 ExecReload=/bin/kill -HUP $MAINPID
 KillMode=process
 Restart=on-failure
 RestartPreventExitStatus=255
 Type=notify
 RuntimeDirectory=sshd-phabricator
 RuntimeDirectoryMode=0755
 
 [Install]
 WantedBy=multi-user.target
 Alias=""" + ssh_name + """.service
 """)
 
     for (config <- configs) {
       progress.echo("phabricator " + quote(config.name) + " port " +  server_port)
       config.execute("config set diffusion.ssh-port " + Bash.string(server_port.toString))
       if (server_port == 22) config.execute("config delete diffusion.ssh-port")
     }
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool4 =
     Isabelle_Tool("phabricator_setup_ssh",
       "setup ssh service for all Phabricator installations", args =>
     {
       var server_port = default_server_port
       var system_port = default_system_port
 
       val getopts =
         Getopts("""
 Usage: isabelle phabricator_setup_ssh [OPTIONS]
 
   Options are:
     -p PORT      sshd port for Phabricator servers (default: """ + default_server_port + """)
     -q PORT      sshd port for the operating system (default: """ + default_system_port + """)
 
   Configure ssh service for all Phabricator installations: a separate sshd
   is run in addition to the one of the operating system, and ports need to
   be distinct.
 
   A particular Phabricator installation is addressed by using its
   name as the ssh user; the actual Phabricator user is determined via
   stored ssh keys.
 """,
           "p:" -> (arg => server_port = Value.Int.parse(arg)),
           "q:" -> (arg => system_port = Value.Int.parse(arg)))
 
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
       val progress = new Console_Progress
 
       phabricator_setup_ssh(
         server_port = server_port, system_port = system_port, progress = progress)
     })
 
 
 
   /** conduit API **/
 
   object API
   {
     /* user information */
 
     sealed case class User(
       id: Long,
       phid: String,
       name: String,
       real_name: String,
       roles: List[String])
     {
       def is_valid: Boolean =
         roles.contains("verified") &&
         roles.contains("approved") &&
         roles.contains("activated")
       def is_admin: Boolean = roles.contains("admin")
       def is_regular: Boolean = !(roles.contains("bot") || roles.contains("list"))
     }
 
 
     /* repository information */
 
     sealed case class Repository(
       vcs: VCS.Value,
       id: Long,
       phid: String,
       name: String,
       callsign: String,
       short_name: String,
       importing: Boolean,
       ssh_url: String)
     {
       def is_hg: Boolean = vcs == VCS.hg
     }
 
     object VCS extends Enumeration
     {
       val hg, git, svn = Value
       def read(s: String): Value =
         try { withName(s) }
         catch { case _: java.util.NoSuchElementException  => error("Unknown vcs type " + quote(s)) }
     }
 
     def edits(typ: String, value: JSON.T): List[JSON.Object.T] =
       List(JSON.Object("type" -> typ, "value" -> value))
 
     def opt_edits(typ: String, value: Option[JSON.T]): List[JSON.Object.T] =
       value.toList.flatMap(edits(typ, _))
 
 
     /* result with optional error */
 
     sealed case class Result(result: JSON.T, error: Option[String])
     {
       def ok: Boolean = error.isEmpty
       def get: JSON.T = if (ok) result else Exn.error(error.get)
 
       def get_value[A](unapply: JSON.T => Option[A]): A =
         unapply(get) getOrElse Exn.error("Bad JSON result: " + JSON.Format(result))
 
       def get_string: String = get_value(JSON.Value.String.unapply)
     }
 
     def make_result(json: JSON.T): Result =
     {
       val result = JSON.value(json, "result").getOrElse(JSON.Object.empty)
       val error_info = JSON.string(json, "error_info")
       val error_code = JSON.string(json, "error_code")
       Result(result, error_info orElse error_code)
     }
 
 
     /* context for operations */
 
     def apply(user: String, host: String, port: Int = 22): API =
       new API(user, host, port)
   }
 
   final class API private(ssh_user: String, ssh_host: String, ssh_port: Int)
   {
     /* connection */
 
     require(ssh_host.nonEmpty && ssh_port >= 0)
 
     private def ssh_user_prefix: String = if (ssh_user.isEmpty) "" else ssh_user + "@"
     private def ssh_port_suffix: String = if (ssh_port == 22) "" else ":" + ssh_port
 
     override def toString: String = ssh_user_prefix + ssh_host + ssh_port_suffix
     def hg_url: String = "ssh://" + ssh_user_prefix + ssh_host + ssh_port_suffix
 
 
     /* execute methods */
 
     def execute_raw(method: String, params: JSON.T = JSON.Object.empty): JSON.T =
     {
       Isabelle_System.with_tmp_file("params", "json")(params_file =>
       {
         File.write(params_file, JSON.Format(JSON.Object("params" -> JSON.Format(params))))
         val result =
           Isabelle_System.bash(
             "ssh -p " + ssh_port + " " + Bash.string(ssh_user_prefix + ssh_host) +
             " conduit " + Bash.string(method) + " < " + File.bash_path(params_file)).check
         JSON.parse(result.out, strict = false)
       })
     }
 
     def execute(method: String, params: JSON.T = JSON.Object.empty): API.Result =
       API.make_result(execute_raw(method, params = params))
 
     def execute_search[A](
       method: String, params: JSON.Object.T, unapply: JSON.T => Option[A]): List[A] =
     {
       val results = new mutable.ListBuffer[A]
       var after = ""
 
       do {
         val result =
           execute(method, params = params ++ JSON.optional("after" -> proper_string(after)))
         results ++= result.get_value(JSON.list(_, "data", unapply))
         after = result.get_value(JSON.value(_, "cursor", JSON.string0(_, "after")))
       } while (after.nonEmpty)
 
       results.toList
     }
 
     def ping(): String = execute("conduit.ping").get_string
 
 
     /* users */
 
     lazy val user_phid: String = execute("user.whoami").get_value(JSON.string(_, "phid"))
     lazy val user_name: String = execute("user.whoami").get_value(JSON.string(_, "userName"))
 
     def get_users(
       all: Boolean = false,
       phid: String = "",
       name: String = ""): List[API.User] =
     {
       val constraints: JSON.Object.T =
         (for { (key, value) <- List("phids" -> phid, "usernames" -> name) if value.nonEmpty }
           yield (key, List(value))).toMap
 
       execute_search("user.search",
           JSON.Object("queryKey" -> (if (all) "all" else "active"), "constraints" -> constraints),
             data => JSON.value(data, "fields", fields =>
               for {
                 id <- JSON.long(data, "id")
                 phid <- JSON.string(data, "phid")
                 name <- JSON.string(fields, "username")
                 real_name <- JSON.string0(fields, "realName")
                 roles <- JSON.strings(fields, "roles")
               } yield API.User(id, phid, name, real_name, roles)))
     }
 
     def the_user(phid: String): API.User =
       get_users(phid = phid) match {
         case List(user) => user
         case _ => error("Bad user PHID " + quote(phid))
       }
 
 
     /* repositories */
 
     def get_repositories(
       all: Boolean = false,
       phid: String = "",
       callsign: String = "",
       short_name: String = ""): List[API.Repository] =
     {
       val constraints: JSON.Object.T =
         (for {
           (key, value) <- List("phids" -> phid, "callsigns" -> callsign, "shortNames" -> short_name)
           if value.nonEmpty
         } yield (key, List(value))).toMap
 
       execute_search("diffusion.repository.search",
           JSON.Object("queryKey" -> (if (all) "all" else "active"), "constraints" -> constraints),
             data => JSON.value(data, "fields", fields =>
               for {
                 vcs_name <- JSON.string(fields, "vcs")
                 id <- JSON.long(data, "id")
                 phid <- JSON.string(data, "phid")
                 name <- JSON.string(fields, "name")
                 callsign <- JSON.string0(fields, "callsign")
                 short_name <- JSON.string0(fields, "shortName")
                 importing <- JSON.bool(fields, "isImporting")
               }
               yield {
                 val vcs = API.VCS.read(vcs_name)
                 val url_path =
                   if (short_name.isEmpty) "/diffusion/" + id else "/source/" + short_name
                 val ssh_url =
                   vcs match {
                     case API.VCS.hg => hg_url + url_path
                     case API.VCS.git => hg_url + url_path + ".git"
                     case API.VCS.svn => ""
                   }
                 API.Repository(vcs, id, phid, name, callsign, short_name, importing, ssh_url)
               }))
     }
 
     def the_repository(phid: String): API.Repository =
       get_repositories(phid = phid) match {
         case List(repo) => repo
         case _ => error("Bad repository PHID " + quote(phid))
       }
 
     def create_repository(
       name: String,
       callsign: String = "",    // unique name, UPPERCASE
       short_name: String = "",  // unique name
       description: String = "",
       public: Boolean = false,
       vcs: API.VCS.Value = API.VCS.hg): API.Repository =
     {
       require(name.nonEmpty)
 
       val transactions =
         API.edits("vcs", vcs.toString) :::
         API.edits("name", name) :::
         API.opt_edits("callsign", proper_string(callsign)) :::
         API.opt_edits("shortName", proper_string(short_name)) :::
         API.opt_edits("description", proper_string(description)) :::
         (if (public) Nil
          else API.edits("view", user_phid) ::: API.edits("policy.push", user_phid)) :::
         API.edits("status", "active")
 
       val phid =
         execute("diffusion.repository.edit", params = JSON.Object("transactions" -> transactions))
           .get_value(JSON.value(_, "object", JSON.string(_, "phid")))
 
       execute("diffusion.looksoon", params = JSON.Object("repositories" -> List(phid))).get
 
       the_repository(phid)
     }
   }
 }