src/Doc/System/Phabricator.thy
changeset 79482 a49db426ffd4
parent 76010 da54ac51266a
child 79484 a11cf449a36e
equal deleted inserted replaced
79479:590a01e3efb4 79482:a49db426ffd4
    72   For production use, a proper \<^emph>\<open>Virtual Server\<close> or \<^emph>\<open>Root Server\<close> product
    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
    73   from a hosting provider will be required, including an Internet Domain Name
    74   (\secref{sec:phabricator-domain}).
    74   (\secref{sec:phabricator-domain}).
    75 
    75 
    76   Initial experimentation also works on a local host, e.g.\ via
    76   Initial experimentation also works on a local host, e.g.\ via
    77   VirtualBox\<^footnote>\<open>\<^url>\<open>https://www.virtualbox.org\<close>\<close>. The Internet domain \<^verbatim>\<open>lvh.me\<close>
    77   VirtualBox\<^footnote>\<open>\<^url>\<open>https://www.virtualbox.org\<close>\<close>. The proforma domain
    78   is used by default: it maps arbitrary subdomains to \<^verbatim>\<open>localhost\<close>.
    78   \<^verbatim>\<open>localhost\<close> is used by default: it maps arbitrary subdomains to the usual
       
    79   \<^verbatim>\<open>localhost\<close> address. This allows to use e.g.
       
    80   \<^verbatim>\<open>http://phabricator-vcs.localhost\<close> for initial setup as described below.
    79 
    81 
    80   All administrative commands need to be run as \<^verbatim>\<open>root\<close> user (e.g.\ via
    82   All administrative commands need to be run as \<^verbatim>\<open>root\<close> user (e.g.\ via
    81   \<^verbatim>\<open>sudo\<close>). Note that Isabelle refers to user-specific configuration in the
    83   \<^verbatim>\<open>sudo\<close>). Note that Isabelle refers to user-specific configuration in the
    82   user home directory via @{setting ISABELLE_HOME_USER}
    84   user home directory via @{setting ISABELLE_HOME_USER}
    83   (\secref{sec:settings}); that may be different or absent for the root user
    85   (\secref{sec:settings}); that may be different or absent for the root user
   214 
   216 
   215 
   217 
   216 subsection \<open>Internet domain name and HTTPS configuration \label{sec:phabricator-domain}\<close>
   218 subsection \<open>Internet domain name and HTTPS configuration \label{sec:phabricator-domain}\<close>
   217 
   219 
   218 text \<open>
   220 text \<open>
   219   So far the Phabricator server has been accessible only on \<^verbatim>\<open>localhost\<close> (via
   221   So far the Phabricator server has been accessible only on \<^verbatim>\<open>localhost\<close>.
   220   the alias \<^verbatim>\<open>lvh.me\<close>). Proper configuration of a public Internet domain name
   222   Proper configuration of a public Internet domain name (with HTTPS
   221   (with HTTPS certificate from \<^emph>\<open>Let's Encrypt\<close>) works as follows.
   223   certificate from \<^emph>\<open>Let's Encrypt\<close>) works as follows.
   222 
   224 
   223     \<^item> Register a subdomain (e.g.\ \<^verbatim>\<open>vcs.example.org\<close>) as an alias for the IP
   225     \<^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
   226     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
   227     interface of the hosting provider to edit DNS entries; it might require
   226     some time for updated DNS records to become publicly available.
   228     some time for updated DNS records to become publicly available.