--- 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.
--- 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 \<open>Quick start\<close>
text \<open>
- The starting point is a fresh installation of \<^bold>\<open>Ubuntu 20.04 or 22.04
+ The starting point is a fresh installation of \<^bold>\<open>Ubuntu 22.04 or 24.04
LTS\<close>\<^footnote>\<open>\<^url>\<open>https://ubuntu.com/download\<close>\<close>: 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 \<open>
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] \<open>Usage: isabelle phabricator_setup [OPTIONS]
Options are:
@@ -419,7 +419,7 @@
further packages required by Phorge. This might require a reboot.
Option \<^verbatim>\<open>-M:\<close> 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>\<open>.tar.gz\<close>).
This option is recommended for production use, but it requires to
\<^emph>\<open>uninstall\<close> existing Mercurial packages provided by the operating system.
--- 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
--- 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")
--- 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("""
--- 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
--- 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