| author | wenzelm | 
| Fri, 04 Apr 2025 16:35:05 +0200 | |
| changeset 82432 | 314d6b215f90 | 
| parent 81723 | b5d329f7fe95 | 
| permissions | -rw-r--r-- | 
| 70965 | 1 | /* Title: Pure/System/linux.scala | 
| 2 | Author: Makarius | |
| 3 | ||
| 4 | Specific support for Linux, notably Ubuntu/Debian. | |
| 5 | */ | |
| 6 | ||
| 7 | package isabelle | |
| 8 | ||
| 9 | ||
| 10 | import scala.util.matching.Regex | |
| 11 | ||
| 12 | ||
| 75393 | 13 | object Linux {
 | 
| 70965 | 14 | /* check system */ | 
| 15 | ||
| 16 | def check_system(): Unit = | |
| 17 |     if (!Platform.is_linux) error("Not a Linux system")
 | |
| 18 | ||
| 75393 | 19 |   def check_system_root(): Unit = {
 | 
| 70965 | 20 | check_system() | 
| 21 |     if (Isabelle_System.bash("id -u").check.out != "0") error("Not running as superuser (root)")
 | |
| 22 | } | |
| 23 | ||
| 24 | ||
| 25 | /* release */ | |
| 26 | ||
| 75393 | 27 |   object Release {
 | 
| 70965 | 28 | private val ID = """^Distributor ID:\s*(\S.*)$""".r | 
| 29 | private val RELEASE = """^Release:\s*(\S.*)$""".r | |
| 30 | private val DESCRIPTION = """^Description:\s*(\S.*)$""".r | |
| 31 | ||
| 75393 | 32 |     def apply(): Release = {
 | 
| 70965 | 33 |       val lines = Isabelle_System.bash("lsb_release -a").check.out_lines
 | 
| 34 |       def find(R: Regex): String = lines.collectFirst({ case R(a) => a }).getOrElse("Unknown")
 | |
| 35 | new Release(find(ID), find(RELEASE), find(DESCRIPTION)) | |
| 36 | } | |
| 37 | } | |
| 38 | ||
| 75393 | 39 |   final class Release private(val id: String, val release: String, val description: String) {
 | 
| 70965 | 40 | override def toString: String = description | 
| 41 | ||
| 42 | def is_ubuntu: Boolean = id == "Ubuntu" | |
| 72521 | 43 | def is_ubuntu_20_04: Boolean = is_ubuntu && release == "20.04" | 
| 79487 
47272fac86d8
support Phabricator on Ubuntu 22.04 LTS with PHP 8.1, using community form we.phorge.it version "2023 week 49";
 wenzelm parents: 
75393diff
changeset | 44 | def is_ubuntu_22_04: Boolean = is_ubuntu && release == "22.04" | 
| 80158 | 45 | def is_ubuntu_24_04: Boolean = is_ubuntu && release == "24.04" | 
| 70965 | 46 | } | 
| 70966 | 47 | |
| 48 | ||
| 49 | /* packages */ | |
| 50 | ||
| 51 | def reboot_required(): Boolean = | |
| 52 |     Path.explode("/var/run/reboot-required").is_file
 | |
| 53 | ||
| 54 | def check_reboot_required(): Unit = | |
| 55 |     if (reboot_required()) error("Reboot required")
 | |
| 56 | ||
| 71726 
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
 wenzelm parents: 
71327diff
changeset | 57 | def package_update(progress: Progress = new Progress): Unit = | 
| 70966 | 58 | progress.bash( | 
| 59 | """apt-get update -y && apt-get upgrade -y && apt autoremove -y""", | |
| 60 | echo = true).check | |
| 61 | ||
| 71726 
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
 wenzelm parents: 
71327diff
changeset | 62 | def package_install(packages: List[String], progress: Progress = new Progress): Unit = | 
| 70966 | 63 |     progress.bash("apt-get install -y -- " + Bash.strings(packages), echo = true).check
 | 
| 71046 | 64 | |
| 75393 | 65 |   def package_installed(name: String): Boolean = {
 | 
| 71327 | 66 |     val result = Isabelle_System.bash("dpkg-query -s " + Bash.string(name))
 | 
| 67 | val pattern = """^Status:.*installed.*$""".r.pattern | |
| 68 | result.ok && result.out_lines.exists(line => pattern.matcher(line).matches) | |
| 69 | } | |
| 71280 
5a2033fc8f3d
avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";
 wenzelm parents: 
71268diff
changeset | 70 | |
| 71046 | 71 | |
| 72 | /* users */ | |
| 73 | ||
| 74 | def user_exists(name: String): Boolean = | |
| 75 |     Isabelle_System.bash("id " + Bash.string(name)).ok
 | |
| 76 | ||
| 75393 | 77 |   def user_entry(name: String, field: Int): String = {
 | 
| 71046 | 78 |     val result = Isabelle_System.bash("getent passwd " + Bash.string(name)).check
 | 
| 79 |     val fields = space_explode(':', result.out)
 | |
| 80 | ||
| 81 | if (1 <= field && field <= fields.length) fields(field - 1) | |
| 82 |     else error("No passwd field " + field + " for user " + quote(name))
 | |
| 83 | } | |
| 84 | ||
| 85 | def user_description(name: String): String = user_entry(name, 5).takeWhile(_ != ',') | |
| 86 | ||
| 87 | def user_home(name: String): String = user_entry(name, 6) | |
| 88 | ||
| 71054 
b64fc38327ae
prefer system user setup, e.g. avoid occurrence on login screen;
 wenzelm parents: 
71051diff
changeset | 89 | def user_add(name: String, | 
| 
b64fc38327ae
prefer system user setup, e.g. avoid occurrence on login screen;
 wenzelm parents: 
71051diff
changeset | 90 | description: String = "", | 
| 
b64fc38327ae
prefer system user setup, e.g. avoid occurrence on login screen;
 wenzelm parents: 
71051diff
changeset | 91 | system: Boolean = false, | 
| 75393 | 92 | ssh_setup: Boolean = false | 
| 93 |   ): Unit = {
 | |
| 73120 
c3589f2dff31
more informative errors: simplify diagnosis of spurious failures reported by users;
 wenzelm parents: 
72521diff
changeset | 94 |     require(!description.contains(','), "malformed description")
 | 
| 71046 | 95 | |
| 96 |     if (user_exists(name)) error("User already exists: " + quote(name))
 | |
| 97 | ||
| 98 | Isabelle_System.bash( | |
| 99 | "adduser --quiet --disabled-password --gecos " + Bash.string(description) + | |
| 81723 | 100 | " --home /home/" + Bash.string(name) + | 
| 71054 
b64fc38327ae
prefer system user setup, e.g. avoid occurrence on login screen;
 wenzelm parents: 
71051diff
changeset | 101 | (if (system) " --system --group --shell /bin/bash " else "") + | 
| 71046 | 102 | " " + Bash.string(name)).check | 
| 103 | ||
| 81723 | 104 |     Isabelle_System.bash("usermod -p '*' " + Bash.string(name)).check
 | 
| 105 | ||
| 71046 | 106 |     if (ssh_setup) {
 | 
| 107 | val id_rsa = user_home(name) + "/.ssh/id_rsa" | |
| 108 |       Isabelle_System.bash("""
 | |
| 109 | if [ ! -f """ + Bash.string(id_rsa) + """ ] | |
| 110 | then | |
| 111 | yes '\n' | sudo -i -u """ + Bash.string(name) + | |
| 112 | """ ssh-keygen -q -f """ + Bash.string(id_rsa) + """ | |
| 113 | fi | |
| 114 | """).check | |
| 115 | } | |
| 116 | } | |
| 71048 | 117 | |
| 118 | ||
| 119 | /* system services */ | |
| 120 | ||
| 71107 | 121 | def service_operation(op: String, name: String): Unit = | 
| 122 |     Isabelle_System.bash("systemctl " + Bash.string(op) + " " + Bash.string(name)).check
 | |
| 71048 | 123 | |
| 73340 | 124 |   def service_enable(name: String): Unit = service_operation("enable", name)
 | 
| 125 |   def service_disable(name: String): Unit = service_operation("disable", name)
 | |
| 126 |   def service_start(name: String): Unit = service_operation("start", name)
 | |
| 127 |   def service_stop(name: String): Unit = service_operation("stop", name)
 | |
| 128 |   def service_restart(name: String): Unit = service_operation("restart", name)
 | |
| 71051 | 129 | |
| 73340 | 130 | def service_shutdown(name: String): Unit = | 
| 71111 
cd166c3904dd
more robust: system ssh service is required for Phabricator ssh service;
 wenzelm parents: 
71108diff
changeset | 131 |     try { service_stop(name) }
 | 
| 
cd166c3904dd
more robust: system ssh service is required for Phabricator ssh service;
 wenzelm parents: 
71108diff
changeset | 132 |     catch { case ERROR(_) => }
 | 
| 
cd166c3904dd
more robust: system ssh service is required for Phabricator ssh service;
 wenzelm parents: 
71108diff
changeset | 133 | |
| 75393 | 134 |   def service_install(name: String, spec: String): Unit = {
 | 
| 71111 
cd166c3904dd
more robust: system ssh service is required for Phabricator ssh service;
 wenzelm parents: 
71108diff
changeset | 135 | service_shutdown(name) | 
| 
cd166c3904dd
more robust: system ssh service is required for Phabricator ssh service;
 wenzelm parents: 
71108diff
changeset | 136 | |
| 71048 | 137 |     val service_file = Path.explode("/lib/systemd/system") + Path.basic(name).ext("service")
 | 
| 138 | File.write(service_file, spec) | |
| 71115 | 139 |     Isabelle_System.chmod("644", service_file)
 | 
| 71048 | 140 | |
| 71107 | 141 | service_enable(name) | 
| 71108 | 142 | service_restart(name) | 
| 71048 | 143 | } | 
| 71265 | 144 | |
| 145 | ||
| 146 | /* passwords */ | |
| 147 | ||
| 75393 | 148 |   def generate_password(length: Int = 10): String = {
 | 
| 73120 
c3589f2dff31
more informative errors: simplify diagnosis of spurious failures reported by users;
 wenzelm parents: 
72521diff
changeset | 149 | require(length >= 6, "password too short") | 
| 71265 | 150 |     Isabelle_System.bash("pwgen " + length + " 1").check.out
 | 
| 151 | } | |
| 79515 | 152 | |
| 153 | ||
| 154 | /* PHP */ | |
| 155 | ||
| 156 | def php_version(): String = | |
| 157 |     Isabelle_System.bash("""php --run 'echo PHP_MAJOR_VERSION . "." . PHP_MINOR_VERSION;'""")
 | |
| 158 | .check.out | |
| 159 | ||
| 160 | def php_conf_dir(name: String): Path = | |
| 161 |     Path.explode("/etc/php") + Path.basic(php_version()) + Path.basic(name) + Path.explode("conf.d")
 | |
| 70965 | 162 | } |