(*:maxLineLen=78:*)

theory Phabricator
imports Base
begin

chapter ‹Phabricator / Phorge server setup \label{ch:phabricator}›

text ‹
 The Isabelle development site 🌐‹https://isabelle-dev.sketis.net› uses
 Phorge to provide a comprehensive view on several repositories: Isabelle
 proper, the Archive of Formal Proofs, and Poly/ML.

 Phorge🚫‹🌐‹https://phorge.it›› is an open-source product to support the
 development process of complex software projects (open or closed ones). It
 is a community fork to replace the former
 Phabricator🚫‹🌐‹https://www.phacility.com/phabricator›› project, which is
 now inactive. Subsequently, the product name is always ∗‹Phorge› instead of
 ∗‹Phabricator›, but files and other formal names usually refer to
 ▩‹phabricator›.

 Following the original tradition of Phabricator, almost everything in Phorge
 is a bit different and unusual. The official project description is:

 \begin{quote}
 Your opinionated Free/Libre and Open Source, community driven platform
 for collaborating, managing, organizing and reviewing software projects.
 \end{quote}

 Ongoing changes and discussions about changes are maintained uniformly
 within a MySQL database. There are standard connections to major version
 control systems: \‹Subversion›, \‹Mercurial›, \‹Git›. So Phorge offers a
 counter-model to trends of monopoly and centralized version control,
 especially due to Microsoft's Github and Atlassian's Bitbucket.

 A notable public instance of Phorge is running on 🌐‹https://gitpull.it›.
 Independent ∗‹self-hosting› requires an old-school LAMP server (Linux,
 Apache, MySQL, PHP): a cheap virtual machine on the Net is sufficient, there
 is no need for special ``cloud'' providers. So it is feasible to remain the
 master of your virtual home, according to the principle ``to own all your
 data''. Thus Phorge is similar to the well-known
 Nextcloud🚫‹🌐‹https://nextcloud.com›› server product, concerning both the
 technology and sociology.

 ┉
 Initial Phorge 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.

 ┉
 Assuming an existing installation of Phorge, the Isabelle 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 Phorge to make a new private repository with hosting on the
 server. (Phorge is a software project management platform, where initial
 repository setup happens rarely in practice.)
 ›


section ‹Quick start›

text ‹
 The starting point is a fresh installation of \‹Ubuntu 22.04 or 24.04
 LTS›🚫‹🌐‹https://ubuntu.com/download››: these versions are mandatory due to
 subtle dependencies on system packages and configuration that is assumed by
 the Isabelle setup tool.

 For production use, a proper ∗‹Virtual Server› or ∗‹Root Server› product
 from a hosting provider will be required, including an Internet Domain Name
 (\secref{sec:phorge-domain}). Initial experimentation also works on a local
 host, e.g.\ via VirtualBox🚫‹🌐‹https://www.virtualbox.org››. The proforma
 domain ▩‹localhost› is used by default: it maps arbitrary subdomains to the
 usual ▩‹localhost› address. This allows to use e.g.
 ▩‹http://phabricator-vcs.localhost› for initial setup as described below.

 All administrative commands need to be run as ▩‹root› user (e.g.\ via
 ▩‹sudo›). 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.
 ›


subsection ‹Initial setup›

text ‹
 Isabelle can manage multiple named Phorge installations: this allows to
 separate administrative responsibilities, e.g.\ different approaches to user
 management for different projects. Subsequently we always use the default
 name ``▩‹vcs›'': 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] ‹ isabelle phabricator_setup -U -M:›}

 After installing many packages, cloning the Phorge 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.

 ▪ An initial user that will get administrator rights. There is no need to
 create a special ▩‹admin› account. Instead, a regular user that will take
 over this responsibility can be used here. Subsequently we assume that
 user ▩‹makarius› becomes the initial administrator.

 ▪ An ∗‹Auth Provider› to manage user names and passwords. None is provided
 by default, and Phorge points out this omission prominently in its
 overview of ∗‹Setup Issues›: following these hints quickly leads to the
 place where a regular ∗‹Username/Password› provider can be added.

 Alternatively, Phorge 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.

 ▪ A proper password for the administrator can now be set, e.g.\ by the
 following command:

 @{verbatim [display] ‹ isabelle phabricator bin/auth recover makarius›}

 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.

 ▪ The list of Phorge \‹Setup Issues› 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] ‹ isabelle phabricator bin/auth lock›}

 ┉ A few other Setup Issues might be relevant as well, e.g.\ the timezone
 of the server. Some more exotic points can be ignored: Phorge provides
 careful explanations about what it thinks could be wrong, while leaving
 some room for interpretation. It may also help to reboot the host machine,
 to make sure that all Webserver + PHP configuration is properly activated.
 ›


subsection ‹Mailer configuration›

text ‹
 The next important thing is messaging: Phorge needs to be able to
 communicate with users on its own account, e.g.\ to reset passwords. The
 documentation has many variations on ∗‹Configuring Outbound
 Email›🚫‹🌐‹https://we.phorge.it/book/phorge/article/configuring_outbound_email››,
 but a conventional SMTP server with a dedicated ▩‹phabricator› 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.

 ┉
 Mailer configuration requires a few command-line invocations as follows:

 @{verbatim [display] ‹ isabelle phabricator_setup_mail›}

 🚫 This generates a JSON template file for the mail account details.
 After editing that, the subsequent command will add and test it with
 Phorge:

 @{verbatim [display] ‹ isabelle phabricator_setup_mail -T makarius›}

 This tells Phorge 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
 ▩‹key› field in the JSON file identifies the name of the configuration that
 will be overwritten each time, when taking over the parameters via
 ▩‹isabelle phabricator_setup_mail›.

 ┉
 The effective mail configuration can be queried like this:

 @{verbatim [display] ‹ isabelle phabricator bin/config get cluster.mailers›}
 ›


subsection ‹SSH configuration›

text ‹
 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 Phorge simultaneously.

 The subsequent configuration is convenient (and ambitious): it takes away
 the standard port 22 from the operating system and assigns it to
 Isabelle/Phorge.

 @{verbatim [display] ‹ isabelle phabricator_setup_ssh -p 22 -q 222›}

 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.

 ┉
 The following alternative is more modest: it uses port 2222 for Phorge, and
 retains port 22 for the operating system.

 @{verbatim [display] ‹ isabelle phabricator_setup_ssh -p 2222 -q 22›}

 ┉
 The tool can be invoked multiple times with different parameters; ports are
 changed back and forth each time and services restarted.
 ›


subsection ‹Internet domain name and HTTPS configuration \label{sec:phorge-domain}›

text ‹
 So far the Phorge server has been accessible only on ▩‹localhost›. Proper
 configuration of a public Internet domain name (with HTTPS certificate from
 ∗‹Let's Encrypt›) works as follows.

 ▪ Register a subdomain (e.g.\ ▩‹vcs.example.org›) 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.

 ▪ Edit the Phorge website configuration file in
 🚫‹/etc/apache2/sites-available/› to specify ▩‹ServerName› and
 ▩‹ServerAdmin› like this: @{verbatim [display] ‹ ServerName vcs.example.org
 ServerAdmin webmaster@example.org›}

 Then reload (or restart) Apache like this:
 @{verbatim [display] ‹ systemctl reload apache2›}

 ▪ Install ▩‹certbot› from 🌐‹https://certbot.eff.org› following the
 description for Apache and Ubuntu Linux. Run ▩‹certbot› interactively and
 let it operate on the domain ▩‹vcs.example.org›.

 ▪ Inform Phorge about its new domain name like this:
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
 phabricator.base-uri https://vcs.example.org›}

 ▪ Visit the website ▩‹https://vcs.example.org› and configure Phorge
 as described before. The following options are particularly relevant for a
 public website:

 ▪ ∗‹Auth Provider / Username/Password›: disable ∗‹Allow Registration› to
 avoid uncontrolled registrants; users can still be invited via email
 instead.

 ▪ Enable ▩‹policy.allow-public› to allow read-only access to resources,
 without requiring user registration.

 ▪ Adjust ▩‹phabricator.cookie-prefix› for multiple installations with
 overlapping domains (see also the documentation of this configuration
 option within Phorge).
 ›


section ‹Global data storage and backups \label{sec:phorge-backup}›

text ‹
 The global state of a Phorge installation consists of two main parts:

 ▸ The ∗‹root directory› according to
 🚫‹/etc/isabelle-phabricator.conf› or ▩‹isabelle phabricator -l›: it
 contains the main PHP program suite with administrative tools, and some
 configuration files. The default setup also puts hosted repositories here
 (subdirectory ▩‹repo›).

 ▸ Multiple ∗‹MySQL databases› with a common prefix derived from the
 installation name --- the same name is used as database user name.

 The root user may invoke ▩‹/usr/local/bin/isabelle-phabricator-dump› to
 create a complete database dump within the root directory. Afterwards it is
 sufficient to make a conventional \‹file-system backup› of everything. To
 restore the database state, see the explanations on ▩‹mysqldump› in
 🌐‹https://we.phorge.it/book/phorge/article/configuring_backups›; some
 background information is in
 🌐‹https://we.phorge.it/book/flavor/article/so_many_databases›.

 ┉ The following command-line tools are particularly interesting for advanced
 database maintenance (within the Phorge root directory that is traditionally
 called ▩‹phabricator›):
 @{verbatim [display] ‹ phabricator/bin/storage help dump
 phabricator/bin/storage help shell
 phabricator/bin/storage help destroy
 phabricator/bin/storage help renamespace›}

 For example, copying a database snapshot from one installation to another
 works as follows. Run on the first installation root directory:

 @{verbatim [display] ‹ phabricator/bin/storage dump > dump1.sql
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
 --to phabricator_xyz --input dump1.sql --output dump2.sql›}

 Then run on the second installation root directory:
 @{verbatim [display] ‹ phabricator/bin/storage destroy
 phabricator/bin/storage shell < .../dump2.sql›}

 Local configuration in ▩‹phabricator/config/local/› and hosted repositories
 need to be treated separately within the file-system. For the latter
 see also these tools:
 @{verbatim [display] ‹ phabricator/bin/repository help list-paths
 phabricator/bin/repository help move-paths›}
 ›


section ‹Upgrading Phorge installations›

text ‹
 The Phorge community publishes a new stable version several times per year:
 see also 🌐‹https://we.phorge.it/w/changelog›. There is no need to follow
 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:phorge-backup} for database dump and backup).

 The Isabelle/Phorge setup provides a convenience tool to upgrade all
 installations uniformly:
 @{verbatim [display] ‹ /usr/local/bin/isabelle-phabricator-upgrade›}

 This refers to the ▩‹stable› branch of the distribution repositories by
 default. Alternatively, it also possible to use the ▩‹master› like this:
 @{verbatim [display] ‹ /usr/local/bin/isabelle-phabricator-upgrade master›}

 ┉
 See 🌐‹https://we.phorge.it/book/phorge/article/upgrading› for further
 explanations on Phorge upgrade.
 ›


section ‹Reference of command-line tools›

text ‹
 The subsequent command-line tools usually require root user privileges on
 the underlying Linux system (e.g.\ via ▩‹sudo bash› to open a subshell, or
 directly via ▩‹sudo isabelle phabricator ...›).
 ›


subsection ‹▩‹isabelle phabricator››

text ‹
 The @{tool_def phabricator} tool invokes a GNU bash command-line within the
 Phorge home directory:
 @{verbatim [display]
 ‹Usage: isabelle phabricator [OPTIONS] COMMAND [ARGS...]

 Options are:
 -l list available Phorge installations
 -n NAME Phorge installation name (default: "vcs")

 Invoke a command-line tool within the home directory of the named
 Phorge installation.›}

 Isabelle/Phorge installations are registered in the global configuration
 file 🚫‹/etc/isabelle-phabricator.conf›, with name and root directory
 separated by colon (no extra whitespace). The home directory is the
 subdirectory ▩‹phabricator› within the root.

 ┉ Option ▩‹-l› lists the available Phorge installations with name and root
 directory --- without invoking a command.

 Option ▩‹-n› selects the explicitly named Phorge installation.
 ›


subsubsection ‹Examples›

text ‹
 Print the home directory of the Phorge installation:
 @{verbatim [display] ‹ isabelle phabricator pwd›}

 Print some Phorge configuration information:
 @{verbatim [display] ‹ isabelle phabricator bin/config get phabricator.base-uri›}

 The latter conforms to typical command templates seen in the original
 Phorge documentation:
 @{verbatim [display] ‹ phabricator/ $ ./bin/config get phabricator.base-uri›}

 Here the user is meant to navigate to the Phorge home manually, in
 contrast to ▩‹isabelle phabricator› doing it automatically thanks to the
 global configuration 🚫‹/etc/isabelle-phabricator.conf›.
 ›


subsection ‹▩‹isabelle phabricator_setup››

text ‹
 The @{tool_def phabricator_setup} tool installs a fresh Phorge instance
 on Ubuntu 22.04 or 24.04 LTS:
 @{verbatim [display] ‹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 Phorge 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 Phorge 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.›}

 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 ▩‹/etc› or a few other directories like ▩‹/var/www›
 uses name prefixes like ▩‹isabelle-phabricator› or ▩‹phabricator›. Local
 configuration for a particular installation uses more specific names derived
 from ▩‹phabricator-›‹NAME›, e.g.\ ▩‹/var/www/phabricator-vcs› for the
 default.

 Knowing the naming conventions, it is possible to purge a Linux installation
 from Isabelle/Phorge 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.

 ┉
 Option ▩‹-U› ensures a full update of system packages, before installing
 further packages required by Phorge. This might require a reboot.

 Option ▩‹-M:› installs a standard Mercurial release from source: a specific
 version that is known to work on Ubuntu 22.04 or 24.04, respectively. It is
 also possible to specify the path or URL of the source archive (▩‹.tar.gz›).
 This option is recommended for production use, but it requires to
 ∗‹uninstall› existing Mercurial packages provided by the operating system.

 Option ▩‹-n› provides an alternative installation name. The default name
 ▩‹vcs› 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 ▩‹-o› augments the environment of Isabelle system options: relevant
 options for Isabelle/Phorge have the prefix ``▩‹phabricator_›'' (see
 also the result of e.g. ``▩‹isabelle options -l›'').

 Option ▩‹-r› specifies an alternative installation root directory: it needs
 to be accessible for the Apache web server.

 Option ▩‹-R› specifies an alternative directory for repositories that are
 hosted by Phorge. Provided that it is accessible for the Apache web
 server, the directory can be reused for the ▩‹hgweb› view by Mercurial.🚫‹See
 also the documentation
 🌐‹https://www.mercurial-scm.org/wiki/PublishingRepositories› and the
 example 🌐‹https://isabelle.sketis.net/repos›.›
 ›


subsection ‹▩‹isabelle phabricator_setup_mail››

text ‹
 The @{tool_def phabricator_setup_mail} tool provides mail configuration for
 an existing Phorge installation:
 @{verbatim [display] ‹Usage: isabelle phabricator_setup_mail [OPTIONS]

 Options are:
 -T USER send test mail to Phorge user
 -f FILE config file (default: "mailers.json" within Phorge root)
 -n NAME Phorge installation name (default: "vcs")

 Provide mail configuration for existing Phorge installation.›}

 Proper mail configuration is vital for Phorge, 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 Phorge installations, but the
 configuration needs to be set for each installation.

 The first invocation of ▩‹isabelle phabricator_setup_mail› without options
 creates a JSON template file. Its ▩‹key› entry should be changed to
 something sensible to identify the configuration, e.g.\ the Internet Domain
 Name of the mail address. The ▩‹options› specify the SMTP server address and
 account information.

 Another invocation of ▩‹isabelle phabricator_setup_mail› with updated JSON
 file will change the underlying Phorge installation. This can be done
 repeatedly, until everything works as expected.

 Option ▩‹-T› invokes a standard Phorge test procedure for the mail
 configuration. The argument needs to be a valid Phorge user: the mail
 address is derived from the user profile.

 Option ▩‹-f› refers to an existing JSON configuration file, e.g.\ from a
 previous successful Phorge installation: sharing mailers setup with the
 same mail address is fine for outgoing mails; incoming mails are optional
 and not configured here.
 ›


subsection ‹▩‹isabelle phabricator_setup_ssh››

text ‹
 The @{tool_def phabricator_setup_ssh} tool configures a special SSH service
 for all Phorge installations:
 @{verbatim [display] ‹Usage: isabelle phabricator_setup_ssh [OPTIONS]

 Options are:
 -p PORT sshd port for Phorge servers (default: 2222)
 -q PORT sshd port for the operating system (default: 22)

 Configure ssh service for all Phorge installations: a separate sshd
 is run in addition to the one of the operating system, and ports need to
 be distinct.

 A particular Phorge installation is addressed by using its
 name as the ssh user; the actual Phorge user is determined via
 stored ssh keys.›}

 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 Phorge server via the JSON API of
 ∗‹Conduit›🚫‹🌐‹https://we.phorge.it/book/phorge/article/conduit››.

 ┉ The Phorge SSH server distinguishes installations by their name,
 e.g.\ ▩‹vcs› as SSH user name. The public key that is used for
 authentication identifies the user within Phorge: 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.

 ┉
 Options ▩‹-p› and ▩‹-q› allow to change the port assignment for both
 servers. A common scheme is ▩‹-p 22 -q 222› to leave the standard port to
 Phorge, to simplify the ssh URL that users will see for remote repository
 clones.🚫‹For the rare case of hosting Subversion repositories, port 22 is
 de-facto required. Otherwise Phorge presents malformed ▩‹svn+ssh› URLs with
 port specification.›

 Redirecting the operating system sshd to port 222 requires some care: it
 requires to adjust the remote login procedure, e.g.\ in ▩‹$HOME/.ssh/config›
 to add a ▩‹Port› specification for the server machine.
 ›

end