# HG changeset patch
# User wenzelm
# Date 1573766450 -3600
# Node ID e5984c853f7729c08d03f677ee0ff56f1885cbac
# Parent  1579a9160c7f48187e3034a49ee8519515b1460e
more documentation;

diff -r 1579a9160c7f -r e5984c853f77 src/Doc/System/Phabricator.thy
--- a/src/Doc/System/Phabricator.thy	Thu Nov 14 21:49:49 2019 +0100
+++ b/src/Doc/System/Phabricator.thy	Thu Nov 14 22:20:50 2019 +0100
@@ -172,6 +172,34 @@
 \<close>
 
 
+subsection \<open>SSH configuration\<close>
+
+text \<open>
+  SSH configuration is optional, but important to access hosted repositories
+  with public-key authentication.
+
+  The subsequent configuration is convenient, but also ambitious: it takes
+  away the standard port 22 from the operating system and assigns it to
+  Isabelle/Phabricator!
+
+  @{verbatim [display] \<open>  isabelle phabricator_setup_ssh -p 22 -q 222\<close>}
+
+  Afterwards, remote login to the server host needs to use that alternative
+  port 222. If there is a problem with it, there is usually remote console
+  access to the hosted virtual machine via some web interface of the provider.
+
+  \<^medskip>
+  The following more modest configuration uses port 2222 for Phabricator,
+  and restains port 22 for the operating system:
+
+  @{verbatim [display] \<open>  isabelle phabricator_setup_ssh -p 2222 -q 22\<close>}
+
+  \<^medskip>
+  The tool can be invoked multiple times with different parameters; ports are
+  changed back and forth each time and services restarted.
+\<close>
+
+
 section \<open>Reference of command-line tools\<close>
 
 text \<open>
@@ -212,14 +240,14 @@
 
 text \<open>
   Print the home directory of the Phabricator installation:
-  @{verbatim [display] \<open>isabelle phabricator pwd\<close>}
+  @{verbatim [display] \<open>  isabelle phabricator pwd\<close>}
 
   Print some Phabricator configuration information:
-  @{verbatim [display] \<open>isabelle phabricator bin/config get phabricator.base-uri\<close>}
+  @{verbatim [display] \<open>  isabelle phabricator bin/config get phabricator.base-uri\<close>}
 
   The latter conforms to typical command templates seen in the original
   Phabricator documentation:
-  @{verbatim [display] \<open>phabricator/ $ ./bin/config get phabricator.base-uri\<close>}
+  @{verbatim [display] \<open>  phabricator/ $ ./bin/config get phabricator.base-uri\<close>}
 
   Here the user is meant to navigate to the Phabricator home manually, in
   contrast to \<^verbatim>\<open>isabelle phabricator\<close> doing it automatically thanks to the
@@ -323,4 +351,54 @@
   and not configured here.
 \<close>
 
+
+subsection \<open>\<^verbatim>\<open>isabelle phabricator_setup_ssh\<close>\<close>
+
+text \<open>
+  The @{tool_def phabricator_setup_ssh} configures a special SSH service
+  for all Phabricator installations:
+  @{verbatim [display] \<open>Usage: isabelle phabricator_setup_ssh [OPTIONS]
+
+  Options are:
+    -p PORT      sshd port for Phabricator servers (default: 2222)
+    -q PORT      sshd port for the operating system (default: 22)
+    -T           test the ssh service for each Phabricator installation
+
+  Configure ssh service for all Phabricator installations: a separate sshd
+  is run in addition to the one of the operating system, and ports need to
+  be distinct.
+
+  A particular Phabricator installation is addressed by using its
+  name as the ssh user; the actual Phabricator user is determined via
+  stored ssh keys.\<close>}
+
+  This is optional, but very useful. It allows to refer to hosted repositories
+  via ssh with the usual public-key authentication. It also allows to
+  communicate with a Phabricator server via the JSON API of
+  \<^emph>\<open>Conduit\<close>\<^footnote>\<open>\<^url>\<open>https://secure.phabricator.com/book/phabricator/article/conduit\<close>\<close>.
+
+  \<^medskip> The Phabricator SSH server distinguishes installations by their name,
+  e.g.\ \<^verbatim>\<open>vcs\<close> as SSH user name. The public key that is used for
+  authentication identifies the user within Phabricator: there is a web
+  interface to provide that as part of the user profile.
+
+  The operating system already has an SSH server (by default on port 22) that
+  remains important for remote administration of the machine.
+
+  \<^medskip>
+  Options \<^verbatim>\<open>-p\<close> and \<^verbatim>\<open>-q\<close> allow to change the port assignment for both servers.
+  A common scheme is \<^verbatim>\<open>-p 22 -q 222\<close> to leave the standard port to
+  Phabricator, to simplify the ssh URL that users will see for remote
+  repository clones.
+
+  Redirecting the operating system sshd to port 222 requires some care: it
+  requires to adjust the remote login procedure, e.g.\ in \<^verbatim>\<open>$HOME/.ssh/config\<close>
+  to add a \<^verbatim>\<open>Port\<close> specification for the server machine.
+
+  \<^medskip>
+  Option \<^verbatim>\<open>-T\<close> tests the SSH connection by communicating via Conduit. This
+  requires to install the public key of the Linux root in some Phabricator
+  user profile, e.g.\ for the administrator.
+\<close>
+
 end