author | wenzelm |
Mon, 16 Dec 2019 19:54:59 +0100 | |
changeset 71290 | 8d21cba3bad4 |
parent 71286 | 058edb8f232c |
child 71292 | 8b745b4d71b5 |
permissions | -rw-r--r-- |
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> |
|
71290 | 40 |
\<^item> Blender development \<^url>\<open>https://developer.blender.org\<close> |
71099 | 41 |
\<^item> Mercurial development \<^url>\<open>https://phab.mercurial-scm.org\<close> |
42 |
\<^item> Isabelle development \<^url>\<open>https://isabelle-dev.sketis.net\<close> |
|
43 |
||
71131 | 44 |
\<^medskip> Initial Phabricator configuration requires many details to be done |
71105 | 45 |
right.\<^footnote>\<open>See also |
46 |
\<^url>\<open>https://secure.phabricator.com/book/phabricator/article/installation_guide\<close> |
|
47 |
in the context of \<^url>\<open>https://help.ubuntu.com/lts/serverguide\<close>.\<close> Isabelle |
|
48 |
provides some command-line tools to help with the setup, and afterwards |
|
49 |
Isabelle support is optional: it is possible to run and maintain the server, |
|
71131 | 50 |
without requiring the somewhat bulky Isabelle distribution again. |
71099 | 51 |
\<close> |
52 |
||
53 |
||
54 |
section \<open>Quick start\<close> |
|
55 |
||
56 |
text \<open> |
|
71131 | 57 |
The starting point is a fresh installation of \<^bold>\<open>Ubuntu 18.04 |
58 |
LTS\<close>\<^footnote>\<open>\<^url>\<open>https://ubuntu.com/download\<close>\<close>: this version is mandatory due to |
|
59 |
subtle dependencies on system packages and configuration that is assumed by |
|
60 |
the Isabelle setup tool. |
|
71099 | 61 |
|
62 |
For production use, a proper \<^emph>\<open>Virtual Server\<close> or \<^emph>\<open>Root Server\<close> product |
|
63 |
from a hosting provider will be required, including an Internet Domain Name |
|
71290 | 64 |
(\secref{sec:phabricator-domain}). |
71099 | 65 |
|
66 |
Initial experimentation also works on a local host, e.g.\ via |
|
71131 | 67 |
VirtualBox\<^footnote>\<open>\<^url>\<open>https://www.virtualbox.org\<close>\<close>. The public domain \<^verbatim>\<open>lvh.me\<close> is |
71290 | 68 |
used by default: it maps arbitrary subdomains to \<^verbatim>\<open>localhost\<close>. |
71099 | 69 |
|
70 |
All administrative commands need to be run as \<^verbatim>\<open>root\<close> user (e.g.\ via |
|
71131 | 71 |
\<^verbatim>\<open>sudo\<close>). Note that Isabelle refers to user-specific configuration in the |
72 |
user home directory via @{setting ISABELLE_HOME_USER} |
|
73 |
(\secref{sec:settings}); that may be different or absent for the root user |
|
74 |
and thus cause confusion. |
|
71099 | 75 |
\<close> |
76 |
||
77 |
||
78 |
subsection \<open>Initial setup\<close> |
|
79 |
||
80 |
text \<open> |
|
71131 | 81 |
Isabelle can manage multiple named Phabricator installations: this allows to |
82 |
separate administrative responsibilities, e.g.\ different approaches to user |
|
83 |
management for different projects. Subsequently we always use the default |
|
71290 | 84 |
name ``\<^verbatim>\<open>vcs\<close>'': the name will appear in file and directory locations, |
85 |
internal database names and URLs. |
|
71099 | 86 |
|
71131 | 87 |
The initial setup works as follows (with full Linux package upgrade): |
71099 | 88 |
|
71280
5a2033fc8f3d
avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents:
71279
diff
changeset
|
89 |
@{verbatim [display] \<open> isabelle phabricator_setup -U -M:\<close>} |
71099 | 90 |
|
71131 | 91 |
After installing many packages, cloning the Phabricator distribution, |
92 |
initializing the MySQL database and Apache, the tool prints an URL for |
|
71290 | 93 |
further configuration. Now the following needs to be provided by the web |
94 |
interface. |
|
71099 | 95 |
|
71131 | 96 |
\<^item> An initial user that will get administrator rights. There is no need to |
97 |
create a special \<^verbatim>\<open>admin\<close> account. Instead, a regular user that will take |
|
98 |
over this responsibility can be used here. Subsequently we assume that |
|
99 |
user \<^verbatim>\<open>makarius\<close> becomes the initial administrator. |
|
71099 | 100 |
|
101 |
\<^item> An \<^emph>\<open>Auth Provider\<close> to manage user names and passwords. None is provided |
|
102 |
by default, and Phabricator points out this omission prominently in its |
|
103 |
overview of \<^emph>\<open>Setup Issues\<close>: following these hints quickly leads to the |
|
104 |
place where a regular \<^emph>\<open>Username/Password\<close> provider can be added. |
|
105 |
||
71131 | 106 |
Alternatively, Phabricator can delegate the responsibility of |
107 |
authentication to big corporations like Google and Facebook, but these can |
|
71290 | 108 |
be easily ignored. Genuine self-hosting means to manage users directly, |
109 |
without outsourcing of authentication. |
|
71099 | 110 |
|
71131 | 111 |
\<^item> A proper password for the administrator can now be set, e.g.\ by the |
112 |
following command: |
|
71099 | 113 |
|
71131 | 114 |
@{verbatim [display] \<open> isabelle phabricator bin/auth recover makarius\<close>} |
71099 | 115 |
|
71131 | 116 |
The printed URL gives access to a login and password dialog in the web |
117 |
interface. |
|
71099 | 118 |
|
71131 | 119 |
Any further users will be able to provide a password directly, because the |
120 |
Auth Provider is already active. |
|
121 |
||
122 |
\<^item> The list of Phabricator \<^bold>\<open>Setup Issues\<close> should be studied with some |
|
71290 | 123 |
care, to make sure that no serious problems are remaining. For example, |
124 |
the request to lock the configuration can be fulfilled as follows: |
|
71099 | 125 |
|
71131 | 126 |
@{verbatim [display] \<open> isabelle phabricator bin/auth lock\<close>} |
71099 | 127 |
|
71131 | 128 |
\<^medskip> A few other Setup Issues might be relevant as well, e.g.\ the timezone |
129 |
of the server. Some more exotic points can be ignored: Phabricator |
|
71290 | 130 |
provides careful explanations about what it thinks could be wrong, while |
71131 | 131 |
leaving some room for interpretation. |
71099 | 132 |
\<close> |
133 |
||
134 |
||
135 |
subsection \<open>Mailer configuration\<close> |
|
136 |
||
137 |
text \<open> |
|
138 |
The next important thing is messaging: Phabricator needs to be able to |
|
71131 | 139 |
communicate with users on its own account, e.g.\ to reset passwords. The |
140 |
documentation has many variations on \<^emph>\<open>Configuring Outbound |
|
141 |
Email\<close>\<^footnote>\<open>\<^url>\<open>https://secure.phabricator.com/book/phabricator/article/configuring_outbound_email\<close>\<close>, |
|
142 |
but a conventional SMTP server with a dedicated \<^verbatim>\<open>phabricator\<close> user is |
|
143 |
sufficient. There is no need to run a separate mail server on the |
|
144 |
self-hosted Linux machine: hosting providers often include such a service |
|
145 |
for free, e.g.\ as part of a web-hosting package. As a last resort it is |
|
146 |
also possible to use a corporate service like Gmail, but such dependency |
|
147 |
dilutes the whole effort of self-hosting. |
|
71099 | 148 |
|
149 |
\<^medskip> |
|
150 |
Mailer configuration requires a few command-line invocations as follows: |
|
151 |
||
152 |
@{verbatim [display] \<open> isabelle phabricator_setup_mail\<close>} |
|
153 |
||
71131 | 154 |
\<^noindent> This generates a JSON template file for the the mail account details. |
155 |
After editing that, the subsequent command will add and test it with |
|
156 |
Phabricator: |
|
71099 | 157 |
|
158 |
@{verbatim [display] \<open> isabelle phabricator_setup_mail -T makarius\<close>} |
|
159 |
||
71131 | 160 |
This tells Phabricator to send a message to the administrator created |
161 |
before; the output informs about success or errors. |
|
162 |
||
163 |
The mail configuration process can be refined and repeated until it works |
|
164 |
properly: host name, port number, protocol etc.\ all need to be correct. The |
|
165 |
\<^verbatim>\<open>key\<close> field in the JSON file identifies the name of the configuration that |
|
71099 | 166 |
will be overwritten each time, when taking over the parameters via |
167 |
\<^verbatim>\<open>isabelle phabricator_setup_mail\<close>. |
|
168 |
||
169 |
\<^medskip> |
|
71290 | 170 |
The effective mail configuration can be queried like this: |
71099 | 171 |
|
71103 | 172 |
@{verbatim [display] \<open> isabelle phabricator bin/config get cluster.mailers\<close>} |
173 |
\<close> |
|
174 |
||
175 |
||
71132 | 176 |
subsection \<open>SSH configuration\<close> |
177 |
||
178 |
text \<open> |
|
179 |
SSH configuration is optional, but important to access hosted repositories |
|
180 |
with public-key authentication. |
|
181 |
||
71290 | 182 |
The subsequent configuration is convenient (and ambitious): it takes away |
183 |
the standard port 22 from the operating system and assigns it to |
|
184 |
Isabelle/Phabricator. |
|
71132 | 185 |
|
186 |
@{verbatim [display] \<open> isabelle phabricator_setup_ssh -p 22 -q 222\<close>} |
|
187 |
||
188 |
Afterwards, remote login to the server host needs to use that alternative |
|
71290 | 189 |
port 222. If there is a problem connecting again, the administrator can |
190 |
usually access a remote console via some web interface of the virtual server |
|
71267 | 191 |
provider. |
71132 | 192 |
|
193 |
\<^medskip> |
|
71267 | 194 |
The following alternative is more modest: it uses port 2222 for Phabricator, |
71290 | 195 |
and retains port 22 for the operating system. |
71132 | 196 |
|
197 |
@{verbatim [display] \<open> isabelle phabricator_setup_ssh -p 2222 -q 22\<close>} |
|
198 |
||
199 |
\<^medskip> |
|
200 |
The tool can be invoked multiple times with different parameters; ports are |
|
201 |
changed back and forth each time and services restarted. |
|
202 |
\<close> |
|
203 |
||
204 |
||
71290 | 205 |
subsection \<open>Public domain name and HTTPS configuration \label{sec:phabricator-domain}\<close> |
71278 | 206 |
|
207 |
text \<open> |
|
208 |
So far the Phabricator server has been accessible only on \<^verbatim>\<open>localhost\<close> (via |
|
209 |
the alias \<^verbatim>\<open>lvh.me\<close>). Proper configuration of a public Internet domain name |
|
210 |
(with HTTPS certificate from \<^emph>\<open>Let's Encrypt\<close>) works as follows. |
|
211 |
||
212 |
\<^item> Register a subdomain (e.g.\ \<^verbatim>\<open>vcs.example.org\<close>) as an alias for the IP |
|
213 |
address of the underlying Linux host. This usually works by some web |
|
214 |
interface of the hosting provider to edit DNS entries; it might require |
|
215 |
some time for updated DNS records to become publicly available. |
|
216 |
||
217 |
\<^item> Edit the Phabricator website configuration file in |
|
218 |
\<^path>\<open>/etc/apache2/sites-available/\<close> to specify \<^verbatim>\<open>ServerName\<close> and |
|
219 |
\<^verbatim>\<open>ServerAdmin\<close> like this: @{verbatim [display] \<open> ServerName vcs.example.org |
|
220 |
ServerAdmin webmaster@example.org\<close>} |
|
221 |
||
222 |
Then reload (or restart) Apache like this: |
|
223 |
@{verbatim [display] \<open> systemctl reload apache2\<close>} |
|
224 |
||
225 |
\<^item> Install \<^verbatim>\<open>certbot\<close> from \<^url>\<open>https://certbot.eff.org\<close> following the |
|
226 |
description for Apache and Ubuntu 18.04 on |
|
227 |
\<^url>\<open>https://certbot.eff.org/lets-encrypt/ubuntubionic-apache\<close>. Run |
|
228 |
\<^verbatim>\<open>certbot\<close> interactively and let it operate on the domain |
|
229 |
\<^verbatim>\<open>vcs.example.org\<close>. |
|
230 |
||
231 |
\<^item> Inform Phabricator about its new domain name like this: |
|
71290 | 232 |
@{verbatim [display] \<open> isabelle phabricator bin/config set \ |
71278 | 233 |
phabricator.base-uri https://vcs.example.org\<close>} |
234 |
||
71290 | 235 |
\<^item> Visit the website \<^verbatim>\<open>https://vcs.example.org\<close> and configure Phabricator |
236 |
as described before. The following options are particularly relevant for a |
|
237 |
public website: |
|
71278 | 238 |
|
239 |
\<^item> \<^emph>\<open>Auth Provider / Username/Password\<close>: disable \<^emph>\<open>Allow Registration\<close> to |
|
71290 | 240 |
avoid uncontrolled registrants; users can still be invited via email |
241 |
instead. |
|
71278 | 242 |
|
243 |
\<^item> Enable \<^verbatim>\<open>policy.allow-public\<close> to allow read-only access to resources, |
|
244 |
without requiring user registration. |
|
245 |
\<close> |
|
246 |
||
247 |
||
71271 | 248 |
section \<open>Global data storage and backups\<close> |
249 |
||
250 |
text \<open> |
|
251 |
The global state of a Phabricator installation consists of two main parts: |
|
252 |
||
253 |
\<^enum> The \<^emph>\<open>root directory\<close> according to |
|
254 |
\<^path>\<open>/etc/isabelle-phabricator.conf\<close> or \<^verbatim>\<open>isabelle phabricator -l\<close>: it |
|
255 |
contains the main PHP program suite with administrative tools, and some |
|
256 |
configuration files. The default setup also puts hosted repositories here |
|
257 |
(subdirectory \<^verbatim>\<open>repo\<close>). |
|
258 |
||
259 |
\<^enum> Multiple \<^emph>\<open>MySQL databases\<close> with a common prefix derived from the |
|
260 |
installation name --- the same name is used as database user name. |
|
261 |
||
71290 | 262 |
The root user may invoke \<^verbatim>\<open>/usr/local/bin/isabelle-phabricator-dump\<close> |
71279 | 263 |
to create a complete database dump within the root directory. Afterwards it |
264 |
is sufficient to make a conventional \<^bold>\<open>file-system backup\<close> of everything. To |
|
71271 | 265 |
restore the database state, see the explanations on \<^verbatim>\<open>mysqldump\<close> in |
266 |
\<^url>\<open>https://secure.phabricator.com/book/phabricator/article/configuring_backups\<close>. |
|
71279 | 267 |
|
268 |
\<^medskip> The following command-line tools are particularly interesting for advanced |
|
269 |
database maintenance (within the Phabricator root directory): |
|
270 |
@{verbatim [display] \<open> phabricator/bin/storage help dump |
|
271 |
phabricator/bin/storage help shell |
|
272 |
phabricator/bin/storage help destroy |
|
273 |
phabricator/bin/storage help renamespace\<close>} |
|
274 |
||
275 |
For example, copying a database snapshot from one installation to another |
|
276 |
works as follows. Run on the first installation root directory: |
|
277 |
||
278 |
@{verbatim [display] \<open> phabricator/bin/storage dump > dump1.sql |
|
71290 | 279 |
phabricator/bin/storage renamespace --from phabricator_vcs \ |
71279 | 280 |
--to phabricator_xyz --input dump1.sql --output dump2.sql\<close>} |
281 |
||
71290 | 282 |
Them run on the second installation root directory: |
71279 | 283 |
@{verbatim [display] \<open> phabricator/bin/storage destroy |
71290 | 284 |
phabricator/bin/storage shell < .../dump2.sql\<close>} |
71279 | 285 |
|
286 |
Local configuration in \<^verbatim>\<open>phabricator/config/local/\<close> and hosted repositories |
|
287 |
need to be treated separately within the file-system. For the latter |
|
288 |
see also these tools: |
|
289 |
@{verbatim [display] \<open> phabricator/bin/repository help list-paths |
|
290 |
phabricator/bin/repository help move-paths\<close>} |
|
71271 | 291 |
\<close> |
292 |
||
293 |
||
71286 | 294 |
section \<open>Upgrading Phabricator installations\<close> |
295 |
||
296 |
text \<open> |
|
297 |
The Phabricator developers publish a new version approx.\ every 1--4 weeks: |
|
298 |
see also \<^url>\<open>https://secure.phabricator.com/w/changelog\<close>. There is no need to |
|
299 |
follow such frequent updates on the spot, but it is a good idea to upgrade |
|
300 |
occasionally, see also |
|
301 |
\<^url>\<open>https://secure.phabricator.com/book/phabricator/article/upgrading\<close> for |
|
302 |
general explanations. |
|
303 |
||
304 |
The Isabelle/Phabricator setup provides a convenience tool to upgrade all |
|
305 |
installations uniformly: |
|
306 |
@{verbatim [display] \<open> /usr/local/bin/isabelle-phabricator-upgrade\<close>} |
|
307 |
||
308 |
This refers to the \<^verbatim>\<open>stable\<close> branch of the distribution repositories by |
|
309 |
default. Alternatively, it also possible to use the \<^verbatim>\<open>master\<close> like this: |
|
310 |
@{verbatim [display] \<open> /usr/local/bin/isabelle-phabricator-upgrade master\<close>} |
|
311 |
\<close> |
|
312 |
||
313 |
||
71103 | 314 |
section \<open>Reference of command-line tools\<close> |
315 |
||
316 |
text \<open> |
|
317 |
The subsequent command-line tools usually require root user privileges on |
|
318 |
the underlying Linux system (e.g.\ via \<^verbatim>\<open>sudo bash\<close> to open a subshell, or |
|
71131 | 319 |
directly via \<^verbatim>\<open>sudo isabelle phabricator ...\<close>). |
71103 | 320 |
\<close> |
321 |
||
322 |
||
323 |
subsection \<open>\<^verbatim>\<open>isabelle phabricator\<close>\<close> |
|
324 |
||
325 |
text \<open> |
|
326 |
The @{tool_def phabricator} tool invokes a GNU bash command-line within the |
|
327 |
Phabricator home directory: |
|
328 |
@{verbatim [display] |
|
329 |
\<open>Usage: isabelle phabricator [OPTIONS] COMMAND [ARGS...] |
|
330 |
||
331 |
Options are: |
|
332 |
-l list available Phabricator installations |
|
333 |
-n NAME Phabricator installation name (default: "vcs") |
|
334 |
||
335 |
Invoke a command-line tool within the home directory of the named |
|
336 |
Phabricator installation.\<close>} |
|
337 |
||
338 |
Isabelle/Phabricator installations are registered in the global |
|
339 |
configuration file \<^path>\<open>/etc/isabelle-phabricator.conf\<close>, with name and |
|
340 |
root directory separated by colon (no extra whitespace). The home directory |
|
341 |
is the subdirectory \<^verbatim>\<open>phabricator\<close> within the root. |
|
342 |
||
343 |
\<^medskip> Option \<^verbatim>\<open>-l\<close> lists the available Phabricator installations with name and |
|
71276
b4401dfd6544
clarified "isabelle phabricator -l": avoid surprise with non-existent default installation;
wenzelm
parents:
71271
diff
changeset
|
344 |
root directory --- without invoking a command. |
71103 | 345 |
|
346 |
Option \<^verbatim>\<open>-n\<close> selects the explicitly named Phabricator installation. |
|
347 |
\<close> |
|
348 |
||
349 |
||
350 |
subsubsection \<open>Examples\<close> |
|
351 |
||
352 |
text \<open> |
|
353 |
Print the home directory of the Phabricator installation: |
|
71132 | 354 |
@{verbatim [display] \<open> isabelle phabricator pwd\<close>} |
71103 | 355 |
|
356 |
Print some Phabricator configuration information: |
|
71132 | 357 |
@{verbatim [display] \<open> isabelle phabricator bin/config get phabricator.base-uri\<close>} |
71103 | 358 |
|
359 |
The latter conforms to typical command templates seen in the original |
|
360 |
Phabricator documentation: |
|
71132 | 361 |
@{verbatim [display] \<open> phabricator/ $ ./bin/config get phabricator.base-uri\<close>} |
71103 | 362 |
|
363 |
Here the user is meant to navigate to the Phabricator home manually, in |
|
71131 | 364 |
contrast to \<^verbatim>\<open>isabelle phabricator\<close> doing it automatically thanks to the |
365 |
global configuration \<^path>\<open>/etc/isabelle-phabricator.conf\<close>. |
|
71103 | 366 |
\<close> |
367 |
||
368 |
||
369 |
subsection \<open>\<^verbatim>\<open>isabelle phabricator_setup\<close>\<close> |
|
370 |
||
371 |
text \<open> |
|
71290 | 372 |
The @{tool_def phabricator_setup} tool installs a fresh Phabricator instance |
373 |
on Ubuntu 18.04 LTS: |
|
71103 | 374 |
@{verbatim [display] \<open>Usage: isabelle phabricator_setup [OPTIONS] |
375 |
||
376 |
Options are: |
|
71280
5a2033fc8f3d
avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents:
71279
diff
changeset
|
377 |
-M SOURCE install Mercurial from source: local PATH, or URL, or ":" |
71103 | 378 |
-R DIR repository directory (default: "/var/www/phabricator-NAME/repo") |
379 |
-U full update of system packages before installation |
|
380 |
-n NAME Phabricator installation name (default: "vcs") |
|
381 |
-r DIR installation root directory (default: "/var/www/phabricator-NAME") |
|
382 |
||
383 |
Install Phabricator as LAMP application (Linux, Apache, MySQL, PHP). |
|
384 |
||
385 |
The installation name (default: "vcs") is mapped to a regular |
|
386 |
Unix user; this is relevant for public SSH access.\<close>} |
|
387 |
||
71131 | 388 |
Installation requires Linux root permissions. All required packages are |
71103 | 389 |
installed automatically beforehand, this includes the Apache web server and |
390 |
the MySQL database engine. |
|
391 |
||
71131 | 392 |
Global configuration in \<^verbatim>\<open>/etc\<close> or a few other directories like \<^verbatim>\<open>/var/www\<close> |
393 |
uses name prefixes like \<^verbatim>\<open>isabelle-phabricator\<close> or \<^verbatim>\<open>phabricator\<close>. Local |
|
71103 | 394 |
configuration for a particular installation uses more specific names derived |
71131 | 395 |
from \<^verbatim>\<open>phabricator-\<close>\<open>NAME\<close>, e.g.\ \<^verbatim>\<open>/var/www/phabricator-vcs\<close> for the |
396 |
default. |
|
71103 | 397 |
|
71131 | 398 |
Knowing the naming conventions, it is possible to purge a Linux installation |
399 |
from Isabelle/Phabricator with some effort, but there is no automated |
|
400 |
procedure for de-installation. In the worst case, it might be better to |
|
401 |
re-install the virtual machine from a clean image. |
|
71103 | 402 |
|
403 |
\<^medskip> |
|
404 |
Option \<^verbatim>\<open>-U\<close> ensures a full update of system packages, before installing |
|
71290 | 405 |
further packages required by Phabricator. This might require a reboot. |
71103 | 406 |
|
71280
5a2033fc8f3d
avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents:
71279
diff
changeset
|
407 |
Option \<^verbatim>\<open>-M:\<close> installs a standard Mercurial release from source: this works |
5a2033fc8f3d
avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents:
71279
diff
changeset
|
408 |
better than the package provided by Ubuntu 18.04. Alternatively, an explicit |
5a2033fc8f3d
avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents:
71279
diff
changeset
|
409 |
file path or URL the source archive (\<^verbatim>\<open>.tar.gz\<close>) may be here. This option is |
5a2033fc8f3d
avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents:
71279
diff
changeset
|
410 |
recommended for production use, but it requires to \<^emph>\<open>uninstall\<close> existing |
5a2033fc8f3d
avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents:
71279
diff
changeset
|
411 |
Mercurial packages provided by the operating system. |
5a2033fc8f3d
avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
wenzelm
parents:
71279
diff
changeset
|
412 |
|
71103 | 413 |
Option \<^verbatim>\<open>-n\<close> provides an alternative installation name. The default name |
71131 | 414 |
\<^verbatim>\<open>vcs\<close> means ``version control system''. The name appears in the URL for SSH |
415 |
access, and thus has some relevance to end-users. The initial server URL |
|
416 |
also uses the same suffix, but that can (and should) be changed later via |
|
417 |
regular Apache configuration. |
|
71103 | 418 |
|
419 |
Option \<^verbatim>\<open>-r\<close> specifies an alternative installation root directory: it needs |
|
420 |
to be accessible for the Apache web server. |
|
421 |
||
422 |
Option \<^verbatim>\<open>-R\<close> specifies an alternative directory for repositories that are |
|
423 |
hosted by Phabricator. Provided that it is accessible for the Apache web |
|
71131 | 424 |
server, the directory can be reused for the \<^verbatim>\<open>hgweb\<close> view by Mercurial.\<^footnote>\<open>See |
425 |
also the documentation |
|
426 |
\<^url>\<open>https://www.mercurial-scm.org/wiki/PublishingRepositories\<close> and the |
|
427 |
example \<^url>\<open>https://isabelle.sketis.net/repos\<close>.\<close> |
|
71103 | 428 |
\<close> |
429 |
||
430 |
||
431 |
subsection \<open>\<^verbatim>\<open>isabelle phabricator_setup_mail\<close>\<close> |
|
432 |
||
433 |
text \<open> |
|
71290 | 434 |
The @{tool_def phabricator_setup_mail} tool provides mail configuration for |
435 |
an existing Phabricator installation: |
|
71103 | 436 |
@{verbatim [display] \<open>Usage: isabelle phabricator_setup_mail [OPTIONS] |
437 |
||
438 |
Options are: |
|
439 |
-T USER send test mail to Phabricator user |
|
440 |
-f FILE config file (default: "mailers.json" within |
|
441 |
Phabricator root) |
|
442 |
-n NAME Phabricator installation name (default: "vcs") |
|
443 |
||
444 |
Provide mail configuration for existing Phabricator installation.\<close>} |
|
445 |
||
446 |
Proper mail configuration is vital for Phabricator, but the details can be |
|
447 |
tricky. A common approach is to re-use an existing SMTP mail service, as is |
|
71131 | 448 |
often included in regular web hosting packages. It is sufficient to create |
449 |
one mail account for multiple Phabricator installations, but the |
|
450 |
configuration needs to be set for each installation. |
|
71103 | 451 |
|
452 |
The first invocation of \<^verbatim>\<open>isabelle phabricator_setup_mail\<close> without options |
|
453 |
creates a JSON template file. Its \<^verbatim>\<open>key\<close> entry should be changed to |
|
454 |
something sensible to identify the configuration, e.g.\ the Internet Domain |
|
71131 | 455 |
Name of the mail address. The \<^verbatim>\<open>options\<close> specify the SMTP server address and |
456 |
account information. |
|
71103 | 457 |
|
458 |
Another invocation of \<^verbatim>\<open>isabelle phabricator_setup_mail\<close> with updated JSON |
|
459 |
file will change the underlying Phabricator installation. This can be done |
|
460 |
repeatedly, until everything works as expected. |
|
461 |
||
462 |
Option \<^verbatim>\<open>-T\<close> invokes a standard Phabricator test procedure for the mail |
|
463 |
configuration. The argument needs to be a valid Phabricator user: the mail |
|
464 |
address is derived from the user profile. |
|
465 |
||
466 |
Option \<^verbatim>\<open>-f\<close> refers to an existing JSON configuration file, e.g.\ from a |
|
71131 | 467 |
previous successful Phabricator installation: sharing mailers setup with the |
468 |
same mail address is fine for outgoing mails; incoming mails are optional |
|
469 |
and not configured here. |
|
71099 | 470 |
\<close> |
471 |
||
71132 | 472 |
|
473 |
subsection \<open>\<^verbatim>\<open>isabelle phabricator_setup_ssh\<close>\<close> |
|
474 |
||
475 |
text \<open> |
|
71290 | 476 |
The @{tool_def phabricator_setup_ssh} tool configures a special SSH service |
71132 | 477 |
for all Phabricator installations: |
478 |
@{verbatim [display] \<open>Usage: isabelle phabricator_setup_ssh [OPTIONS] |
|
479 |
||
480 |
Options are: |
|
481 |
-p PORT sshd port for Phabricator servers (default: 2222) |
|
482 |
-q PORT sshd port for the operating system (default: 22) |
|
483 |
-T test the ssh service for each Phabricator installation |
|
484 |
||
485 |
Configure ssh service for all Phabricator installations: a separate sshd |
|
486 |
is run in addition to the one of the operating system, and ports need to |
|
487 |
be distinct. |
|
488 |
||
489 |
A particular Phabricator installation is addressed by using its |
|
490 |
name as the ssh user; the actual Phabricator user is determined via |
|
491 |
stored ssh keys.\<close>} |
|
492 |
||
493 |
This is optional, but very useful. It allows to refer to hosted repositories |
|
494 |
via ssh with the usual public-key authentication. It also allows to |
|
495 |
communicate with a Phabricator server via the JSON API of |
|
496 |
\<^emph>\<open>Conduit\<close>\<^footnote>\<open>\<^url>\<open>https://secure.phabricator.com/book/phabricator/article/conduit\<close>\<close>. |
|
497 |
||
498 |
\<^medskip> The Phabricator SSH server distinguishes installations by their name, |
|
499 |
e.g.\ \<^verbatim>\<open>vcs\<close> as SSH user name. The public key that is used for |
|
500 |
authentication identifies the user within Phabricator: there is a web |
|
501 |
interface to provide that as part of the user profile. |
|
502 |
||
503 |
The operating system already has an SSH server (by default on port 22) that |
|
504 |
remains important for remote administration of the machine. |
|
505 |
||
506 |
\<^medskip> |
|
507 |
Options \<^verbatim>\<open>-p\<close> and \<^verbatim>\<open>-q\<close> allow to change the port assignment for both servers. |
|
508 |
A common scheme is \<^verbatim>\<open>-p 22 -q 222\<close> to leave the standard port to |
|
509 |
Phabricator, to simplify the ssh URL that users will see for remote |
|
510 |
repository clones. |
|
511 |
||
512 |
Redirecting the operating system sshd to port 222 requires some care: it |
|
513 |
requires to adjust the remote login procedure, e.g.\ in \<^verbatim>\<open>$HOME/.ssh/config\<close> |
|
514 |
to add a \<^verbatim>\<open>Port\<close> specification for the server machine. |
|
515 |
||
516 |
\<^medskip> |
|
517 |
Option \<^verbatim>\<open>-T\<close> tests the SSH connection by communicating via Conduit. This |
|
518 |
requires to install the public key of the Linux root in some Phabricator |
|
519 |
user profile, e.g.\ for the administrator. |
|
520 |
\<close> |
|
521 |
||
71099 | 522 |
end |