(*: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:
@{verbatim [display]
‹ isabelle phabricator bin/config set java.lang.NullPointerExcepti
on
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
phabricator/bin/storage renamespace --from phabricator_vcs java.lang.NullPointerException
--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
