71099
|
1 |
(*:maxLineLen=78:*)
|
|
2 |
|
|
3 |
theory Phabricator
|
|
4 |
imports Base
|
|
5 |
begin
|
|
6 |
|
|
7 |
chapter \<open>Phabricator server administration\<close>
|
|
8 |
|
|
9 |
text \<open>
|
|
10 |
Phabricator\<^footnote>\<open>\<^url>\<open>https://www.phacility.com/phabricator\<close>\<close> is an open-source
|
|
11 |
product to support the development process of complex software projects
|
|
12 |
(open or closed ones). The official slogan is:
|
|
13 |
|
|
14 |
\begin{quote}
|
|
15 |
Discuss. Plan. Code. Review. Test. \\
|
|
16 |
Every application your project needs, all in one tool.
|
|
17 |
\end{quote}
|
|
18 |
|
|
19 |
Ongoing changes and discussions about changes are maintained uniformly
|
|
20 |
within a MySQL database. There are standard connections to major version
|
|
21 |
control systems: \<^bold>\<open>Subversion\<close>, \<^bold>\<open>Mercurial\<close>, \<^bold>\<open>Git\<close>. So Phabricator offers
|
|
22 |
a counter-model to trends of monoculture and centralized version control,
|
|
23 |
especially due to Microsoft's Github and Atlassian's Bitbucket.
|
|
24 |
|
|
25 |
The small company behind Phabricator provides paid plans for support and
|
71131
|
26 |
hosting of servers, but it is easy to do \<^emph>\<open>independent self-hosting\<close> on a
|
|
27 |
standard LAMP server (Linux, Apache, MySQL, PHP). This merely requires a
|
|
28 |
virtual machine on the Net, which can be rented cheaply from local hosting
|
|
29 |
providers --- there is no need to follow big cloud corporations. So it is
|
|
30 |
feasible to remain the master of your virtual home, following the slogan
|
|
31 |
``own all your data''. In many respects, Phabricator is similar to the
|
|
32 |
well-known Nextcloud\<^footnote>\<open>\<^url>\<open>https://nextcloud.org\<close>\<close> product, concerning both
|
|
33 |
the technology and sociology.
|
71099
|
34 |
|
|
35 |
\<^medskip>
|
|
36 |
The following Phabricator instances may serve as examples:
|
|
37 |
|
|
38 |
\<^item> Phabricator development \<^url>\<open>https://secure.phabricator.com\<close>
|
|
39 |
\<^item> Wikimedia development \<^url>\<open>https://phabricator.wikimedia.org\<close>
|
|
40 |
\<^item> Mercurial development \<^url>\<open>https://phab.mercurial-scm.org\<close>
|
|
41 |
\<^item> Isabelle development \<^url>\<open>https://isabelle-dev.sketis.net\<close>
|
|
42 |
|
71131
|
43 |
\<^medskip> Initial Phabricator configuration requires many details to be done
|
71105
|
44 |
right.\<^footnote>\<open>See also
|
|
45 |
\<^url>\<open>https://secure.phabricator.com/book/phabricator/article/installation_guide\<close>
|
|
46 |
in the context of \<^url>\<open>https://help.ubuntu.com/lts/serverguide\<close>.\<close> Isabelle
|
|
47 |
provides some command-line tools to help with the setup, and afterwards
|
|
48 |
Isabelle support is optional: it is possible to run and maintain the server,
|
71131
|
49 |
without requiring the somewhat bulky Isabelle distribution again.
|
71099
|
50 |
\<close>
|
|
51 |
|
|
52 |
|
|
53 |
section \<open>Quick start\<close>
|
|
54 |
|
|
55 |
text \<open>
|
71131
|
56 |
The starting point is a fresh installation of \<^bold>\<open>Ubuntu 18.04
|
|
57 |
LTS\<close>\<^footnote>\<open>\<^url>\<open>https://ubuntu.com/download\<close>\<close>: this version is mandatory due to
|
|
58 |
subtle dependencies on system packages and configuration that is assumed by
|
|
59 |
the Isabelle setup tool.
|
71099
|
60 |
|
|
61 |
For production use, a proper \<^emph>\<open>Virtual Server\<close> or \<^emph>\<open>Root Server\<close> product
|
|
62 |
from a hosting provider will be required, including an Internet Domain Name
|
|
63 |
(a pseudo sub-domain in the style of Apache is sufficient).
|
|
64 |
|
|
65 |
Initial experimentation also works on a local host, e.g.\ via
|
71131
|
66 |
VirtualBox\<^footnote>\<open>\<^url>\<open>https://www.virtualbox.org\<close>\<close>. The public domain \<^verbatim>\<open>lvh.me\<close> is
|
|
67 |
used below: it maps arbitrary subdomains to \<^verbatim>\<open>localhost\<close>.
|
71099
|
68 |
|
|
69 |
All administrative commands need to be run as \<^verbatim>\<open>root\<close> user (e.g.\ via
|
71131
|
70 |
\<^verbatim>\<open>sudo\<close>). Note that Isabelle refers to user-specific configuration in the
|
|
71 |
user home directory via @{setting ISABELLE_HOME_USER}
|
|
72 |
(\secref{sec:settings}); that may be different or absent for the root user
|
|
73 |
and thus cause confusion.
|
71099
|
74 |
\<close>
|
|
75 |
|
|
76 |
|
|
77 |
subsection \<open>Initial setup\<close>
|
|
78 |
|
|
79 |
text \<open>
|
71131
|
80 |
Isabelle can manage multiple named Phabricator installations: this allows to
|
|
81 |
separate administrative responsibilities, e.g.\ different approaches to user
|
|
82 |
management for different projects. Subsequently we always use the default
|
|
83 |
name ``\<^verbatim>\<open>vcs\<close>'': it will appear in file and directory locations, internal
|
|
84 |
database names and URLs.
|
71099
|
85 |
|
71131
|
86 |
The initial setup works as follows (with full Linux package upgrade):
|
71099
|
87 |
|
|
88 |
@{verbatim [display] \<open> isabelle phabricator_setup -U\<close>}
|
|
89 |
|
71131
|
90 |
After installing many packages, cloning the Phabricator distribution,
|
|
91 |
initializing the MySQL database and Apache, the tool prints an URL for
|
|
92 |
further configuration. The following needs to be provided by the web
|
|
93 |
interface:
|
71099
|
94 |
|
71131
|
95 |
\<^item> An initial user that will get administrator rights. There is no need to
|
|
96 |
create a special \<^verbatim>\<open>admin\<close> account. Instead, a regular user that will take
|
|
97 |
over this responsibility can be used here. Subsequently we assume that
|
|
98 |
user \<^verbatim>\<open>makarius\<close> becomes the initial administrator.
|
71099
|
99 |
|
|
100 |
\<^item> An \<^emph>\<open>Auth Provider\<close> to manage user names and passwords. None is provided
|
|
101 |
by default, and Phabricator points out this omission prominently in its
|
|
102 |
overview of \<^emph>\<open>Setup Issues\<close>: following these hints quickly leads to the
|
|
103 |
place where a regular \<^emph>\<open>Username/Password\<close> provider can be added.
|
|
104 |
|
71131
|
105 |
Alternatively, Phabricator can delegate the responsibility of
|
|
106 |
authentication to big corporations like Google and Facebook, but these can
|
|
107 |
be ignored. Genuine self-hosting means to manage users directly, without
|
|
108 |
outsourcing of authentication.
|
71099
|
109 |
|
71131
|
110 |
\<^item> A proper password for the administrator can now be set, e.g.\ by the
|
|
111 |
following command:
|
71099
|
112 |
|
71131
|
113 |
@{verbatim [display] \<open> isabelle phabricator bin/auth recover makarius\<close>}
|
71099
|
114 |
|
71131
|
115 |
The printed URL gives access to a login and password dialog in the web
|
|
116 |
interface.
|
71099
|
117 |
|
71131
|
118 |
Any further users will be able to provide a password directly, because the
|
|
119 |
Auth Provider is already active.
|
|
120 |
|
|
121 |
\<^item> The list of Phabricator \<^bold>\<open>Setup Issues\<close> should be studied with some
|
|
122 |
care, to make sure that no serious problems are remaining. The request to
|
|
123 |
lock the configuration can be fulfilled as follows:
|
71099
|
124 |
|
71131
|
125 |
@{verbatim [display] \<open> isabelle phabricator bin/auth lock\<close>}
|
71099
|
126 |
|
71131
|
127 |
\<^medskip> A few other Setup Issues might be relevant as well, e.g.\ the timezone
|
|
128 |
of the server. Some more exotic points can be ignored: Phabricator
|
|
129 |
provides careful explanations about what it thinks could be wrong, always
|
|
130 |
leaving some room for interpretation.
|
71099
|
131 |
\<close>
|
|
132 |
|
|
133 |
|
|
134 |
subsection \<open>Mailer configuration\<close>
|
|
135 |
|
|
136 |
text \<open>
|
|
137 |
The next important thing is messaging: Phabricator needs to be able to
|
71131
|
138 |
communicate with users on its own account, e.g.\ to reset passwords. The
|
|
139 |
documentation has many variations on \<^emph>\<open>Configuring Outbound
|
|
140 |
Email\<close>\<^footnote>\<open>\<^url>\<open>https://secure.phabricator.com/book/phabricator/article/configuring_outbound_email\<close>\<close>,
|
|
141 |
but a conventional SMTP server with a dedicated \<^verbatim>\<open>phabricator\<close> user is
|
|
142 |
sufficient. There is no need to run a separate mail server on the
|
|
143 |
self-hosted Linux machine: hosting providers often include such a service
|
|
144 |
for free, e.g.\ as part of a web-hosting package. As a last resort it is
|
|
145 |
also possible to use a corporate service like Gmail, but such dependency
|
|
146 |
dilutes the whole effort of self-hosting.
|
71099
|
147 |
|
|
148 |
\<^medskip>
|
|
149 |
Mailer configuration requires a few command-line invocations as follows:
|
|
150 |
|
|
151 |
@{verbatim [display] \<open> isabelle phabricator_setup_mail\<close>}
|
|
152 |
|
71131
|
153 |
\<^noindent> This generates a JSON template file for the the mail account details.
|
|
154 |
After editing that, the subsequent command will add and test it with
|
|
155 |
Phabricator:
|
71099
|
156 |
|
|
157 |
@{verbatim [display] \<open> isabelle phabricator_setup_mail -T makarius\<close>}
|
|
158 |
|
71131
|
159 |
This tells Phabricator to send a message to the administrator created
|
|
160 |
before; the output informs about success or errors.
|
|
161 |
|
|
162 |
The mail configuration process can be refined and repeated until it works
|
|
163 |
properly: host name, port number, protocol etc.\ all need to be correct. The
|
|
164 |
\<^verbatim>\<open>key\<close> field in the JSON file identifies the name of the configuration that
|
71099
|
165 |
will be overwritten each time, when taking over the parameters via
|
|
166 |
\<^verbatim>\<open>isabelle phabricator_setup_mail\<close>.
|
|
167 |
|
|
168 |
\<^medskip>
|
71131
|
169 |
This is how to query the current mail configuration:
|
71099
|
170 |
|
71103
|
171 |
@{verbatim [display] \<open> isabelle phabricator bin/config get cluster.mailers\<close>}
|
|
172 |
\<close>
|
|
173 |
|
|
174 |
|
|
175 |
section \<open>Reference of command-line tools\<close>
|
|
176 |
|
|
177 |
text \<open>
|
|
178 |
The subsequent command-line tools usually require root user privileges on
|
|
179 |
the underlying Linux system (e.g.\ via \<^verbatim>\<open>sudo bash\<close> to open a subshell, or
|
71131
|
180 |
directly via \<^verbatim>\<open>sudo isabelle phabricator ...\<close>).
|
71103
|
181 |
\<close>
|
|
182 |
|
|
183 |
|
|
184 |
subsection \<open>\<^verbatim>\<open>isabelle phabricator\<close>\<close>
|
|
185 |
|
|
186 |
text \<open>
|
|
187 |
The @{tool_def phabricator} tool invokes a GNU bash command-line within the
|
|
188 |
Phabricator home directory:
|
|
189 |
@{verbatim [display]
|
|
190 |
\<open>Usage: isabelle phabricator [OPTIONS] COMMAND [ARGS...]
|
|
191 |
|
|
192 |
Options are:
|
|
193 |
-l list available Phabricator installations
|
|
194 |
-n NAME Phabricator installation name (default: "vcs")
|
|
195 |
|
|
196 |
Invoke a command-line tool within the home directory of the named
|
|
197 |
Phabricator installation.\<close>}
|
|
198 |
|
|
199 |
Isabelle/Phabricator installations are registered in the global
|
|
200 |
configuration file \<^path>\<open>/etc/isabelle-phabricator.conf\<close>, with name and
|
|
201 |
root directory separated by colon (no extra whitespace). The home directory
|
|
202 |
is the subdirectory \<^verbatim>\<open>phabricator\<close> within the root.
|
|
203 |
|
|
204 |
\<^medskip> Option \<^verbatim>\<open>-l\<close> lists the available Phabricator installations with name and
|
|
205 |
root directory.
|
|
206 |
|
|
207 |
Option \<^verbatim>\<open>-n\<close> selects the explicitly named Phabricator installation.
|
|
208 |
\<close>
|
|
209 |
|
|
210 |
|
|
211 |
subsubsection \<open>Examples\<close>
|
|
212 |
|
|
213 |
text \<open>
|
|
214 |
Print the home directory of the Phabricator installation:
|
|
215 |
@{verbatim [display] \<open>isabelle phabricator pwd\<close>}
|
|
216 |
|
|
217 |
Print some Phabricator configuration information:
|
|
218 |
@{verbatim [display] \<open>isabelle phabricator bin/config get phabricator.base-uri\<close>}
|
|
219 |
|
|
220 |
The latter conforms to typical command templates seen in the original
|
|
221 |
Phabricator documentation:
|
|
222 |
@{verbatim [display] \<open>phabricator/ $ ./bin/config get phabricator.base-uri\<close>}
|
|
223 |
|
|
224 |
Here the user is meant to navigate to the Phabricator home manually, in
|
71131
|
225 |
contrast to \<^verbatim>\<open>isabelle phabricator\<close> doing it automatically thanks to the
|
|
226 |
global configuration \<^path>\<open>/etc/isabelle-phabricator.conf\<close>.
|
71103
|
227 |
\<close>
|
|
228 |
|
|
229 |
|
|
230 |
subsection \<open>\<^verbatim>\<open>isabelle phabricator_setup\<close>\<close>
|
|
231 |
|
|
232 |
text \<open>
|
|
233 |
The @{tool_def phabricator_setup} installs a fresh Phabricator instance on
|
71131
|
234 |
Ubuntu 18.04 LTS:
|
71103
|
235 |
@{verbatim [display] \<open>Usage: isabelle phabricator_setup [OPTIONS]
|
|
236 |
|
|
237 |
Options are:
|
|
238 |
-R DIR repository directory (default: "/var/www/phabricator-NAME/repo")
|
|
239 |
-U full update of system packages before installation
|
|
240 |
-n NAME Phabricator installation name (default: "vcs")
|
|
241 |
-r DIR installation root directory (default: "/var/www/phabricator-NAME")
|
|
242 |
|
|
243 |
Install Phabricator as LAMP application (Linux, Apache, MySQL, PHP).
|
|
244 |
|
|
245 |
The installation name (default: "vcs") is mapped to a regular
|
|
246 |
Unix user; this is relevant for public SSH access.\<close>}
|
|
247 |
|
71131
|
248 |
Installation requires Linux root permissions. All required packages are
|
71103
|
249 |
installed automatically beforehand, this includes the Apache web server and
|
|
250 |
the MySQL database engine.
|
|
251 |
|
71131
|
252 |
Global configuration in \<^verbatim>\<open>/etc\<close> or a few other directories like \<^verbatim>\<open>/var/www\<close>
|
|
253 |
uses name prefixes like \<^verbatim>\<open>isabelle-phabricator\<close> or \<^verbatim>\<open>phabricator\<close>. Local
|
71103
|
254 |
configuration for a particular installation uses more specific names derived
|
71131
|
255 |
from \<^verbatim>\<open>phabricator-\<close>\<open>NAME\<close>, e.g.\ \<^verbatim>\<open>/var/www/phabricator-vcs\<close> for the
|
|
256 |
default.
|
71103
|
257 |
|
71131
|
258 |
Knowing the naming conventions, it is possible to purge a Linux installation
|
|
259 |
from Isabelle/Phabricator with some effort, but there is no automated
|
|
260 |
procedure for de-installation. In the worst case, it might be better to
|
|
261 |
re-install the virtual machine from a clean image.
|
71103
|
262 |
|
|
263 |
\<^medskip>
|
|
264 |
Option \<^verbatim>\<open>-U\<close> ensures a full update of system packages, before installing
|
71131
|
265 |
further packages required by Phabricator. This might require to reboot.
|
71103
|
266 |
|
|
267 |
Option \<^verbatim>\<open>-n\<close> provides an alternative installation name. The default name
|
71131
|
268 |
\<^verbatim>\<open>vcs\<close> means ``version control system''. The name appears in the URL for SSH
|
|
269 |
access, and thus has some relevance to end-users. The initial server URL
|
|
270 |
also uses the same suffix, but that can (and should) be changed later via
|
|
271 |
regular Apache configuration.
|
71103
|
272 |
|
|
273 |
Option \<^verbatim>\<open>-r\<close> specifies an alternative installation root directory: it needs
|
|
274 |
to be accessible for the Apache web server.
|
|
275 |
|
|
276 |
Option \<^verbatim>\<open>-R\<close> specifies an alternative directory for repositories that are
|
|
277 |
hosted by Phabricator. Provided that it is accessible for the Apache web
|
71131
|
278 |
server, the directory can be reused for the \<^verbatim>\<open>hgweb\<close> view by Mercurial.\<^footnote>\<open>See
|
|
279 |
also the documentation
|
|
280 |
\<^url>\<open>https://www.mercurial-scm.org/wiki/PublishingRepositories\<close> and the
|
|
281 |
example \<^url>\<open>https://isabelle.sketis.net/repos\<close>.\<close>
|
71103
|
282 |
\<close>
|
|
283 |
|
|
284 |
|
|
285 |
subsection \<open>\<^verbatim>\<open>isabelle phabricator_setup_mail\<close>\<close>
|
|
286 |
|
|
287 |
text \<open>
|
|
288 |
The @{tool_def phabricator_setup_mail} provides mail configuration for an
|
71131
|
289 |
existing Phabricator installation:
|
71103
|
290 |
@{verbatim [display] \<open>Usage: isabelle phabricator_setup_mail [OPTIONS]
|
|
291 |
|
|
292 |
Options are:
|
|
293 |
-T USER send test mail to Phabricator user
|
|
294 |
-f FILE config file (default: "mailers.json" within
|
|
295 |
Phabricator root)
|
|
296 |
-n NAME Phabricator installation name (default: "vcs")
|
|
297 |
|
|
298 |
Provide mail configuration for existing Phabricator installation.\<close>}
|
|
299 |
|
|
300 |
Proper mail configuration is vital for Phabricator, but the details can be
|
|
301 |
tricky. A common approach is to re-use an existing SMTP mail service, as is
|
71131
|
302 |
often included in regular web hosting packages. It is sufficient to create
|
|
303 |
one mail account for multiple Phabricator installations, but the
|
|
304 |
configuration needs to be set for each installation.
|
71103
|
305 |
|
|
306 |
The first invocation of \<^verbatim>\<open>isabelle phabricator_setup_mail\<close> without options
|
|
307 |
creates a JSON template file. Its \<^verbatim>\<open>key\<close> entry should be changed to
|
|
308 |
something sensible to identify the configuration, e.g.\ the Internet Domain
|
71131
|
309 |
Name of the mail address. The \<^verbatim>\<open>options\<close> specify the SMTP server address and
|
|
310 |
account information.
|
71103
|
311 |
|
|
312 |
Another invocation of \<^verbatim>\<open>isabelle phabricator_setup_mail\<close> with updated JSON
|
|
313 |
file will change the underlying Phabricator installation. This can be done
|
|
314 |
repeatedly, until everything works as expected.
|
|
315 |
|
|
316 |
Option \<^verbatim>\<open>-T\<close> invokes a standard Phabricator test procedure for the mail
|
|
317 |
configuration. The argument needs to be a valid Phabricator user: the mail
|
|
318 |
address is derived from the user profile.
|
|
319 |
|
|
320 |
Option \<^verbatim>\<open>-f\<close> refers to an existing JSON configuration file, e.g.\ from a
|
71131
|
321 |
previous successful Phabricator installation: sharing mailers setup with the
|
|
322 |
same mail address is fine for outgoing mails; incoming mails are optional
|
|
323 |
and not configured here.
|
71099
|
324 |
\<close>
|
|
325 |
|
|
326 |
end
|