| author | wenzelm | 
| Fri, 23 Dec 2022 15:07:48 +0100 | |
| changeset 76759 | 35f41096de36 | 
| 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: 
71327 
diff
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: 
71327 
diff
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: 
71268 
diff
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: 
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 | 90  | 
ssh_setup: Boolean = false  | 
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 | 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: 
71051 
diff
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: 
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 | 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 | 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: 
72521 
diff
changeset
 | 
144  | 
require(length >= 6, "password too short")  | 
| 71265 | 145  | 
    Isabelle_System.bash("pwgen " + length + " 1").check.out
 | 
146  | 
}  | 
|
| 70965 | 147  | 
}  |