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