diff --git a/src/Pure/PIDE/prover.scala b/src/Pure/PIDE/prover.scala --- a/src/Pure/PIDE/prover.scala +++ b/src/Pure/PIDE/prover.scala @@ -1,368 +1,368 @@ /* Title: Pure/PIDE/prover.scala Author: Makarius Options: :folding=explicit: Prover process wrapping. */ package isabelle import java.io.{InputStream, OutputStream, BufferedOutputStream, IOException} object Prover { /* messages */ sealed abstract class Message type Receiver = Message => Unit class Input(val name: String, val args: List[String]) extends Message { override def toString: String = XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))), args.flatMap(s => List(XML.newline, XML.elem(Markup.PROVER_ARG, YXML.parse_body(s))))).toString } class Output(val message: XML.Elem) extends Message { def kind: String = message.markup.name def properties: Properties.T = message.markup.properties def body: XML.Body = message.body def is_init: Boolean = kind == Markup.INIT def is_exit: Boolean = kind == Markup.EXIT def is_stdout: Boolean = kind == Markup.STDOUT def is_stderr: Boolean = kind == Markup.STDERR def is_system: Boolean = kind == Markup.SYSTEM def is_status: Boolean = kind == Markup.STATUS def is_report: Boolean = kind == Markup.REPORT def is_syslog: Boolean = is_init || is_exit || is_system || is_stderr override def toString: String = { val res = if (is_status || is_report) message.body.map(_.toString).mkString else Pretty.string_of(message.body, metric = Symbol.Metric) if (properties.isEmpty) kind.toString + " [[" + res + "]]" else kind.toString + " " + (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]" } } class Protocol_Output(props: Properties.T, val bytes: Bytes) extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil)) { lazy val text: String = bytes.text } } class Prover( receiver: Prover.Receiver, xml_cache: XML.Cache, channel: System_Channel, process: Bash.Process) extends Protocol { /** receiver output **/ private def system_output(text: String) { receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))) } private def protocol_output(props: Properties.T, bytes: Bytes) { receiver(new Prover.Protocol_Output(props, bytes)) } private def output(kind: String, props: Properties.T, body: XML.Body) { val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body)) val reports = Protocol_Message.reports(props, body) for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg))) } private def exit_message(result: Process_Result) { output(Markup.EXIT, Markup.Process_Result(result), - List(XML.Text("Return code: " + result.rc.toString))) + List(XML.Text(result.print_return_code))) } /** process manager **/ private val process_result: Future[Process_Result] = Future.thread("process_result") { val rc = process.join val timing = process.get_timing Process_Result(rc, timing = timing) } private def terminate_process() { try { process.terminate } catch { case exn @ ERROR(_) => system_output("Failed to terminate prover process: " + exn.getMessage) } } private val process_manager = Isabelle_Thread.fork(name = "process_manager") { val stdout = physical_output(false) val (startup_failed, startup_errors) = { var finished: Option[Boolean] = None val result = new StringBuilder(100) while (finished.isEmpty && (process.stderr.ready || !process_result.is_finished)) { while (finished.isEmpty && process.stderr.ready) { try { val c = process.stderr.read if (c == 2) finished = Some(true) else result += c.toChar } catch { case _: IOException => finished = Some(false) } } Time.seconds(0.05).sleep } (finished.isEmpty || !finished.get, result.toString.trim) } if (startup_errors != "") system_output(startup_errors) if (startup_failed) { terminate_process() process_result.join stdout.join exit_message(Process_Result(127)) } else { val (command_stream, message_stream) = channel.rendezvous() command_input_init(command_stream) val stderr = physical_output(true) val message = message_output(message_stream) val result = process_result.join system_output("process terminated") command_input_close() for (thread <- List(stdout, stderr, message)) thread.join system_output("process_manager terminated") exit_message(result) } channel.shutdown() } /* management methods */ def join() { process_manager.join() } def terminate() { system_output("Terminating prover process") command_input_close() var count = 10 while (!process_result.is_finished && count > 0) { Time.seconds(0.1).sleep count -= 1 } if (!process_result.is_finished) terminate_process() } /** process streams **/ /* command input */ private var command_input: Option[Consumer_Thread[List[Bytes]]] = None private def command_input_close(): Unit = command_input.foreach(_.shutdown) private def command_input_init(raw_stream: OutputStream) { val name = "command_input" val stream = new BufferedOutputStream(raw_stream) command_input = Some( Consumer_Thread.fork(name)( consume = { case chunks => try { Bytes(chunks.map(_.length).mkString("", ",", "\n")).write_stream(stream) chunks.foreach(_.write_stream(stream)) stream.flush true } catch { case e: IOException => system_output(name + ": " + e.getMessage); false } }, finish = { case () => stream.close; system_output(name + " terminated") } ) ) } /* physical output */ private def physical_output(err: Boolean): Thread = { val (name, reader, markup) = if (err) ("standard_error", process.stderr, Markup.STDERR) else ("standard_output", process.stdout, Markup.STDOUT) Isabelle_Thread.fork(name = name) { try { var result = new StringBuilder(100) var finished = false while (!finished) { //{{{ var c = -1 var done = false while (!done && (result.isEmpty || reader.ready)) { c = reader.read if (c >= 0) result.append(c.asInstanceOf[Char]) else done = true } if (result.nonEmpty) { output(markup, Nil, List(XML.Text(Symbol.decode(result.toString)))) result.clear } else { reader.close finished = true } //}}} } } catch { case e: IOException => system_output(name + ": " + e.getMessage) } system_output(name + " terminated") } } /* message output */ private def message_output(stream: InputStream): Thread = { class EOF extends Exception class Protocol_Error(msg: String) extends Exception(msg) val name = "message_output" Isabelle_Thread.fork(name = name) { val default_buffer = new Array[Byte](65536) var c = -1 def read_int(): Int = //{{{ { var n = 0 c = stream.read if (c == -1) throw new EOF while (48 <= c && c <= 57) { n = 10 * n + (c - 48) c = stream.read } if (c != 10) throw new Protocol_Error("malformed header: expected integer followed by newline") else n } //}}} def read_chunk_bytes(): (Array[Byte], Int) = //{{{ { val n = read_int() val buf = if (n <= default_buffer.length) default_buffer else new Array[Byte](n) var i = 0 var m = 0 do { m = stream.read(buf, i, n - i) if (m != -1) i += m } while (m != -1 && n > i) if (i != n) throw new Protocol_Error("bad chunk (unexpected EOF after " + i + " of " + n + " bytes)") (buf, n) } //}}} def read_chunk(): XML.Body = { val (buf, n) = read_chunk_bytes() YXML.parse_body_failsafe(UTF8.decode_chars(Symbol.decode, buf, 0, n)) } try { do { try { val header = read_chunk() header match { case List(XML.Elem(Markup(name, props), Nil)) => val kind = name.intern if (kind == Markup.PROTOCOL) { val (buf, n) = read_chunk_bytes() protocol_output(props, Bytes(buf, 0, n)) } else { val body = read_chunk() output(kind, props, body) } case _ => read_chunk() throw new Protocol_Error("bad header: " + header.toString) } } catch { case _: EOF => } } while (c != -1) } catch { case e: IOException => system_output("Cannot read message:\n" + e.getMessage) case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage) } stream.close system_output(name + " terminated") } } /** protocol commands **/ var trace: Boolean = false def protocol_command_raw(name: String, args: List[Bytes]): Unit = command_input match { case Some(thread) if thread.is_active => if (trace) { val payload = (0 /: args)({ case (n, b) => n + b.length }) Output.writeln( "protocol_command " + name + ", args = " + args.length + ", payload = " + payload) } thread.send(Bytes(name) :: args) case _ => error("Inactive prover input thread for command " + quote(name)) } def protocol_command_args(name: String, args: List[String]) { receiver(new Prover.Input(name, args)) protocol_command_raw(name, args.map(Bytes(_))) } def protocol_command(name: String, args: String*): Unit = protocol_command_args(name, args.toList) } diff --git a/src/Pure/System/process_result.scala b/src/Pure/System/process_result.scala --- a/src/Pure/System/process_result.scala +++ b/src/Pure/System/process_result.scala @@ -1,55 +1,64 @@ /* Title: Pure/System/process_result.scala Author: Makarius Result of system process. */ package isabelle +object Process_Result +{ + def print_return_code(rc: Int): String = "Return code: " + rc + def print_rc(rc: Int): String = "return code " + rc +} + final case class Process_Result( rc: Int, out_lines: List[String] = Nil, err_lines: List[String] = Nil, timeout: Boolean = false, timing: Timing = Timing.zero) { def out: String = cat_lines(out_lines) def err: String = cat_lines(err_lines) def output(outs: List[String]): Process_Result = copy(out_lines = out_lines ::: outs.flatMap(split_lines)) def errors(errs: List[String]): Process_Result = copy(err_lines = err_lines ::: errs.flatMap(split_lines)) def error(err: String): Process_Result = errors(List(err)) def was_timeout: Process_Result = copy(rc = 1, timeout = true) def ok: Boolean = rc == 0 def interrupted: Boolean = rc == Exn.Interrupt.return_code def error_rc: Process_Result = if (interrupted) this else copy(rc = rc max 1) def check_rc(pred: Int => Boolean): Process_Result = if (pred(rc)) this else if (interrupted) throw Exn.Interrupt() else Exn.error(err) def check: Process_Result = check_rc(_ == 0) + def print_return_code: String = Process_Result.print_return_code(rc) + def print_rc: String = Process_Result.print_rc(rc) + def print: Process_Result = { Output.warning(err) Output.writeln(out) copy(out_lines = Nil, err_lines = Nil) } def print_stdout: Process_Result = { Output.warning(err, stdout = true) Output.writeln(out, stdout = true) copy(out_lines = Nil, err_lines = Nil) } def print_if(b: Boolean): Process_Result = if (b) print else this def print_stdout_if(b: Boolean): Process_Result = if (b) print_stdout else this } diff --git a/src/Pure/Tools/phabricator.scala b/src/Pure/Tools/phabricator.scala --- a/src/Pure/Tools/phabricator.scala +++ b/src/Pure/Tools/phabricator.scala @@ -1,1079 +1,1079 @@ /* Title: Pure/Tools/phabricator.scala Author: Makarius Support for Phabricator server, notably for Ubuntu 18.04 LTS. See also: - https://www.phacility.com/phabricator - https://secure.phabricator.com/book/phabricator */ package isabelle import scala.collection.mutable import scala.util.matching.Regex object Phabricator { /** defaults **/ /* required packages */ val packages: List[String] = Build_Docker.packages ::: Linux.packages ::: List( // https://secure.phabricator.com/source/phabricator/browse/master/scripts/install/install_ubuntu.sh 15e6e2adea61 "git", "mysql-server", "apache2", "libapache2-mod-php", "php", "php-mysql", "php-gd", "php-curl", "php-apcu", "php-cli", "php-json", "php-mbstring", // more packages "php-xml", "php-zip", "python-pygments", "ssh", "subversion", // mercurial build packages "make", "gcc", "python", "python-dev", "python-docutils", "python-pygments", "python-openssl") /* global system resources */ val www_user = "www-data" val daemon_user = "phabricator" val sshd_config: Path = Path.explode("/etc/ssh/sshd_config") /* installation parameters */ val default_name = "vcs" def phabricator_name(name: String = "", ext: String = ""): String = "phabricator" + (if (name.isEmpty) "" else "-" + name) + (if (ext.isEmpty) "" else "." + ext) def isabelle_phabricator_name(name: String = "", ext: String = ""): String = "isabelle-" + phabricator_name(name = name, ext = ext) def default_root(name: String): Path = Path.explode("/var/www") + Path.basic(phabricator_name(name = name)) def default_repo(name: String): Path = default_root(name) + Path.basic("repo") val default_mailers: Path = Path.explode("mailers.json") val default_system_port: Int = SSH.default_port val alternative_system_port = 222 val default_server_port = 2222 val standard_mercurial_source = "https://www.mercurial-scm.org/release/mercurial-3.9.2.tar.gz" /** global configuration **/ val global_config: Path = Path.explode("/etc/" + isabelle_phabricator_name(ext = "conf")) def global_config_script( init: String = "", body: String = "", exit: String = ""): String = { """#!/bin/bash """ + (if (init.nonEmpty) "\n" + init else "") + """ { while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; } do NAME="$(echo "$REPLY" | cut -d: -f1)" ROOT="$(echo "$REPLY" | cut -d: -f2)" { """ + Library.prefix_lines(" ", body) + """ } < /dev/null done } < """ + File.bash_path(global_config) + "\n" + (if (exit.nonEmpty) "\n" + exit + "\n" else "") } sealed case class Config(name: String, root: Path) { def home: Path = root + Path.explode(phabricator_name()) def execute(command: String): Process_Result = Isabelle_System.bash("bin/" + command, cwd = home.file, redirect = true).check } def read_config(): List[Config] = { if (global_config.is_file) { for (entry <- Library.trim_split_lines(File.read(global_config)) if entry.nonEmpty) yield { space_explode(':', entry) match { case List(name, root) => Config(name, Path.explode(root)) case _ => error("Malformed config file " + global_config + "\nentry " + quote(entry)) } } } else Nil } def write_config(configs: List[Config]) { File.write(global_config, configs.map(config => config.name + ":" + config.root.implode).mkString("", "\n", "\n")) } def get_config(name: String): Config = read_config().find(config => config.name == name) getOrElse error("Bad Isabelle/Phabricator installation " + quote(name)) /** administrative tools **/ /* Isabelle tool wrapper */ val isabelle_tool1 = Isabelle_Tool("phabricator", "invoke command-line tool within Phabricator home directory", args => { var list = false var name = default_name val getopts = Getopts(""" Usage: isabelle phabricator [OPTIONS] COMMAND [ARGS...] Options are: -l list available Phabricator installations -n NAME Phabricator installation name (default: """ + quote(default_name) + """) Invoke a command-line tool within the home directory of the named Phabricator installation. """, "l" -> (_ => list = true), "n:" -> (arg => name = arg)) val more_args = getopts(args) if (more_args.isEmpty && !list) getopts.usage() val progress = new Console_Progress if (list) { for (config <- read_config()) { progress.echo("phabricator " + quote(config.name) + " root " + config.root) } } else { val config = get_config(name) val result = progress.bash(Bash.strings(more_args), cwd = config.home.file, echo = true) - if (!result.ok) error("Return code: " + result.rc.toString) + if (!result.ok) error(result.print_return_code) } }) /** setup **/ def user_setup(name: String, description: String, ssh_setup: Boolean = false) { if (!Linux.user_exists(name)) { Linux.user_add(name, description = description, system = true, ssh_setup = ssh_setup) } else if (Linux.user_description(name) != description) { error("User " + quote(name) + " already exists --" + " for Phabricator it should have the description:\n " + quote(description)) } } def command_setup(name: String, init: String = "", body: String = "", exit: String = ""): Path = { val command = Path.explode("/usr/local/bin") + Path.basic(name) File.write(command, global_config_script(init = init, body = body, exit = exit)) Isabelle_System.chmod("755", command) Isabelle_System.chown("root:root", command) command } def mercurial_setup(mercurial_source: String, progress: Progress = new Progress) { progress.echo("\nMercurial installation from source " + quote(mercurial_source) + " ...") Isabelle_System.with_tmp_dir("mercurial")(tmp_dir => { val archive = if (Url.is_wellformed(mercurial_source)) { val archive = tmp_dir + Path.basic("mercurial.tar.gz") Bytes.write(archive, Url.read_bytes(Url(mercurial_source))) archive } else Path.explode(mercurial_source) Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check File.read_dir(tmp_dir).filter(name => (tmp_dir + Path.basic(name)).is_dir) match { case List(dir) => val build_dir = tmp_dir + Path.basic(dir) progress.bash("make all && make install", cwd = build_dir.file, echo = true).check case dirs => error("Bad archive " + archive + (if (dirs.isEmpty) "" else "\nmultiple directory entries " + commas_quote(dirs))) } }) } def phabricator_setup( options: Options, name: String = default_name, root: String = "", repo: String = "", package_update: Boolean = false, mercurial_source: String = "", progress: Progress = new Progress) { /* system environment */ Linux.check_system_root() progress.echo("System packages ...") if (package_update) { Linux.package_update(progress = progress) Linux.check_reboot_required() } Linux.package_install(packages, progress = progress) Linux.check_reboot_required() if (mercurial_source.nonEmpty) { for { name <- List("mercurial", "mercurial-common") if Linux.package_installed(name) } { error("Cannot install Mercurial from source:\n" + "package package " + quote(name) + " already installed") } mercurial_setup(mercurial_source, progress = progress) } /* users */ if (name.contains((c: Char) => !(Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c))) || Set("", "ssh", "phd", "dump", daemon_user).contains(name)) { error("Bad installation name: " + quote(name)) } user_setup(daemon_user, "Phabricator Daemon User", ssh_setup = true) user_setup(name, "Phabricator SSH User") /* basic installation */ progress.echo("\nPhabricator installation ...") val root_path = if (root.nonEmpty) Path.explode(root) else default_root(name) val repo_path = if (repo.nonEmpty) Path.explode(repo) else default_repo(name) val configs = read_config() for (config <- configs if config.name == name) { error("Duplicate Phabricator installation " + quote(name) + " in " + config.root) } if (!Isabelle_System.bash("mkdir -p " + File.bash_path(root_path)).ok) { error("Failed to create root directory " + root_path) } Isabelle_System.chown(Bash.string(www_user) + ":" + Bash.string(www_user), root_path) Isabelle_System.chmod("755", root_path) progress.bash(cwd = root_path.file, echo = true, script = """ set -e echo "Cloning distribution repositories:" git clone --branch stable https://github.com/phacility/arcanist.git git -C arcanist reset --hard """ + Bash.string(options.string("phabricator_version_arcanist")) + """ git clone --branch stable https://github.com/phacility/libphutil.git git -C libphutil reset --hard """ + Bash.string(options.string("phabricator_version_libphutil")) + """ git clone --branch stable https://github.com/phacility/phabricator.git git -C phabricator reset --hard """ + Bash.string(options.string("phabricator_version_phabricator")) + """ """).check val config = Config(name, root_path) write_config(configs ::: List(config)) config.execute("config set pygments.enabled true") /* local repository directory */ progress.echo("\nRepository hosting setup ...") if (!Isabelle_System.bash("mkdir -p " + File.bash_path(repo_path)).ok) { error("Failed to create local repository directory " + repo_path) } Isabelle_System.chown( "-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), repo_path) Isabelle_System.chmod("755", repo_path) config.execute("config set repository.default-local-path " + File.bash_path(repo_path)) val sudoers_file = Path.explode("/etc/sudoers.d") + Path.basic(isabelle_phabricator_name(name = name)) File.write(sudoers_file, www_user + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/local/bin/hg, /usr/bin/hg, /usr/bin/ssh, /usr/bin/id\n" + name + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/bin/git-upload-pack, /usr/bin/git-receive-pack, /usr/local/bin/hg, /usr/bin/hg, /usr/bin/svnserve, /usr/bin/ssh, /usr/bin/id\n") Isabelle_System.chmod("440", sudoers_file) config.execute("config set diffusion.ssh-user " + Bash.string(config.name)) /* MySQL setup */ progress.echo("\nMySQL setup ...") File.write(Path.explode("/etc/mysql/mysql.conf.d/" + phabricator_name(ext = "cnf")), """[mysqld] max_allowed_packet = 32M innodb_buffer_pool_size = 1600M local_infile = 0 """) Linux.service_restart("mysql") def mysql_conf(R: Regex, which: String): String = { val conf = Path.explode("/etc/mysql/debian.cnf") split_lines(File.read(conf)).collectFirst({ case R(a) => a }) match { case Some(res) => res case None => error("Cannot determine " + which + " from " + conf) } } val mysql_root_user = mysql_conf("""^user\s*=\s*(\S*)\s*$""".r, "superuser name") val mysql_root_password = mysql_conf("""^password\s*=\s*(\S*)\s*$""".r, "superuser password") val mysql_name = phabricator_name(name = name).replace("-", "_") val mysql_user_string = SQL.string(mysql_name) + "@'localhost'" val mysql_password = Linux.generate_password() Isabelle_System.bash("mysql --user=" + Bash.string(mysql_root_user) + " --password=" + Bash.string(mysql_root_password) + " --execute=" + Bash.string( """DROP USER IF EXISTS """ + mysql_user_string + "; " + """CREATE USER """ + mysql_user_string + """ IDENTIFIED BY """ + SQL.string(mysql_password) + """ PASSWORD EXPIRE NEVER; """ + """GRANT ALL ON `""" + (mysql_name + "_%").replace("_", "\\_") + """`.* TO """ + mysql_user_string + ";")).check config.execute("config set mysql.user " + Bash.string(mysql_name)) config.execute("config set mysql.pass " + Bash.string(mysql_password)) config.execute("config set phabricator.cache-namespace " + Bash.string(mysql_name)) config.execute("config set storage.default-namespace " + Bash.string(mysql_name)) config.execute("config set storage.mysql-engine.max-size 8388608") progress.bash("bin/storage upgrade --force", cwd = config.home.file, echo = true).check /* database dump */ val dump_name = isabelle_phabricator_name(name = "dump") command_setup(dump_name, body = """mkdir -p "$ROOT/database" && chown root:root "$ROOT/database" && chmod 700 "$ROOT/database" [ -e "$ROOT/database/dump.sql.gz" ] && mv -f "$ROOT/database/dump.sql.gz" "$ROOT/database/dump-old.sql.gz" echo -n "Creating $ROOT/database/dump.sql.gz ..." "$ROOT/phabricator/bin/storage" dump --compress --output "$ROOT/database/dump.sql.gz" 2>&1 | fgrep -v '[Warning] Using a password on the command line interface can be insecure' echo " $(ls -hs "$ROOT/database/dump.sql.gz" | cut -d" " -f1)" """) /* Phabricator upgrade */ command_setup(isabelle_phabricator_name(name = "upgrade"), init = """BRANCH="${1:-stable}" if [ "$BRANCH" != "master" -a "$BRANCH" != "stable" ] then echo "Bad branch: \"$BRANCH\"" exit 1 fi systemctl stop isabelle-phabricator-phd systemctl stop apache2 """, body = """echo -e "\nUpgrading phabricator \"$NAME\" root \"$ROOT\" ..." for REPO in libphutil arcanist phabricator do cd "$ROOT/$REPO" echo -e "\nUpdating \"$REPO\" ..." git checkout "$BRANCH" git pull done echo -e "\nUpgrading storage ..." "$ROOT/phabricator/bin/storage" upgrade --force """, exit = """systemctl start apache2 systemctl start isabelle-phabricator-phd""") /* PHP setup */ val php_version = Isabelle_System.bash("""php --run 'echo PHP_MAJOR_VERSION . "." . PHP_MINOR_VERSION;'""") .check.out val php_conf = Path.explode("/etc/php") + Path.basic(php_version) + // educated guess Path.explode("apache2/conf.d") + Path.basic(isabelle_phabricator_name(ext = "ini")) File.write(php_conf, "post_max_size = 32M\n" + "opcache.validate_timestamps = 0\n" + "memory_limit = 512M\n" + "max_execution_time = 120\n") /* Apache setup */ progress.echo("Apache setup ...") val apache_root = Path.explode("/etc/apache2") val apache_sites = apache_root + Path.explode("sites-available") if (!apache_sites.is_dir) error("Bad Apache sites directory " + apache_sites) val server_name = phabricator_name(name = name, ext = "lvh.me") // alias for "localhost" for testing val server_url = "http://" + server_name File.write(apache_sites + Path.basic(isabelle_phabricator_name(name = name, ext = "conf")), """ ServerName """ + server_name + """ ServerAdmin webmaster@localhost DocumentRoot """ + config.home.implode + """/webroot ErrorLog ${APACHE_LOG_DIR}/error.log CustomLog ${APACHE_LOG_DIR}/access.log combined RewriteEngine on RewriteRule ^(.*)$ /index.php?__path__=$1 [B,L,QSA] # vim: syntax=apache ts=4 sw=4 sts=4 sr noet """) Isabelle_System.bash( """ set -e a2enmod rewrite a2ensite """ + Bash.string(isabelle_phabricator_name(name = name))).check config.execute("config set phabricator.base-uri " + Bash.string(server_url)) Linux.service_restart("apache2") progress.echo("\nFurther manual configuration via " + server_url) /* PHP daemon */ progress.echo("\nPHP daemon setup ...") val phd_log_path = Path.explode("/var/tmp/phd") Isabelle_System.mkdirs(phd_log_path) Isabelle_System.chown( "-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), phd_log_path) Isabelle_System.chmod("755", phd_log_path) config.execute("config set phd.user " + Bash.string(daemon_user)) config.execute("config set phd.log-directory /var/tmp/phd/" + isabelle_phabricator_name(name = name) + "/log") val phd_name = isabelle_phabricator_name(name = "phd") Linux.service_shutdown(phd_name) val phd_command = command_setup(phd_name, body = """"$ROOT/phabricator/bin/phd" "$@" """) try { Linux.service_install(phd_name, """[Unit] Description=PHP daemon manager for Isabelle/Phabricator After=syslog.target network.target apache2.service mysql.service [Service] Type=oneshot User=""" + daemon_user + """ Group=""" + daemon_user + """ Environment=PATH=/sbin:/usr/sbin:/usr/local/sbin:/usr/local/bin:/usr/bin:/bin ExecStart=""" + phd_command.implode + """ start --force ExecStop=""" + phd_command.implode + """ stop RemainAfterExit=yes [Install] WantedBy=multi-user.target """) } catch { case ERROR(msg) => progress.bash("bin/phd status", cwd = config.home.file, echo = true).check error(msg) } } /* Isabelle tool wrapper */ val isabelle_tool2 = Isabelle_Tool("phabricator_setup", "setup Phabricator server on Ubuntu Linux", args => { var mercurial_source = "" var repo = "" var package_update = false var name = default_name var options = Options.init() var root = "" val getopts = Getopts(""" Usage: isabelle phabricator_setup [OPTIONS] Options are: -M SOURCE install Mercurial from source: local PATH, or URL, or ":" for """ + standard_mercurial_source + """ -R DIR repository directory (default: """ + default_repo("NAME") + """) -U full update of system packages before installation -n NAME Phabricator installation name (default: """ + quote(default_name) + """) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -r DIR installation root directory (default: """ + default_root("NAME") + """) Install Phabricator as LAMP application (Linux, Apache, MySQL, PHP). The installation name (default: """ + quote(default_name) + """) is mapped to a regular Unix user; this is relevant for public SSH access. """, "M:" -> (arg => mercurial_source = (if (arg == ":") standard_mercurial_source else arg)), "R:" -> (arg => repo = arg), "U" -> (_ => package_update = true), "n:" -> (arg => name = arg), "o:" -> (arg => options = options + arg), "r:" -> (arg => root = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress val release = Linux.Release() if (!release.is_ubuntu_18_04) error("Bad Linux version: Ubuntu 18.04 LTS required") phabricator_setup(options, name = name, root = root, repo = repo, package_update = package_update, mercurial_source = mercurial_source, progress = progress) }) /** setup mail **/ val mailers_template: String = """[ { "key": "example.org", "type": "smtp", "options": { "host": "mail.example.org", "port": 465, "user": "phabricator@example.org", "password": "********", "protocol": "ssl", "message-id": true } } ]""" def phabricator_setup_mail( name: String = default_name, config_file: Option[Path] = None, test_user: String = "", progress: Progress = new Progress) { Linux.check_system_root() val config = get_config(name) val default_config_file = config.root + default_mailers val mail_config = config_file getOrElse default_config_file def setup_mail { progress.echo("Using mail configuration from " + mail_config) config.execute("config set cluster.mailers --stdin < " + File.bash_path(mail_config)) if (test_user.nonEmpty) { progress.echo("Sending test mail to " + quote(test_user)) progress.bash(cwd = config.home.file, echo = true, script = """echo "Test from Phabricator ($(date))" | bin/mail send-test --subject "Test" --to """ + Bash.string(test_user)).check } } if (config_file.isEmpty) { if (!default_config_file.is_file) { File.write(default_config_file, mailers_template) Isabelle_System.chmod("600", default_config_file) } if (File.read(default_config_file) == mailers_template) { progress.echo("Please invoke the tool again, after providing details in\n " + default_config_file.implode + "\n") } else setup_mail } else setup_mail } /* Isabelle tool wrapper */ val isabelle_tool3 = Isabelle_Tool("phabricator_setup_mail", "setup mail for one Phabricator installation", args => { var test_user = "" var name = default_name var config_file: Option[Path] = None val getopts = Getopts(""" Usage: isabelle phabricator_setup_mail [OPTIONS] Options are: -T USER send test mail to Phabricator user -f FILE config file (default: """ + default_mailers + """ within Phabricator root) -n NAME Phabricator installation name (default: """ + quote(default_name) + """) Provide mail configuration for existing Phabricator installation. """, "T:" -> (arg => test_user = arg), "f:" -> (arg => config_file = Some(Path.explode(arg))), "n:" -> (arg => name = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress phabricator_setup_mail(name = name, config_file = config_file, test_user = test_user, progress = progress) }) /** setup ssh **/ /* sshd config */ private val Port = """^\s*Port\s+(\d+)\s*$""".r private val No_Port = """^#\s*Port\b.*$""".r private val Any_Port = """^#?\s*Port\b.*$""".r def conf_ssh_port(port: Int): String = if (port == SSH.default_port) "#Port " + SSH.default_port else "Port " + port def read_ssh_port(conf: Path): Int = { val lines = split_lines(File.read(conf)) val ports = lines.flatMap({ case Port(Value.Int(p)) => Some(p) case No_Port() => Some(SSH.default_port) case _ => None }) ports match { case List(port) => port case Nil => error("Missing Port specification in " + conf) case _ => error("Multiple Port specifications in " + conf) } } def write_ssh_port(conf: Path, port: Int): Boolean = { val old_port = read_ssh_port(conf) if (old_port == port) false else { val lines = split_lines(File.read(conf)) val lines1 = lines.map({ case Any_Port() => conf_ssh_port(port) case line => line }) File.write(conf, cat_lines(lines1)) true } } /* phabricator_setup_ssh */ def phabricator_setup_ssh( server_port: Int = default_server_port, system_port: Int = default_system_port, progress: Progress = new Progress) { Linux.check_system_root() val configs = read_config() if (server_port == system_port) { error("Port for Phabricator sshd coincides with system port: " + system_port) } val sshd_conf_system = Path.explode("/etc/ssh/sshd_config") val sshd_conf_server = sshd_conf_system.ext(isabelle_phabricator_name()) val ssh_name = isabelle_phabricator_name(name = "ssh") Linux.service_shutdown(ssh_name) val old_system_port = read_ssh_port(sshd_conf_system) if (old_system_port != system_port) { progress.echo("Reconfigurig system ssh service") Linux.service_shutdown("ssh") write_ssh_port(sshd_conf_system, system_port) Linux.service_start("ssh") } progress.echo("Configuring " + ssh_name + " service") val ssh_command = command_setup(ssh_name, body = """if [ "$1" = "$NAME" ] then exec "$ROOT/phabricator/bin/ssh-auth" "$@" fi""", exit = "exit 1") File.write(sshd_conf_server, """# OpenBSD Secure Shell server for Isabelle/Phabricator AuthorizedKeysCommand """ + ssh_command.implode + """ AuthorizedKeysCommandUser """ + daemon_user + """ AuthorizedKeysFile none AllowUsers """ + configs.map(_.name).mkString(" ") + """ Port """ + server_port + """ Protocol 2 PermitRootLogin no AllowAgentForwarding no AllowTcpForwarding no PrintMotd no PrintLastLog no PasswordAuthentication no ChallengeResponseAuthentication no PidFile /var/run/""" + ssh_name + """.pid """) Linux.service_install(ssh_name, """[Unit] Description=OpenBSD Secure Shell server for Isabelle/Phabricator After=network.target auditd.service ConditionPathExists=!/etc/ssh/sshd_not_to_be_run [Service] EnvironmentFile=-/etc/default/ssh ExecStartPre=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t ExecStart=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -D $SSHD_OPTS ExecReload=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t ExecReload=/bin/kill -HUP $MAINPID KillMode=process Restart=on-failure RestartPreventExitStatus=255 Type=notify RuntimeDirectory=sshd-phabricator RuntimeDirectoryMode=0755 [Install] WantedBy=multi-user.target Alias=""" + ssh_name + """.service """) for (config <- configs) { progress.echo("phabricator " + quote(config.name) + " port " + server_port) config.execute("config set diffusion.ssh-port " + Bash.string(server_port.toString)) if (server_port == SSH.default_port) config.execute("config delete diffusion.ssh-port") } } /* Isabelle tool wrapper */ val isabelle_tool4 = Isabelle_Tool("phabricator_setup_ssh", "setup ssh service for all Phabricator installations", args => { var server_port = default_server_port var system_port = default_system_port val getopts = Getopts(""" Usage: isabelle phabricator_setup_ssh [OPTIONS] Options are: -p PORT sshd port for Phabricator servers (default: """ + default_server_port + """) -q PORT sshd port for the operating system (default: """ + default_system_port + """) Configure ssh service for all Phabricator installations: a separate sshd is run in addition to the one of the operating system, and ports need to be distinct. A particular Phabricator installation is addressed by using its name as the ssh user; the actual Phabricator user is determined via stored ssh keys. """, "p:" -> (arg => server_port = Value.Int.parse(arg)), "q:" -> (arg => system_port = Value.Int.parse(arg))) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress phabricator_setup_ssh( server_port = server_port, system_port = system_port, progress = progress) }) /** conduit API **/ object API { /* user information */ sealed case class User( id: Long, phid: String, name: String, real_name: String, roles: List[String]) { def is_valid: Boolean = roles.contains("verified") && roles.contains("approved") && roles.contains("activated") def is_admin: Boolean = roles.contains("admin") def is_regular: Boolean = !(roles.contains("bot") || roles.contains("list")) } /* repository information */ sealed case class Repository( vcs: VCS.Value, id: Long, phid: String, name: String, callsign: String, short_name: String, importing: Boolean, ssh_url: String) { def is_hg: Boolean = vcs == VCS.hg } object VCS extends Enumeration { val hg, git, svn = Value def read(s: String): Value = try { withName(s) } catch { case _: java.util.NoSuchElementException => error("Unknown vcs type " + quote(s)) } } def edits(typ: String, value: JSON.T): List[JSON.Object.T] = List(JSON.Object("type" -> typ, "value" -> value)) def opt_edits(typ: String, value: Option[JSON.T]): List[JSON.Object.T] = value.toList.flatMap(edits(typ, _)) /* result with optional error */ sealed case class Result(result: JSON.T, error: Option[String]) { def ok: Boolean = error.isEmpty def get: JSON.T = if (ok) result else Exn.error(error.get) def get_value[A](unapply: JSON.T => Option[A]): A = unapply(get) getOrElse Exn.error("Bad JSON result: " + JSON.Format(result)) def get_string: String = get_value(JSON.Value.String.unapply) } def make_result(json: JSON.T): Result = { val result = JSON.value(json, "result").getOrElse(JSON.Object.empty) val error_info = JSON.string(json, "error_info") val error_code = JSON.string(json, "error_code") Result(result, error_info orElse error_code) } /* context for operations */ def apply(user: String, host: String, port: Int = SSH.default_port): API = new API(user, host, port) } final class API private(ssh_user: String, ssh_host: String, ssh_port: Int) { /* connection */ require(ssh_host.nonEmpty && ssh_port >= 0) private def ssh_user_prefix: String = SSH.user_prefix(ssh_user) private def ssh_port_suffix: String = SSH.port_suffix(ssh_port) override def toString: String = ssh_user_prefix + ssh_host + ssh_port_suffix def hg_url: String = "ssh://" + ssh_user_prefix + ssh_host + ssh_port_suffix /* execute methods */ def execute_raw(method: String, params: JSON.T = JSON.Object.empty): JSON.T = { Isabelle_System.with_tmp_file("params", "json")(params_file => { File.write(params_file, JSON.Format(JSON.Object("params" -> JSON.Format(params)))) val result = Isabelle_System.bash( "ssh -p " + ssh_port + " " + Bash.string(ssh_user_prefix + ssh_host) + " conduit " + Bash.string(method) + " < " + File.bash_path(params_file)).check JSON.parse(result.out, strict = false) }) } def execute(method: String, params: JSON.T = JSON.Object.empty): API.Result = API.make_result(execute_raw(method, params = params)) def execute_search[A]( method: String, params: JSON.Object.T, unapply: JSON.T => Option[A]): List[A] = { val results = new mutable.ListBuffer[A] var after = "" do { val result = execute(method, params = params ++ JSON.optional("after" -> proper_string(after))) results ++= result.get_value(JSON.list(_, "data", unapply)) after = result.get_value(JSON.value(_, "cursor", JSON.string0(_, "after"))) } while (after.nonEmpty) results.toList } def ping(): String = execute("conduit.ping").get_string /* users */ lazy val user_phid: String = execute("user.whoami").get_value(JSON.string(_, "phid")) lazy val user_name: String = execute("user.whoami").get_value(JSON.string(_, "userName")) def get_users( all: Boolean = false, phid: String = "", name: String = ""): List[API.User] = { val constraints: JSON.Object.T = (for { (key, value) <- List("phids" -> phid, "usernames" -> name) if value.nonEmpty } yield (key, List(value))).toMap execute_search("user.search", JSON.Object("queryKey" -> (if (all) "all" else "active"), "constraints" -> constraints), data => JSON.value(data, "fields", fields => for { id <- JSON.long(data, "id") phid <- JSON.string(data, "phid") name <- JSON.string(fields, "username") real_name <- JSON.string0(fields, "realName") roles <- JSON.strings(fields, "roles") } yield API.User(id, phid, name, real_name, roles))) } def the_user(phid: String): API.User = get_users(phid = phid) match { case List(user) => user case _ => error("Bad user PHID " + quote(phid)) } /* repositories */ def get_repositories( all: Boolean = false, phid: String = "", callsign: String = "", short_name: String = ""): List[API.Repository] = { val constraints: JSON.Object.T = (for { (key, value) <- List("phids" -> phid, "callsigns" -> callsign, "shortNames" -> short_name) if value.nonEmpty } yield (key, List(value))).toMap execute_search("diffusion.repository.search", JSON.Object("queryKey" -> (if (all) "all" else "active"), "constraints" -> constraints), data => JSON.value(data, "fields", fields => for { vcs_name <- JSON.string(fields, "vcs") id <- JSON.long(data, "id") phid <- JSON.string(data, "phid") name <- JSON.string(fields, "name") callsign <- JSON.string0(fields, "callsign") short_name <- JSON.string0(fields, "shortName") importing <- JSON.bool(fields, "isImporting") } yield { val vcs = API.VCS.read(vcs_name) val url_path = if (short_name.isEmpty) "/diffusion/" + id else "/source/" + short_name val ssh_url = vcs match { case API.VCS.hg => hg_url + url_path case API.VCS.git => hg_url + url_path + ".git" case API.VCS.svn => "" } API.Repository(vcs, id, phid, name, callsign, short_name, importing, ssh_url) })) } def the_repository(phid: String): API.Repository = get_repositories(phid = phid) match { case List(repo) => repo case _ => error("Bad repository PHID " + quote(phid)) } def create_repository( name: String, callsign: String = "", // unique name, UPPERCASE short_name: String = "", // unique name description: String = "", public: Boolean = false, vcs: API.VCS.Value = API.VCS.hg): API.Repository = { require(name.nonEmpty) val transactions = API.edits("vcs", vcs.toString) ::: API.edits("name", name) ::: API.opt_edits("callsign", proper_string(callsign)) ::: API.opt_edits("shortName", proper_string(short_name)) ::: API.opt_edits("description", proper_string(description)) ::: (if (public) Nil else API.edits("view", user_phid) ::: API.edits("policy.push", user_phid)) ::: API.edits("status", "active") val phid = execute("diffusion.repository.edit", params = JSON.Object("transactions" -> transactions)) .get_value(JSON.value(_, "object", JSON.string(_, "phid"))) execute("diffusion.looksoon", params = JSON.Object("repositories" -> List(phid))).get the_repository(phid) } } } diff --git a/src/Pure/Tools/server.scala b/src/Pure/Tools/server.scala --- a/src/Pure/Tools/server.scala +++ b/src/Pure/Tools/server.scala @@ -1,614 +1,614 @@ /* Title: Pure/Tools/server.scala Author: Makarius Resident Isabelle servers. Message formats: - short message (single line): NAME ARGUMENT - long message (multiple lines): BYTE_LENGTH NAME ARGUMENT Argument formats: - Unit as empty string - XML.Elem in YXML notation - JSON.T in standard notation */ package isabelle import java.io.{BufferedInputStream, BufferedOutputStream, InputStreamReader, OutputStreamWriter, IOException} import java.net.{Socket, SocketException, SocketTimeoutException, ServerSocket, InetAddress} object Server { /* message argument */ object Argument { def is_name_char(c: Char): Boolean = Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c) || c == '_' || c == '.' def split(msg: String): (String, String) = { val name = msg.takeWhile(is_name_char) val argument = msg.substring(name.length).dropWhile(Symbol.is_ascii_blank) (name, argument) } def print(arg: Any): String = arg match { case () => "" case t: XML.Elem => YXML.string_of_tree(t) case t: JSON.T => JSON.Format(t) } def parse(argument: String): Any = if (argument == "") () else if (YXML.detect_elem(argument)) YXML.parse_elem(argument) else JSON.parse(argument, strict = false) def unapply(argument: String): Option[Any] = try { Some(parse(argument)) } catch { case ERROR(_) => None } } /* input command */ object Command { type T = PartialFunction[(Context, Any), Any] private val table: Map[String, T] = Map( "help" -> { case (_, ()) => table.keySet.toList.sorted }, "echo" -> { case (_, t) => t }, "shutdown" -> { case (context, ()) => context.server.shutdown() }, "cancel" -> { case (context, Server_Commands.Cancel(args)) => context.cancel_task(args.task) }, "session_build" -> { case (context, Server_Commands.Session_Build(args)) => context.make_task(task => Server_Commands.Session_Build.command(args, progress = task.progress)._1) }, "session_start" -> { case (context, Server_Commands.Session_Start(args)) => context.make_task(task => { val (res, entry) = Server_Commands.Session_Start.command( args, progress = task.progress, log = context.server.log) context.server.add_session(entry) res }) }, "session_stop" -> { case (context, Server_Commands.Session_Stop(id)) => context.make_task(_ => { val session = context.server.remove_session(id) Server_Commands.Session_Stop.command(session)._1 }) }, "use_theories" -> { case (context, Server_Commands.Use_Theories(args)) => context.make_task(task => { val session = context.server.the_session(args.session_id) Server_Commands.Use_Theories.command( args, session, id = task.id, progress = task.progress)._1 }) }, "purge_theories" -> { case (context, Server_Commands.Purge_Theories(args)) => val session = context.server.the_session(args.session_id) Server_Commands.Purge_Theories.command(args, session)._1 }) def unapply(name: String): Option[T] = table.get(name) } /* output reply */ class Error(val message: String, val json: JSON.Object.T = JSON.Object.empty) extends RuntimeException(message) def json_error(exn: Throwable): JSON.Object.T = exn match { case e: Error => Reply.error_message(e.message) ++ e.json case ERROR(msg) => Reply.error_message(msg) case _ if Exn.is_interrupt(exn) => Reply.error_message(Exn.message(exn)) case _ => JSON.Object.empty } object Reply extends Enumeration { val OK, ERROR, FINISHED, FAILED, NOTE = Value def message(msg: String, kind: String = ""): JSON.Object.T = JSON.Object(Markup.KIND -> proper_string(kind).getOrElse(Markup.WRITELN), "message" -> msg) def error_message(msg: String): JSON.Object.T = message(msg, kind = Markup.ERROR) def unapply(msg: String): Option[(Reply.Value, Any)] = { if (msg == "") None else { val (name, argument) = Argument.split(msg) for { reply <- try { Some(withName(name)) } catch { case _: NoSuchElementException => None } arg <- Argument.unapply(argument) } yield (reply, arg) } } } /* socket connection */ object Connection { def apply(socket: Socket): Connection = new Connection(socket) } class Connection private(socket: Socket) extends AutoCloseable { override def toString: String = socket.toString def close() { socket.close } def set_timeout(t: Time) { socket.setSoTimeout(t.ms.toInt) } private val in = new BufferedInputStream(socket.getInputStream) private val out = new BufferedOutputStream(socket.getOutputStream) private val out_lock: AnyRef = new Object def tty_loop(): TTY_Loop = new TTY_Loop( new OutputStreamWriter(out), new InputStreamReader(in), writer_lock = out_lock) def read_password(password: String): Boolean = try { Byte_Message.read_line(in).map(_.text) == Some(password) } catch { case _: IOException => false } def read_message(): Option[String] = try { Byte_Message.read_line_message(in).map(_.text) } catch { case _: IOException => None } def write_message(msg: String): Unit = out_lock.synchronized { Byte_Message.write_line_message(out, Bytes(UTF8.bytes(msg))) } def reply(r: Reply.Value, arg: Any) { val argument = Argument.print(arg) write_message(if (argument == "") r.toString else r.toString + " " + argument) } def reply_ok(arg: Any) { reply(Reply.OK, arg) } def reply_error(arg: Any) { reply(Reply.ERROR, arg) } def reply_error_message(message: String, more: JSON.Object.Entry*): Unit = reply_error(Reply.error_message(message) ++ more) def notify(arg: Any) { reply(Reply.NOTE, arg) } } /* context with output channels */ class Context private[Server](val server: Server, connection: Connection) extends AutoCloseable { context => def reply(r: Reply.Value, arg: Any) { connection.reply(r, arg) } def notify(arg: Any) { connection.notify(arg) } def message(kind: String, msg: String, more: JSON.Object.Entry*): Unit = notify(Reply.message(msg, kind = kind) ++ more) def writeln(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WRITELN, msg, more:_*) def warning(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WARNING, msg, more:_*) def error_message(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.ERROR, msg, more:_*) def progress(more: JSON.Object.Entry*): Connection_Progress = new Connection_Progress(context, more:_*) override def toString: String = connection.toString /* asynchronous tasks */ private val _tasks = Synchronized(Set.empty[Task]) def make_task(body: Task => JSON.Object.T): Task = { val task = new Task(context, body) _tasks.change(_ + task) task } def remove_task(task: Task): Unit = _tasks.change(_ - task) def cancel_task(id: UUID.T): Unit = _tasks.change(tasks => { tasks.find(task => task.id == id).foreach(_.cancel); tasks }) def close() { while(_tasks.change_result(tasks => { tasks.foreach(_.cancel); (tasks.nonEmpty, tasks) })) { _tasks.value.foreach(_.join) } } } class Connection_Progress private[Server](context: Context, more: JSON.Object.Entry*) extends Progress { override def echo(msg: String): Unit = context.writeln(msg, more:_*) override def echo_warning(msg: String): Unit = context.warning(msg, more:_*) override def echo_error_message(msg: String): Unit = context.error_message(msg, more:_*) override def theory(theory: Progress.Theory) { val entries: List[JSON.Object.Entry] = List("theory" -> theory.theory, "session" -> theory.session) ::: (theory.percentage match { case None => Nil case Some(p) => List("percentage" -> p) }) context.writeln(theory.message, entries ::: more.toList:_*) } override def nodes_status(nodes_status: Document_Status.Nodes_Status) { val json = for ((name, node_status) <- nodes_status.present) yield name.json + ("status" -> nodes_status(name).json) context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json)) } override def toString: String = context.toString } class Task private[Server](val context: Context, body: Task => JSON.Object.T) { task => val id: UUID.T = UUID.random() val ident: JSON.Object.Entry = ("task" -> id.toString) val progress: Connection_Progress = context.progress(ident) def cancel { progress.stop } private lazy val thread = Isabelle_Thread.fork(name = "server_task") { Exn.capture { body(task) } match { case Exn.Res(res) => context.reply(Reply.FINISHED, res + ident) case Exn.Exn(exn) => val err = json_error(exn) if (err.isEmpty) throw exn else context.reply(Reply.FAILED, err + ident) } progress.stop context.remove_task(task) } def start { thread } def join { thread.join } } /* server info */ val localhost_name: String = "127.0.0.1" def localhost: InetAddress = InetAddress.getByName(localhost_name) def print_address(port: Int): String = localhost_name + ":" + port def print(port: Int, password: String): String = print_address(port) + " (password " + quote(password) + ")" object Info { private val Pattern = ("""server "([^"]*)" = \Q""" + localhost_name + """\E:(\d+) \(password "([^"]*)"\)""").r def parse(s: String): Option[Info] = s match { case Pattern(name, Value.Int(port), password) => Some(Info(name, port, password)) case _ => None } def apply(name: String, port: Int, password: String): Info = new Info(name, port, password) } class Info private(val name: String, val port: Int, val password: String) { def address: String = print_address(port) override def toString: String = "server " + quote(name) + " = " + print(port, password) def connection(): Connection = { val connection = Connection(new Socket(localhost, port)) connection.write_message(password) connection } def active(): Boolean = try { using(connection())(connection => { connection.set_timeout(Time.seconds(2.0)) connection.read_message() match { case Some(Reply(Reply.OK, _)) => true case _ => false } }) } catch { case _: IOException => false case _: SocketException => false case _: SocketTimeoutException => false } } /* per-user servers */ val default_name = "isabelle" object Data { val database = Path.explode("$ISABELLE_HOME_USER/servers.db") val name = SQL.Column.string("name").make_primary_key val port = SQL.Column.int("port") val password = SQL.Column.string("password") val table = SQL.Table("isabelle_servers", List(name, port, password)) } def list(db: SQLite.Database): List[Info] = if (db.tables.contains(Data.table.name)) { db.using_statement(Data.table.select())(stmt => stmt.execute_query().iterator(res => Info( res.string(Data.name), res.int(Data.port), res.string(Data.password))).toList.sortBy(_.name)) } else Nil def find(db: SQLite.Database, name: String): Option[Info] = list(db).find(server_info => server_info.name == name && server_info.active) def init( name: String = default_name, port: Int = 0, existing_server: Boolean = false, log: Logger = No_Logger): (Info, Option[Server]) = { using(SQLite.open_database(Data.database))(db => { db.transaction { Isabelle_System.chmod("600", Data.database) db.create_table(Data.table) list(db).filterNot(_.active).foreach(server_info => db.using_statement(Data.table.delete(Data.name.where_equal(server_info.name)))( _.execute)) } db.transaction { find(db, name) match { case Some(server_info) => (server_info, None) case None => if (existing_server) error("Isabelle server " + quote(name) + " not running") val server = new Server(port, log) val server_info = Info(name, server.port, server.password) db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute) db.using_statement(Data.table.insert())(stmt => { stmt.string(1) = server_info.name stmt.int(2) = server_info.port stmt.string(3) = server_info.password stmt.execute() }) server.start (server_info, Some(server)) } } }) } def exit(name: String = default_name): Boolean = { using(SQLite.open_database(Data.database))(db => db.transaction { find(db, name) match { case Some(server_info) => using(server_info.connection())(_.write_message("shutdown")) while(server_info.active) { Time.seconds(0.05).sleep } true case None => false } }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("server", "manage resident Isabelle servers", args => { var console = false var log_file: Option[Path] = None var operation_list = false var operation_exit = false var name = default_name var port = 0 var existing_server = false val getopts = Getopts(""" Usage: isabelle server [OPTIONS] Options are: -L FILE logging on FILE -c console interaction with specified server -l list servers (alternative operation) -n NAME explicit server name (default: """ + default_name + """) -p PORT explicit server port -s assume existing server, no implicit startup -x exit specified server (alternative operation) Manage resident Isabelle servers. """, "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))), "c" -> (_ => console = true), "l" -> (_ => operation_list = true), "n:" -> (arg => name = arg), "p:" -> (arg => port = Value.Int.parse(arg)), "s" -> (_ => existing_server = true), "x" -> (_ => operation_exit = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() if (operation_list) { for { server_info <- using(SQLite.open_database(Data.database))(list) if server_info.active } Output.writeln(server_info.toString, stdout = true) } else if (operation_exit) { val ok = Server.exit(name) sys.exit(if (ok) 0 else 2) } else { val log = Logger.make(log_file) val (server_info, server) = init(name, port = port, existing_server = existing_server, log = log) Output.writeln(server_info.toString, stdout = true) if (console) { using(server_info.connection())(connection => connection.tty_loop().join) } server.foreach(_.join) } }) } class Server private(_port: Int, val log: Logger) { server => private val server_socket = new ServerSocket(_port, 50, Server.localhost) private val _sessions = Synchronized(Map.empty[UUID.T, Headless.Session]) def err_session(id: UUID.T): Nothing = error("No session " + Library.single_quote(id.toString)) def the_session(id: UUID.T): Headless.Session = _sessions.value.getOrElse(id, err_session(id)) def add_session(entry: (UUID.T, Headless.Session)) { _sessions.change(_ + entry) } def remove_session(id: UUID.T): Headless.Session = { _sessions.change_result(sessions => sessions.get(id) match { case Some(session) => (session, sessions - id) case None => err_session(id) }) } def shutdown() { server_socket.close val sessions = _sessions.change_result(sessions => (sessions, Map.empty)) for ((_, session) <- sessions) { try { val result = session.stop() - if (!result.ok) log("Session shutdown failed: return code " + result.rc) + if (!result.ok) log("Session shutdown failed: " + result.print_rc) } catch { case ERROR(msg) => log("Session shutdown failed: " + msg) } } } def port: Int = server_socket.getLocalPort val password: String = UUID.random_string() override def toString: String = Server.print(port, password) private def handle(connection: Server.Connection) { using(new Server.Context(server, connection))(context => { if (connection.read_password(password)) { connection.reply_ok( JSON.Object( "isabelle_id" -> Isabelle_System.isabelle_id(), "isabelle_version" -> Distribution.version)) var finished = false while (!finished) { connection.read_message() match { case None => finished = true case Some("") => context.notify("Command 'help' provides list of commands") case Some(msg) => val (name, argument) = Server.Argument.split(msg) name match { case Server.Command(cmd) => argument match { case Server.Argument(arg) => if (cmd.isDefinedAt((context, arg))) { Exn.capture { cmd((context, arg)) } match { case Exn.Res(task: Server.Task) => connection.reply_ok(JSON.Object(task.ident)) task.start case Exn.Res(res) => connection.reply_ok(res) case Exn.Exn(exn) => val err = Server.json_error(exn) if (err.isEmpty) throw exn else connection.reply_error(err) } } else { connection.reply_error_message( "Bad argument for command " + Library.single_quote(name), "argument" -> argument) } case _ => connection.reply_error_message( "Malformed argument for command " + Library.single_quote(name), "argument" -> argument) } case _ => connection.reply_error("Bad command " + Library.single_quote(name)) } } } } }) } private lazy val server_thread: Thread = Isabelle_Thread.fork(name = "server") { var finished = false while (!finished) { Exn.capture(server_socket.accept) match { case Exn.Res(socket) => Isabelle_Thread.fork(name = "server_connection") { using(Server.Connection(socket))(handle) } case Exn.Exn(_) => finished = true } } } def start { server_thread } def join { server_thread.join; shutdown() } } diff --git a/src/Pure/Tools/server_commands.scala b/src/Pure/Tools/server_commands.scala --- a/src/Pure/Tools/server_commands.scala +++ b/src/Pure/Tools/server_commands.scala @@ -1,273 +1,276 @@ /* Title: Pure/Tools/server_commands.scala Author: Makarius Miscellaneous Isabelle server commands. */ package isabelle object Server_Commands { def default_preferences: String = Options.read_prefs() object Cancel { sealed case class Args(task: UUID.T) def unapply(json: JSON.T): Option[Args] = for { task <- JSON.uuid(json, "task") } yield Args(task) } object Session_Build { sealed case class Args( session: String, preferences: String = default_preferences, options: List[String] = Nil, dirs: List[String] = Nil, include_sessions: List[String] = Nil, verbose: Boolean = false) def unapply(json: JSON.T): Option[Args] = for { session <- JSON.string(json, "session") preferences <- JSON.string_default(json, "preferences", default_preferences) options <- JSON.strings_default(json, "options") dirs <- JSON.strings_default(json, "dirs") include_sessions <- JSON.strings_default(json, "include_sessions") verbose <- JSON.bool_default(json, "verbose") } yield { Args(session, preferences = preferences, options = options, dirs = dirs, include_sessions = include_sessions, verbose = verbose) } def command(args: Args, progress: Progress = new Progress) : (JSON.Object.T, Build.Results, Options, Sessions.Base_Info) = { val options = Options.init(prefs = args.preferences, opts = args.options) val dirs = args.dirs.map(Path.explode) val base_info = Sessions.base_info(options, args.session, progress = progress, dirs = dirs, include_sessions = args.include_sessions) val base = base_info.check_base val results = Build.build(options, progress = progress, build_heap = true, dirs = dirs, infos = base_info.infos, verbose = args.verbose, sessions = List(args.session)) val sessions_order = base_info.sessions_structure.imports_topological_order.zipWithIndex. toMap.withDefaultValue(-1) val results_json = JSON.Object( "ok" -> results.ok, "return_code" -> results.rc, "sessions" -> results.sessions.toList.sortBy(sessions_order).map(session => { val result = results(session) JSON.Object( "session" -> session, "ok" -> result.ok, "return_code" -> result.rc, "timeout" -> result.timeout, "timing" -> result.timing.json) })) if (results.ok) (results_json, results, options, base_info) - else throw new Server.Error("Session build failed: return code " + results.rc, results_json) + else { + throw new Server.Error("Session build failed: " + Process_Result.print_rc(results.rc), + results_json) + } } } object Session_Start { sealed case class Args( build: Session_Build.Args, print_mode: List[String] = Nil) def unapply(json: JSON.T): Option[Args] = for { build <- Session_Build.unapply(json) print_mode <- JSON.strings_default(json, "print_mode") } yield Args(build = build, print_mode = print_mode) def command(args: Args, progress: Progress = new Progress, log: Logger = No_Logger) : (JSON.Object.T, (UUID.T, Headless.Session)) = { val (_, _, options, base_info) = try { Session_Build.command(args.build, progress = progress) } catch { case exn: Server.Error => error(exn.message) } val resources = Headless.Resources(options, base_info, log = log) val session = resources.start_session(print_mode = args.print_mode, progress = progress) val id = UUID.random() val res = JSON.Object( "session_id" -> id.toString, "tmp_dir" -> File.path(session.tmp_dir).implode) (res, id -> session) } } object Session_Stop { def unapply(json: JSON.T): Option[UUID.T] = JSON.uuid(json, "session_id") def command(session: Headless.Session): (JSON.Object.T, Process_Result) = { val result = session.stop() val result_json = JSON.Object("ok" -> result.ok, "return_code" -> result.rc) if (result.ok) (result_json, result) - else throw new Server.Error("Session shutdown failed: return code " + result.rc, result_json) + else throw new Server.Error("Session shutdown failed: " + result.print_rc, result_json) } } object Use_Theories { sealed case class Args( session_id: UUID.T, theories: List[String], master_dir: String = "", pretty_margin: Double = Pretty.default_margin, unicode_symbols: Boolean = false, export_pattern: String = "", check_delay: Option[Time] = None, check_limit: Option[Int] = None, watchdog_timeout: Option[Time] = None, nodes_status_delay: Option[Time] = None, commit_cleanup_delay: Option[Time] = None) def unapply(json: JSON.T): Option[Args] = for { session_id <- JSON.uuid(json, "session_id") theories <- JSON.strings(json, "theories") master_dir <- JSON.string_default(json, "master_dir") pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin) unicode_symbols <- JSON.bool_default(json, "unicode_symbols") export_pattern <- JSON.string_default(json, "export_pattern") check_delay = JSON.seconds(json, "check_delay") check_limit = JSON.int(json, "check_limit") watchdog_timeout = JSON.seconds(json, "watchdog_timeout") nodes_status_delay = JSON.seconds(json, "nodes_status_delay") commit_cleanup_delay = JSON.seconds(json, "commit_cleanup_delay") } yield { Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin, unicode_symbols = unicode_symbols, export_pattern = export_pattern, check_delay = check_delay, check_limit = check_limit, watchdog_timeout = watchdog_timeout, nodes_status_delay = nodes_status_delay, commit_cleanup_delay = commit_cleanup_delay) } def command(args: Args, session: Headless.Session, id: UUID.T = UUID.random(), progress: Progress = new Progress): (JSON.Object.T, Headless.Use_Theories_Result) = { val result = session.use_theories(args.theories, master_dir = args.master_dir, check_delay = args.check_delay.getOrElse(session.default_check_delay), check_limit = args.check_limit.getOrElse(session.default_check_limit), watchdog_timeout = args.watchdog_timeout.getOrElse(session.default_watchdog_timeout), nodes_status_delay = args.nodes_status_delay.getOrElse(session.default_nodes_status_delay), commit_cleanup_delay = args.commit_cleanup_delay.getOrElse(session.default_commit_cleanup_delay), id = id, progress = progress) def output_text(s: String): String = if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s) def output_message(tree: XML.Tree, pos: Position.T): JSON.Object.T = { val position = "pos" -> Position.JSON(pos) tree match { case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position case elem: XML.Elem => val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin)) val kind = Markup.messages.collectFirst({ case (a, b) if b == elem.name => if (Protocol.is_legacy(elem)) Markup.WARNING else a }) getOrElse "" Server.Reply.message(output_text(msg), kind = kind) + position } } val result_json = JSON.Object( "ok" -> result.ok, "errors" -> (for { (name, status) <- result.nodes if !status.ok (tree, pos) <- result.snapshot(name).messages if Protocol.is_error(tree) } yield output_message(tree, pos)), "nodes" -> (for ((name, status) <- result.nodes) yield { val snapshot = result.snapshot(name) name.json + ("status" -> status.json) + ("messages" -> (for { (tree, pos) <- snapshot.messages if Protocol.is_exported(tree) } yield output_message(tree, pos))) + ("exports" -> (if (args.export_pattern == "") Nil else { val matcher = Export.make_matcher(args.export_pattern) for { entry <- snapshot.exports if matcher(entry.theory_name, entry.name) } yield { val (base64, body) = entry.uncompressed().maybe_base64 JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body) } })) })) (result_json, result) } } object Purge_Theories { sealed case class Args( session_id: UUID.T, theories: List[String] = Nil, master_dir: String = "", all: Boolean = false) def unapply(json: JSON.T): Option[Args] = for { session_id <- JSON.uuid(json, "session_id") theories <- JSON.strings_default(json, "theories") master_dir <- JSON.string_default(json, "master_dir") all <- JSON.bool_default(json, "all") } yield { Args(session_id, theories = theories, master_dir = master_dir, all = all) } def command(args: Args, session: Headless.Session) : (JSON.Object.T, (List[Document.Node.Name], List[Document.Node.Name])) = { val (purged, retained) = session.purge_theories( theories = args.theories, master_dir = args.master_dir, all = args.all) val result_json = JSON.Object("purged" -> purged.map(_.json), "retained" -> retained.map(_.json)) (result_json, (purged, retained)) } } } diff --git a/src/Tools/VSCode/src/server.scala b/src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala +++ b/src/Tools/VSCode/src/server.scala @@ -1,561 +1,562 @@ /* Title: Tools/VSCode/src/server.scala Author: Makarius Server for VS Code Language Server Protocol 2.0/3.0, see also https://github.com/Microsoft/language-server-protocol https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md PIDE protocol extensions depend on system option "vscode_pide_extensions". */ package isabelle.vscode import isabelle._ import isabelle.vscode.{Protocol, Server} import java.io.{PrintStream, OutputStream, File => JFile} import scala.annotation.tailrec import scala.collection.mutable object Server { type Editor = isabelle.Editor[Unit] /* Isabelle tool wrapper */ private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC") val isabelle_tool = Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", args => { try { var logic_ancestor: Option[String] = None var log_file: Option[Path] = None var logic_requirements = false var dirs: List[Path] = Nil var include_sessions: List[String] = Nil var logic = default_logic var modes: List[String] = Nil var options = Options.init() var verbose = false val getopts = Getopts(""" Usage: isabelle vscode_server [OPTIONS] Options are: -A NAME ancestor session for option -R (default: parent) -L FILE logging on FILE -R NAME build image with requirements from other sessions -d DIR include session directory -i NAME include session in name-space of theories -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """) -m MODE add print mode for output -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose logging Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout. """, "A:" -> (arg => logic_ancestor = Some(arg)), "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))), "R:" -> (arg => { logic = arg; logic_requirements = true }), "d:" -> (arg => dirs = dirs ::: List(Path.explode(File.standard_path(arg)))), "i:" -> (arg => include_sessions = include_sessions ::: List(arg)), "l:" -> (arg => logic = arg), "m:" -> (arg => modes = arg :: modes), "o:" -> (arg => options = options + arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val log = Logger.make(log_file) val channel = new Channel(System.in, System.out, log, verbose) val server = new Server(channel, options, session_name = logic, session_dirs = dirs, include_sessions = include_sessions, session_ancestor = logic_ancestor, session_requirements = logic_requirements, modes = modes, log = log) // prevent spurious garbage on the main protocol channel val orig_out = System.out try { System.setOut(new PrintStream(new OutputStream { def write(n: Int) {} })) server.start() } finally { System.setOut(orig_out) } } catch { case exn: Throwable => val channel = new Channel(System.in, System.out, No_Logger) channel.error_message(Exn.message(exn)) throw(exn) } }) } class Server( val channel: Channel, options: Options, session_name: String = Server.default_logic, session_dirs: List[Path] = Nil, include_sessions: List[String] = Nil, session_ancestor: Option[String] = None, session_requirements: Boolean = false, modes: List[String] = Nil, log: Logger = No_Logger) { server => /* prover session */ private val session_ = Synchronized(None: Option[Session]) def session: Session = session_.value getOrElse error("Server inactive") def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources] def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] = for { model <- resources.get_model(new JFile(node_pos.name)) rendering = model.rendering() offset <- model.content.doc.offset(node_pos.pos) } yield (rendering, offset) private val dynamic_output = Dynamic_Output(server) /* input from client or file-system */ private val delay_input: Delay = Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger) { resources.flush_input(session, channel) } private val delay_load: Delay = Delay.last(options.seconds("vscode_load_delay"), channel.Error_Logger) { val (invoke_input, invoke_load) = resources.resolve_dependencies(session, editor, file_watcher) if (invoke_input) delay_input.invoke() if (invoke_load) delay_load.invoke } private val file_watcher = File_Watcher(sync_documents, options.seconds("vscode_load_delay")) private def close_document(file: JFile) { if (resources.close_model(file)) { file_watcher.register_parent(file) sync_documents(Set(file)) delay_input.invoke() delay_output.invoke() } } private def sync_documents(changed: Set[JFile]) { resources.sync_models(changed) delay_input.invoke() delay_output.invoke() } private def change_document(file: JFile, version: Long, changes: List[Protocol.TextDocumentChange]) { val norm_changes = new mutable.ListBuffer[Protocol.TextDocumentChange] @tailrec def norm(chs: List[Protocol.TextDocumentChange]) { if (chs.nonEmpty) { val (full_texts, rest1) = chs.span(_.range.isEmpty) val (edits, rest2) = rest1.span(_.range.nonEmpty) norm_changes ++= full_texts norm_changes ++= edits.sortBy(_.range.get.start)(Line.Position.Ordering).reverse norm(rest2) } } norm(changes) norm_changes.foreach(change => resources.change_model(session, editor, file, version, change.text, change.range)) delay_input.invoke() delay_output.invoke() } /* caret handling */ private val delay_caret_update: Delay = Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger) { session.caret_focus.post(Session.Caret_Focus) } private def update_caret(caret: Option[(JFile, Line.Position)]) { resources.update_caret(caret) delay_caret_update.invoke() delay_input.invoke() } /* preview */ private lazy val preview_panel = new Preview_Panel(resources) private lazy val delay_preview: Delay = Delay.last(options.seconds("vscode_output_delay"), channel.Error_Logger) { if (preview_panel.flush(channel)) delay_preview.invoke() } private def request_preview(file: JFile, column: Int) { preview_panel.request(file, column) delay_preview.invoke() } /* output to client */ private val delay_output: Delay = Delay.last(options.seconds("vscode_output_delay"), channel.Error_Logger) { if (resources.flush_output(channel)) delay_output.invoke() } def update_output(changed_nodes: Traversable[JFile]) { resources.update_output(changed_nodes) delay_output.invoke() } def update_output_visible() { resources.update_output_visible() delay_output.invoke() } private val prover_output = Session.Consumer[Session.Commands_Changed](getClass.getName) { case changed => update_output(changed.nodes.toList.map(resources.node_file(_))) } private val syslog_messages = Session.Consumer[Prover.Output](getClass.getName) { case output => channel.log_writeln(resources.output_xml(output.message)) } /* init and exit */ def init(id: Protocol.Id) { def reply_ok(msg: String) { channel.write(Protocol.Initialize.reply(id, "")) channel.writeln(msg) } def reply_error(msg: String) { channel.write(Protocol.Initialize.reply(id, msg)) channel.error_message(msg) } val try_session = try { val base_info = Sessions.base_info( options, session_name, dirs = session_dirs, include_sessions = include_sessions, session_ancestor = session_ancestor, session_requirements = session_requirements) base_info.check_base def build(no_build: Boolean = false): Build.Results = Build.build(options, build_heap = true, no_build = no_build, dirs = session_dirs, infos = base_info.infos, sessions = List(base_info.session)) if (!build(no_build = true).ok) { val start_msg = "Build started for Isabelle/" + base_info.session + " ..." val fail_msg = "Session build failed -- prover process remains inactive!" val progress = channel.progress(verbose = true) progress.echo(start_msg); channel.writeln(start_msg) if (!build().ok) { progress.echo(fail_msg); error(fail_msg) } } val resources = new VSCode_Resources(options, base_info, log) { override def commit(change: Session.Change): Unit = if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty) delay_load.invoke() } val session_options = options.bool("editor_output_state") = true val session = new Session(session_options, resources) Some((base_info, session)) } catch { case ERROR(msg) => reply_error(msg); None } for ((base_info, session) <- try_session) { session_.change(_ => Some(session)) session.commands_changed += prover_output session.syslog_messages += syslog_messages dynamic_output.init() try { Isabelle_Process(session, options, base_info.sessions_structure, Sessions.store(options), modes = modes, logic = base_info.session).await_startup reply_ok("Welcome to Isabelle/" + base_info.session + " (" + Distribution.version + ")") } catch { case ERROR(msg) => reply_error(msg) } } } def shutdown(id: Protocol.Id) { def reply(err: String): Unit = channel.write(Protocol.Shutdown.reply(id, err)) session_.change({ case Some(session) => session.commands_changed -= prover_output session.syslog_messages -= syslog_messages dynamic_output.exit() delay_load.revoke() file_watcher.shutdown() delay_input.revoke() delay_output.revoke() delay_caret_update.revoke() delay_preview.revoke() val result = session.stop() - if (result.ok) reply("") else reply("Prover shutdown failed: return code " + result.rc) + if (result.ok) reply("") + else reply("Prover shutdown failed: " + result.rc) None case None => reply("Prover inactive") None }) } def exit() { log("\n") sys.exit(if (session_.value.isDefined) 2 else 0) } /* completion */ def completion(id: Protocol.Id, node_pos: Line.Node_Position) { val result = (for ((rendering, offset) <- rendering_offset(node_pos)) yield rendering.completion(node_pos.pos, offset)) getOrElse Nil channel.write(Protocol.Completion.reply(id, result)) } /* spell-checker dictionary */ def update_dictionary(include: Boolean, permanent: Boolean) { for { spell_checker <- resources.spell_checker.get caret <- resources.get_caret() rendering = caret.model.rendering() range = rendering.before_caret_range(caret.offset) Text.Info(_, word) <- Spell_Checker.current_word(rendering, range) } { spell_checker.update(word, include, permanent) update_output_visible() } } def reset_dictionary() { for (spell_checker <- resources.spell_checker.get) { spell_checker.reset() update_output_visible() } } /* hover */ def hover(id: Protocol.Id, node_pos: Line.Node_Position) { val result = for { (rendering, offset) <- rendering_offset(node_pos) info <- rendering.tooltips(VSCode_Rendering.tooltip_elements, Text.Range(offset, offset + 1)) } yield { val range = rendering.model.content.doc.range(info.range) val contents = info.info.map(t => Protocol.MarkedString(resources.output_pretty_tooltip(List(t)))) (range, contents) } channel.write(Protocol.Hover.reply(id, result)) } /* goto definition */ def goto_definition(id: Protocol.Id, node_pos: Line.Node_Position) { val result = (for ((rendering, offset) <- rendering_offset(node_pos)) yield rendering.hyperlinks(Text.Range(offset, offset + 1))) getOrElse Nil channel.write(Protocol.GotoDefinition.reply(id, result)) } /* document highlights */ def document_highlights(id: Protocol.Id, node_pos: Line.Node_Position) { val result = (for ((rendering, offset) <- rendering_offset(node_pos)) yield { val model = rendering.model rendering.caret_focus_ranges(Text.Range(offset, offset + 1), model.content.text_range) .map(r => Protocol.DocumentHighlight.text(model.content.doc.range(r))) }) getOrElse Nil channel.write(Protocol.DocumentHighlights.reply(id, result)) } /* main loop */ def start() { log("Server started " + Date.now()) def handle(json: JSON.T) { try { json match { case Protocol.Initialize(id) => init(id) case Protocol.Initialized(()) => case Protocol.Shutdown(id) => shutdown(id) case Protocol.Exit(()) => exit() case Protocol.DidOpenTextDocument(file, _, version, text) => change_document(file, version, List(Protocol.TextDocumentChange(None, text))) delay_load.invoke() case Protocol.DidChangeTextDocument(file, version, changes) => change_document(file, version, changes) case Protocol.DidCloseTextDocument(file) => close_document(file) case Protocol.Completion(id, node_pos) => completion(id, node_pos) case Protocol.Include_Word(()) => update_dictionary(true, false) case Protocol.Include_Word_Permanently(()) => update_dictionary(true, true) case Protocol.Exclude_Word(()) => update_dictionary(false, false) case Protocol.Exclude_Word_Permanently(()) => update_dictionary(false, true) case Protocol.Reset_Words(()) => reset_dictionary() case Protocol.Hover(id, node_pos) => hover(id, node_pos) case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos) case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos) case Protocol.Caret_Update(caret) => update_caret(caret) case Protocol.State_Init(()) => State_Panel.init(server) case Protocol.State_Exit(id) => State_Panel.exit(id) case Protocol.State_Locate(id) => State_Panel.locate(id) case Protocol.State_Update(id) => State_Panel.update(id) case Protocol.State_Auto_Update(id, enabled) => State_Panel.auto_update(id, enabled) case Protocol.Preview_Request(file, column) => request_preview(file, column) case Protocol.Symbols_Request(()) => channel.write(Protocol.Symbols()) case _ => if (!Protocol.ResponseMessage.is_empty(json)) log("### IGNORED") } } catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) } } @tailrec def loop() { channel.read() match { case Some(json) => json match { case bulk: List[_] => bulk.foreach(handle) case _ => handle(json) } loop() case None => log("### TERMINATE") } } loop() } /* abstract editor operations */ object editor extends Server.Editor { /* session */ override def session: Session = server.session override def flush(): Unit = resources.flush_input(session, channel) override def invoke(): Unit = delay_input.invoke() /* current situation */ override def current_node(context: Unit): Option[Document.Node.Name] = resources.get_caret().map(_.model.node_name) override def current_node_snapshot(context: Unit): Option[Document.Snapshot] = resources.get_caret().map(_.model.snapshot()) override def node_snapshot(name: Document.Node.Name): Document.Snapshot = { resources.get_model(name) match { case Some(model) => model.snapshot() case None => session.snapshot(name) } } def current_command(snapshot: Document.Snapshot): Option[Command] = { resources.get_caret() match { case Some(caret) => snapshot.current_command(caret.node_name, caret.offset) case None => None } } override def current_command(context: Unit, snapshot: Document.Snapshot): Option[Command] = current_command(snapshot) /* overlays */ override def node_overlays(name: Document.Node.Name): Document.Node.Overlays = resources.node_overlays(name) override def insert_overlay(command: Command, fn: String, args: List[String]): Unit = resources.insert_overlay(command, fn, args) override def remove_overlay(command: Command, fn: String, args: List[String]): Unit = resources.remove_overlay(command, fn, args) /* hyperlinks */ override def hyperlink_command( focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0): Option[Hyperlink] = { if (snapshot.is_outdated) None else snapshot.find_command_position(id, offset).map(node_pos => new Hyperlink { def follow(unit: Unit) { channel.write(Protocol.Caret_Update(node_pos, focus)) } }) } /* dispatcher thread */ override def assert_dispatcher[A](body: => A): A = session.assert_dispatcher(body) override def require_dispatcher[A](body: => A): A = session.require_dispatcher(body) override def send_dispatcher(body: => Unit): Unit = session.send_dispatcher(body) override def send_wait_dispatcher(body: => Unit): Unit = session.send_wait_dispatcher(body) } } diff --git a/src/Tools/jEdit/src/session_build.scala b/src/Tools/jEdit/src/session_build.scala --- a/src/Tools/jEdit/src/session_build.scala +++ b/src/Tools/jEdit/src/session_build.scala @@ -1,182 +1,182 @@ /* Title: Tools/jEdit/src/session_build.scala Author: Makarius Session build management. */ package isabelle.jedit import isabelle._ import java.awt.event.{WindowEvent, WindowAdapter} import javax.swing.{WindowConstants, JDialog} import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel, BorderPanel, TextArea, Component, Label} import scala.swing.event.ButtonClicked import org.gjt.sp.jedit.View object Session_Build { def check_dialog(view: View) { val options = PIDE.options.value Isabelle_Thread.fork() { try { if (JEdit_Sessions.session_no_build || JEdit_Sessions.session_build(options, no_build = true) == 0) JEdit_Sessions.session_start(options) else GUI_Thread.later { new Dialog(view) } } catch { case exn: Throwable => GUI.dialog(view, "Isabelle", GUI.scrollable_text(Exn.message(exn))) } } } private class Dialog(view: View) extends JDialog(view) { val options: Options = PIDE.options.value /* text */ private val text = new TextArea { editable = false columns = 65 rows = 24 } text.font = GUI.copy_font((new Label).font) private val scroll_text = new ScrollPane(text) /* progress */ private val progress = new Progress { override def echo(txt: String): Unit = GUI_Thread.later { text.append(txt + "\n") val vertical = scroll_text.peer.getVerticalScrollBar vertical.setValue(vertical.getMaximum) } override def theory(theory: Progress.Theory): Unit = echo(theory.message) } /* layout panel with dynamic actions */ private val action_panel = new FlowPanel(FlowPanel.Alignment.Center)() private val layout_panel = new BorderPanel layout_panel.layout(scroll_text) = BorderPanel.Position.Center layout_panel.layout(action_panel) = BorderPanel.Position.South setContentPane(layout_panel.peer) private def set_actions(cs: Component*) { action_panel.contents.clear action_panel.contents ++= cs layout_panel.revalidate layout_panel.repaint } /* return code and exit */ private var _return_code: Option[Int] = None private def return_code(rc: Int): Unit = GUI_Thread.later { _return_code = Some(rc) delay_exit.invoke } private val delay_exit = Delay.first(Time.seconds(1.0), gui = true) { if (can_auto_close) conclude() else { val button = new Button("Close") { reactions += { case ButtonClicked(_) => conclude() } } set_actions(button) button.peer.getRootPane.setDefaultButton(button.peer) } } private def conclude() { setVisible(false) dispose() } /* close */ setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE) addWindowListener(new WindowAdapter { override def windowClosing(e: WindowEvent) { if (_return_code.isDefined) conclude() else stopping() } }) private def stopping() { progress.stop set_actions(new Label("Stopping ...")) } private val stop_button = new Button("Stop") { reactions += { case ButtonClicked(_) => stopping() } } private var do_auto_close = true private def can_auto_close: Boolean = do_auto_close && _return_code == Some(0) private val auto_close = new CheckBox("Auto close") { reactions += { case ButtonClicked(_) => do_auto_close = this.selected if (can_auto_close) conclude() } } auto_close.selected = do_auto_close auto_close.tooltip = "Automatically close dialog when finished" set_actions(stop_button, auto_close) /* main */ setTitle("Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + " / " + "jdk-" + Platform.jvm_version + "_" + Platform.jvm_platform + ")") pack() setLocationRelativeTo(view) setVisible(true) Isabelle_Thread.fork(name = "session_build") { progress.echo("Build started for Isabelle/" + PIDE.resources.session_name + " ...") val (out, rc) = try { ("", JEdit_Sessions.session_build(options, progress = progress)) } catch { case exn: Throwable => (Output.error_message_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2)) } - progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n")) + progress.echo(out + (if (rc == 0) "OK" else Process_Result.print_return_code(rc)) + "\n") if (rc == 0) JEdit_Sessions.session_start(options) else progress.echo("Session build failed -- prover process remains inactive!") return_code(rc) } } }