src/Pure/System/linux.scala
author wenzelm
Thu, 19 Dec 2019 22:21:43 +0100
changeset 71327 a89729bdde89
parent 71280 5a2033fc8f3d
child 71726 a5fda30edae2
permissions -rw-r--r--
more robust;
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
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    13
object Linux
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    14
{
71265
6ca561001244 support for pwgen;
wenzelm
parents: 71115
diff changeset
    15
  /* required packages */
6ca561001244 support for pwgen;
wenzelm
parents: 71115
diff changeset
    16
6ca561001244 support for pwgen;
wenzelm
parents: 71115
diff changeset
    17
  val packages: List[String] = List("pwgen")
6ca561001244 support for pwgen;
wenzelm
parents: 71115
diff changeset
    18
6ca561001244 support for pwgen;
wenzelm
parents: 71115
diff changeset
    19
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
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    22
  def check_system(): Unit =
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    23
    if (!Platform.is_linux) error("Not a Linux system")
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
  def check_system_root(): Unit =
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    26
  {
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    27
    check_system()
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    28
    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
    29
  }
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    30
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    31
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    32
  /* release */
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    33
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    34
  object Release
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    35
  {
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    36
    private val ID = """^Distributor ID:\s*(\S.*)$""".r
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    37
    private val RELEASE = """^Release:\s*(\S.*)$""".r
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    38
    private val DESCRIPTION = """^Description:\s*(\S.*)$""".r
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    39
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    40
    def apply(): Release =
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
      val lines = Isabelle_System.bash("lsb_release -a").check.out_lines
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    43
      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
    44
      new Release(find(ID), find(RELEASE), find(DESCRIPTION))
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    45
    }
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    46
  }
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    47
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    48
  final class Release private(val id: String, val release: String, val description: String)
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    49
  {
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    50
    override def toString: String = description
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    51
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    52
    def is_ubuntu: Boolean = id == "Ubuntu"
71268
e2fb60756fb8 proper check of Linux version;
wenzelm
parents: 71265
diff changeset
    53
    def is_ubuntu_18_04: Boolean = is_ubuntu && release == "18.04"
70965
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
    54
  }
70966
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    55
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    56
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    57
  /* packages */
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    58
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    59
  def reboot_required(): Boolean =
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    60
    Path.explode("/var/run/reboot-required").is_file
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    61
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    62
  def check_reboot_required(): Unit =
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    63
    if (reboot_required()) error("Reboot required")
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    64
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    65
  def package_update(progress: Progress = No_Progress): Unit =
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    66
    progress.bash(
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    67
      """apt-get update -y && apt-get upgrade -y && apt autoremove -y""",
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    68
      echo = true).check
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    69
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    70
  def package_install(packages: List[String], progress: Progress = No_Progress): Unit =
acc3bac0d7c5 support for Linux packages;
wenzelm
parents: 70965
diff changeset
    71
    progress.bash("apt-get install -y -- " + Bash.strings(packages), echo = true).check
71046
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    72
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
    73
  def package_installed(name: String): Boolean =
71327
a89729bdde89 more robust;
wenzelm
parents: 71280
diff changeset
    74
  {
a89729bdde89 more robust;
wenzelm
parents: 71280
diff changeset
    75
    val result = Isabelle_System.bash("dpkg-query -s " + Bash.string(name))
a89729bdde89 more robust;
wenzelm
parents: 71280
diff changeset
    76
    val pattern = """^Status:.*installed.*$""".r.pattern
a89729bdde89 more robust;
wenzelm
parents: 71280
diff changeset
    77
    result.ok && result.out_lines.exists(line => pattern.matcher(line).matches)
a89729bdde89 more robust;
wenzelm
parents: 71280
diff changeset
    78
  }
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
    79
71046
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    80
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    81
  /* users */
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_exists(name: String): Boolean =
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    84
    Isabelle_System.bash("id " + Bash.string(name)).ok
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    85
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    86
  def user_entry(name: String, field: Int): String =
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    87
  {
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    88
    val result = Isabelle_System.bash("getent passwd " + Bash.string(name)).check
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    89
    val fields = space_explode(':', result.out)
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    90
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    91
    if (1 <= field && field <= fields.length) fields(field - 1)
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    92
    else error("No passwd field " + field + " for user " + quote(name))
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    93
  }
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    94
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    95
  def user_description(name: String): String = user_entry(name, 5).takeWhile(_ != ',')
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    96
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    97
  def user_home(name: String): String = user_entry(name, 6)
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
    98
71054
b64fc38327ae prefer system user setup, e.g. avoid occurrence on login screen;
wenzelm
parents: 71051
diff changeset
    99
  def user_add(name: String,
b64fc38327ae prefer system user setup, e.g. avoid occurrence on login screen;
wenzelm
parents: 71051
diff changeset
   100
    description: String = "",
b64fc38327ae prefer system user setup, e.g. avoid occurrence on login screen;
wenzelm
parents: 71051
diff changeset
   101
    system: Boolean = false,
b64fc38327ae prefer system user setup, e.g. avoid occurrence on login screen;
wenzelm
parents: 71051
diff changeset
   102
    ssh_setup: Boolean = false)
71046
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   103
  {
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   104
    require(!description.contains(','))
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   105
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   106
    if (user_exists(name)) error("User already exists: " + quote(name))
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   107
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   108
    Isabelle_System.bash(
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   109
      "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
   110
        (if (system) " --system --group --shell /bin/bash " else "") +
71046
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   111
        " " + Bash.string(name)).check
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   112
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   113
    if (ssh_setup) {
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   114
      val id_rsa = user_home(name) + "/.ssh/id_rsa"
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   115
      Isabelle_System.bash("""
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   116
if [ ! -f """ + Bash.string(id_rsa) + """ ]
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   117
then
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   118
  yes '\n' | sudo -i -u """ + Bash.string(name) +
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   119
    """ ssh-keygen -q -f """ + Bash.string(id_rsa) + """
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   120
fi
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   121
      """).check
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   122
    }
b8aeeedf7e68 support for Linux user management;
wenzelm
parents: 70966
diff changeset
   123
  }
71048
5f02ecbb19d6 support for system services;
wenzelm
parents: 71046
diff changeset
   124
5f02ecbb19d6 support for system services;
wenzelm
parents: 71046
diff changeset
   125
5f02ecbb19d6 support for system services;
wenzelm
parents: 71046
diff changeset
   126
  /* system services */
5f02ecbb19d6 support for system services;
wenzelm
parents: 71046
diff changeset
   127
71107
25c85cc3bc71 clarified signature;
wenzelm
parents: 71054
diff changeset
   128
  def service_operation(op: String, name: String): Unit =
25c85cc3bc71 clarified signature;
wenzelm
parents: 71054
diff changeset
   129
    Isabelle_System.bash("systemctl " + Bash.string(op) + " " + Bash.string(name)).check
71048
5f02ecbb19d6 support for system services;
wenzelm
parents: 71046
diff changeset
   130
71107
25c85cc3bc71 clarified signature;
wenzelm
parents: 71054
diff changeset
   131
  def service_enable(name: String) { service_operation("enable", name) }
25c85cc3bc71 clarified signature;
wenzelm
parents: 71054
diff changeset
   132
  def service_disable(name: String) { service_operation("disable", name) }
25c85cc3bc71 clarified signature;
wenzelm
parents: 71054
diff changeset
   133
  def service_start(name: String) { service_operation("start", name) }
25c85cc3bc71 clarified signature;
wenzelm
parents: 71054
diff changeset
   134
  def service_stop(name: String) { service_operation("stop", name) }
25c85cc3bc71 clarified signature;
wenzelm
parents: 71054
diff changeset
   135
  def service_restart(name: String) { service_operation("restart", name) }
71051
4eeff87c5072 more phabricator setup;
wenzelm
parents: 71048
diff changeset
   136
71111
cd166c3904dd more robust: system ssh service is required for Phabricator ssh service;
wenzelm
parents: 71108
diff changeset
   137
  def service_shutdown(name: String)
cd166c3904dd more robust: system ssh service is required for Phabricator ssh service;
wenzelm
parents: 71108
diff changeset
   138
  {
cd166c3904dd more robust: system ssh service is required for Phabricator ssh service;
wenzelm
parents: 71108
diff changeset
   139
    try { service_stop(name) }
cd166c3904dd more robust: system ssh service is required for Phabricator ssh service;
wenzelm
parents: 71108
diff changeset
   140
    catch { case ERROR(_) => }
cd166c3904dd more robust: system ssh service is required for Phabricator ssh service;
wenzelm
parents: 71108
diff changeset
   141
  }
cd166c3904dd more robust: system ssh service is required for Phabricator ssh service;
wenzelm
parents: 71108
diff changeset
   142
71048
5f02ecbb19d6 support for system services;
wenzelm
parents: 71046
diff changeset
   143
  def service_install(name: String, spec: String)
5f02ecbb19d6 support for system services;
wenzelm
parents: 71046
diff changeset
   144
  {
71111
cd166c3904dd more robust: system ssh service is required for Phabricator ssh service;
wenzelm
parents: 71108
diff changeset
   145
    service_shutdown(name)
cd166c3904dd more robust: system ssh service is required for Phabricator ssh service;
wenzelm
parents: 71108
diff changeset
   146
71048
5f02ecbb19d6 support for system services;
wenzelm
parents: 71046
diff changeset
   147
    val service_file = Path.explode("/lib/systemd/system") + Path.basic(name).ext("service")
5f02ecbb19d6 support for system services;
wenzelm
parents: 71046
diff changeset
   148
    File.write(service_file, spec)
71115
wenzelm
parents: 71114
diff changeset
   149
    Isabelle_System.chmod("644", service_file)
71048
5f02ecbb19d6 support for system services;
wenzelm
parents: 71046
diff changeset
   150
71107
25c85cc3bc71 clarified signature;
wenzelm
parents: 71054
diff changeset
   151
    service_enable(name)
71108
783d5786255d more robust;
wenzelm
parents: 71107
diff changeset
   152
    service_restart(name)
71048
5f02ecbb19d6 support for system services;
wenzelm
parents: 71046
diff changeset
   153
  }
71265
6ca561001244 support for pwgen;
wenzelm
parents: 71115
diff changeset
   154
6ca561001244 support for pwgen;
wenzelm
parents: 71115
diff changeset
   155
6ca561001244 support for pwgen;
wenzelm
parents: 71115
diff changeset
   156
  /* passwords */
6ca561001244 support for pwgen;
wenzelm
parents: 71115
diff changeset
   157
6ca561001244 support for pwgen;
wenzelm
parents: 71115
diff changeset
   158
  def generate_password(length: Int = 10): String =
6ca561001244 support for pwgen;
wenzelm
parents: 71115
diff changeset
   159
  {
6ca561001244 support for pwgen;
wenzelm
parents: 71115
diff changeset
   160
    require(length >= 6)
6ca561001244 support for pwgen;
wenzelm
parents: 71115
diff changeset
   161
    Isabelle_System.bash("pwgen " + length + " 1").check.out
6ca561001244 support for pwgen;
wenzelm
parents: 71115
diff changeset
   162
  }
70965
fe9496df6298 specific support for Linux, notably Ubuntu/Debian;
wenzelm
parents:
diff changeset
   163
}