170 |
170 |
171 @{verbatim [display] \<open> isabelle phabricator bin/config get cluster.mailers\<close>} |
171 @{verbatim [display] \<open> isabelle phabricator bin/config get cluster.mailers\<close>} |
172 \<close> |
172 \<close> |
173 |
173 |
174 |
174 |
|
175 subsection \<open>SSH configuration\<close> |
|
176 |
|
177 text \<open> |
|
178 SSH configuration is optional, but important to access hosted repositories |
|
179 with public-key authentication. |
|
180 |
|
181 The subsequent configuration is convenient, but also ambitious: it takes |
|
182 away the standard port 22 from the operating system and assigns it to |
|
183 Isabelle/Phabricator! |
|
184 |
|
185 @{verbatim [display] \<open> isabelle phabricator_setup_ssh -p 22 -q 222\<close>} |
|
186 |
|
187 Afterwards, remote login to the server host needs to use that alternative |
|
188 port 222. If there is a problem with it, there is usually remote console |
|
189 access to the hosted virtual machine via some web interface of the provider. |
|
190 |
|
191 \<^medskip> |
|
192 The following more modest configuration uses port 2222 for Phabricator, |
|
193 and restains port 22 for the operating system: |
|
194 |
|
195 @{verbatim [display] \<open> isabelle phabricator_setup_ssh -p 2222 -q 22\<close>} |
|
196 |
|
197 \<^medskip> |
|
198 The tool can be invoked multiple times with different parameters; ports are |
|
199 changed back and forth each time and services restarted. |
|
200 \<close> |
|
201 |
|
202 |
175 section \<open>Reference of command-line tools\<close> |
203 section \<open>Reference of command-line tools\<close> |
176 |
204 |
177 text \<open> |
205 text \<open> |
178 The subsequent command-line tools usually require root user privileges on |
206 The subsequent command-line tools usually require root user privileges on |
179 the underlying Linux system (e.g.\ via \<^verbatim>\<open>sudo bash\<close> to open a subshell, or |
207 the underlying Linux system (e.g.\ via \<^verbatim>\<open>sudo bash\<close> to open a subshell, or |
210 |
238 |
211 subsubsection \<open>Examples\<close> |
239 subsubsection \<open>Examples\<close> |
212 |
240 |
213 text \<open> |
241 text \<open> |
214 Print the home directory of the Phabricator installation: |
242 Print the home directory of the Phabricator installation: |
215 @{verbatim [display] \<open>isabelle phabricator pwd\<close>} |
243 @{verbatim [display] \<open> isabelle phabricator pwd\<close>} |
216 |
244 |
217 Print some Phabricator configuration information: |
245 Print some Phabricator configuration information: |
218 @{verbatim [display] \<open>isabelle phabricator bin/config get phabricator.base-uri\<close>} |
246 @{verbatim [display] \<open> isabelle phabricator bin/config get phabricator.base-uri\<close>} |
219 |
247 |
220 The latter conforms to typical command templates seen in the original |
248 The latter conforms to typical command templates seen in the original |
221 Phabricator documentation: |
249 Phabricator documentation: |
222 @{verbatim [display] \<open>phabricator/ $ ./bin/config get phabricator.base-uri\<close>} |
250 @{verbatim [display] \<open> phabricator/ $ ./bin/config get phabricator.base-uri\<close>} |
223 |
251 |
224 Here the user is meant to navigate to the Phabricator home manually, in |
252 Here the user is meant to navigate to the Phabricator home manually, in |
225 contrast to \<^verbatim>\<open>isabelle phabricator\<close> doing it automatically thanks to the |
253 contrast to \<^verbatim>\<open>isabelle phabricator\<close> doing it automatically thanks to the |
226 global configuration \<^path>\<open>/etc/isabelle-phabricator.conf\<close>. |
254 global configuration \<^path>\<open>/etc/isabelle-phabricator.conf\<close>. |
227 \<close> |
255 \<close> |
321 previous successful Phabricator installation: sharing mailers setup with the |
349 previous successful Phabricator installation: sharing mailers setup with the |
322 same mail address is fine for outgoing mails; incoming mails are optional |
350 same mail address is fine for outgoing mails; incoming mails are optional |
323 and not configured here. |
351 and not configured here. |
324 \<close> |
352 \<close> |
325 |
353 |
|
354 |
|
355 subsection \<open>\<^verbatim>\<open>isabelle phabricator_setup_ssh\<close>\<close> |
|
356 |
|
357 text \<open> |
|
358 The @{tool_def phabricator_setup_ssh} configures a special SSH service |
|
359 for all Phabricator installations: |
|
360 @{verbatim [display] \<open>Usage: isabelle phabricator_setup_ssh [OPTIONS] |
|
361 |
|
362 Options are: |
|
363 -p PORT sshd port for Phabricator servers (default: 2222) |
|
364 -q PORT sshd port for the operating system (default: 22) |
|
365 -T test the ssh service for each Phabricator installation |
|
366 |
|
367 Configure ssh service for all Phabricator installations: a separate sshd |
|
368 is run in addition to the one of the operating system, and ports need to |
|
369 be distinct. |
|
370 |
|
371 A particular Phabricator installation is addressed by using its |
|
372 name as the ssh user; the actual Phabricator user is determined via |
|
373 stored ssh keys.\<close>} |
|
374 |
|
375 This is optional, but very useful. It allows to refer to hosted repositories |
|
376 via ssh with the usual public-key authentication. It also allows to |
|
377 communicate with a Phabricator server via the JSON API of |
|
378 \<^emph>\<open>Conduit\<close>\<^footnote>\<open>\<^url>\<open>https://secure.phabricator.com/book/phabricator/article/conduit\<close>\<close>. |
|
379 |
|
380 \<^medskip> The Phabricator SSH server distinguishes installations by their name, |
|
381 e.g.\ \<^verbatim>\<open>vcs\<close> as SSH user name. The public key that is used for |
|
382 authentication identifies the user within Phabricator: there is a web |
|
383 interface to provide that as part of the user profile. |
|
384 |
|
385 The operating system already has an SSH server (by default on port 22) that |
|
386 remains important for remote administration of the machine. |
|
387 |
|
388 \<^medskip> |
|
389 Options \<^verbatim>\<open>-p\<close> and \<^verbatim>\<open>-q\<close> allow to change the port assignment for both servers. |
|
390 A common scheme is \<^verbatim>\<open>-p 22 -q 222\<close> to leave the standard port to |
|
391 Phabricator, to simplify the ssh URL that users will see for remote |
|
392 repository clones. |
|
393 |
|
394 Redirecting the operating system sshd to port 222 requires some care: it |
|
395 requires to adjust the remote login procedure, e.g.\ in \<^verbatim>\<open>$HOME/.ssh/config\<close> |
|
396 to add a \<^verbatim>\<open>Port\<close> specification for the server machine. |
|
397 |
|
398 \<^medskip> |
|
399 Option \<^verbatim>\<open>-T\<close> tests the SSH connection by communicating via Conduit. This |
|
400 requires to install the public key of the Linux root in some Phabricator |
|
401 user profile, e.g.\ for the administrator. |
|
402 \<close> |
|
403 |
326 end |
404 end |