author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 73534 | e7fb17bca374 |
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 |
} |