| author | wenzelm | 
| Wed, 13 Nov 2019 13:28:58 +0100 | |
| changeset 71107 | 25c85cc3bc71 | 
| parent 71054 | b64fc38327ae | 
| child 71108 | 783d5786255d | 
| 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"  | 
|
48  | 
}  | 
|
| 70966 | 49  | 
|
50  | 
||
51  | 
/* packages */  | 
|
52  | 
||
53  | 
def reboot_required(): Boolean =  | 
|
54  | 
    Path.explode("/var/run/reboot-required").is_file
 | 
|
55  | 
||
56  | 
def check_reboot_required(): Unit =  | 
|
57  | 
    if (reboot_required()) error("Reboot required")
 | 
|
58  | 
||
59  | 
def package_update(progress: Progress = No_Progress): Unit =  | 
|
60  | 
progress.bash(  | 
|
61  | 
"""apt-get update -y && apt-get upgrade -y && apt autoremove -y""",  | 
|
62  | 
echo = true).check  | 
|
63  | 
||
64  | 
def package_install(packages: List[String], progress: Progress = No_Progress): Unit =  | 
|
65  | 
    progress.bash("apt-get install -y -- " + Bash.strings(packages), echo = true).check
 | 
|
| 71046 | 66  | 
|
67  | 
||
68  | 
/* users */  | 
|
69  | 
||
70  | 
def user_exists(name: String): Boolean =  | 
|
71  | 
    Isabelle_System.bash("id " + Bash.string(name)).ok
 | 
|
72  | 
||
73  | 
def user_entry(name: String, field: Int): String =  | 
|
74  | 
  {
 | 
|
75  | 
    val result = Isabelle_System.bash("getent passwd " + Bash.string(name)).check
 | 
|
76  | 
    val fields = space_explode(':', result.out)
 | 
|
77  | 
||
78  | 
if (1 <= field && field <= fields.length) fields(field - 1)  | 
|
79  | 
    else error("No passwd field " + field + " for user " + quote(name))
 | 
|
80  | 
}  | 
|
81  | 
||
82  | 
def user_description(name: String): String = user_entry(name, 5).takeWhile(_ != ',')  | 
|
83  | 
||
84  | 
def user_home(name: String): String = user_entry(name, 6)  | 
|
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 | 90  | 
  {
 | 
91  | 
    require(!description.contains(','))
 | 
|
92  | 
||
93  | 
    if (user_exists(name)) error("User already exists: " + quote(name))
 | 
|
94  | 
||
95  | 
Isabelle_System.bash(  | 
|
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 | 98  | 
" " + Bash.string(name)).check  | 
99  | 
||
100  | 
    if (ssh_setup) {
 | 
|
101  | 
val id_rsa = user_home(name) + "/.ssh/id_rsa"  | 
|
102  | 
      Isabelle_System.bash("""
 | 
|
103  | 
if [ ! -f """ + Bash.string(id_rsa) + """ ]  | 
|
104  | 
then  | 
|
105  | 
yes '\n' | sudo -i -u """ + Bash.string(name) +  | 
|
106  | 
""" ssh-keygen -q -f """ + Bash.string(id_rsa) + """  | 
|
107  | 
fi  | 
|
108  | 
""").check  | 
|
109  | 
}  | 
|
110  | 
}  | 
|
| 71048 | 111  | 
|
112  | 
||
113  | 
/* system services */  | 
|
114  | 
||
| 71107 | 115  | 
def service_operation(op: String, name: String): Unit =  | 
116  | 
    Isabelle_System.bash("systemctl " + Bash.string(op) + " " + Bash.string(name)).check
 | 
|
| 71048 | 117  | 
|
| 71107 | 118  | 
  def service_enable(name: String) { service_operation("enable", name) }
 | 
119  | 
  def service_disable(name: String) { service_operation("disable", name) }
 | 
|
120  | 
  def service_start(name: String) { service_operation("start", name) }
 | 
|
121  | 
  def service_stop(name: String) { service_operation("stop", name) }
 | 
|
122  | 
  def service_restart(name: String) { service_operation("restart", name) }
 | 
|
| 71051 | 123  | 
|
| 71048 | 124  | 
def service_install(name: String, spec: String)  | 
125  | 
  {
 | 
|
126  | 
    val service_file = Path.explode("/lib/systemd/system") + Path.basic(name).ext("service")
 | 
|
127  | 
File.write(service_file, spec)  | 
|
| 71107 | 128  | 
    Isabelle_System.bash("chmod 0644 " + File.bash_path(service_file)).check
 | 
| 71048 | 129  | 
|
| 71107 | 130  | 
service_enable(name)  | 
131  | 
service_start(name)  | 
|
| 71048 | 132  | 
}  | 
| 70965 | 133  | 
}  |