| author | haftmann | 
| Tue, 02 May 2023 08:39:46 +0000 | |
| changeset 77927 | f041d5060892 | 
| parent 75393 | 87ebf5a50283 | 
| child 79487 | 47272fac86d8 | 
| 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" | 
| 70965 | 44 | } | 
| 70966 | 45 | |
| 46 | ||
| 47 | /* packages */ | |
| 48 | ||
| 49 | def reboot_required(): Boolean = | |
| 50 |     Path.explode("/var/run/reboot-required").is_file
 | |
| 51 | ||
| 52 | def check_reboot_required(): Unit = | |
| 53 |     if (reboot_required()) error("Reboot required")
 | |
| 54 | ||
| 71726 
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
 wenzelm parents: 
71327diff
changeset | 55 | def package_update(progress: Progress = new Progress): Unit = | 
| 70966 | 56 | progress.bash( | 
| 57 | """apt-get update -y && apt-get upgrade -y && apt autoremove -y""", | |
| 58 | echo = true).check | |
| 59 | ||
| 71726 
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
 wenzelm parents: 
71327diff
changeset | 60 | def package_install(packages: List[String], progress: Progress = new Progress): Unit = | 
| 70966 | 61 |     progress.bash("apt-get install -y -- " + Bash.strings(packages), echo = true).check
 | 
| 71046 | 62 | |
| 75393 | 63 |   def package_installed(name: String): Boolean = {
 | 
| 71327 | 64 |     val result = Isabelle_System.bash("dpkg-query -s " + Bash.string(name))
 | 
| 65 | val pattern = """^Status:.*installed.*$""".r.pattern | |
| 66 | result.ok && result.out_lines.exists(line => pattern.matcher(line).matches) | |
| 67 | } | |
| 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 | 68 | |
| 71046 | 69 | |
| 70 | /* users */ | |
| 71 | ||
| 72 | def user_exists(name: String): Boolean = | |
| 73 |     Isabelle_System.bash("id " + Bash.string(name)).ok
 | |
| 74 | ||
| 75393 | 75 |   def user_entry(name: String, field: Int): String = {
 | 
| 71046 | 76 |     val result = Isabelle_System.bash("getent passwd " + Bash.string(name)).check
 | 
| 77 |     val fields = space_explode(':', result.out)
 | |
| 78 | ||
| 79 | if (1 <= field && field <= fields.length) fields(field - 1) | |
| 80 |     else error("No passwd field " + field + " for user " + quote(name))
 | |
| 81 | } | |
| 82 | ||
| 83 | def user_description(name: String): String = user_entry(name, 5).takeWhile(_ != ',') | |
| 84 | ||
| 85 | def user_home(name: String): String = user_entry(name, 6) | |
| 86 | ||
| 71054 
b64fc38327ae
prefer system user setup, e.g. avoid occurrence on login screen;
 wenzelm parents: 
71051diff
changeset | 87 | def user_add(name: String, | 
| 
b64fc38327ae
prefer system user setup, e.g. avoid occurrence on login screen;
 wenzelm parents: 
71051diff
changeset | 88 | description: String = "", | 
| 
b64fc38327ae
prefer system user setup, e.g. avoid occurrence on login screen;
 wenzelm parents: 
71051diff
changeset | 89 | system: Boolean = false, | 
| 75393 | 90 | ssh_setup: Boolean = false | 
| 91 |   ): Unit = {
 | |
| 73120 
c3589f2dff31
more informative errors: simplify diagnosis of spurious failures reported by users;
 wenzelm parents: 
72521diff
changeset | 92 |     require(!description.contains(','), "malformed description")
 | 
| 71046 | 93 | |
| 94 |     if (user_exists(name)) error("User already exists: " + quote(name))
 | |
| 95 | ||
| 96 | Isabelle_System.bash( | |
| 97 | "adduser --quiet --disabled-password --gecos " + Bash.string(description) + | |
| 71054 
b64fc38327ae
prefer system user setup, e.g. avoid occurrence on login screen;
 wenzelm parents: 
71051diff
changeset | 98 | (if (system) " --system --group --shell /bin/bash " else "") + | 
| 71046 | 99 | " " + Bash.string(name)).check | 
| 100 | ||
| 101 |     if (ssh_setup) {
 | |
| 102 | val id_rsa = user_home(name) + "/.ssh/id_rsa" | |
| 103 |       Isabelle_System.bash("""
 | |
| 104 | if [ ! -f """ + Bash.string(id_rsa) + """ ] | |
| 105 | then | |
| 106 | yes '\n' | sudo -i -u """ + Bash.string(name) + | |
| 107 | """ ssh-keygen -q -f """ + Bash.string(id_rsa) + """ | |
| 108 | fi | |
| 109 | """).check | |
| 110 | } | |
| 111 | } | |
| 71048 | 112 | |
| 113 | ||
| 114 | /* system services */ | |
| 115 | ||
| 71107 | 116 | def service_operation(op: String, name: String): Unit = | 
| 117 |     Isabelle_System.bash("systemctl " + Bash.string(op) + " " + Bash.string(name)).check
 | |
| 71048 | 118 | |
| 73340 | 119 |   def service_enable(name: String): Unit = service_operation("enable", name)
 | 
| 120 |   def service_disable(name: String): Unit = service_operation("disable", name)
 | |
| 121 |   def service_start(name: String): Unit = service_operation("start", name)
 | |
| 122 |   def service_stop(name: String): Unit = service_operation("stop", name)
 | |
| 123 |   def service_restart(name: String): Unit = service_operation("restart", name)
 | |
| 71051 | 124 | |
| 73340 | 125 | def service_shutdown(name: String): Unit = | 
| 71111 
cd166c3904dd
more robust: system ssh service is required for Phabricator ssh service;
 wenzelm parents: 
71108diff
changeset | 126 |     try { service_stop(name) }
 | 
| 
cd166c3904dd
more robust: system ssh service is required for Phabricator ssh service;
 wenzelm parents: 
71108diff
changeset | 127 |     catch { case ERROR(_) => }
 | 
| 
cd166c3904dd
more robust: system ssh service is required for Phabricator ssh service;
 wenzelm parents: 
71108diff
changeset | 128 | |
| 75393 | 129 |   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 | 130 | service_shutdown(name) | 
| 
cd166c3904dd
more robust: system ssh service is required for Phabricator ssh service;
 wenzelm parents: 
71108diff
changeset | 131 | |
| 71048 | 132 |     val service_file = Path.explode("/lib/systemd/system") + Path.basic(name).ext("service")
 | 
| 133 | File.write(service_file, spec) | |
| 71115 | 134 |     Isabelle_System.chmod("644", service_file)
 | 
| 71048 | 135 | |
| 71107 | 136 | service_enable(name) | 
| 71108 | 137 | service_restart(name) | 
| 71048 | 138 | } | 
| 71265 | 139 | |
| 140 | ||
| 141 | /* passwords */ | |
| 142 | ||
| 75393 | 143 |   def generate_password(length: Int = 10): String = {
 | 
| 73120 
c3589f2dff31
more informative errors: simplify diagnosis of spurious failures reported by users;
 wenzelm parents: 
72521diff
changeset | 144 | require(length >= 6, "password too short") | 
| 71265 | 145 |     Isabelle_System.bash("pwgen " + length + " 1").check.out
 | 
| 146 | } | |
| 70965 | 147 | } |