merged
authorpaulson
Sat, 31 Oct 2020 21:24:40 +0000
changeset 72532 088e2141f5e6
parent 72526 a3d096a98b69 (diff)
parent 72531 ee2ba879afb5 (current diff)
child 72533 63ec86626ec3
merged
--- a/Admin/PLATFORMS	Sat Oct 31 21:18:31 2020 +0000
+++ b/Admin/PLATFORMS	Sat Oct 31 21:24:40 2020 +0000
@@ -39,7 +39,7 @@
                     macOS 10.14 Mojave (mini2 Macmini8,1)
                     macOS 10.15 Catalina (laramac01 Macmini8,1)
 
-  x86_64-windows    Windows 7
+  x86_64-windows    Windows 10
   x86_64-cygwin     Cygwin 3.1.x https://isabelle.sketis.net/cygwin_2021 (x86_64/release)
 
 Old (partial support):
--- a/NEWS	Sat Oct 31 21:18:31 2020 +0000
+++ b/NEWS	Sat Oct 31 21:24:40 2020 +0000
@@ -244,6 +244,8 @@
 * Isabelle server allows user-defined commands via
 isabelle_scala_service.
 
+* Isabelle/Phabricator supports Ubuntu 20.04 LTS.
+
 * Isabelle/Phabricator setup has been updated to follow ongoing
 development: libphutil has been discontinued. Minor INCOMPATIBILITY:
 existing server installations should remove libphutil from
--- a/lib/Tools/components	Sat Oct 31 21:18:31 2020 +0000
+++ b/lib/Tools/components	Sat Oct 31 21:24:40 2020 +0000
@@ -99,7 +99,11 @@
   else
     echo "Initializing \"$SETTINGS\""
     mkdir -p "$(dirname "$SETTINGS")"
-    echo "$SETTINGS_CONTENT" > "$SETTINGS"
+    {
+      echo "#-*- shell-script -*- :mode=shellscript:"
+      echo
+      echo "$SETTINGS_CONTENT"
+    } > "$SETTINGS"
   fi
 elif [ -n "$LIST_ONLY" ]; then
   echo
--- a/src/Doc/System/Misc.thy	Sat Oct 31 21:18:31 2020 +0000
+++ b/src/Doc/System/Misc.thy	Sat Oct 31 21:24:40 2020 +0000
@@ -39,7 +39,7 @@
 
   Options are:
     -B NAME      base image (default "ubuntu")
-    -E           set bin/isabelle as entrypoint
+    -E           set Isabelle/bin/isabelle as entrypoint
     -P NAME      additional Ubuntu package collection ("X11", "latex")
     -l NAME      default logic (default ISABELLE_LOGIC="HOL")
     -n           no docker build
--- a/src/Doc/System/Phabricator.thy	Sat Oct 31 21:18:31 2020 +0000
+++ b/src/Doc/System/Phabricator.thy	Sat Oct 31 21:24:40 2020 +0000
@@ -63,7 +63,7 @@
 section \<open>Quick start\<close>
 
 text \<open>
-  The starting point is a fresh installation of \<^bold>\<open>Ubuntu 18.04
+  The starting point is a fresh installation of \<^bold>\<open>Ubuntu 18.04 or 20.04
   LTS\<close>\<^footnote>\<open>\<^url>\<open>https://ubuntu.com/download\<close>\<close>: this version is mandatory due to
   subtle dependencies on system packages and configuration that is assumed by
   the Isabelle setup tool.
@@ -73,8 +73,8 @@
   (\secref{sec:phabricator-domain}).
 
   Initial experimentation also works on a local host, e.g.\ via
-  VirtualBox\<^footnote>\<open>\<^url>\<open>https://www.virtualbox.org\<close>\<close>. The public domain \<^verbatim>\<open>lvh.me\<close> is
-  used by default: it maps arbitrary subdomains to \<^verbatim>\<open>localhost\<close>.
+  VirtualBox\<^footnote>\<open>\<^url>\<open>https://www.virtualbox.org\<close>\<close>. The Internet domain \<^verbatim>\<open>lvh.me\<close>
+  is used by default: it maps arbitrary subdomains to \<^verbatim>\<open>localhost\<close>.
 
   All administrative commands need to be run as \<^verbatim>\<open>root\<close> user (e.g.\ via
   \<^verbatim>\<open>sudo\<close>). Note that Isabelle refers to user-specific configuration in the
@@ -212,7 +212,7 @@
 \<close>
 
 
-subsection \<open>Public domain name and HTTPS configuration \label{sec:phabricator-domain}\<close>
+subsection \<open>Internet domain name and HTTPS configuration \label{sec:phabricator-domain}\<close>
 
 text \<open>
   So far the Phabricator server has been accessible only on \<^verbatim>\<open>localhost\<close> (via
@@ -233,7 +233,7 @@
     @{verbatim [display] \<open>  systemctl reload apache2\<close>}
 
     \<^item> Install \<^verbatim>\<open>certbot\<close> from \<^url>\<open>https://certbot.eff.org\<close> following the
-    description for Apache and Ubuntu 18.04 on
+    description for Apache and Ubuntu 18.04 or 20.04 on
     \<^url>\<open>https://certbot.eff.org/lets-encrypt/ubuntubionic-apache\<close>. Run
     \<^verbatim>\<open>certbot\<close> interactively and let it operate on the domain
     \<^verbatim>\<open>vcs.example.org\<close>.
@@ -390,7 +390,7 @@
 
 text \<open>
   The @{tool_def phabricator_setup} tool installs a fresh Phabricator instance
-  on Ubuntu 18.04 LTS:
+  on Ubuntu 18.04 or 20.04 LTS:
   @{verbatim [display] \<open>Usage: isabelle phabricator_setup [OPTIONS]
 
   Options are:
@@ -428,9 +428,9 @@
   Option \<^verbatim>\<open>-M:\<close> installs a standard Mercurial release from source --- the one
   that is used by the Phabricator hosting service
   \<^url>\<open>https://admin.phacility.com\<close>. This avoids various problems with the
-  package provided by Ubuntu 18.04. Alternatively, an explicit file path or
-  URL the source archive (\<^verbatim>\<open>.tar.gz\<close>) may be given here. This option is
-  recommended for production use, but it requires to \<^emph>\<open>uninstall\<close> existing
+  package provided by Ubuntu 18.04 or 20.04. Alternatively, an explicit file
+  path or URL the source archive (\<^verbatim>\<open>.tar.gz\<close>) may be given here. This option
+  is recommended for production use, but it requires to \<^emph>\<open>uninstall\<close> existing
   Mercurial packages provided by the operating system.
 
   Option \<^verbatim>\<open>-n\<close> provides an alternative installation name. The default name
--- a/src/Pure/System/linux.scala	Sat Oct 31 21:18:31 2020 +0000
+++ b/src/Pure/System/linux.scala	Sat Oct 31 21:24:40 2020 +0000
@@ -46,6 +46,7 @@
 
     def is_ubuntu: Boolean = id == "Ubuntu"
     def is_ubuntu_18_04: Boolean = is_ubuntu && release == "18.04"
+    def is_ubuntu_20_04: Boolean = is_ubuntu && release == "20.04"
   }
 
 
--- a/src/Pure/Tools/build_docker.scala	Sat Oct 31 21:18:31 2020 +0000
+++ b/src/Pure/Tools/build_docker.scala	Sat Oct 31 21:24:40 2020 +0000
@@ -117,7 +117,7 @@
 
   Options are:
     -B NAME      base image (default """ + quote(default_base) + """)
-    -E           set bin/isabelle as entrypoint
+    -E           set Isabelle/bin/isabelle as entrypoint
     -P NAME      additional Ubuntu package collection (""" +
           package_collections.keySet.toList.sorted.map(quote(_)).mkString(", ") + """)
     -l NAME      default logic (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
--- a/src/Pure/Tools/phabricator.scala	Sat Oct 31 21:18:31 2020 +0000
+++ b/src/Pure/Tools/phabricator.scala	Sat Oct 31 21:24:40 2020 +0000
@@ -21,16 +21,32 @@
 
   /* required packages */
 
-  val packages: List[String] =
+  val packages_ubuntu_18_04: List[String] =
     Build_Docker.packages :::
     List(
       // https://secure.phabricator.com/source/phabricator/browse/master/scripts/install/install_ubuntu.sh 15e6e2adea61
       "git", "mysql-server", "apache2", "libapache2-mod-php", "php", "php-mysql",
       "php-gd", "php-curl", "php-apcu", "php-cli", "php-json", "php-mbstring",
       // more packages
-      "php-xml", "php-zip", "python-pygments", "ssh", "subversion",
+      "php-xml", "php-zip", "python-pygments", "ssh", "subversion", "python-pygments",
       // mercurial build packages
-      "make", "gcc", "python", "python-dev", "python-docutils", "python-pygments", "python-openssl")
+      "make", "gcc", "python", "python-dev", "python-docutils", "python-openssl")
+
+  val packages_ubuntu_20_04: List[String] =
+    packages_ubuntu_18_04.map(
+      {
+        case "python-pygments" => "python3-pygments"
+        case "python-dev" => "python2-dev"
+        case name => name
+      })
+
+  def packages: List[String] =
+  {
+    val release = Linux.Release()
+    if (release.is_ubuntu_18_04) packages_ubuntu_18_04
+    else if (release.is_ubuntu_20_04) packages_ubuntu_20_04
+    else error("Bad Linux version: expected Ubuntu 18.04 or 20.04 LTS")
+  }
 
 
   /* global system resources */
@@ -248,7 +264,7 @@
 
     /* users */
 
-    if (name.contains((c: Char) => !(Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c))) ||
+    if (name.exists((c: Char) => !(Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c))) ||
         Set("", "ssh", "phd", "dump", daemon_user).contains(name)) {
       error("Bad installation name: " + quote(name))
     }
@@ -360,7 +376,8 @@
         """CREATE USER """ + mysql_user_string +
         """ IDENTIFIED BY """ + SQL.string(mysql_password) + """ PASSWORD EXPIRE NEVER; """ +
         """GRANT ALL ON `""" + (mysql_name + "_%").replace("_", "\\_") +
-        """`.* TO """ + mysql_user_string + ";")).check
+        """`.* TO """ + mysql_user_string + ";" +
+        """GRANT PROCESS ON *.* TO """ + mysql_user_string + ";")).check
 
     config.execute("config set mysql.user " + Bash.string(mysql_name))
     config.execute("config set mysql.pass " + Bash.string(mysql_password))
@@ -557,9 +574,6 @@
 
       val progress = new Console_Progress
 
-      val release = Linux.Release()
-      if (!release.is_ubuntu_18_04) error("Bad Linux version: Ubuntu 18.04 LTS required")
-
       phabricator_setup(options, name = name, root = root, repo = repo,
         package_update = package_update, mercurial_source = mercurial_source, progress = progress)
     })