--- a/src/Doc/System/Phabricator.thy Thu Nov 14 16:22:21 2019 +0100
+++ b/src/Doc/System/Phabricator.thy Thu Nov 14 21:49:49 2019 +0100
@@ -23,15 +23,14 @@
especially due to Microsoft's Github and Atlassian's Bitbucket.
The small company behind Phabricator provides paid plans for support and
- hosting of servers, but it is relatively easy to do \<^emph>\<open>independent
- self-hosting\<close> on a standard LAMP server (Linux, Apache, MySQL, PHP). This
- merely requires a virtual Ubuntu server on the net, which can be rented
- rather cheaply from local hosting providers (there is no need to follow big
- cloud corporations). So it is feasible to remain the master of your virtual
- home, following the slogan ``own all your data''. In many respects,
- Phabricator is similar to the well-known
- Nextcloud\<^footnote>\<open>\<^url>\<open>https://nextcloud.com\<close>\<close> product, concerning both the
- technology and sociology.
+ 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:
@@ -41,89 +40,94 @@
\<^item> Mercurial development \<^url>\<open>https://phab.mercurial-scm.org\<close>
\<^item> Isabelle development \<^url>\<open>https://isabelle-dev.sketis.net\<close>
- \<^medskip> Initial Phabricator server configuration requires many details to be done
+ \<^medskip> Initial Phabricator configuration requires many details to be done
right.\<^footnote>\<open>See also
\<^url>\<open>https://secure.phabricator.com/book/phabricator/article/installation_guide\<close>
in the context of \<^url>\<open>https://help.ubuntu.com/lts/serverguide\<close>.\<close> 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 a full Isabelle distribution again.
+ without requiring the somewhat bulky Isabelle distribution again.
\<close>
section \<open>Quick start\<close>
text \<open>
- The starting point is a fresh installation of \<^bold>\<open>Ubuntu 18.04 LTS\<close>: that
- particular version is required due to subtle dependencies on system
- configuration and add-on packages.
+ The starting point is a fresh installation of \<^bold>\<open>Ubuntu 18.04
+ LTS\<close>\<^footnote>\<open>\<^url>\<open>https://ubuntu.com/download\<close>\<close>: this version is mandatory due to
+ subtle dependencies on system packages and configuration that is assumed by
+ the Isabelle setup tool.
For production use, a proper \<^emph>\<open>Virtual Server\<close> or \<^emph>\<open>Root Server\<close> product
from a hosting provider will be required, including an Internet Domain Name
(a pseudo sub-domain in the style of Apache is sufficient).
Initial experimentation also works on a local host, e.g.\ via
- VirtualBox\<^footnote>\<open>\<^url>\<open>https://www.virtualbox.org\<close>\<close>. The public server behind
- \<^verbatim>\<open>lvh.me\<close> provides arbitrary subdomains as an alias to \<^verbatim>\<open>localhost\<close>, which
- will be used for the default installation below.
+ VirtualBox\<^footnote>\<open>\<^url>\<open>https://www.virtualbox.org\<close>\<close>. The public domain \<^verbatim>\<open>lvh.me\<close> is
+ used below: 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>).
+ \<^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 managed multiple named installations Phabricator installations:
- this allows to separate administrative responsibilities, e.g.\ different
- approaches to user management for different projects. Subsequently we always
- use the implicit default name ``\<^verbatim>\<open>vcs\<close>'': it will appear in file and
- directory locations, internal database names and URLs.
+ 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>'': it will appear in file and directory locations, internal
+ database names and URLs.
- The initial setup (with full Linux package upgrade) works as follows:
+ The initial setup works as follows (with full Linux package upgrade):
@{verbatim [display] \<open> isabelle phabricator_setup -U\<close>}
- After installing many packages and cloning the Phabricator distribution, the
- final output of the tool should be the URL for further manual configuration
- (using a local web browser). Here the key points are:
+ After installing many packages, cloning the Phabricator distribution,
+ initializing the MySQL database and Apache, the tool prints an URL for
+ further configuration. The following needs to be provided by the web
+ interface:
- \<^item> An initial user account that will get administrator rights. There is no
- need to create a separate \<^verbatim>\<open>admin\<close> account. Instead, a regular user that
- will take over this responsibility can be used here. Subsequently we
- assume that user \<^verbatim>\<open>makarius\<close> becomes the initial administrator.
+ \<^item> An 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.
- Note that Phabricator allows to delegate the responsibility of
- authentication to big corporations like Google and Facebook, but these can
- be easily avoided. Genuine self-hosting means to manage users directly,
- without outsourcing of authentication.
+ Alternatively, Phabricator can delegate the responsibility of
+ authentication to big corporations like Google and Facebook, but these can
+ be ignored. Genuine self-hosting means to manage users directly, without
+ outsourcing of authentication.
- \<^medskip>
- With the Auth Provider available, the administrator can now set a proper
- password. This works e.g.\ by initiating a local password reset procedure:
+ \<^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>}
+ @{verbatim [display] \<open> isabelle phabricator bin/auth recover makarius\<close>}
- The printed URL gives access to a password dialog in the web browser.
+ The printed URL gives access to a login and password dialog in the web
+ interface.
- Further users will be able to provide a password more directly, because the
- Auth Provider is now active.
+ 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. The request to
+ lock the configuration can be fulfilled as follows:
- \<^medskip>
- The pending request in Phabricator \<^bold>\<open>Setup Issues\<close> to lock the configuration
- can be fulfilled as follows:
+ @{verbatim [display] \<open> isabelle phabricator bin/auth lock\<close>}
- @{verbatim [display] \<open> isabelle phabricator bin/auth lock\<close>}
-
- \<^medskip>
- Most other Setup Issues can be ignored, after reading through them briefly
- to make sure that there are no genuine problems remaining.
+ \<^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, always
+ leaving some room for interpretation.
\<close>
@@ -131,34 +135,38 @@
text \<open>
The next important thing is messaging: Phabricator needs to be able to
- communicate with users. There are many variations on \<^emph>\<open>Mailer
- Configuration\<close>, but a conventional SMTP server connection with a dedicated
- \<^verbatim>\<open>phabricator\<close> user is sufficient. Note that there is no need to run a mail
- server on the self-hosted Linux machine: regular web-hosting packages
- usually allow to create new mail accounts easily. (As a last resort it is
- possible to use a service like Gmail, but that would again introduce
- unnecessary dependency on Google.)
+ 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> Now edit the generated JSON file to provide the mail account details. Then
- add and test it with Phabricator like this (to let Phabricator send a
- message to the administrator from above):
+ \<^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>}
- The mail configuration process can be refined and repeated until it really
- works: host name, port number, protocol etc.\ all need to be correct. The
- \<^verbatim>\<open>key\<close> field in the JSON file identifies the name of the configuration; it
+ 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>
- For information, the resulting mailer configuration can be queried like
- this:
+ This is how to query the current mail configuration:
@{verbatim [display] \<open> isabelle phabricator bin/config get cluster.mailers\<close>}
\<close>
@@ -169,10 +177,7 @@
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 ...\<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.
+ directly via \<^verbatim>\<open>sudo isabelle phabricator ...\<close>).
\<close>
@@ -217,8 +222,8 @@
@{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 based on
- \<^path>\<open>/etc/isabelle-phabricator.conf\<close>.
+ contrast to \<^verbatim>\<open>isabelle phabricator\<close> doing it automatically thanks to the
+ global configuration \<^path>\<open>/etc/isabelle-phabricator.conf\<close>.
\<close>
@@ -226,7 +231,7 @@
text \<open>
The @{tool_def phabricator_setup} installs a fresh Phabricator instance on
- Ubuntu Linux (notably 18.04 LTS):
+ Ubuntu 18.04 LTS:
@{verbatim [display] \<open>Usage: isabelle phabricator_setup [OPTIONS]
Options are:
@@ -240,41 +245,40 @@
The installation name (default: "vcs") is mapped to a regular
Unix user; this is relevant for public SSH access.\<close>}
- Installation requires Linux root user access. All required packages are
+ 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> and other directories like \<^verbatim>\<open>/var/www\<close>
- always use name prefixes \<^verbatim>\<open>isabelle-phabricator\<close> or \<^verbatim>\<open>phabricator\<close>. Local
+ 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 a default
- installation.
+ from \<^verbatim>\<open>phabricator-\<close>\<open>NAME\<close>, e.g.\ \<^verbatim>\<open>/var/www/phabricator-vcs\<close> for the
+ default.
- Knowing the conventions, it is possible to purge a Linux installation from
- Isabelle/Phabricator with some effort. There is no automated
- de-installation: it is often better to re-install a clean virtual machine
- image.
+ 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.
+ further packages required by Phabricator. This might require to reboot.
Option \<^verbatim>\<open>-n\<close> provides an alternative installation name. The default name
- \<^verbatim>\<open>vcs\<close> means ``Version Control System''. The name will appear in the URL for
- SSH access, and thus has some relevance to end-users. The initial server URL
- also uses that name suffix, but it can be changed later via regular Apache
- configuration.
+ \<^verbatim>\<open>vcs\<close> means ``version control system''. The name appears in the URL for SSH
+ access, and thus has some relevance to end-users. The initial server URL
+ also uses the same suffix, but that can (and should) be changed later via
+ regular Apache configuration.
Option \<^verbatim>\<open>-r\<close> specifies an alternative installation root directory: it needs
to be accessible for the Apache web server.
Option \<^verbatim>\<open>-R\<close> specifies an alternative directory for repositories that are
hosted by Phabricator. Provided that it is accessible for the Apache web
- server, the directory can be re-used directly for the builtin \<^verbatim>\<open>hgweb\<close> view
- by Mercurial. See also the documentation
- \<^url>\<open>https://www.mercurial-scm.org/wiki/PublishingRepositories#hgweb\<close> and the
- example \<^url>\<open>https://isabelle.sketis.net/repos\<close> for repositories in
- \<^url>\<open>https://isabelle-dev.sketis.net/diffusion\<close>.
+ 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>
@@ -282,7 +286,7 @@
text \<open>
The @{tool_def phabricator_setup_mail} provides mail configuration for an
- existing Phabricator installation (preferably via SMTP):
+ existing Phabricator installation:
@{verbatim [display] \<open>Usage: isabelle phabricator_setup_mail [OPTIONS]
Options are:
@@ -295,15 +299,15 @@
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. A single account for
- multiple Phabricator installations is sufficient, but the configuration
- needs to be set for each installation separately.
+ 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 being used here. The \<^verbatim>\<open>options\<close> specify the SMTP
- server address and account information.
+ 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
@@ -314,8 +318,9 @@
address is derived from the user profile.
Option \<^verbatim>\<open>-f\<close> refers to an existing JSON configuration file, e.g.\ from a
- different Phabricator installation: sharing mailers setup with the same mail
- address works for outgoing mails; incoming mails are not strictly needed.
+ 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>
end