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