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