# HG changeset patch # User wenzelm # Date 1736087404 -3600 # Node ID b836e9ac0cf3a081aeef13cfba474ec6c9b98b7e # Parent 658f1b5168f26488c50612ab77d65e56bb576941# Parent 560a069a537f0dc38972b1a0d4874102f0e4b572 merged diff -r 658f1b5168f2 -r b836e9ac0cf3 NEWS --- a/NEWS Sat Jan 04 20:24:12 2025 +0100 +++ b/NEWS Sun Jan 05 15:30:04 2025 +0100 @@ -660,10 +660,10 @@ * Update to .NET / Fsharp 8.0.x: the current long-term support version. -* Update to current Phorge 2024 week 35 (formerly Phabricator), with -support for Ubuntu 20.4 and 22.04. The Isabelle "system" manual now -refers to the project as "Phorge", but "phabricator" remains for formal -names (files, DNS etc.). +* Update to current Phorge (formerly Phabricator) on Ubuntu 22.04 and +24.04; see also https://we.phorge.it/w/changelog/2024.35/. The Isabelle +"system" manual now refers to the project as "Phorge", but "phabricator" +remains for formal names (files, DNS etc.). * Update to official Poly/ML 5.9.1. diff -r 658f1b5168f2 -r b836e9ac0cf3 src/Doc/System/Phabricator.thy --- a/src/Doc/System/Phabricator.thy Sat Jan 04 20:24:12 2025 +0100 +++ b/src/Doc/System/Phabricator.thy Sun Jan 05 15:30:04 2025 +0100 @@ -58,7 +58,7 @@ section \Quick start\ text \ - The starting point is a fresh installation of \<^bold>\Ubuntu 20.04 or 22.04 + The starting point is a fresh installation of \<^bold>\Ubuntu 22.04 or 24.04 LTS\\<^footnote>\\<^url>\https://ubuntu.com/download\\: these versions are mandatory due to subtle dependencies on system packages and configuration that is assumed by the Isabelle setup tool. @@ -383,7 +383,7 @@ text \ The @{tool_def phabricator_setup} tool installs a fresh Phorge instance - on Ubuntu 20.04 or 22.04 LTS: + on Ubuntu 22.04 or 24.04 LTS: @{verbatim [display] \Usage: isabelle phabricator_setup [OPTIONS] Options are: @@ -419,7 +419,7 @@ further packages required by Phorge. This might require a reboot. Option \<^verbatim>\-M:\ installs a standard Mercurial release from source: a specific - version that is known to work on Ubuntu 20.04 or 22.04, respectively. It is + version that is known to work on Ubuntu 22.04 or 24.04, respectively. It is also possible to specify the path or URL of the source archive (\<^verbatim>\.tar.gz\). This option is recommended for production use, but it requires to \<^emph>\uninstall\ existing Mercurial packages provided by the operating system. diff -r 658f1b5168f2 -r b836e9ac0cf3 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Jan 04 20:24:12 2025 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Sun Jan 05 15:30:04 2025 +0100 @@ -230,7 +230,7 @@ fun check_deadline () = let val t = Time.now () in - if Time.compare (t, deadline) <> LESS + if t >= deadline then raise Timeout.TIMEOUT (t - time_start) else () end diff -r 658f1b5168f2 -r b836e9ac0cf3 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Sat Jan 04 20:24:12 2025 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Sun Jan 05 15:30:04 2025 +0100 @@ -204,10 +204,10 @@ val old_e_config : atp_config = make_e_config default_max_new_mono_instances (let val (format, type_enc, lam_trans, extra_options) = - if string_ord (getenv "E_VERSION", "3.0") <> LESS then + if is_greater_equal (string_ord (getenv "E_VERSION", "3.0")) then (* '$ite' support appears to be unsound. *) (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule=4 --serialize-schedule=true --demod-under-lambda=true") - else if string_ord (getenv "E_VERSION", "2.6") <> LESS then + else if is_greater_equal (string_ord (getenv "E_VERSION", "2.6")) then (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule") else (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN, "--auto-schedule") diff -r 658f1b5168f2 -r b836e9ac0cf3 src/Pure/System/linux.scala --- a/src/Pure/System/linux.scala Sat Jan 04 20:24:12 2025 +0100 +++ b/src/Pure/System/linux.scala Sun Jan 05 15:30:04 2025 +0100 @@ -97,9 +97,12 @@ Isabelle_System.bash( "adduser --quiet --disabled-password --gecos " + Bash.string(description) + + " --home /home/" + Bash.string(name) + (if (system) " --system --group --shell /bin/bash " else "") + " " + Bash.string(name)).check + Isabelle_System.bash("usermod -p '*' " + Bash.string(name)).check + if (ssh_setup) { val id_rsa = user_home(name) + "/.ssh/id_rsa" Isabelle_System.bash(""" diff -r 658f1b5168f2 -r b836e9ac0cf3 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Sat Jan 04 20:24:12 2025 +0100 +++ b/src/Pure/Tools/find_theorems.ML Sun Jan 05 15:30:04 2025 +0100 @@ -345,7 +345,7 @@ (case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord) | ord => ord) | ord => ord) - | ord => ord) <> GREATER; + | ord => ord) |> is_less_equal; fun rem_cdups nicer xs = let diff -r 658f1b5168f2 -r b836e9ac0cf3 src/Pure/Tools/phabricator.scala --- a/src/Pure/Tools/phabricator.scala Sat Jan 04 20:24:12 2025 +0100 +++ b/src/Pure/Tools/phabricator.scala Sun Jan 05 15:30:04 2025 +0100 @@ -20,21 +20,10 @@ /* system packages */ - val packages_ubuntu_20_04: List[String] = - Docker_Build.packages ::: - List( - // https://secure.phabricator.com/source/phabricator/browse/master/scripts/install/install_ubuntu.sh 15e6e2adea61 - "git", "mysql-server", "php", "php-mysql", "php-gd", "php-curl", "php-apcu", "php-cli", - "php-json", "php-mbstring", - // more packages - "php-xml", "php-zip", "python3-pygments", "ssh", "subversion", "python-pygments", - // mercurial build packages - "make", "gcc", "python", "python2-dev", "python-docutils", "python-openssl") - val packages_ubuntu_22_04: List[String] = Docker_Build.packages ::: List( - // https://secure.phabricator.com/source/phabricator/browse/master/scripts/install/install_ubuntu.sh 15e6e2adea61 + // base packages "git", "mysql-server", "php", "php-mysql", "php-gd", "php-curl", "php-apcu", "php-cli", "php-json", "php-mbstring", // more packages @@ -45,7 +34,7 @@ val packages_ubuntu_24_04: List[String] = Docker_Build.packages ::: List( - // https://secure.phabricator.com/source/phabricator/browse/master/scripts/install/install_ubuntu.sh 15e6e2adea61 + // base packages "git", "mysql-server", "php", "php-mysql", "php-gd", "php-curl", "php-apcu", "php-cli", "php-json", "php-mbstring", // more packages @@ -53,14 +42,11 @@ // mercurial build packages "make", "gcc", "gettext", "python3", "python3-dev", "python3-docutils", "python3-setuptools") - def packages(webserver: Webserver): List[String] = { + def system_packages(): List[String] = { val release = Linux.Release() - val pkgs = - if (release.is_ubuntu_20_04) packages_ubuntu_20_04 - else if (release.is_ubuntu_22_04) packages_ubuntu_22_04 - else if (release.is_ubuntu_24_04) packages_ubuntu_24_04 - else error("Bad Linux version: expected Ubuntu 20.04 or 22.04 or 24.04 LTS") - pkgs ::: webserver.packages() + if (release.is_ubuntu_22_04) packages_ubuntu_22_04 + else if (release.is_ubuntu_24_04) packages_ubuntu_24_04 + else error("Bad Linux version: expected Ubuntu 20.04 or 22.04 or 24.04 LTS") } @@ -216,8 +202,7 @@ def standard_mercurial_source: String = { val release = Linux.Release() - if (release.is_ubuntu_20_04) "https://www.mercurial-scm.org/release/mercurial-3.9.2.tar.gz" - else if (release.is_ubuntu_22_04) "https://www.mercurial-scm.org/release/mercurial-6.1.4.tar.gz" + if (release.is_ubuntu_22_04) "https://www.mercurial-scm.org/release/mercurial-6.1.4.tar.gz" else "https://www.mercurial-scm.org/release/mercurial-6.8.2.tar.gz" } @@ -385,7 +370,8 @@ Linux.check_reboot_required() } - Linux.package_install(packages(webserver), progress = progress) + Linux.package_install(webserver.packages(), progress = progress) + Linux.package_install(system_packages(), progress = progress) Linux.check_reboot_required() @@ -777,6 +763,9 @@ /** setup ssh **/ + // see also https://we.phorge.it/book/phorge/article/diffusion_hosting/#sshd-setup + + /* sshd config */ private val Port = """^\s*Port\s+(\d+)\s*$""".r