src/Pure/System/linux.scala
author wenzelm
Fri, 01 Apr 2022 17:06:10 +0200
changeset 75393 87ebf5a50283
parent 73534 e7fb17bca374
child 79487 47272fac86d8
permissions -rw-r--r--
clarified formatting, for the sake of scala3;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
70965
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/System/linux.scala
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
     3
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
     4
Specific support for Linux, notably Ubuntu/Debian.
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
     5
*/
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
     6
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
     7
package isabelle
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
     8
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
     9
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    10
import scala.util.matching.Regex
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    11
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    12
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73534
diff changeset
    13
object Linux {
70965
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    14
  /* check system */
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    15
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    16
  def check_system(): Unit =
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    17
    if (!Platform.is_linux) error("Not a Linux system")
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    18
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73534
diff changeset
    19
  def check_system_root(): Unit = {
70965
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    20
    check_system()
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    21
    if (Isabelle_System.bash("id -u").check.out != "0") error("Not running as superuser (root)")
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    22
  }
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    23
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    24
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    25
  /* release */
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    26
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73534
diff changeset
    27
  object Release {
70965
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    28
    private val ID = """^Distributor ID:\s*(\S.*)$""".r
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    29
    private val RELEASE = """^Release:\s*(\S.*)$""".r
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    30
    private val DESCRIPTION = """^Description:\s*(\S.*)$""".r
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    31
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73534
diff changeset
    32
    def apply(): Release = {
70965
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    33
      val lines = Isabelle_System.bash("lsb_release -a").check.out_lines
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    34
      def find(R: Regex): String = lines.collectFirst({ case R(a) => a }).getOrElse("Unknown")
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    35
      new Release(find(ID), find(RELEASE), find(DESCRIPTION))
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    36
    }
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    37
  }
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    38
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73534
diff changeset
    39
  final class Release private(val id: String, val release: String, val description: String) {
70965
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    40
    override def toString: String = description
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    41
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    42
    def is_ubuntu: Boolean = id == "Ubuntu"
72521
354bfab78cbf Isabelle/Phabricator supports Ubuntu 20.04 LTS;
wenzelm
parents: 72494
diff changeset
    43
    def is_ubuntu_20_04: Boolean = is_ubuntu && release == "20.04"
70965
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    44
  }
70966
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    45
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    46
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    47
  /* packages */
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    48
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    49
  def reboot_required(): Boolean =
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    50
    Path.explode("/var/run/reboot-required").is_file
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    51
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    52
  def check_reboot_required(): Unit =
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    53
    if (reboot_required()) error("Reboot required")
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    54
71726
a5fda30edae2 clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents: 71327
diff changeset
    55
  def package_update(progress: Progress = new Progress): Unit =
70966
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    56
    progress.bash(
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    57
      """apt-get update -y && apt-get upgrade -y && apt autoremove -y""",
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    58
      echo = true).check
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    59
71726
a5fda30edae2 clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents: 71327
diff changeset
    60
  def package_install(packages: List[String], progress: Progress = new Progress): Unit =
70966
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    61
    progress.bash("apt-get install -y -- " + Bash.strings(packages), echo = true).check
71046
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    62
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73534
diff changeset
    63
  def package_installed(name: String): Boolean = {
71327
a89729bdde89 more robust;
wenzelm
parents: 71280
diff changeset
    64
    val result = Isabelle_System.bash("dpkg-query -s " + Bash.string(name))
a89729bdde89 more robust;
wenzelm
parents: 71280
diff changeset
    65
    val pattern = """^Status:.*installed.*$""".r.pattern
a89729bdde89 more robust;
wenzelm
parents: 71280
diff changeset
    66
    result.ok && result.out_lines.exists(line => pattern.matcher(line).matches)
a89729bdde89 more robust;
wenzelm
parents: 71280
diff changeset
    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: 71268
diff changeset
    68
71046
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    69
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    70
  /* users */
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    71
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    72
  def user_exists(name: String): Boolean =
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    73
    Isabelle_System.bash("id " + Bash.string(name)).ok
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    74
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73534
diff changeset
    75
  def user_entry(name: String, field: Int): String = {
71046
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    76
    val result = Isabelle_System.bash("getent passwd " + Bash.string(name)).check
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    77
    val fields = space_explode(':', result.out)
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    78
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    79
    if (1 <= field && field <= fields.length) fields(field - 1)
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    80
    else error("No passwd field " + field + " for user " + quote(name))
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    81
  }
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    82
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    83
  def user_description(name: String): String = user_entry(name, 5).takeWhile(_ != ',')
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    84
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    85
  def user_home(name: String): String = user_entry(name, 6)
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    86
71054
b64fc38327ae prefer system user setup, e.g. avoid occurrence on login screen;
wenzelm
parents: 71051
diff changeset
    87
  def user_add(name: String,
b64fc38327ae prefer system user setup, e.g. avoid occurrence on login screen;
wenzelm
parents: 71051
diff changeset
    88
    description: String = "",
b64fc38327ae prefer system user setup, e.g. avoid occurrence on login screen;
wenzelm
parents: 71051
diff changeset
    89
    system: Boolean = false,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73534
diff changeset
    90
    ssh_setup: Boolean = false
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73534
diff changeset
    91
  ): Unit = {
73120
c3589f2dff31 more informative errors: simplify diagnosis of spurious failures reported by users;
wenzelm
parents: 72521
diff changeset
    92
    require(!description.contains(','), "malformed description")
71046
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    93
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    94
    if (user_exists(name)) error("User already exists: " + quote(name))
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    95
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    96
    Isabelle_System.bash(
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    97
      "adduser --quiet --disabled-password --gecos " + Bash.string(description) +
71054
b64fc38327ae prefer system user setup, e.g. avoid occurrence on login screen;
wenzelm
parents: 71051
diff changeset
    98
        (if (system) " --system --group --shell /bin/bash " else "") +
71046
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    99
        " " + Bash.string(name)).check
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   100
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   101
    if (ssh_setup) {
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   102
      val id_rsa = user_home(name) + "/.ssh/id_rsa"
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   103
      Isabelle_System.bash("""
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   104
if [ ! -f """ + Bash.string(id_rsa) + """ ]
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   105
then
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   106
  yes '\n' | sudo -i -u """ + Bash.string(name) +
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   107
    """ ssh-keygen -q -f """ + Bash.string(id_rsa) + """
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   108
fi
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   109
      """).check
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   110
    }
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   111
  }
71048
5f02ecbb19d6 support for system services;
wenzelm
parents: 71046
diff changeset
   112
5f02ecbb19d6 support for system services;
wenzelm
parents: 71046
diff changeset
   113
5f02ecbb19d6 support for system services;
wenzelm
parents: 71046
diff changeset
   114
  /* system services */
5f02ecbb19d6 support for system services;
wenzelm
parents: 71046
diff changeset
   115
71107
25c85cc3bc71 clarified signature;
wenzelm
parents: 71054
diff changeset
   116
  def service_operation(op: String, name: String): Unit =
25c85cc3bc71 clarified signature;
wenzelm
parents: 71054
diff changeset
   117
    Isabelle_System.bash("systemctl " + Bash.string(op) + " " + Bash.string(name)).check
71048
5f02ecbb19d6 support for system services;
wenzelm
parents: 71046
diff changeset
   118
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73120
diff changeset
   119
  def service_enable(name: String): Unit = service_operation("enable", name)
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73120
diff changeset
   120
  def service_disable(name: String): Unit = service_operation("disable", name)
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73120
diff changeset
   121
  def service_start(name: String): Unit = service_operation("start", name)
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73120
diff changeset
   122
  def service_stop(name: String): Unit = service_operation("stop", name)
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73120
diff changeset
   123
  def service_restart(name: String): Unit = service_operation("restart", name)
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71048
diff changeset
   124
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73120
diff changeset
   125
  def service_shutdown(name: String): Unit =
71111
cd166c3904dd more robust: system ssh service is required for Phabricator ssh service;
wenzelm
parents: 71108
diff changeset
   126
    try { service_stop(name) }
cd166c3904dd more robust: system ssh service is required for Phabricator ssh service;
wenzelm
parents: 71108
diff changeset
   127
    catch { case ERROR(_) => }
cd166c3904dd more robust: system ssh service is required for Phabricator ssh service;
wenzelm
parents: 71108
diff changeset
   128
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73534
diff changeset
   129
  def service_install(name: String, spec: String): Unit = {
71111
cd166c3904dd more robust: system ssh service is required for Phabricator ssh service;
wenzelm
parents: 71108
diff changeset
   130
    service_shutdown(name)
cd166c3904dd more robust: system ssh service is required for Phabricator ssh service;
wenzelm
parents: 71108
diff changeset
   131
71048
5f02ecbb19d6 support for system services;
wenzelm
parents: 71046
diff changeset
   132
    val service_file = Path.explode("/lib/systemd/system") + Path.basic(name).ext("service")
5f02ecbb19d6 support for system services;
wenzelm
parents: 71046
diff changeset
   133
    File.write(service_file, spec)
71115
wenzelm
parents: 71114
diff changeset
   134
    Isabelle_System.chmod("644", service_file)
71048
5f02ecbb19d6 support for system services;
wenzelm
parents: 71046
diff changeset
   135
71107
25c85cc3bc71 clarified signature;
wenzelm
parents: 71054
diff changeset
   136
    service_enable(name)
71108
783d5786255d more robust;
wenzelm
parents: 71107
diff changeset
   137
    service_restart(name)
71048
5f02ecbb19d6 support for system services;
wenzelm
parents: 71046
diff changeset
   138
  }
71265
6ca561001244 support for pwgen;
wenzelm
parents: 71115
diff changeset
   139
6ca561001244 support for pwgen;
wenzelm
parents: 71115
diff changeset
   140
6ca561001244 support for pwgen;
wenzelm
parents: 71115
diff changeset
   141
  /* passwords */
6ca561001244 support for pwgen;
wenzelm
parents: 71115
diff changeset
   142
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73534
diff changeset
   143
  def generate_password(length: Int = 10): String = {
73120
c3589f2dff31 more informative errors: simplify diagnosis of spurious failures reported by users;
wenzelm
parents: 72521
diff changeset
   144
    require(length >= 6, "password too short")
71265
6ca561001244 support for pwgen;
wenzelm
parents: 71115
diff changeset
   145
    Isabelle_System.bash("pwgen " + length + " 1").check.out
6ca561001244 support for pwgen;
wenzelm
parents: 71115
diff changeset
   146
  }
70965
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
   147
}