--- a/Admin/Phabricator/README Thu Nov 14 11:54:52 2019 +0100
+++ b/Admin/Phabricator/README Thu Nov 14 13:48:36 2019 +0100
@@ -1,96 +1,25 @@
Phabricator server
==================
-- https://www.phacility.com/phabricator
-
- Slogan: "Discuss. Plan. Code. Review. Test.
- Every application your project needs, all in one tool."
-
-- Ubuntu 18.04 LTS Linux Server standard installation with
- Apache and MySQL
- https://help.ubuntu.com/lts/serverguide
- https://help.ubuntu.com/lts/serverguide/httpd.html
- https://help.ubuntu.com/lts/serverguide/mysql.html
-
- Apache HTTPS via "Let's Encrypt":
https://letsencrypt.org/getting-started
https://certbot.eff.org/lets-encrypt/ubuntubionic-apache.html
-- Installation:
-
- https://secure.phabricator.com/book/phabricator/article/installation_guide
- https://secure.phabricator.com/source/phabricator/browse/master/scripts/install/install_ubuntu.sh
-
- ./bin/storage upgrade --force
- admin user: makarius
-
-- Configuration/Setup Issues:
-
- ignore "Alternate File Domain Not Configured"
-
- Add Auth Provider: Username/Password
- ./bin/auth lock
-
- ./bin/phd start
-
- Configuration / Authentication:
https://secure.phabricator.com/book/phabricator/article/configuring_accounts_and_registration
- . only local User/Password, *not* Google, Github etc.
. auth.require-email-verification true
. policy.allow-public true
-- Configuration/Mail:
- https://secure.phabricator.com/book/phabricator/article/configuring_outbound_email
-
- e.g. external SMTP via suitable mailers.json:
- $ ./bin/config set --stdin cluster.mailers < mailers.json
-
-- Configuration/SSH:
- https://secure.phabricator.com/book/phabricator/article/diffusion_hosting
-
- /etc/ssh/sshd_config:
- Port 222
-
- /etc/passwd:
- phabricator:x:118:126::/home/phabricator:/bin/bash
- vcs:x:119:125::/home/vcs:/bin/bash
-
- /etc/group:
- phabricator:x:126:
- vcs:x:125:
-
- $ cp ssh/ssh-hook /usr/local/bin/.
- $ cp ssh/sshd_config.phabricator /etc/ssh/.
- $ cp ssh/sshd-phabricator.service /lib/systemd/system/.
- $ cp ssh/sudoers.d/phabricator /etc/sudoers.d/.
-
- $ ./bin/config set phd.user phabricator
- $ ./bin/config set diffusion.ssh-user vcs
- $ ./bin/config set diffusion.ssh-port 22
-
- $ systemctl enable sshd-phabricator
- $ systemctl start sshd-phabricator
-
- Test on local machine:
- $ echo "{}" | ssh vcs@phabricator.sketis.net conduit conduit.ping
-
-- Repository Local Path:
- mkdir -p /var/www/phabricator/repo
- chown phabricator:phabricator /var/www/phabricator/repo
-
-- PHP Daemon:
- $ cp phd/phd-phabricator.service /lib/systemd/system/.
- $ systemctl enable phd-phabricator
- $ systemctl start phd-phabricator
-
- Update:
https://secure.phabricator.com/book/phabricator/article/upgrading
sudo ./update
- ./bin/diviner generate
+- Documentation:
+ /var/www/phabricator-vcs/libphutil/scripts/build_xhpast.php
+ ./bin/diviner generate #slow
- Backup:
https://secure.phabricator.com/book/phabricator/article/configuring_backups
--- a/Admin/Phabricator/phd/phd-phabricator.service Thu Nov 14 11:54:52 2019 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-[Unit]
-Description=PHP daemon (Phabricator)
-After=syslog.target network.target apache2.service mysql.service
-
-[Service]
-Type=oneshot
-User=phabricator
-Group=phabricator
-Environment=PATH=/sbin:/usr/sbin:/usr/local/sbin:/usr/local/bin:/usr/bin:/bin
-ExecStart=/var/www/phabricator/phabricator/bin/phd start
-ExecStop=/var/www/phabricator/phabricator/bin/phd stop
-RemainAfterExit=yes
-
-[Install]
-WantedBy=multi-user.target
--- a/Admin/Phabricator/ssh/ssh-hook Thu Nov 14 11:54:52 2019 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-#!/bin/sh
-
-# NOTE: Replace this with the username that you expect users to connect with.
-VCSUSER="vcs"
-
-# NOTE: Replace this with the path to your Phabricator directory.
-ROOT="/var/www/phabricator/phabricator"
-
-if [ "$1" != "$VCSUSER" ];
-then
- exit 1
-fi
-
-exec "$ROOT/bin/ssh-auth" $@
--- a/Admin/Phabricator/ssh/sshd-phabricator.service Thu Nov 14 11:54:52 2019 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-[Unit]
-Description=OpenBSD Secure Shell server (Phabricator)
-After=network.target auditd.service
-ConditionPathExists=!/etc/ssh/sshd_not_to_be_run
-
-[Service]
-EnvironmentFile=-/etc/default/ssh
-ExecStartPre=/usr/sbin/sshd -f /etc/ssh/sshd_config.phabricator -t
-ExecStart=/usr/sbin/sshd -f /etc/ssh/sshd_config.phabricator -D $SSHD_OPTS
-ExecReload=/usr/sbin/sshd -f /etc/ssh/sshd_config.phabricator -t
-ExecReload=/bin/kill -HUP $MAINPID
-KillMode=process
-Restart=on-failure
-RestartPreventExitStatus=255
-Type=notify
-RuntimeDirectory=sshd-phabricator
-RuntimeDirectoryMode=0755
-
-[Install]
-WantedBy=multi-user.target
-Alias=sshd-phabricator.service
--- a/Admin/Phabricator/ssh/sshd_config.phabricator Thu Nov 14 11:54:52 2019 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-# NOTE: You must have OpenSSHD 6.2 or newer; support for AuthorizedKeysCommand
-# was added in this version.
-
-# NOTE: Edit these to the correct values for your setup.
-
-AuthorizedKeysCommand /usr/local/bin/ssh-hook
-AuthorizedKeysCommandUser vcs
-AllowUsers vcs
-
-# You may need to tweak these options, but mostly they just turn off everything
-# dangerous.
-
-Port 22
-Protocol 2
-PermitRootLogin no
-AllowAgentForwarding no
-AllowTcpForwarding no
-PrintMotd no
-PrintLastLog no
-PasswordAuthentication no
-ChallengeResponseAuthentication no
-AuthorizedKeysFile none
-
-PidFile /var/run/sshd-phabricator.pid
--- a/Admin/Phabricator/ssh/sudoers.d/phabricator Thu Nov 14 11:54:52 2019 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-www-data ALL=(phabricator) SETENV: NOPASSWD: /usr/bin/git, /usr/bin/hg, /usr/bin/ssh, /usr/bin/id
-vcs ALL=(phabricator) SETENV: NOPASSWD: /usr/bin/git, /usr/bin/git-upload-pack, /usr/bin/git-receive-pack, /usr/bin/hg, /usr/bin/svnserve, /usr/bin/ssh, /usr/bin/id
--- a/Admin/components/components.sha1 Thu Nov 14 11:54:52 2019 +0100
+++ b/Admin/components/components.sha1 Thu Nov 14 13:48:36 2019 +0100
@@ -217,6 +217,8 @@
51e024225b460900da5279f0b91b217085f98cf9 polyml-5.8-20190220.tar.gz
20a83fa58d497b533150defe39bcd4540529b25f polyml-5.8-20190306.tar.gz
9f0e9cd10df4c3383b063eb076e8b698ca50c3d0 polyml-5.8.1-20191101.tar.gz
+f46deb909d645ac8c140968e4d32b5763beb9add polyml-5.8.1-20191113.tar.gz
+36a40a981b57daae0463d14940a8edf6fa1af179 polyml-5.8.1-20191114.tar.gz
d1fd6eced69dc1df7226432fcb824568e0994ff2 polyml-5.8.tar.gz
49f1adfacdd6d29fa9f72035d94a31eaac411a97 polyml-test-0a6ebca445fc.tar.gz
2a8c4421e0a03c0d6ad556b3c36c34eb11568adb polyml-test-1236652ebd55.tar.gz
--- a/Admin/components/main Thu Nov 14 11:54:52 2019 +0100
+++ b/Admin/components/main Thu Nov 14 13:48:36 2019 +0100
@@ -12,7 +12,7 @@
kodkodi-1.5.2-1
nunchaku-0.5
opam-2.0.3-1
-polyml-5.8.1-20191101
+polyml-5.8.1-20191114
postgresql-42.2.5
scala-2.12.10
smbc-0.4.1
--- a/Admin/polyml/INSTALL-MinGW Thu Nov 14 11:54:52 2019 +0100
+++ b/Admin/polyml/INSTALL-MinGW Thu Nov 14 13:48:36 2019 +0100
@@ -3,29 +3,19 @@
- always "Run as administrator ..."
-- http://sourceforge.net/projects/msys2
-
- target c:\msys64
-
-- http://sourceforge.net/projects/mingw-w64
+- download from https://www.msys2.org
+ install target c:\msys64
- mingw-w64-install.exe
+- package update and installation within msys2 shell:
- i686-4.9.3-win32-dwarf-rt_v4-rev0
- x86_64-4.9.3-win32-seh-rt_v4-rev0
-
- target c:\msys64
+ pacman -Syuu
-- within msys shell:
+ pacman -Su
- pacman --needed -Sy bash pacman pacman-mirrors msys2-runtime
-
- after restart of msys shell:
+ pacman -S --needed base-devel gmp-devel mingw-w64-x86_64-toolchain mingw-w64-x86_64-gmp
- pacman -Su
- pacman -S make diffutils texinfo gmp-devel mingw-w64-i686-gmp mingw-w64-x86_64-gmp
+- build (as regular user) e.g. on vmnipkow9 with Cygwin-Terminal from Isabelle2018
+ (to avoid address relocation problems):
-- build (as regular user) e.g. on vmnipkow9
-
- isabelle/repos/Admin/polyml/build polyml-git x86-windows --build=i686-pc-msys --with-gmp
- isabelle/repos/Admin/polyml/build polyml-git x86_64-windows --build=x86_64-pc-msys --with-gmp
+ isabelle build_polyml -M /cygdrive/c/msys64 -m32 -s sha1 src
+ isabelle build_polyml -M /cygdrive/c/msys64 -m64 -s sha1 src
--- a/Admin/polyml/README Thu Nov 14 11:54:52 2019 +0100
+++ b/Admin/polyml/README Thu Nov 14 13:48:36 2019 +0100
@@ -2,7 +2,7 @@
====================
This test version of Poly/ML pre-5.8.1 is based on the repository
-snapshot https://github.com/polyml/polyml/commit/51f3ce2ae95f
+snapshot https://github.com/polyml/polyml/commit/67e87c763417
The Isabelle repository provides an administrative tool "isabelle
build_polyml", which can be used in the polyml component directory as
@@ -47,4 +47,4 @@
Makarius
- 01-Nov-2019
+ 14-Nov-2019
--- a/src/Doc/ROOT Thu Nov 14 11:54:52 2019 +0100
+++ b/src/Doc/ROOT Thu Nov 14 13:48:36 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 Thu Nov 14 13:48:36 2019 +0100
@@ -0,0 +1,321 @@
+(*: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.\<^footnote>\<open>See also
+ \<^url>\<open>https://secure.phabricator.com/book/phabricator/article/installation_guide\<close>
+ in the context of \<^url>\<open>https://help.ubuntu.com/lts/serverguide\<close>.\<close> Isabelle
+ provides some command-line tools to help with the setup, and 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 \<^bold>\<open>Setup Issues\<close> to lock the configuration
+ can be fulfilled as follows:
+
+ @{verbatim [display] \<open> isabelle phabricator bin/auth lock\<close>}
+
+ \<^medskip>
+ Most other Setup Issues can be ignored, after reading through them briefly
+ to make sure that there are no genuine problems remaining.
+\<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 Thu Nov 14 11:54:52 2019 +0100
+++ b/src/Doc/System/document/root.tex Thu Nov 14 13:48:36 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/Admin/build_polyml.scala Thu Nov 14 11:54:52 2019 +0100
+++ b/src/Pure/Admin/build_polyml.scala Thu Nov 14 13:48:36 2019 +0100
@@ -39,11 +39,12 @@
List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"),
setup =
"""PATH=/usr/bin:/bin:/mingw64/bin
- export CONFIG_SITE=/etc/config.site""",
+ export CONFIG_SITE=/mingw64/etc/config.site""",
copy_files =
List("$MSYS/mingw64/bin/libgcc_s_seh-1.dll",
"$MSYS/mingw64/bin/libgmp-10.dll",
- "$MSYS/mingw64/bin/libstdc++-6.dll")))
+ "$MSYS/mingw64/bin/libstdc++-6.dll",
+ "$MSYS/mingw64/bin/libwinpthread-1.dll")))
def build_polyml(
root: Path,
--- a/src/Pure/General/file.scala Thu Nov 14 11:54:52 2019 +0100
+++ b/src/Pure/General/file.scala Thu Nov 14 13:48:36 2019 +0100
@@ -351,8 +351,8 @@
def set_executable(path: Path, flag: Boolean)
{
- if (Platform.is_windows && flag) Isabelle_System.bash("chmod a+x " + bash_path(path)).check
- else if (Platform.is_windows) Isabelle_System.bash("chmod a-x " + bash_path(path)).check
+ if (Platform.is_windows && flag) Isabelle_System.chmod("a+x", path)
+ else if (Platform.is_windows) Isabelle_System.chmod("a-x", path)
else path.file.setExecutable(flag, false)
}
}
--- a/src/Pure/General/output.scala Thu Nov 14 11:54:52 2019 +0100
+++ b/src/Pure/General/output.scala Thu Nov 14 13:48:36 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/ML/ml_process.scala Thu Nov 14 11:54:52 2019 +0100
+++ b/src/Pure/ML/ml_process.scala Thu Nov 14 13:48:36 2019 +0100
@@ -75,7 +75,7 @@
// options
val isabelle_process_options = Isabelle_System.tmp_file("options")
- Isabelle_System.bash("chmod 600 " + File.bash_path(File.path(isabelle_process_options))).check
+ Isabelle_System.chmod("600", File.path(isabelle_process_options))
File.write(isabelle_process_options, YXML.string_of_body(options.encode))
val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
--- a/src/Pure/System/isabelle_system.scala Thu Nov 14 11:54:52 2019 +0100
+++ b/src/Pure/System/isabelle_system.scala Thu Nov 14 13:48:36 2019 +0100
@@ -149,6 +149,15 @@
/** file-system operations **/
+ /* permissions */
+
+ def chmod(arg: String, path: Path): Unit =
+ bash("chmod " + Bash.string(arg) + " " + File.bash_path(path)).check
+
+ def chown(arg: String, path: Path): Unit =
+ bash("chown " + Bash.string(arg) + " " + File.bash_path(path)).check
+
+
/* directories */
def mkdirs(path: Path): Unit =
--- a/src/Pure/System/isabelle_tool.scala Thu Nov 14 11:54:52 2019 +0100
+++ b/src/Pure/System/isabelle_tool.scala Thu Nov 14 13:48:36 2019 +0100
@@ -153,6 +153,8 @@
Options.isabelle_tool,
Phabricator.isabelle_tool1,
Phabricator.isabelle_tool2,
+ Phabricator.isabelle_tool3,
+ Phabricator.isabelle_tool4,
Present.isabelle_tool,
Profiling_Report.isabelle_tool,
Server.isabelle_tool,
--- a/src/Pure/System/linux.scala Thu Nov 14 11:54:52 2019 +0100
+++ b/src/Pure/System/linux.scala Thu Nov 14 13:48:36 2019 +0100
@@ -112,24 +112,30 @@
/* system services */
- def service_start(name: String): Unit =
- Isabelle_System.bash("systemctl start " + Bash.string(name)).check
+ def service_operation(op: String, name: String): Unit =
+ Isabelle_System.bash("systemctl " + Bash.string(op) + " " + Bash.string(name)).check
- def service_stop(name: String): Unit =
- Isabelle_System.bash("systemctl stop " + Bash.string(name)).check
+ def service_enable(name: String) { service_operation("enable", name) }
+ def service_disable(name: String) { service_operation("disable", name) }
+ def service_start(name: String) { service_operation("start", name) }
+ def service_stop(name: String) { service_operation("stop", name) }
+ def service_restart(name: String) { service_operation("restart", name) }
- def service_restart(name: String): Unit =
- Isabelle_System.bash("systemctl restart " + Bash.string(name)).check
+ def service_shutdown(name: String)
+ {
+ try { service_stop(name) }
+ catch { case ERROR(_) => }
+ }
def service_install(name: String, spec: String)
{
+ service_shutdown(name)
+
val service_file = Path.explode("/lib/systemd/system") + Path.basic(name).ext("service")
File.write(service_file, spec)
+ Isabelle_System.chmod("644", service_file)
- Isabelle_System.bash("""
- set -e
- chmod 0644 """ + File.bash_path(service_file) + """
- systemctl enable """ + Bash.string(name) + """
- systemctl start """ + Bash.string(name)).check
+ service_enable(name)
+ service_restart(name)
}
}
--- a/src/Pure/System/progress.scala Thu Nov 14 11:54:52 2019 +0100
+++ b/src/Pure/System/progress.scala Thu Nov 14 13:48:36 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/Thy/present.scala Thu Nov 14 11:54:52 2019 +0100
+++ b/src/Pure/Thy/present.scala Thu Nov 14 13:48:36 2019 +0100
@@ -92,7 +92,7 @@
val session_graph = session_prefix + Path.basic("session_graph.pdf")
File.copy(graph_file, session_graph.file)
- Isabelle_System.bash("chmod a+r " + File.bash_path(session_graph))
+ Isabelle_System.chmod("a+r", session_graph)
HTML.write_isabelle_css(session_prefix)
--- a/src/Pure/Tools/phabricator.scala Thu Nov 14 11:54:52 2019 +0100
+++ b/src/Pure/Tools/phabricator.scala Thu Nov 14 13:48:36 2019 +0100
@@ -36,9 +36,7 @@
val daemon_user = "phabricator"
- val ssh_standard = 22
- val ssh_alternative1 = 222
- val ssh_alternative2 = 2222
+ val sshd_config = Path.explode("/etc/ssh/sshd_config")
/* installation parameters */
@@ -58,6 +56,10 @@
val default_mailers: Path = Path.explode("mailers.json")
+ val default_system_port = 22
+ val alternative_system_port = 222
+ val default_server_port = 2222
+
/** global configuration **/
@@ -69,7 +71,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 +100,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)
@@ -160,12 +205,13 @@
error("Failed to create root directory " + root_path)
}
+ Isabelle_System.chown(Bash.string(www_user) + ":" + Bash.string(www_user), root_path)
+ Isabelle_System.chmod("755", root_path)
+
progress.bash(cwd = root_path.file, echo = true,
script = """
set -e
- chown """ + Bash.string(www_user) + ":" + Bash.string(www_user) + """ .
- chmod 755 .
-
+ echo "Cloning distribution repositories"
git clone https://github.com/phacility/libphutil.git
git clone https://github.com/phacility/arcanist.git
git clone https://github.com/phacility/phabricator.git
@@ -179,20 +225,29 @@
/* local repository directory */
+ progress.echo("\nRepository hosting setup ...")
+
if (!Isabelle_System.bash("mkdir -p " + File.bash_path(repo_path)).ok) {
error("Failed to create local repository directory " + repo_path)
}
- Isabelle_System.bash(cwd = repo_path.file,
- script = """
- set -e
- chown -R """ + Bash.string(daemon_user) + ":" + Bash.string(daemon_user) + """ .
- chmod 755 .
- """).check
+ Isabelle_System.chown(
+ "-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), repo_path)
+ Isabelle_System.chmod("755", repo_path)
config.execute("config set repository.default-local-path " + File.bash_path(repo_path))
+ val sudoers_file = Path.explode("/etc/sudoers.d") + Path.basic(isabelle_phabricator_name())
+ File.write(sudoers_file,
+ www_user + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/bin/hg, /usr/bin/ssh, /usr/bin/id\n" +
+ name + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/bin/git-upload-pack, /usr/bin/git-receive-pack, /usr/bin/hg, /usr/bin/svnserve, /usr/bin/ssh, /usr/bin/id\n")
+
+ Isabelle_System.chmod("440", sudoers_file)
+
+ config.execute("config set diffusion.ssh-user " + Bash.string(config.name))
+
+
/* MySQL setup */
progress.echo("\nMySQL setup ...")
@@ -223,24 +278,7 @@
config.execute("config set storage.mysql-engine.max-size 8388608")
- progress.bash("./bin/storage upgrade --force", cwd = config.home.file, echo = true).check
-
-
- /* SSH hosting */
-
- progress.echo("\nSSH hosting setup ...")
-
- val ssh_port = ssh_alternative2
-
- config.execute("config set diffusion.ssh-user " + Bash.string(name))
- config.execute("config set diffusion.ssh-port " + ssh_port)
-
- val sudoers_file = Path.explode("/etc/sudoers.d") + Path.basic(isabelle_phabricator_name())
- File.write(sudoers_file,
- www_user + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/bin/hg, /usr/bin/ssh, /usr/bin/id\n" +
- name + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/bin/git-upload-pack, /usr/bin/git-receive-pack, /usr/bin/hg, /usr/bin/svnserve, /usr/bin/ssh, /usr/bin/id\n")
-
- Isabelle_System.bash("chmod 0440 " + File.bash_path(sudoers_file)).check
+ progress.bash("bin/storage upgrade --force", cwd = config.home.file, echo = true).check
/* PHP setup */
@@ -301,6 +339,8 @@
progress.echo("PHP daemon setup ...")
config.execute("config set phd.user " + Bash.string(daemon_user))
+ config.execute("config set phd.log-directory /var/tmp/phd/" +
+ isabelle_phabricator_name(name = name) + "/log")
Linux.service_install(isabelle_phabricator_name(name = name),
"""[Unit]
@@ -312,7 +352,7 @@
User=""" + daemon_user + """
Group=""" + daemon_user + """
Environment=PATH=/sbin:/usr/sbin:/usr/local/sbin:/usr/local/bin:/usr/bin:/bin
-ExecStart=""" + config.home.implode + """/bin/phd start
+ExecStart=""" + config.home.implode + """/bin/phd start --force
ExecStop=""" + config.home.implode + """/bin/phd stop
RemainAfterExit=yes
@@ -327,7 +367,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 +385,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 +445,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
}
}
@@ -416,7 +453,7 @@
if (config_file.isEmpty) {
if (!default_config_file.is_file) {
File.write(default_config_file, mailers_template)
- Isabelle_System.bash("chmod 600 " + File.bash_path(default_config_file)).check
+ Isabelle_System.chmod("600", default_config_file)
}
if (File.read(default_config_file) == mailers_template) {
progress.echo(
@@ -436,9 +473,9 @@
/* Isabelle tool wrapper */
- val isabelle_tool2 =
+ val isabelle_tool3 =
Isabelle_Tool("phabricator_setup_mail",
- "setup mail configuration for existing Phabricator server", args =>
+ "setup mail for one Phabricator installation", args =>
{
var test_user = ""
var name = default_name
@@ -450,7 +487,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.
@@ -467,4 +504,196 @@
phabricator_setup_mail(name = name, config_file = config_file,
test_user = test_user, progress = progress)
})
+
+
+
+ /** setup ssh **/
+
+ /* sshd config */
+
+ private val Port = """^\s*Port\s+(\d+)\s*$""".r
+ private val No_Port = """^#\s*Port\b.*$""".r
+ private val Any_Port = """^#?\s*Port\b.*$""".r
+
+ def conf_ssh_port(port: Int): String =
+ if (port == 22) "#Port 22" else "Port " + port
+
+ def read_ssh_port(conf: Path): Int =
+ {
+ val lines = split_lines(File.read(conf))
+ val ports =
+ lines.flatMap({
+ case Port(Value.Int(p)) => Some(p)
+ case No_Port() => Some(22)
+ case _ => None
+ })
+ ports match {
+ case List(port) => port
+ case Nil => error("Missing Port specification in " + conf)
+ case _ => error("Multiple Port specifications in " + conf)
+ }
+ }
+
+ def write_ssh_port(conf: Path, port: Int): Boolean =
+ {
+ val old_port = read_ssh_port(conf)
+ if (old_port == port) false
+ else {
+ val lines = split_lines(File.read(conf))
+ val lines1 = lines.map({ case Any_Port() => conf_ssh_port(port) case line => line })
+ File.write(conf, cat_lines(lines1))
+ true
+ }
+ }
+
+
+ /* phabricator_setup_ssh */
+
+ def phabricator_setup_ssh(
+ server_port: Int = default_server_port,
+ system_port: Int = default_system_port,
+ test_server: Boolean = false,
+ progress: Progress = No_Progress)
+ {
+ Linux.check_system_root()
+
+ val configs = read_config()
+
+ if (server_port == system_port) {
+ error("Port for Phabricator sshd coincides with system port: " + system_port)
+ }
+
+ val sshd_conf_system = Path.explode("/etc/ssh/sshd_config")
+ val sshd_conf_server = sshd_conf_system.ext(isabelle_phabricator_name())
+
+ val ssh_name = isabelle_phabricator_name(name = "ssh")
+ val ssh_command = Path.explode("/usr/local/bin") + Path.basic(ssh_name)
+
+ Linux.service_shutdown(ssh_name)
+
+ val old_system_port = read_ssh_port(sshd_conf_system)
+ if (old_system_port != system_port) {
+ progress.echo("Reconfigurig system ssh service")
+ Linux.service_shutdown("ssh")
+ write_ssh_port(sshd_conf_system, system_port)
+ Linux.service_start("ssh")
+ }
+
+ progress.echo("Configuring " + ssh_name + " service")
+
+ File.write(ssh_command,
+"""#!/bin/bash
+{
+ while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
+ do
+ NAME="$(echo "$REPLY" | cut -d: -f1)"
+ ROOT="$(echo "$REPLY" | cut -d: -f2)"
+ if [ "$1" = "$NAME" ]
+ then
+ exec "$ROOT/phabricator/bin/ssh-auth" "$@"
+ fi
+ done
+ exit 1
+} < /etc/isabelle-phabricator.conf
+""")
+ Isabelle_System.chmod("755", ssh_command)
+ Isabelle_System.chown("root:root", ssh_command)
+
+ File.write(sshd_conf_server,
+"""# OpenBSD Secure Shell server for Isabelle/Phabricator
+AuthorizedKeysCommand """ + ssh_command.implode + """
+AuthorizedKeysCommandUser """ + daemon_user + """
+AuthorizedKeysFile none
+AllowUsers """ + configs.map(_.name).mkString(" ") + """
+Port """ + server_port + """
+Protocol 2
+PermitRootLogin no
+AllowAgentForwarding no
+AllowTcpForwarding no
+PrintMotd no
+PrintLastLog no
+PasswordAuthentication no
+ChallengeResponseAuthentication no
+PidFile /var/run/""" + ssh_name + """.pid
+""")
+
+ Linux.service_install(ssh_name,
+"""[Unit]
+Description=OpenBSD Secure Shell server for Isabelle/Phabricator
+After=network.target auditd.service
+ConditionPathExists=!/etc/ssh/sshd_not_to_be_run
+
+[Service]
+EnvironmentFile=-/etc/default/ssh
+ExecStartPre=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t
+ExecStart=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -D $SSHD_OPTS
+ExecReload=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t
+ExecReload=/bin/kill -HUP $MAINPID
+KillMode=process
+Restart=on-failure
+RestartPreventExitStatus=255
+Type=notify
+RuntimeDirectory=sshd-phabricator
+RuntimeDirectoryMode=0755
+
+[Install]
+WantedBy=multi-user.target
+Alias=""" + ssh_name + """.service
+""")
+
+ for (config <- configs) {
+ progress.echo("phabricator " + quote(config.name) + " port " + server_port)
+ config.execute("config set diffusion.ssh-port " + Bash.string(server_port.toString))
+
+ if (test_server) {
+ progress.bash(
+ """unset DISPLAY
+ echo "{}" | ssh -p """ + Bash.string(server_port.toString) +
+ " -o StrictHostKeyChecking=false " +
+ Bash.string(config.name) + """@localhost conduit conduit.ping""").print
+ }
+ }
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool4 =
+ Isabelle_Tool("phabricator_setup_ssh",
+ "setup ssh service for all Phabricator installations", args =>
+ {
+ var server_port = default_server_port
+ var system_port = default_system_port
+ var test_server = false
+
+ val getopts =
+ Getopts("""
+Usage: isabelle phabricator_setup_ssh [OPTIONS]
+
+ Options are:
+ -p PORT sshd port for Phabricator servers (default: """ + default_server_port + """)
+ -q PORT sshd port for the operating system (default: """ + default_system_port + """)
+ -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.
+""",
+ "p:" -> (arg => server_port = Value.Int.parse(arg)),
+ "q:" -> (arg => system_port = Value.Int.parse(arg)),
+ "T" -> (_ => test_server = true))
+
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
+
+ val progress = new Console_Progress
+
+ phabricator_setup_ssh(
+ server_port = server_port, system_port = system_port, test_server = test_server,
+ progress = progress)
+ })
}
--- a/src/Pure/Tools/server.scala Thu Nov 14 11:54:52 2019 +0100
+++ b/src/Pure/Tools/server.scala Thu Nov 14 13:48:36 2019 +0100
@@ -404,7 +404,7 @@
using(SQLite.open_database(Data.database))(db =>
{
db.transaction {
- Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check
+ Isabelle_System.chmod("600", Data.database)
db.create_table(Data.table)
list(db).filterNot(_.active).foreach(server_info =>
db.using_statement(Data.table.delete(Data.name.where_equal(server_info.name)))(