diff --git a/Admin/cronjob/README b/Admin/cronjob/README
--- a/Admin/cronjob/README
+++ b/Admin/cronjob/README
@@ -1,59 +1,59 @@
 Administrative Isabelle cronjob
 ===============================
 
 - main server: virtual machine with cronjob and build_log database
 - backup file-system (for cumulative log files): i21isatest@lxbroy10:cronjob
 - backup identify job: i21isatest@lxcisa0
 
 - jobs: manual installation on target directory:
     cp "$ISABELLE_HOME/Admin/cronjob/self_update "$HOME/cronjob/self_update"
     cp "$ISABELLE_HOME/Admin/cronjob/plain_identify "$HOME/cronjob/plain_identify"
 
 - crontab: manual update on target machine
     crontab -l
     crontab -e
 
 - $HOME/cronjob/run/ -- run-time state
 
 - $HOME/cronjob/log/ -- cumulative log area
 
 
 Build Log Database Server
 =========================
 
-- Ubuntu 18.04 LTS Linux Server standard installation
+- Ubuntu 20.04 LTS Linux Server standard installation
   https://help.ubuntu.com/lts/serverguide
 
 - apt install unattended-upgrades
 
 - special user account:
   useradd -m -s /bin/bash isatest
 
 - SSH access for jsch (on each client):
   LOCALHOST$ ssh-keyscan -t rsa DBSERVER
   >> ~/.ssh/known_hosts
 
 - PostgreSQL:
 
   $ apt install postgresql
   $ apt install postgresql-client
 
   $ sudo -u postgres psql template1
   ALTER USER postgres with encrypted password '***';
 
   $ edit /etc/postgresql/10/main/pg_hba.conf
   local all postgres md5
   local all all md5
 
   $ systemctl restart postgresql.service
 
   $ createuser -U postgres --interactive isatest
   ALTER USER isatest with encrypted password '***';
 
   $ createdb -E UTF8 -T template0 --locale=en_US.utf8 -U postgres -O isatest isatest
 
 - Database backup or migration:
   https://www.postgresql.org/docs/9.5/static/backup-dump.html
 
      pg_dump -U postgres -Fc -v -d isatest > db.dump
   pg_restore -U postgres -Fc -v -d isatest < db.dump
diff --git a/src/Doc/System/Misc.thy b/src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy
+++ b/src/Doc/System/Misc.thy
@@ -1,389 +1,389 @@
 (*:maxLineLen=78:*)
 
 theory Misc
 imports Base
 begin
 
 chapter \<open>Miscellaneous tools \label{ch:tools}\<close>
 
 text \<open>
   Subsequently we describe various Isabelle related utilities, given in
   alphabetical order.
 \<close>
 
 section \<open>Building Isabelle docker images\<close>
 
 text \<open>
   Docker\<^footnote>\<open>\<^url>\<open>https://docs.docker.com\<close>\<close> provides a self-contained environment
   for complex applications called \<^emph>\<open>container\<close>, although it does not fully
   contain the program in a strict sense of the word. This includes basic
   operating system services (usually based on Linux), shared libraries and
   other required packages. Thus Docker is a light-weight alternative to
   regular virtual machines, or a heavy-weight alternative to conventional
   self-contained applications.
 
   Although Isabelle can be easily run on a variety of OS environments without
   extra containment, Docker images may occasionally be useful when a
   standardized Linux environment is required, even on
   Windows\<^footnote>\<open>\<^url>\<open>https://docs.docker.com/docker-for-windows\<close>\<close> and
   macOS\<^footnote>\<open>\<^url>\<open>https://docs.docker.com/docker-for-mac\<close>\<close>. Further uses are in
   common cloud computing environments, where applications need to be submitted
   as Docker images in the first place.
 
   \<^medskip>
   The @{tool_def build_docker} tool builds docker images from a standard
   Isabelle application archive for Linux:
 
   @{verbatim [display]
 \<open>Usage: isabelle build_docker [OPTIONS] APP_ARCHIVE
 
   Options are:
     -B NAME      base image (default "ubuntu")
     -E           set Isabelle/bin/isabelle as entrypoint
     -P NAME      additional Ubuntu package collection ("X11", "latex")
     -l NAME      default logic (default ISABELLE_LOGIC="HOL")
     -n           no docker build
     -o FILE      output generated Dockerfile
     -p NAME      additional Ubuntu package
     -t TAG       docker build tag
     -v           verbose
 
   Build Isabelle docker image with default logic image, using a standard
   Isabelle application archive for Linux (local file or remote URL).\<close>}
 
   Option \<^verbatim>\<open>-E\<close> sets \<^verbatim>\<open>bin/isabelle\<close> of the contained Isabelle distribution as
   the standard entry point of the Docker image. Thus \<^verbatim>\<open>docker run\<close> will
   imitate the \<^verbatim>\<open>isabelle\<close> command-line tool (\secref{sec:isabelle-tool}) of a
   regular local installation, but it lacks proper GUI support: \<^verbatim>\<open>isabelle jedit\<close>
   will not work without further provisions. Note that the default entrypoint
   may be changed later via \<^verbatim>\<open>docker run --entrypoint="..."\<close>.
 
   Option \<^verbatim>\<open>-t\<close> specifies the Docker image tag: this a symbolic name within the
   local Docker name space, but also relevant for Docker
   Hub\<^footnote>\<open>\<^url>\<open>https://hub.docker.com\<close>\<close>.
 
   Option \<^verbatim>\<open>-l\<close> specifies the default logic image of the Isabelle distribution
   contained in the Docker environment: it will be produced by \<^verbatim>\<open>isabelle build -b\<close>
   as usual (\secref{sec:tool-build}) and stored within the image.
 
   \<^medskip>
   Option \<^verbatim>\<open>-B\<close> specifies the Docker image taken as starting point for the
   Isabelle installation: it needs to be a suitable version of Ubuntu Linux.
   The default \<^verbatim>\<open>ubuntu\<close> refers to the latest LTS version provided by Canonical
   as the official Ubuntu vendor\<^footnote>\<open>\<^url>\<open>https://hub.docker.com/_/ubuntu\<close>\<close>. For
   Isabelle2021 this should be Ubuntu 20.04 LTS.
 
   Option \<^verbatim>\<open>-p\<close> includes additional Ubuntu packages, using the terminology
   of \<^verbatim>\<open>apt-get install\<close> within the underlying Linux distribution.
 
   Option \<^verbatim>\<open>-P\<close> refers to high-level package collections: \<^verbatim>\<open>X11\<close> or \<^verbatim>\<open>latex\<close> as
-  provided by \<^verbatim>\<open>isabelle build_docker\<close> (assuming Ubuntu 18.04 LTS). This
+  provided by \<^verbatim>\<open>isabelle build_docker\<close> (assuming Ubuntu 20.04 LTS). This
   imposes extra weight on the resulting Docker images. Note that \<^verbatim>\<open>X11\<close> will
   only provide remote X11 support according to the modest GUI quality
   standards of the late 1990-ies.
 
   \<^medskip>
   Option \<^verbatim>\<open>-n\<close> suppresses the actual \<^verbatim>\<open>docker build\<close> process. Option \<^verbatim>\<open>-o\<close>
   outputs the generated \<^verbatim>\<open>Dockerfile\<close>. Both options together produce a
   Dockerfile only, which might be useful for informative purposes or other
   tools.
 
   Option \<^verbatim>\<open>-v\<close> disables quiet-mode of the underlying \<^verbatim>\<open>docker build\<close> process.
 \<close>
 
 
 subsubsection \<open>Examples\<close>
 
 text \<open>
   Produce a Dockerfile (without image) from a remote Isabelle distribution:
   @{verbatim [display]
 \<open>  isabelle build_docker -E -n -o Dockerfile
     https://isabelle.in.tum.de/website-Isabelle2021/dist/Isabelle2021_linux.tar.gz\<close>}
 
   Build a standard Isabelle Docker image from a local Isabelle distribution,
   with \<^verbatim>\<open>bin/isabelle\<close> as executable entry point:
 
   @{verbatim [display]
 \<open>  isabelle build_docker -E -t test/isabelle:Isabelle2021 Isabelle2021_linux.tar.gz\<close>}
 
   Invoke the raw Isabelle/ML process within that image:
   @{verbatim [display]
 \<open>  docker run test/isabelle:Isabelle2021 process -e "Session.welcome ()"\<close>}
 
   Invoke a Linux command-line tool within the contained Isabelle system
   environment:
   @{verbatim [display]
 \<open>  docker run test/isabelle:Isabelle2021 env uname -a\<close>}
   The latter should always report a Linux operating system, even when running
   on Windows or macOS.
 \<close>
 
 
 section \<open>Managing Isabelle components \label{sec:tool-components}\<close>
 
 text \<open>
   The @{tool_def components} tool manages Isabelle components:
   @{verbatim [display]
 \<open>Usage: isabelle components [OPTIONS] [COMPONENTS ...]
 
   Options are:
     -I           init user settings
     -R URL       component repository (default $ISABELLE_COMPONENT_REPOSITORY)
     -a           resolve all missing components
     -l           list status
     -u DIR       update $ISABELLE_HOME_USER/components: add directory
     -x DIR       update $ISABELLE_HOME_USER/components: remove directory
 
   Resolve Isabelle components via download and installation: given COMPONENTS
   are identified via base name. Further operations manage etc/settings and
   etc/components in $ISABELLE_HOME_USER.
 
   ISABELLE_COMPONENT_REPOSITORY="..."
   ISABELLE_HOME_USER="..."
 \<close>}
 
   Components are initialized as described in \secref{sec:components} in a
   permissive manner, which can mark components as ``missing''. This state is
   amended by letting @{tool "components"} download and unpack components that
   are published on the default component repository
   \<^url>\<open>https://isabelle.in.tum.de/components\<close> in particular.
 
   Option \<^verbatim>\<open>-R\<close> specifies an alternative component repository. Note that
   \<^verbatim>\<open>file:///\<close> URLs can be used for local directories.
 
   Option \<^verbatim>\<open>-a\<close> selects all missing components to be resolved. Explicit
   components may be named as command line-arguments as well. Note that
   components are uniquely identified by their base name, while the
   installation takes place in the location that was specified in the attempt
   to initialize the component before.
 
   \<^medskip>
   Option \<^verbatim>\<open>-l\<close> lists the current state of available and missing components
   with their location (full name) within the file-system.
 
   \<^medskip>
   Option \<^verbatim>\<open>-I\<close> initializes the user settings file to subscribe to the standard
   components specified in the Isabelle repository clone --- this does not make
   any sense for regular Isabelle releases. An existing file that does not
   contain a suitable line ``\<^verbatim>\<open>init_components\<close>\<open>\<dots>\<close>\<^verbatim>\<open>components/main\<close>'' needs
   to be edited according to the printed explanation.
 
   \<^medskip>
   Options \<^verbatim>\<open>-u\<close> and \<^verbatim>\<open>-x\<close> operate on user components listed in
   \<^path>\<open>$ISABELLE_HOME_USER/etc/components\<close>: this avoid manual editing if
   Isabelle configuration files.
 \<close>
 
 
 section \<open>Viewing documentation \label{sec:tool-doc}\<close>
 
 text \<open>
   The @{tool_def doc} tool displays Isabelle documentation:
   @{verbatim [display]
 \<open>Usage: isabelle doc [DOC ...]
 
   View Isabelle documentation.\<close>}
 
   If called without arguments, it lists all available documents. Each line
   starts with an identifier, followed by a short description. Any of these
   identifiers may be specified as arguments, in order to display the
   corresponding document.
 
   \<^medskip>
   The @{setting ISABELLE_DOCS} setting specifies the list of directories
   (separated by colons) to be scanned for documentations.
 \<close>
 
 
 section \<open>Shell commands within the settings environment \label{sec:tool-env}\<close>
 
 text \<open>
   The @{tool_def env} tool is a direct wrapper for the standard
   \<^verbatim>\<open>/usr/bin/env\<close> command on POSIX systems, running within the Isabelle
   settings environment (\secref{sec:settings}).
 
   The command-line arguments are that of the underlying version of \<^verbatim>\<open>env\<close>. For
   example, the following invokes an instance of the GNU Bash shell within the
   Isabelle environment:
   @{verbatim [display] \<open>isabelle env bash\<close>}
 \<close>
 
 
 section \<open>Inspecting the settings environment \label{sec:tool-getenv}\<close>
 
 text \<open>The Isabelle settings environment --- as provided by the
   site-default and user-specific settings files --- can be inspected
   with the @{tool_def getenv} tool:
   @{verbatim [display]
 \<open>Usage: isabelle getenv [OPTIONS] [VARNAMES ...]
 
   Options are:
     -a           display complete environment
     -b           print values only (doesn't work for -a)
     -d FILE      dump complete environment to FILE
                  (null terminated entries)
 
   Get value of VARNAMES from the Isabelle settings.\<close>}
 
   With the \<^verbatim>\<open>-a\<close> option, one may inspect the full process environment that
   Isabelle related programs are run in. This usually contains much more
   variables than are actually Isabelle settings. Normally, output is a list of
   lines of the form \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close>. The \<^verbatim>\<open>-b\<close> option causes only the values
   to be printed.
 
   Option \<^verbatim>\<open>-d\<close> produces a dump of the complete environment to the specified
   file. Entries are terminated by the ASCII null character, i.e.\ the C string
   terminator.
 \<close>
 
 
 subsubsection \<open>Examples\<close>
 
 text \<open>
   Get the location of @{setting ISABELLE_HOME_USER} where user-specific
   information is stored:
   @{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>}
 
   \<^medskip>
   Get the value only of the same settings variable, which is particularly
   useful in shell scripts:
   @{verbatim [display] \<open>isabelle getenv -b ISABELLE_HOME_USER\<close>}
 \<close>
 
 
 section \<open>Mercurial repository setup \label{sec:hg-setup}\<close>
 
 text \<open>
   The @{tool_def hg_setup} tool simplifies the setup of Mercurial
   repositories, with hosting via Phabricator (\chref{ch:phabricator}) or SSH
   file server access.
 
   @{verbatim [display]
 \<open>Usage: isabelle hg_setup [OPTIONS] REMOTE LOCAL_DIR
 
   Options are:
     -n NAME      remote repository name (default: base name of LOCAL_DIR)
     -p PATH      Mercurial path name (default: "default")
     -r           assume that remote repository already exists
 
   Setup a remote vs. local Mercurial repository: REMOTE either refers to a
   Phabricator server "user@host" or SSH file server "ssh://user@host/path".\<close>}
 
   The \<^verbatim>\<open>REMOTE\<close> repository specification \<^emph>\<open>excludes\<close> the actual repository
   name: that is given by the base name of \<^verbatim>\<open>LOCAL_DIR\<close>, or via option \<^verbatim>\<open>-n\<close>.
 
   By default, both sides of the repository are created on demand by default.
   In contrast, option \<^verbatim>\<open>-r\<close> assumes that the remote repository already exists:
   it avoids accidental creation of a persistent repository with unintended
   name.
 
   The local \<^verbatim>\<open>.hg/hgrc\<close> file is changed to refer to the remote repository,
   usually via the symbolic path name ``\<^verbatim>\<open>default\<close>''; option \<^verbatim>\<open>-p\<close> allows to
   provided a different name.
 \<close>
 
 subsubsection \<open>Examples\<close>
 
 text \<open>
   Setup the current directory as a repository with Phabricator server hosting:
   @{verbatim [display] \<open>  isabelle hg_setup vcs@vcs.example.org .\<close>}
 
   \<^medskip>
   Setup the current directory as a repository with plain SSH server hosting:
   @{verbatim [display] \<open>  isabelle hg_setup ssh://files.example.org/data/repositories .\<close>}
 
   \<^medskip>
   Both variants require SSH access to the target server, via public key
   without password.
 \<close>
 
 
 section \<open>Installing standalone Isabelle executables \label{sec:tool-install}\<close>
 
 text \<open>
   By default, the main Isabelle binaries (@{executable "isabelle"} etc.) are
   just run from their location within the distribution directory, probably
   indirectly by the shell through its @{setting PATH}. Other schemes of
   installation are supported by the @{tool_def install} tool:
   @{verbatim [display]
 \<open>Usage: isabelle install [OPTIONS] BINDIR
 
   Options are:
     -d DISTDIR   refer to DISTDIR as Isabelle distribution
                  (default ISABELLE_HOME)
 
   Install Isabelle executables with absolute references to the
   distribution directory.\<close>}
 
   The \<^verbatim>\<open>-d\<close> option overrides the current Isabelle distribution directory as
   determined by @{setting ISABELLE_HOME}.
 
   The \<open>BINDIR\<close> argument tells where executable wrapper scripts for
   @{executable "isabelle"} and @{executable isabelle_scala_script} should be
   placed, which is typically a directory in the shell's @{setting PATH}, such
   as \<^verbatim>\<open>$HOME/bin\<close>.
 
   \<^medskip>
   It is also possible to make symbolic links of the main Isabelle executables
   manually, but making separate copies outside the Isabelle distribution
   directory will not work!
 \<close>
 
 
 section \<open>Creating instances of the Isabelle logo\<close>
 
 text \<open>
   The @{tool_def logo} tool creates variants of the Isabelle logo, for
   inclusion in PDF{\LaTeX} documents.
 
   @{verbatim [display]
 \<open>Usage: isabelle logo [OPTIONS] [NAME]
 
   Options are:
     -o FILE      alternative output file
     -q           quiet mode
 
   Create variant NAME of the Isabelle logo as "isabelle_name.pdf".\<close>}
 
   Option \<^verbatim>\<open>-o\<close> provides an alternative output file, instead of the default in
   the current directory: \<^verbatim>\<open>isabelle_\<close>\<open>name\<close>\<^verbatim>\<open>.pdf\<close> with the lower-case version
   of the given name.
 
   \<^medskip>
   Option \<^verbatim>\<open>-q\<close> omits printing of the resulting output file name.
 
   \<^medskip>
   Implementors of Isabelle tools and applications are encouraged to make
   derived Isabelle logos for their own projects using this template. The
   license is the same as for the regular Isabelle distribution (BSD).
 \<close>
 
 
 section \<open>Output the version identifier of the Isabelle distribution\<close>
 
 text \<open>
   The @{tool_def version} tool displays Isabelle version information:
   @{verbatim [display]
 \<open>Usage: isabelle version [OPTIONS]
 
   Options are:
     -i           short identification (derived from Mercurial id)
     -t           symbolic tags (derived from Mercurial id)
 
   Display Isabelle version information.\<close>}
 
   \<^medskip>
   The default is to output the full version string of the Isabelle
   distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2021: February 2021\<close>.
 
   \<^medskip>
   Option \<^verbatim>\<open>-i\<close> produces a short identification derived from the Mercurial id
   of the @{setting ISABELLE_HOME} directory; option \<^verbatim>\<open>-t\<close> prints version tags
   (if available).
 
   These options require either a repository clone or a repository archive
   (e.g. download of
   \<^url>\<open>https://isabelle.sketis.net/repos/isabelle/archive/tip.tar.gz\<close>).
 \<close>
 
 end
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,545 +1,545 @@
 (*: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 or 20.04
+  The starting point is a fresh installation of \<^bold>\<open>Ubuntu 20.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 Internet 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>Internet 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 or 20.04 on
+    description for Apache and Ubuntu 20.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.
 
     \<^item> Adjust \<^verbatim>\<open>phabricator.cookie-prefix\<close> for multiple installations with
     overlapping domains (see also the documentation of this configuration
     option within Phabricator).
 \<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 --- with the usual care to avoid breaking a production system
   (see also \secref{sec:phabricator-backup} for database dump and 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 or 20.04 LTS:
+  on Ubuntu 20.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")
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -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 --- 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 or 20.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
+  package provided by Ubuntu 20.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>-o\<close> augments the environment of Isabelle system options: relevant
   options for Isabelle/Phabricator have the prefix ``\<^verbatim>\<open>phabricator_\<close>'' (see
   also the result of e.g. ``\<^verbatim>\<open>isabelle options -l\<close>'').
 
   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/System/linux.scala b/src/Pure/System/linux.scala
--- a/src/Pure/System/linux.scala
+++ b/src/Pure/System/linux.scala
@@ -1,157 +1,156 @@
 /*  Title:      Pure/System/linux.scala
     Author:     Makarius
 
 Specific support for Linux, notably Ubuntu/Debian.
 */
 
 package isabelle
 
 
 import scala.util.matching.Regex
 
 
 object Linux
 {
   /* check system */
 
   def check_system(): Unit =
     if (!Platform.is_linux) error("Not a Linux system")
 
   def check_system_root(): Unit =
   {
     check_system()
     if (Isabelle_System.bash("id -u").check.out != "0") error("Not running as superuser (root)")
   }
 
 
   /* release */
 
   object Release
   {
     private val ID = """^Distributor ID:\s*(\S.*)$""".r
     private val RELEASE = """^Release:\s*(\S.*)$""".r
     private val DESCRIPTION = """^Description:\s*(\S.*)$""".r
 
     def apply(): Release =
     {
       val lines = Isabelle_System.bash("lsb_release -a").check.out_lines
       def find(R: Regex): String = lines.collectFirst({ case R(a) => a }).getOrElse("Unknown")
       new Release(find(ID), find(RELEASE), find(DESCRIPTION))
     }
   }
 
   final class Release private(val id: String, val release: String, val description: String)
   {
     override def toString: String = description
 
     def is_ubuntu: Boolean = id == "Ubuntu"
-    def is_ubuntu_18_04: Boolean = is_ubuntu && release == "18.04"
     def is_ubuntu_20_04: Boolean = is_ubuntu && release == "20.04"
   }
 
 
   /* packages */
 
   def reboot_required(): Boolean =
     Path.explode("/var/run/reboot-required").is_file
 
   def check_reboot_required(): Unit =
     if (reboot_required()) error("Reboot required")
 
   def package_update(progress: Progress = new Progress): Unit =
     progress.bash(
       """apt-get update -y && apt-get upgrade -y && apt autoremove -y""",
       echo = true).check
 
   def package_install(packages: List[String], progress: Progress = new Progress): Unit =
     progress.bash("apt-get install -y -- " + Bash.strings(packages), echo = true).check
 
   def package_installed(name: String): Boolean =
   {
     val result = Isabelle_System.bash("dpkg-query -s " + Bash.string(name))
     val pattern = """^Status:.*installed.*$""".r.pattern
     result.ok && result.out_lines.exists(line => pattern.matcher(line).matches)
   }
 
 
   /* users */
 
   def user_exists(name: String): Boolean =
     Isabelle_System.bash("id " + Bash.string(name)).ok
 
   def user_entry(name: String, field: Int): String =
   {
     val result = Isabelle_System.bash("getent passwd " + Bash.string(name)).check
     val fields = space_explode(':', result.out)
 
     if (1 <= field && field <= fields.length) fields(field - 1)
     else error("No passwd field " + field + " for user " + quote(name))
   }
 
   def user_description(name: String): String = user_entry(name, 5).takeWhile(_ != ',')
 
   def user_home(name: String): String = user_entry(name, 6)
 
   def user_add(name: String,
     description: String = "",
     system: Boolean = false,
     ssh_setup: Boolean = false): Unit =
   {
     require(!description.contains(','), "malformed description")
 
     if (user_exists(name)) error("User already exists: " + quote(name))
 
     Isabelle_System.bash(
       "adduser --quiet --disabled-password --gecos " + Bash.string(description) +
         (if (system) " --system --group --shell /bin/bash " else "") +
         " " + Bash.string(name)).check
 
     if (ssh_setup) {
       val id_rsa = user_home(name) + "/.ssh/id_rsa"
       Isabelle_System.bash("""
 if [ ! -f """ + Bash.string(id_rsa) + """ ]
 then
   yes '\n' | sudo -i -u """ + Bash.string(name) +
     """ ssh-keygen -q -f """ + Bash.string(id_rsa) + """
 fi
       """).check
     }
   }
 
 
   /* system services */
 
   def service_operation(op: String, name: String): Unit =
     Isabelle_System.bash("systemctl " + Bash.string(op) + " " + Bash.string(name)).check
 
   def service_enable(name: String): Unit = service_operation("enable", name)
   def service_disable(name: String): Unit = service_operation("disable", name)
   def service_start(name: String): Unit = service_operation("start", name)
   def service_stop(name: String): Unit = service_operation("stop", name)
   def service_restart(name: String): Unit = service_operation("restart", name)
 
   def service_shutdown(name: String): Unit =
     try { service_stop(name) }
     catch { case ERROR(_) => }
 
   def service_install(name: String, spec: String): Unit =
   {
     service_shutdown(name)
 
     val service_file = Path.explode("/lib/systemd/system") + Path.basic(name).ext("service")
     File.write(service_file, spec)
     Isabelle_System.chmod("644", service_file)
 
     service_enable(name)
     service_restart(name)
   }
 
 
   /* passwords */
 
   def generate_password(length: Int = 10): String =
   {
     require(length >= 6, "password too short")
     Isabelle_System.bash("pwgen " + length + " 1").check.out
   }
 }
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,1084 +1,1075 @@
 /*  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_ubuntu_18_04: List[String] =
+  val packages_ubuntu_20_04: List[String] =
     Build_Docker.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", "python-pygments",
+      "php-xml", "php-zip", "python3-pygments", "ssh", "subversion", "python-pygments",
       // mercurial build packages
-      "make", "gcc", "python", "python-dev", "python-docutils", "python-openssl")
-
-  val packages_ubuntu_20_04: List[String] =
-    packages_ubuntu_18_04.map(
-      {
-        case "python-pygments" => "python3-pygments"
-        case "python-dev" => "python2-dev"
-        case name => name
-      })
+      "make", "gcc", "python", "python2-dev", "python-docutils", "python-openssl")
 
   def packages: List[String] =
   {
     val release = Linux.Release()
-    if (release.is_ubuntu_18_04) packages_ubuntu_18_04
-    else if (release.is_ubuntu_20_04) packages_ubuntu_20_04
-    else error("Bad Linux version: expected Ubuntu 18.04 or 20.04 LTS")
+    if (release.is_ubuntu_20_04) packages_ubuntu_20_04
+    else error("Bad Linux version: expected Ubuntu 20.04 LTS")
   }
 
 
   /* global system resources */
 
   val www_user = "www-data"
 
   val daemon_user = "phabricator"
 
   val sshd_config: Path = 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: Int = SSH.default_port
   val alternative_system_port = 222
   val default_server_port = 2222
 
   val standard_mercurial_source = "https://www.mercurial-scm.org/release/mercurial-3.9.2.tar.gz"
 
 
 
   /** global configuration **/
 
   val global_config: Path = 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]): Unit =
   {
     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",
       Scala_Project.here, 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(result.print_return_code)
       }
     })
 
 
 
   /** setup **/
 
   def user_setup(name: String, description: String, ssh_setup: Boolean = false): Unit =
   {
     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 = new Progress): Unit =
   {
     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")
           Isabelle_System.download(mercurial_source, archive)
           archive
         }
         else Path.explode(mercurial_source)
 
       Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
       val build_dir = tmp_dir + Path.basic(File.get_dir(tmp_dir))
 
       progress.bash("make all && make install", cwd = build_dir.file, echo = true).check
     })
   }
 
   def phabricator_setup(
     options: Options,
     name: String = default_name,
     root: String = "",
     repo: String = "",
     package_update: Boolean = false,
     mercurial_source: String = "",
     progress: Progress = new Progress): Unit =
   {
     /* 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.exists((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/arcanist.git
         git -C arcanist reset --hard """ +
           Bash.string(options.string("phabricator_version_arcanist")) + """
 
         git clone --branch stable https://github.com/phacility/phabricator.git
         git -C phabricator reset --hard """ +
           Bash.string(options.string("phabricator_version_phabricator")) + """
       """).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 + ";" +
         """GRANT PROCESS ON *.* 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 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
     CustomLog ${APACHE_LOG_DIR}/access.log combined
 
     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 = Isabelle_System.make_directory(Path.explode("/var/tmp/phd"))
     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",
       Scala_Project.here, args =>
     {
       var mercurial_source = ""
       var repo = ""
       var package_update = false
       var name = default_name
       var options = Options.init()
       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) + """)
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or 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),
           "o:" -> (arg => options = options + arg),
           "r:" -> (arg => root = arg))
 
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
       val progress = new Console_Progress
 
       phabricator_setup(options, 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 = new Progress): Unit =
   {
     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: Unit =
     {
       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",
       Scala_Project.here, 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 == SSH.default_port) "#Port " + SSH.default_port 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(SSH.default_port)
         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 = new Progress): Unit =
   {
     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 == SSH.default_port) 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",
       Scala_Project.here, 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 = SSH.default_port): 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, "bad ssh host or port")
 
     private def ssh_user_prefix: String = SSH.user_prefix(ssh_user)
     private def ssh_port_suffix: String = SSH.port_suffix(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, "bad repository name")
 
       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)
     }
   }
 }