# HG changeset patch # User wenzelm # Date 1572959776 -3600 # Node ID b8aeeedf7e6866c8722d836953ae5b02b5888043 # Parent acedd04c1a4235bd7ef8be4a11345a4a131facd1 support for Linux user management; diff -r acedd04c1a42 -r b8aeeedf7e68 src/Pure/System/linux.scala --- a/src/Pure/System/linux.scala Tue Nov 05 13:56:34 2019 +0100 +++ b/src/Pure/System/linux.scala Tue Nov 05 14:16:16 2019 +0100 @@ -63,4 +63,45 @@ def package_install(packages: List[String], progress: Progress = No_Progress): Unit = progress.bash("apt-get install -y -- " + Bash.strings(packages), echo = true).check + + + /* users */ + + def user_exists(name: String): Boolean = + Isabelle_System.bash("id " + Bash.string(name)).ok + + def user_entry(name: String, field: Int): String = + { + val result = Isabelle_System.bash("getent passwd " + Bash.string(name)).check + val fields = space_explode(':', result.out) + + if (1 <= field && field <= fields.length) fields(field - 1) + else error("No passwd field " + field + " for user " + quote(name)) + } + + def user_description(name: String): String = user_entry(name, 5).takeWhile(_ != ',') + + def user_home(name: String): String = user_entry(name, 6) + + def user_add(name: String, description: String = "", ssh_setup: Boolean = false) + { + require(!description.contains(',')) + + if (user_exists(name)) error("User already exists: " + quote(name)) + + Isabelle_System.bash( + "adduser --quiet --disabled-password --gecos " + Bash.string(description) + + " " + Bash.string(name)).check + + if (ssh_setup) { + val id_rsa = user_home(name) + "/.ssh/id_rsa" + Isabelle_System.bash(""" +if [ ! -f """ + Bash.string(id_rsa) + """ ] +then + yes '\n' | sudo -i -u """ + Bash.string(name) + + """ ssh-keygen -q -f """ + Bash.string(id_rsa) + """ +fi + """).check + } + } }