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