src/Pure/System/linux.scala
changeset 75393 87ebf5a50283
parent 73534 e7fb17bca374
child 79487 47272fac86d8
equal deleted inserted replaced
75388:b3ca4a6ed74b 75393:87ebf5a50283
     8 
     8 
     9 
     9 
    10 import scala.util.matching.Regex
    10 import scala.util.matching.Regex
    11 
    11 
    12 
    12 
    13 object Linux
    13 object Linux {
    14 {
       
    15   /* check system */
    14   /* check system */
    16 
    15 
    17   def check_system(): Unit =
    16   def check_system(): Unit =
    18     if (!Platform.is_linux) error("Not a Linux system")
    17     if (!Platform.is_linux) error("Not a Linux system")
    19 
    18 
    20   def check_system_root(): Unit =
    19   def check_system_root(): Unit = {
    21   {
       
    22     check_system()
    20     check_system()
    23     if (Isabelle_System.bash("id -u").check.out != "0") error("Not running as superuser (root)")
    21     if (Isabelle_System.bash("id -u").check.out != "0") error("Not running as superuser (root)")
    24   }
    22   }
    25 
    23 
    26 
    24 
    27   /* release */
    25   /* release */
    28 
    26 
    29   object Release
    27   object Release {
    30   {
       
    31     private val ID = """^Distributor ID:\s*(\S.*)$""".r
    28     private val ID = """^Distributor ID:\s*(\S.*)$""".r
    32     private val RELEASE = """^Release:\s*(\S.*)$""".r
    29     private val RELEASE = """^Release:\s*(\S.*)$""".r
    33     private val DESCRIPTION = """^Description:\s*(\S.*)$""".r
    30     private val DESCRIPTION = """^Description:\s*(\S.*)$""".r
    34 
    31 
    35     def apply(): Release =
    32     def apply(): Release = {
    36     {
       
    37       val lines = Isabelle_System.bash("lsb_release -a").check.out_lines
    33       val lines = Isabelle_System.bash("lsb_release -a").check.out_lines
    38       def find(R: Regex): String = lines.collectFirst({ case R(a) => a }).getOrElse("Unknown")
    34       def find(R: Regex): String = lines.collectFirst({ case R(a) => a }).getOrElse("Unknown")
    39       new Release(find(ID), find(RELEASE), find(DESCRIPTION))
    35       new Release(find(ID), find(RELEASE), find(DESCRIPTION))
    40     }
    36     }
    41   }
    37   }
    42 
    38 
    43   final class Release private(val id: String, val release: String, val description: String)
    39   final class Release private(val id: String, val release: String, val description: String) {
    44   {
       
    45     override def toString: String = description
    40     override def toString: String = description
    46 
    41 
    47     def is_ubuntu: Boolean = id == "Ubuntu"
    42     def is_ubuntu: Boolean = id == "Ubuntu"
    48     def is_ubuntu_20_04: Boolean = is_ubuntu && release == "20.04"
    43     def is_ubuntu_20_04: Boolean = is_ubuntu && release == "20.04"
    49   }
    44   }
    63       echo = true).check
    58       echo = true).check
    64 
    59 
    65   def package_install(packages: List[String], progress: Progress = new Progress): Unit =
    60   def package_install(packages: List[String], progress: Progress = new Progress): Unit =
    66     progress.bash("apt-get install -y -- " + Bash.strings(packages), echo = true).check
    61     progress.bash("apt-get install -y -- " + Bash.strings(packages), echo = true).check
    67 
    62 
    68   def package_installed(name: String): Boolean =
    63   def package_installed(name: String): Boolean = {
    69   {
       
    70     val result = Isabelle_System.bash("dpkg-query -s " + Bash.string(name))
    64     val result = Isabelle_System.bash("dpkg-query -s " + Bash.string(name))
    71     val pattern = """^Status:.*installed.*$""".r.pattern
    65     val pattern = """^Status:.*installed.*$""".r.pattern
    72     result.ok && result.out_lines.exists(line => pattern.matcher(line).matches)
    66     result.ok && result.out_lines.exists(line => pattern.matcher(line).matches)
    73   }
    67   }
    74 
    68 
    76   /* users */
    70   /* users */
    77 
    71 
    78   def user_exists(name: String): Boolean =
    72   def user_exists(name: String): Boolean =
    79     Isabelle_System.bash("id " + Bash.string(name)).ok
    73     Isabelle_System.bash("id " + Bash.string(name)).ok
    80 
    74 
    81   def user_entry(name: String, field: Int): String =
    75   def user_entry(name: String, field: Int): String = {
    82   {
       
    83     val result = Isabelle_System.bash("getent passwd " + Bash.string(name)).check
    76     val result = Isabelle_System.bash("getent passwd " + Bash.string(name)).check
    84     val fields = space_explode(':', result.out)
    77     val fields = space_explode(':', result.out)
    85 
    78 
    86     if (1 <= field && field <= fields.length) fields(field - 1)
    79     if (1 <= field && field <= fields.length) fields(field - 1)
    87     else error("No passwd field " + field + " for user " + quote(name))
    80     else error("No passwd field " + field + " for user " + quote(name))
    92   def user_home(name: String): String = user_entry(name, 6)
    85   def user_home(name: String): String = user_entry(name, 6)
    93 
    86 
    94   def user_add(name: String,
    87   def user_add(name: String,
    95     description: String = "",
    88     description: String = "",
    96     system: Boolean = false,
    89     system: Boolean = false,
    97     ssh_setup: Boolean = false): Unit =
    90     ssh_setup: Boolean = false
    98   {
    91   ): Unit = {
    99     require(!description.contains(','), "malformed description")
    92     require(!description.contains(','), "malformed description")
   100 
    93 
   101     if (user_exists(name)) error("User already exists: " + quote(name))
    94     if (user_exists(name)) error("User already exists: " + quote(name))
   102 
    95 
   103     Isabelle_System.bash(
    96     Isabelle_System.bash(
   131 
   124 
   132   def service_shutdown(name: String): Unit =
   125   def service_shutdown(name: String): Unit =
   133     try { service_stop(name) }
   126     try { service_stop(name) }
   134     catch { case ERROR(_) => }
   127     catch { case ERROR(_) => }
   135 
   128 
   136   def service_install(name: String, spec: String): Unit =
   129   def service_install(name: String, spec: String): Unit = {
   137   {
       
   138     service_shutdown(name)
   130     service_shutdown(name)
   139 
   131 
   140     val service_file = Path.explode("/lib/systemd/system") + Path.basic(name).ext("service")
   132     val service_file = Path.explode("/lib/systemd/system") + Path.basic(name).ext("service")
   141     File.write(service_file, spec)
   133     File.write(service_file, spec)
   142     Isabelle_System.chmod("644", service_file)
   134     Isabelle_System.chmod("644", service_file)
   146   }
   138   }
   147 
   139 
   148 
   140 
   149   /* passwords */
   141   /* passwords */
   150 
   142 
   151   def generate_password(length: Int = 10): String =
   143   def generate_password(length: Int = 10): String = {
   152   {
       
   153     require(length >= 6, "password too short")
   144     require(length >= 6, "password too short")
   154     Isabelle_System.bash("pwgen " + length + " 1").check.out
   145     Isabelle_System.bash("pwgen " + length + " 1").check.out
   155   }
   146   }
   156 }
   147 }