# HG changeset patch # User wenzelm # Date 1573583539 -3600 # Node ID c073c4e795181069ae47e587548c91ce444ef379 # Parent 3d228a3a88e04a166613890a498d0579b4ca8530 more documentation; tuned; diff -r 3d228a3a88e0 -r c073c4e79518 src/Doc/System/Phabricator.thy --- a/src/Doc/System/Phabricator.thy Tue Nov 12 16:17:25 2019 +0100 +++ b/src/Doc/System/Phabricator.thy Tue Nov 12 19:32:19 2019 +0100 @@ -105,7 +105,7 @@ With the Auth Provider available, the administrator can now set a proper password. This works e.g.\ by initiating a local password reset procedure: - @{verbatim [display] \ isabelle phabricator ./bin/auth recover makarius\} + @{verbatim [display] \ isabelle phabricator bin/auth recover makarius\} The printed URL gives access to a password dialog in the web browser. @@ -116,7 +116,7 @@ The pending request in Phabricator Setup Issues to lock the configuration can be fulfilled as follows: - @{verbatim [display] \ isabelle phabricator ./bin/auth lock\} + @{verbatim [display] \ isabelle phabricator bin/auth lock\} \ @@ -153,7 +153,162 @@ For information, the resulting mailer configuration can be queried like this: - @{verbatim [display] \ isabelle phabricator ./bin/config get cluster.mailers\} + @{verbatim [display] \ isabelle phabricator bin/config get cluster.mailers\} +\ + + +section \Reference of command-line tools\ + +text \ + The subsequent command-line tools usually require root user privileges on + the underlying Linux system (e.g.\ via \<^verbatim>\sudo bash\ to open a subshell, or + directly via \<^verbatim>\sudo isabelle ...\). Note that Isabelle refers to + user-specific configuration in the user home directory via @{setting + ISABELLE_HOME_USER} (\secref{sec:settings}); that may be different or absent + for the root user and thus cause confusion. +\ + + +subsection \\<^verbatim>\isabelle phabricator\\ + +text \ + The @{tool_def phabricator} tool invokes a GNU bash command-line within the + Phabricator home directory: + @{verbatim [display] +\Usage: isabelle phabricator [OPTIONS] COMMAND [ARGS...] + + Options are: + -l list available Phabricator installations + -n NAME Phabricator installation name (default: "vcs") + + Invoke a command-line tool within the home directory of the named + Phabricator installation.\} + + Isabelle/Phabricator installations are registered in the global + configuration file \<^path>\/etc/isabelle-phabricator.conf\, with name and + root directory separated by colon (no extra whitespace). The home directory + is the subdirectory \<^verbatim>\phabricator\ within the root. + + \<^medskip> Option \<^verbatim>\-l\ lists the available Phabricator installations with name and + root directory. + + Option \<^verbatim>\-n\ selects the explicitly named Phabricator installation. +\ + + +subsubsection \Examples\ + +text \ + Print the home directory of the Phabricator installation: + @{verbatim [display] \isabelle phabricator pwd\} + + Print some Phabricator configuration information: + @{verbatim [display] \isabelle phabricator bin/config get phabricator.base-uri\} + + The latter conforms to typical command templates seen in the original + Phabricator documentation: + @{verbatim [display] \phabricator/ $ ./bin/config get phabricator.base-uri\} + + Here the user is meant to navigate to the Phabricator home manually, in + contrast to \<^verbatim>\isabelle phabricator\ doing it automatically based on + \<^path>\/etc/isabelle-phabricator.conf\. +\ + + +subsection \\<^verbatim>\isabelle phabricator_setup\\ + +text \ + The @{tool_def phabricator_setup} installs a fresh Phabricator instance on + Ubuntu Linux (notably 18.04 LTS): + @{verbatim [display] \Usage: isabelle phabricator_setup [OPTIONS] + + Options are: + -R DIR repository directory (default: "/var/www/phabricator-NAME/repo") + -U full update of system packages before installation + -n NAME Phabricator installation name (default: "vcs") + -r DIR installation root directory (default: "/var/www/phabricator-NAME") + + Install Phabricator as LAMP application (Linux, Apache, MySQL, PHP). + + The installation name (default: "vcs") is mapped to a regular + Unix user; this is relevant for public SSH access.\} + + Installation requires Linux root user access. All required packages are + installed automatically beforehand, this includes the Apache web server and + the MySQL database engine. + + Global configuration in \<^verbatim>\/etc\ and other directories like \<^verbatim>\/var/www\ + always use name prefixes \<^verbatim>\isabelle-phabricator\ or \<^verbatim>\phabricator\. Local + configuration for a particular installation uses more specific names derived + from \<^verbatim>\phabricator-\\NAME\, e.g. \<^verbatim>\/var/www/phabricator-vcs\ for a default + installation. + + Knowing the conventions, it is possible to purge a Linux installation from + Isabelle/Phabricator with some effort. There is no automated + de-installation: it is often better to re-install a clean virtual machine + image. + + \<^medskip> + Option \<^verbatim>\-U\ ensures a full update of system packages, before installing + further packages required by Phabricator. + + Option \<^verbatim>\-n\ provides an alternative installation name. The default name + \<^verbatim>\vcs\ means ``Version Control System''. The name will appear in the URL for + SSH access, and thus has some relevance to end-users. The initial server URL + also uses that name suffix, but it can be changed later via regular Apache + configuration. + + Option \<^verbatim>\-r\ specifies an alternative installation root directory: it needs + to be accessible for the Apache web server. + + Option \<^verbatim>\-R\ specifies an alternative directory for repositories that are + hosted by Phabricator. Provided that it is accessible for the Apache web + server, the directory can be re-used directly for the builtin \<^verbatim>\hgweb\ view + by Mercurial. See also the documentation + \<^url>\https://www.mercurial-scm.org/wiki/PublishingRepositories#hgweb\ and the + example \<^url>\https://isabelle.sketis.net/repos\ for repositories in + \<^url>\https://isabelle-dev.sketis.net/diffusion\. +\ + + +subsection \\<^verbatim>\isabelle phabricator_setup_mail\\ + +text \ + The @{tool_def phabricator_setup_mail} provides mail configuration for an + existing Phabricator installation (preferably via SMTP): + @{verbatim [display] \Usage: isabelle phabricator_setup_mail [OPTIONS] + + Options are: + -T USER send test mail to Phabricator user + -f FILE config file (default: "mailers.json" within + Phabricator root) + -n NAME Phabricator installation name (default: "vcs") + + Provide mail configuration for existing Phabricator installation.\} + + Proper mail configuration is vital for Phabricator, but the details can be + tricky. A common approach is to re-use an existing SMTP mail service, as is + often included in regular web hosting packages. A single account for + multiple Phabricator installations is sufficient, but the configuration + needs to be set for each installation separately. + + The first invocation of \<^verbatim>\isabelle phabricator_setup_mail\ without options + creates a JSON template file. Its \<^verbatim>\key\ entry should be changed to + something sensible to identify the configuration, e.g.\ the Internet Domain + Name of the mail address being used here. The \<^verbatim>\options\ specify the SMTP + server address and account information. + + Another invocation of \<^verbatim>\isabelle phabricator_setup_mail\ with updated JSON + file will change the underlying Phabricator installation. This can be done + repeatedly, until everything works as expected. + + Option \<^verbatim>\-T\ invokes a standard Phabricator test procedure for the mail + configuration. The argument needs to be a valid Phabricator user: the mail + address is derived from the user profile. + + Option \<^verbatim>\-f\ refers to an existing JSON configuration file, e.g.\ from a + different Phabricator installation: sharing mailers setup with the same mail + address works for outgoing mails; incoming mails are not strictly needed. \ end diff -r 3d228a3a88e0 -r c073c4e79518 src/Pure/Tools/phabricator.scala --- a/src/Pure/Tools/phabricator.scala Tue Nov 12 16:17:25 2019 +0100 +++ b/src/Pure/Tools/phabricator.scala Tue Nov 12 19:32:19 2019 +0100 @@ -116,8 +116,8 @@ -l list available Phabricator installations -n NAME Phabricator installation name (default: """ + quote(default_name) + """) - Invoke a command-line tool within the home directory of the named Phabricator - installation. + Invoke a command-line tool within the home directory of the named + Phabricator installation. """, "l" -> (_ => list = true), "n:" -> (arg => name = arg)) @@ -129,7 +129,7 @@ if (list) { for (config <- read_config()) { - progress.echo("phabricator " + quote(config.name) + " in " + config.root.implode) + progress.echo("phabricator " + quote(config.name) + " root " + config.root) } } @@ -388,10 +388,7 @@ -n NAME Phabricator installation name (default: """ + quote(default_name) + """) -r DIR installation root directory (default: """ + default_root("NAME") + """) - Install Phabricator as Ubuntu LAMP application (Linux, Apache, MySQL, PHP). - - Slogan: "Discuss. Plan. Code. Review. Test. - Every application your project needs, all in one tool." + Install Phabricator as LAMP application (Linux, Apache, MySQL, PHP). The installation name (default: """ + quote(default_name) + """) is mapped to a regular Unix user; this is relevant for public SSH access. @@ -493,7 +490,7 @@ Options are: -T USER send test mail to Phabricator user - -f FILE config file (default: """ + default_mailers + """ within installation root) + -f FILE config file (default: """ + default_mailers + """ within Phabricator root) -n NAME Phabricator installation name (default: """ + quote(default_name) + """) Provide mail configuration for existing Phabricator installation.