merged

--- a/src/Doc/ROOT	Tue Nov 12 12:33:05 2019 +0000
+++ b/src/Doc/ROOT	Tue Nov 12 19:47:44 2019 +0100
@@ -387,6 +387,7 @@
     Presentation
     Server
     Scala
+    Phabricator
     Misc
   document_files (in "..")
     "prepare_document"

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/System/Phabricator.thy	Tue Nov 12 19:47:44 2019 +0100
@@ -0,0 +1,314 @@
+(*:maxLineLen=78:*)
+
+theory Phabricator
+imports Base
+begin
+
+chapter \<open>Phabricator server administration\<close>
+
+text \<open>
+  Phabricator\<^footnote>\<open>\<^url>\<open>https://www.phacility.com/phabricator\<close>\<close> is an open-source
+  product to support the development process of complex software projects
+  (open or closed ones). The official slogan is:
+
+  \begin{quote}
+    Discuss. Plan. Code. Review. Test. \\
+    Every application your project needs, all in one tool.
+  \end{quote}
+
+  Ongoing changes and discussions about changes are maintained uniformly
+  within a MySQL database. There are standard connections to major version
+  control systems: \<^bold>\<open>Subversion\<close>, \<^bold>\<open>Mercurial\<close>, \<^bold>\<open>Git\<close>. So Phabricator offers
+  a counter-model to trends of monoculture and centralized version control,
+  especially due to Microsoft's Github and Atlassian's Bitbucket.
+
+  The small company behind Phabricator provides paid plans for support and
+  hosting of servers, but it is relatively easy to do \<^emph>\<open>independent
+  self-hosting\<close> on a standard LAMP server (Linux, Apache, MySQL, PHP). This
+  merely requires a virtual Ubuntu server on the net, which can be rented
+  rather cheaply from local hosting providers (there is no need to follow big
+  cloud corporations). So it is feasible to remain the master of your virtual
+  home, following the slogan ``own all your data''. In many respects,
+  Phabricator is similar to the well-known
+  Nextcloud\<^footnote>\<open>\<^url>\<open>https://nextcloud.com\<close>\<close> product, concerning both the
+  technology and sociology.
+
+  \<^medskip>
+  The following Phabricator instances may serve as examples:
+
+    \<^item> Phabricator development \<^url>\<open>https://secure.phabricator.com\<close>
+    \<^item> Wikimedia development \<^url>\<open>https://phabricator.wikimedia.org\<close>
+    \<^item> Mercurial development \<^url>\<open>https://phab.mercurial-scm.org\<close>
+    \<^item> Isabelle development \<^url>\<open>https://isabelle-dev.sketis.net\<close>
+
+  \<^medskip> Initial Phabricator server configuration requires many details to be done
+  right. Isabelle provides some command-line tools to help with it, but
+  afterwards Isabelle support is optional: it is possible to run and maintain
+  the server, without requiring a full Isabelle distribution again.
+\<close>
+
+
+section \<open>Quick start\<close>
+
+text \<open>
+  The starting point is a fresh installation of \<^bold>\<open>Ubuntu 18.04 LTS\<close>: that
+  particular version is required due to subtle dependencies on system
+  configuration and add-on packages.
+
+  For production use, a proper \<^emph>\<open>Virtual Server\<close> or \<^emph>\<open>Root Server\<close> product
+  from a hosting provider will be required, including an Internet Domain Name
+  (a pseudo sub-domain in the style of Apache is sufficient).
+
+  Initial experimentation also works on a local host, e.g.\ via
+  VirtualBox\<^footnote>\<open>\<^url>\<open>https://www.virtualbox.org\<close>\<close>. The public server behind
+  \<^verbatim>\<open>lvh.me\<close> provides arbitrary subdomains as an alias to \<^verbatim>\<open>localhost\<close>, which
+  will be used for the default installation below.
+
+  All administrative commands need to be run as \<^verbatim>\<open>root\<close> user (e.g.\ via
+  \<^verbatim>\<open>sudo\<close>).
+\<close>
+
+
+subsection \<open>Initial setup\<close>
+
+text \<open>
+  Isabelle can managed multiple named installations Phabricator installations:
+  this allows to separate administrative responsibilities, e.g.\ different
+  approaches to user management for different projects. Subsequently we always
+  use the implicit default name ``\<^verbatim>\<open>vcs\<close>'': it will appear in file and
+  directory locations, internal database names and URLs.
+
+  The initial setup (with full Linux package upgrade) works as follows:
+
+  @{verbatim [display] \<open>  isabelle phabricator_setup -U\<close>}
+
+  After installing many packages and cloning the Phabricator distribution, the
+  final output of the tool should be the URL for further manual configuration
+  (using a local web browser). Here the key points are:
+
+    \<^item> An initial user account that will get administrator rights. There is no
+    need to create a separate \<^verbatim>\<open>admin\<close> account. Instead, a regular user that
+    will take over this responsibility can be used here. Subsequently we
+    assume that user \<^verbatim>\<open>makarius\<close> becomes the initial administrator.
+
+    \<^item> An \<^emph>\<open>Auth Provider\<close> to manage user names and passwords. None is provided
+    by default, and Phabricator points out this omission prominently in its
+    overview of \<^emph>\<open>Setup Issues\<close>: following these hints quickly leads to the
+    place where a regular \<^emph>\<open>Username/Password\<close> provider can be added.
+
+  Note that Phabricator allows to delegate the responsibility of
+  authentication to big corporations like Google and Facebook, but these can
+  be easily avoided. Genuine self-hosting means to manage users directly,
+  without outsourcing of authentication.
+
+  \<^medskip>
+  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] \<open>  isabelle phabricator bin/auth recover makarius\<close>}
+
+  The printed URL gives access to a password dialog in the web browser.
+
+  Further users will be able to provide a password more directly, because the
+  Auth Provider is now active.
+
+  \<^medskip>
+  The pending request in Phabricator Setup Issues to lock the configuration
+  can be fulfilled as follows:
+
+  @{verbatim [display] \<open>  isabelle phabricator bin/auth lock\<close>}
+\<close>
+
+
+subsection \<open>Mailer configuration\<close>
+
+text \<open>
+  The next important thing is messaging: Phabricator needs to be able to
+  communicate with users. There are many variations on \<^emph>\<open>Mailer
+  Configuration\<close>, but a conventional SMTP server connection with a dedicated
+  \<^verbatim>\<open>phabricator\<close> user is sufficient. Note that there is no need to run a mail
+  server on the self-hosted Linux machine: regular web-hosting packages
+  usually allow to create new mail accounts easily. (As a last resort it is
+  possible to use a service like Gmail, but that would again introduce
+  unnecessary dependency on Google.)
+
+  \<^medskip>
+  Mailer configuration requires a few command-line invocations as follows:
+
+  @{verbatim [display] \<open>  isabelle phabricator_setup_mail\<close>}
+
+  \<^noindent> Now edit the generated JSON file to provide the mail account details. Then
+  add and test it with Phabricator like this (to let Phabricator send a
+  message to the administrator from above):
+
+  @{verbatim [display] \<open>  isabelle phabricator_setup_mail -T makarius\<close>}
+
+  The mail configuration process can be refined and repeated until it really
+  works: host name, port number, protocol etc.\ all need to be correct. The
+  \<^verbatim>\<open>key\<close> field in the JSON file identifies the name of the configuration; it
+  will be overwritten each time, when taking over the parameters via
+  \<^verbatim>\<open>isabelle phabricator_setup_mail\<close>.
+
+  \<^medskip>
+  For information, the resulting mailer configuration can be queried like
+  this:
+
+  @{verbatim [display] \<open>  isabelle phabricator bin/config get cluster.mailers\<close>}
+\<close>
+
+
+section \<open>Reference of command-line tools\<close>
+
+text \<open>
+  The subsequent command-line tools usually require root user privileges on
+  the underlying Linux system (e.g.\ via \<^verbatim>\<open>sudo bash\<close> to open a subshell, or
+  directly via \<^verbatim>\<open>sudo isabelle ...\<close>). 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.
+\<close>
+
+
+subsection \<open>\<^verbatim>\<open>isabelle phabricator\<close>\<close>
+
+text \<open>
+  The @{tool_def phabricator} tool invokes a GNU bash command-line within the
+  Phabricator home directory:
+  @{verbatim [display]
+\<open>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.\<close>}
+
+  Isabelle/Phabricator installations are registered in the global
+  configuration file \<^path>\<open>/etc/isabelle-phabricator.conf\<close>, with name and
+  root directory separated by colon (no extra whitespace). The home directory
+  is the subdirectory \<^verbatim>\<open>phabricator\<close> within the root.
+
+  \<^medskip> Option \<^verbatim>\<open>-l\<close> lists the available Phabricator installations with name and
+  root directory.
+
+  Option \<^verbatim>\<open>-n\<close> selects the explicitly named Phabricator installation.
+\<close>
+
+
+subsubsection \<open>Examples\<close>
+
+text \<open>
+  Print the home directory of the Phabricator installation:
+  @{verbatim [display] \<open>isabelle phabricator pwd\<close>}
+
+  Print some Phabricator configuration information:
+  @{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>}
+
+  Here the user is meant to navigate to the Phabricator home manually, in
+  contrast to \<^verbatim>\<open>isabelle phabricator\<close> doing it automatically based on
+  \<^path>\<open>/etc/isabelle-phabricator.conf\<close>.
+\<close>
+
+
+subsection \<open>\<^verbatim>\<open>isabelle phabricator_setup\<close>\<close>
+
+text \<open>
+  The @{tool_def phabricator_setup} installs a fresh Phabricator instance on
+  Ubuntu Linux (notably 18.04 LTS):
+  @{verbatim [display] \<open>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.\<close>}
+
+  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>\<open>/etc\<close> and other directories like \<^verbatim>\<open>/var/www\<close>
+  always use name prefixes \<^verbatim>\<open>isabelle-phabricator\<close> or \<^verbatim>\<open>phabricator\<close>. Local
+  configuration for a particular installation uses more specific names derived
+  from \<^verbatim>\<open>phabricator-\<close>\<open>NAME\<close>, e.g. \<^verbatim>\<open>/var/www/phabricator-vcs\<close> 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>\<open>-U\<close> ensures a full update of system packages, before installing
+  further packages required by Phabricator.
+
+  Option \<^verbatim>\<open>-n\<close> provides an alternative installation name. The default name
+  \<^verbatim>\<open>vcs\<close> 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>\<open>-r\<close> specifies an alternative installation root directory: it needs
+  to be accessible for the Apache web server.
+
+  Option \<^verbatim>\<open>-R\<close> 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>\<open>hgweb\<close> view
+  by Mercurial. See also the documentation
+  \<^url>\<open>https://www.mercurial-scm.org/wiki/PublishingRepositories#hgweb\<close> and the
+  example \<^url>\<open>https://isabelle.sketis.net/repos\<close> for repositories in
+  \<^url>\<open>https://isabelle-dev.sketis.net/diffusion\<close>.
+\<close>
+
+
+subsection \<open>\<^verbatim>\<open>isabelle phabricator_setup_mail\<close>\<close>
+
+text \<open>
+  The @{tool_def phabricator_setup_mail} provides mail configuration for an
+  existing Phabricator installation (preferably via SMTP):
+  @{verbatim [display] \<open>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.\<close>}
+
+  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>\<open>isabelle phabricator_setup_mail\<close> without options
+  creates a JSON template file. Its \<^verbatim>\<open>key\<close> 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>\<open>options\<close> specify the SMTP
+  server address and account information.
+
+  Another invocation of \<^verbatim>\<open>isabelle phabricator_setup_mail\<close> with updated JSON
+  file will change the underlying Phabricator installation. This can be done
+  repeatedly, until everything works as expected.
+
+  Option \<^verbatim>\<open>-T\<close> 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>\<open>-f\<close> 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.
+\<close>
+
+end

--- a/src/Doc/System/document/root.tex	Tue Nov 12 12:33:05 2019 +0000
+++ b/src/Doc/System/document/root.tex	Tue Nov 12 19:47:44 2019 +0100
@@ -35,6 +35,7 @@
 \input{Presentation.tex}
 \input{Server.tex}
 \input{Scala.tex}
+\input{Phabricator.tex}
 \input{Misc.tex}
 
 \begingroup

--- a/src/Pure/General/output.scala	Tue Nov 12 12:33:05 2019 +0000
+++ b/src/Pure/General/output.scala	Tue Nov 12 19:47:44 2019 +0100
@@ -21,25 +21,25 @@
   def error_message_text(msg: String): String =
     cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
 
-  def writeln(msg: String, stdout: Boolean = false)
+  def writeln(msg: String, stdout: Boolean = false, include_empty: Boolean = false)
   {
-    if (msg != "") {
+    if (msg.nonEmpty || include_empty) {
       if (stdout) Console.print(writeln_text(msg) + "\n")
       else Console.err.print(writeln_text(msg) + "\n")
     }
   }
 
-  def warning(msg: String, stdout: Boolean = false)
+  def warning(msg: String, stdout: Boolean = false, include_empty: Boolean = false)
   {
-    if (msg != "") {
+    if (msg.nonEmpty || include_empty) {
       if (stdout) Console.print(warning_text(msg) + "\n")
       else Console.err.print(warning_text(msg) + "\n")
     }
   }
 
-  def error_message(msg: String, stdout: Boolean = false)
+  def error_message(msg: String, stdout: Boolean = false, include_empty: Boolean = false)
   {
-    if (msg != "") {
+    if (msg.nonEmpty || include_empty) {
       if (stdout) Console.print(error_message_text(msg) + "\n")
       else Console.err.print(error_message_text(msg) + "\n")
     }

--- a/src/Pure/System/isabelle_tool.scala	Tue Nov 12 12:33:05 2019 +0000
+++ b/src/Pure/System/isabelle_tool.scala	Tue Nov 12 19:47:44 2019 +0100
@@ -153,6 +153,7 @@
   Options.isabelle_tool,
   Phabricator.isabelle_tool1,
   Phabricator.isabelle_tool2,
+  Phabricator.isabelle_tool3,
   Present.isabelle_tool,
   Profiling_Report.isabelle_tool,
   Server.isabelle_tool,

--- a/src/Pure/System/progress.scala	Tue Nov 12 12:33:05 2019 +0000
+++ b/src/Pure/System/progress.scala	Tue Nov 12 19:47:44 2019 +0100
@@ -60,7 +60,7 @@
 class Console_Progress(verbose: Boolean = false, stderr: Boolean = false) extends Progress
 {
   override def echo(msg: String): Unit =
-    Output.writeln(msg, stdout = !stderr)
+    Output.writeln(msg, stdout = !stderr, include_empty = true)
 
   override def theory(theory: Progress.Theory): Unit =
     if (verbose) echo(theory.message)

--- a/src/Pure/Tools/phabricator.scala	Tue Nov 12 12:33:05 2019 +0000
+++ b/src/Pure/Tools/phabricator.scala	Tue Nov 12 19:47:44 2019 +0100
@@ -69,7 +69,7 @@
     def home: Path = root + Path.explode(phabricator_name())
 
     def execute(command: String): Process_Result =
-      Isabelle_System.bash("./bin/" + command, cwd = home.file, redirect = true).check
+      Isabelle_System.bash("bin/" + command, cwd = home.file, redirect = true).check
   }
 
   def read_config(): List[Config] =
@@ -98,6 +98,49 @@
 
 
 
+  /** command-line tools **/
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool1 =
+    Isabelle_Tool("phabricator", "invoke command-line tool within Phabricator home directory", args =>
+    {
+      var list = false
+      var name = default_name
+
+      val getopts =
+        Getopts("""
+Usage: isabelle phabricator [OPTIONS] COMMAND [ARGS...]
+
+  Options are:
+    -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.
+""",
+          "l" -> (_ => list = true),
+          "n:" -> (arg => name = arg))
+
+      val more_args = getopts(args)
+      if (more_args.isEmpty && !list) getopts.usage()
+
+      val progress = new Console_Progress
+
+      if (list) {
+        for (config <- read_config()) {
+          progress.echo("phabricator " + quote(config.name) + " root " + config.root)
+        }
+      }
+
+      val config = get_config(name)
+
+      val result = progress.bash(Bash.strings(more_args), cwd = config.home.file, echo = true)
+      if (!result.ok) error("Return code: " + result.rc.toString)
+    })
+
+
+
   /** setup **/
 
   def user_setup(name: String, description: String, ssh_setup: Boolean = false)
@@ -223,7 +266,7 @@
 
     config.execute("config set storage.mysql-engine.max-size 8388608")
 
-    progress.bash("./bin/storage upgrade --force", cwd = config.home.file, echo = true).check
+    progress.bash("bin/storage upgrade --force", cwd = config.home.file, echo = true).check
 
 
     /* SSH hosting */
@@ -327,7 +370,7 @@
 
   /* Isabelle tool wrapper */
 
-  val isabelle_tool1 =
+  val isabelle_tool2 =
     Isabelle_Tool("phabricator_setup", "setup Phabricator server on Ubuntu Linux", args =>
     {
       var repo = ""
@@ -345,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.
@@ -408,7 +448,7 @@
       if (test_user.nonEmpty) {
         progress.echo("Sending test mail to " + quote(test_user))
         progress.bash(cwd = config.home.file, echo = true,
-          script = """echo "Test from Phabricator ($(date))" | ./bin/mail send-test --subject "Test" --to """ +
+          script = """echo "Test from Phabricator ($(date))" | bin/mail send-test --subject "Test" --to """ +
             Bash.string(test_user)).check
       }
     }
@@ -436,7 +476,7 @@
 
   /* Isabelle tool wrapper */
 
-  val isabelle_tool2 =
+  val isabelle_tool3 =
     Isabelle_Tool("phabricator_setup_mail",
       "setup mail configuration for existing Phabricator server", args =>
     {
@@ -450,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.