diff --git a/src/HOL/Tools/Mirabelle/mirabelle.scala b/src/HOL/Tools/Mirabelle/mirabelle.scala --- a/src/HOL/Tools/Mirabelle/mirabelle.scala +++ b/src/HOL/Tools/Mirabelle/mirabelle.scala @@ -1,228 +1,226 @@ /* Title: HOL/Tools/Mirabelle/mirabelle.scala Author: Makarius Isabelle/Scala front-end for Mirabelle. */ package isabelle.mirabelle import isabelle._ object Mirabelle { /* actions and options */ def action_names(): List[String] = { val Pattern = """Mirabelle action: "(\w+)".*""".r (for { file <- File.find_files(Path.explode("~~/src/HOL/Tools/Mirabelle").file, pred = file => File.is_ML(file.getName)) line <- split_lines(File.read(file)) name <- line match { case Pattern(a) => Some(a) case _ => None } } yield name).sorted } def sledgehammer_options(): List[String] = { val Pattern = """val .*K *= *"(.*)" *\(\*(.*)\*\)""".r split_lines(File.read(Path.explode("~~/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML"))). flatMap(line => line match { case Pattern(a, b) => Some (a + b) case _ => None }) } /* main mirabelle */ def mirabelle( options: Options, actions: List[String], output_dir: Path, theories: List[String] = Nil, selection: Sessions.Selection = Sessions.Selection.empty, progress: Progress = new Progress, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, numa_shuffling: Boolean = false, max_jobs: Int = 1, ): Build.Results = { require(!selection.requirements) Isabelle_System.make_directory(output_dir) progress.echo("Building required heaps ...") val build_results0 = Build.build(options, build_heap = true, selection = selection.copy(requirements = true), progress = progress, dirs = dirs, select_dirs = select_dirs, numa_shuffling = numa_shuffling, max_jobs = max_jobs) if (build_results0.ok) { val build_options = options + "timeout_build=false" + ("mirabelle_actions=" + actions.mkString(";")) + ("mirabelle_theories=" + theories.mkString(",")) + ("mirabelle_output_dir=" + output_dir.implode) progress.echo("Running Mirabelle on " + Isabelle_System.identification() + "...") def session_setup(session_name: String, session: Session): Unit = { session.all_messages += Session.Consumer[Prover.Message]("mirabelle_export") { case msg: Prover.Protocol_Output => msg.properties match { case Protocol.Export(args) if args.name.startsWith("mirabelle/") => progress.echo( "Mirabelle export " + quote(args.compound_name) + " (in " + session_name + ")", verbose = true) val yxml = YXML.parse_body(UTF8.decode_permissive(msg.chunk), cache = build_results0.cache) val lines = Pretty.string_of(yxml).trim() val prefix = Export.explode_name(args.name) match { case List("mirabelle", action, "initialize") => action + " initialize " case List("mirabelle", action, "finalize") => action + " finalize " case List("mirabelle", action, "goal", goal_name, line, offset, cpu_ms) => action + " goal." + String.format("%-9s", goal_name) + " " + String.format("%5sms", cpu_ms) + " " + args.theory_name + " " + line + ":" + offset + " " case _ => "" } val body = (if (lines == "") prefix else Library.prefix_lines(prefix, lines)) + "\n" val log_file = output_dir + Path.basic("mirabelle.log") File.append(log_file, body) case _ => } case _ => } } Build.build(build_options, clean_build = true, selection = selection, progress = progress, dirs = dirs, select_dirs = select_dirs, numa_shuffling = numa_shuffling, max_jobs = max_jobs, session_setup = session_setup) } else build_results0 } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("mirabelle", "testing tool for automated proof tools", Scala_Project.here, { args => - val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")) - - var options = Options.init(opts = build_options) + var options = Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS) val mirabelle_dry_run = options.check_name("mirabelle_dry_run") val mirabelle_max_calls = options.check_name("mirabelle_max_calls") val mirabelle_randomize = options.check_name("mirabelle_randomize") val mirabelle_stride = options.check_name("mirabelle_stride") val mirabelle_timeout = options.check_name("mirabelle_timeout") val mirabelle_output_dir = options.check_name("mirabelle_output_dir") var actions: List[String] = Nil var base_sessions: List[String] = Nil var select_dirs: List[Path] = Nil var numa_shuffling = false var output_dir = Path.explode(mirabelle_output_dir.default_value) var theories: List[String] = Nil var exclude_session_groups: List[String] = Nil var all_sessions = false var dirs: List[Path] = Nil var session_groups: List[String] = Nil var max_jobs = 1 var verbose = false var exclude_sessions: List[String] = Nil val getopts = Getopts(""" Usage: isabelle mirabelle [OPTIONS] [SESSIONS ...] Options are: -A ACTION add to list of actions -B NAME include session NAME and all descendants -D DIR include session directory and select its sessions -N cyclic shuffling of NUMA CPU nodes (performance tuning) -O DIR """ + mirabelle_output_dir.description + " (default: " + mirabelle_output_dir.default_value + """) -T THEORY theory restriction: NAME or NAME[FIRST_LINE:LAST_LINE] -X NAME exclude sessions from group NAME and all descendants -a select all sessions -d DIR include session directory -g NAME select session group NAME -j INT maximum number of parallel jobs (default 1) -m INT """ + mirabelle_max_calls.description + " (default " + mirabelle_max_calls.default_value + """) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -r INT """ + mirabelle_randomize.description + " (default " + mirabelle_randomize.default_value + """) -s INT """ + mirabelle_stride.description + " (default " + mirabelle_stride.default_value + """) -t SECONDS """ + mirabelle_timeout.description + " (default " + mirabelle_timeout.default_value + """) -v verbose -x NAME exclude session NAME and all descendants -y """ + mirabelle_dry_run.description + " (default " + mirabelle_dry_run.default_value + """) Apply the given ACTIONs at all theories and proof steps of the specified sessions. The absence of theory restrictions (option -T) means to check all theories fully. Otherwise only the named theories are checked. Each ACTION is either of the form NAME or NAME [OPTION, ...] following Isabelle/Isar outer syntax. Available actions are:""" + action_names().mkString("\n ", "\n ", "") + """ For the ACTION "sledgehammer", the usual sledgehammer as well as the following mirabelle-specific OPTIONs are available:""" + sledgehammer_options().mkString("\n ", "\n ", "\n"), "A:" -> (arg => actions = actions ::: List(arg)), "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), "N" -> (_ => numa_shuffling = true), "O:" -> (arg => output_dir = Path.explode(arg)), "T:" -> (arg => theories = theories ::: List(arg)), "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), "a" -> (_ => all_sessions = true), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "g:" -> (arg => session_groups = session_groups ::: List(arg)), "j:" -> (arg => max_jobs = Value.Int.parse(arg)), "m:" -> (arg => options = options + ("mirabelle_max_calls=" + arg)), "o:" -> (arg => options = options + arg), "r:" -> (arg => options = options + ("mirabelle_randomize=" + arg)), "s:" -> (arg => options = options + ("mirabelle_stride=" + arg)), "t:" -> (arg => options = options + ("mirabelle_timeout=" + arg)), "v" -> (_ => verbose = true), "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)), "y" -> (arg => options = options + ("mirabelle_dry_run=true"))) val sessions = getopts(args) if (actions.isEmpty) getopts.usage() val progress = new Console_Progress(verbose = verbose) val start_date = Date.now() progress.echo("Started at " + Build_Log.print_date(start_date), verbose = true) val results = progress.interrupt_handler { mirabelle(options, actions, output_dir.absolute, theories = theories, selection = Sessions.Selection( all_sessions = all_sessions, base_sessions = base_sessions, exclude_session_groups = exclude_session_groups, exclude_sessions = exclude_sessions, session_groups = session_groups, sessions = sessions), progress = progress, dirs = dirs, select_dirs = select_dirs, numa_shuffling = Host.numa_check(progress, numa_shuffling), max_jobs = max_jobs) } val end_date = Date.now() val elapsed_time = end_date.time - start_date.time progress.echo("\nFinished at " + Build_Log.print_date(end_date), verbose = true) val total_timing = results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _). copy(elapsed = elapsed_time) progress.echo(total_timing.message_resources) sys.exit(results.rc) }) } diff --git a/src/Pure/System/options.scala b/src/Pure/System/options.scala --- a/src/Pure/System/options.scala +++ b/src/Pure/System/options.scala @@ -1,502 +1,502 @@ /* Title: Pure/System/options.scala Author: Makarius System options with external string representation. */ package isabelle object Options { val empty: Options = new Options() object Spec { def make(s: String): Spec = s match { case Properties.Eq(a, b) => Spec(a, Some(b)) case _ => Spec(s) } + + def ISABELLE_BUILD_OPTIONS: List[Spec] = + Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")).map(make) } sealed case class Spec(name: String, value: Option[String] = None, permissive: Boolean = false) { override def toString: String = name + if_proper(value, "=" + value.get) } sealed case class Change(name: String, value: String, unknown: Boolean) { def spec: Spec = Spec(name, Some(value)) def print_prefs: String = name + " = " + Outer_Syntax.quote_string(value) + if_proper(unknown, " (* unknown *)") + "\n" } /* typed access */ abstract class Access[A](val options: Options) { def apply(name: String): A def update(name: String, x: A): Options def change(name: String, f: A => A): Options = update(name, f(apply(name))) } class Access_Variable[A]( val options: Options_Variable, val pure_access: Options => Access[A] ) { def apply(name: String): A = pure_access(options.value)(name) def update(name: String, x: A): Unit = options.change(options => pure_access(options).update(name, x)) def change(name: String, f: A => A): Unit = update(name, f(apply(name))) } /* representation */ sealed abstract class Type { def print: String = Word.lowercase(toString) } case object Bool extends Type case object Int extends Type case object Real extends Type case object String extends Type case object Unknown extends Type val TAG_CONTENT = "content" // formal theory content val TAG_DOCUMENT = "document" // document preparation val TAG_BUILD = "build" // relavant for "isabelle build" val TAG_UPDATE = "update" // relevant for "isabelle update" val TAG_CONNECTION = "connection" // private information about connections (password etc.) val TAG_COLOR_DIALOG = "color_dialog" // special color selection dialog case class Entry( public: Boolean, pos: Position.T, name: String, typ: Type, value: String, default_value: String, standard_value: Option[String], tags: List[String], description: String, section: String ) { private def print_value(x: String): String = if (typ == Options.String) quote(x) else x private def print_standard: String = standard_value match { case None => "" case Some(s) if s == default_value => " (standard)" case Some(s) => " (standard " + print_value(s) + ")" } private def print(default: Boolean): String = { val x = if (default) default_value else value "option " + name + " : " + typ.print + " = " + print_value(x) + print_standard + if_proper(description, "\n -- " + quote(description)) } def print: String = print(false) def print_default: String = print(true) def title(strip: String = ""): String = { val words = Word.explode('_', name) val words1 = words match { case word :: rest if word == strip => rest case _ => words } Word.implode(words1.map(Word.perhaps_capitalize)) } def title_jedit: String = title("jedit") def unknown: Boolean = typ == Unknown def for_tag(tag: String): Boolean = tags.contains(tag) def for_content: Boolean = for_tag(TAG_CONTENT) def for_document: Boolean = for_tag(TAG_DOCUMENT) def for_color_dialog: Boolean = for_tag(TAG_COLOR_DIALOG) def session_content: Boolean = for_content || for_document } /* parsing */ private val SECTION = "section" private val PUBLIC = "public" private val OPTION = "option" private val STANDARD = "standard" private val FOR = "for" private val OPTIONS = Path.explode("etc/options") private val PREFS = Path.explode("$ISABELLE_HOME_USER/etc/preferences") val options_syntax: Outer_Syntax = Outer_Syntax.empty + ":" + "=" + "--" + "(" + ")" + Symbol.comment + Symbol.comment_decoded + (SECTION, Keyword.DOCUMENT_HEADING) + (PUBLIC, Keyword.BEFORE_COMMAND) + (OPTION, Keyword.THY_DECL) + STANDARD + FOR val prefs_syntax: Outer_Syntax = Outer_Syntax.empty + "=" trait Parsers extends Parse.Parsers { val option_name: Parser[String] = atom("option name", _.is_name) val option_type: Parser[String] = atom("option type", _.is_name) val option_value: Parser[String] = opt(token("-", tok => tok.is_sym_ident && tok.content == "-")) ~ atom("nat", _.is_nat) ^^ { case s ~ n => if (s.isDefined) "-" + n else n } | atom("option value", tok => tok.is_name || tok.is_float) val option_standard: Parser[Option[String]] = $$$("(") ~! $$$(STANDARD) ~ opt(option_value) ~ $$$(")") ^^ { case _ ~ _ ~ a ~ _ => a } val option_tag: Parser[String] = atom("option tag", _.is_name) val option_tags: Parser[List[String]] = $$$(FOR) ~! rep(option_tag) ^^ { case _ ~ x => x } | success(Nil) } private object Parsers extends Parsers { def comment_marker: Parser[String] = $$$("--") | $$$(Symbol.comment) | $$$(Symbol.comment_decoded) val option_entry: Parser[Options => Options] = { command(SECTION) ~! text ^^ { case _ ~ a => (options: Options) => options.set_section(a) } | opt($$$(PUBLIC)) ~ command(OPTION) ~! (position(option_name) ~ $$$(":") ~ option_type ~ $$$("=") ~ option_value ~ opt(option_standard) ~ option_tags ~ (comment_marker ~! text ^^ { case _ ~ x => x } | success(""))) ^^ { case a ~ _ ~ ((b, pos) ~ _ ~ c ~ _ ~ d ~ e ~ f ~ g) => (options: Options) => options.declare(a.isDefined, pos, b, c, d, e, f, g) } } val prefs_entry: Parser[Options => Options] = { option_name ~ ($$$("=") ~! option_value) ^^ { case a ~ (_ ~ b) => (options: Options) => options + Options.Spec(a, Some(b), permissive = true) } } def parse_file( options: Options, file_name: String, content: String, syntax: Outer_Syntax = options_syntax, parser: Parser[Options => Options] = option_entry ): Options = { val toks = Token.explode(syntax.keywords, content) val ops = parse_all(rep(parser), Token.reader(toks, Token.Pos.file(file_name))) match { case Success(result, _) => result case bad => error(bad.toString) } try { ops.foldLeft(options.set_section("")) { case (opts, op) => op(opts) } } catch { case ERROR(msg) => error(msg + Position.here(Position.File(file_name))) } } def parse_prefs(options: Options, content: String): Options = parse_file(options, PREFS.file_name, content, syntax = prefs_syntax, parser = prefs_entry) } def read_prefs(file: Path = PREFS): String = if (file.is_file) File.read(file) else "" - def init(prefs: String = read_prefs(file = PREFS), opts: List[String] = Nil): Options = { + def init(prefs: String = read_prefs(file = PREFS), specs: List[Spec] = Nil): Options = { var options = empty for { dir <- Components.directories() file = dir + OPTIONS if file.is_file } { options = Parsers.parse_file(options, file.implode, File.read(file)) } - opts.foldLeft(Parsers.parse_prefs(options, prefs))(_ + _) + Parsers.parse_prefs(options, prefs) ++ specs } def init0(): Options = init(prefs = "") /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("options", "print Isabelle system options", Scala_Project.here, { args => var build_options = false var get_option = "" var list_options = false var list_tags = List.empty[String] var export_file = "" val getopts = Getopts(""" Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...] Options are: -b include $ISABELLE_BUILD_OPTIONS -g OPTION get value of OPTION -l list options -t TAGS restrict list to given tags (comma-separated) -x FILE export options to FILE in YXML format Report Isabelle system options, augmented by MORE_OPTIONS given as arguments NAME=VAL or NAME. """, "b" -> (_ => build_options = true), "g:" -> (arg => get_option = arg), "l" -> (_ => list_options = true), "t:" -> (arg => list_tags = space_explode(',', arg)), "x:" -> (arg => export_file = arg)) val more_options = getopts(args) if (get_option == "" && !list_options && export_file == "") getopts.usage() val options = { val options0 = Options.init() val options1 = - if (build_options) { - Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")).foldLeft(options0)(_ + _) - } - else options0 + if (build_options) options0 ++ Options.Spec.ISABELLE_BUILD_OPTIONS else options0 more_options.foldLeft(options1)(_ + _) } if (get_option != "") { Output.writeln(options.check_name(get_option).value, stdout = true) } if (export_file != "") { File.write(Path.explode(export_file), YXML.string_of_body(options.encode)) } if (get_option == "" && export_file == "") { val filter: Options.Entry => Boolean = if (list_tags.isEmpty) (_ => true) else opt => list_tags.exists(opt.for_tag) Output.writeln(options.print(filter = filter), stdout = true) } }) } final class Options private( options: Map[String, Options.Entry] = Map.empty, val section: String = "" ) { def iterator: Iterator[Options.Entry] = options.valuesIterator override def toString: String = iterator.mkString("Options(", ",", ")") private def print_entry(opt: Options.Entry): String = if_proper(opt.public, "public ") + opt.print def print(filter: Options.Entry => Boolean = _ => true): String = cat_lines(iterator.filter(filter).toList.sortBy(_.name).map(print_entry)) def description(name: String): String = check_name(name).description /* check */ def get(name: String): Option[Options.Entry] = options.get(name) def check_name(name: String): Options.Entry = get(name) match { case Some(opt) if !opt.unknown => opt case _ => error("Unknown option " + quote(name)) } private def check_type(name: String, typ: Options.Type): Options.Entry = { val opt = check_name(name) if (opt.typ == typ) opt else error("Ill-typed option " + quote(name) + " : " + opt.typ.print + " vs. " + typ.print) } /* basic operations */ private def put(name: String, typ: Options.Type, value: String): Options = { val opt = check_type(name, typ) new Options(options + (name -> opt.copy(value = value)), section) } private def get[A](name: String, typ: Options.Type, parse: String => Option[A]): A = { val opt = check_type(name, typ) parse(opt.value) match { case Some(x) => x case None => error("Malformed value for option " + quote(name) + " : " + typ.print + " =\n" + quote(opt.value)) } } /* internal lookup and update */ val bool: Options.Access[Boolean] = new Options.Access[Boolean](this) { def apply(name: String): Boolean = get(name, Options.Bool, Value.Boolean.unapply) def update(name: String, x: Boolean): Options = put(name, Options.Bool, Value.Boolean(x)) } val int: Options.Access[Int] = new Options.Access[Int](this) { def apply(name: String): Int = get(name, Options.Int, Value.Int.unapply) def update(name: String, x: Int): Options = put(name, Options.Int, Value.Int(x)) } val real: Options.Access[Double] = new Options.Access[Double](this) { def apply(name: String): Double = get(name, Options.Real, Value.Double.unapply) def update(name: String, x: Double): Options = put(name, Options.Real, Value.Double(x)) } val string: Options.Access[String] = new Options.Access[String](this) { def apply(name: String): String = get(name, Options.String, Some(_)) def update(name: String, x: String): Options = put(name, Options.String, x) } def seconds(name: String): Time = Time.seconds(real(name)) /* external updates */ private def check_value(name: String): Options = { val opt = check_name(name) opt.typ match { case Options.Bool => bool(name); this case Options.Int => int(name); this case Options.Real => real(name); this case Options.String => string(name); this case Options.Unknown => this } } def declare( public: Boolean, pos: Position.T, name: String, typ_name: String, value: String, standard: Option[Option[String]], tags: List[String], description: String ): Options = { get(name) match { case Some(other) => error("Duplicate declaration of option " + quote(name) + Position.here(pos) + Position.here(other.pos)) case None => val typ = typ_name match { case "bool" => Options.Bool case "int" => Options.Int case "real" => Options.Real case "string" => Options.String case _ => error("Unknown type for option " + quote(name) + " : " + quote(typ_name) + Position.here(pos)) } val standard_value = standard match { case None => None case Some(_) if typ == Options.Bool => error("Illegal standard value for option " + quote(name) + " : " + typ_name + Position.here) case Some(s) => Some(s.getOrElse(value)) } val opt = Options.Entry( public, pos, name, typ, value, value, standard_value, tags, description, section) (new Options(options + (name -> opt), section)).check_value(name) } } def + (spec: Options.Spec): Options = { val name = spec.name if (spec.permissive && !options.isDefinedAt(name)) { val value = spec.value.getOrElse("") val opt = Options.Entry(false, Position.none, name, Options.Unknown, value, value, None, Nil, "", "") new Options(options + (name -> opt), section) } else { val opt = check_name(name) def put(value: String): Options = (new Options(options + (name -> opt.copy(value = value)), section)).check_value(name) spec.value orElse opt.standard_value match { case Some(value) => put(value) case None if opt.typ == Options.Bool => put("true") case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print) } } } def + (s: String): Options = this + Options.Spec.make(s) def ++ (specs: List[Options.Spec]): Options = specs.foldLeft(this)(_ + _) /* sections */ def set_section(new_section: String): Options = new Options(options, new_section) def sections: List[(String, List[Options.Entry])] = options.groupBy(_._2.section).toList.map({ case (a, opts) => (a, opts.toList.map(_._2)) }) /* encode */ def encode: XML.Body = { val opts = for ((_, opt) <- options.toList; if !opt.unknown) yield (opt.pos, (opt.name, (opt.typ.print, opt.value))) import XML.Encode.{string => string_, _} list(pair(properties, pair(string_, pair(string_, string_))))(opts) } /* changed options */ def changed( defaults: Options = Options.init0(), filter: Options.Entry => Boolean = _ => true ): List[Options.Change] = { List.from( for { (name, opt2) <- options.iterator opt1 = defaults.get(name) if (opt1.isEmpty || opt1.get.value != opt2.value) && filter(opt2) } yield Options.Change(name, opt2.value, opt1.isEmpty)) } /* preferences */ def make_prefs( defaults: Options = Options.init0(), filter: Options.Entry => Boolean = _ => true ): String = changed(defaults = defaults, filter = filter).map(_.print_prefs).mkString def save_prefs(file: Path = Options.PREFS, defaults: Options = Options.init0()): Unit = { val prefs = make_prefs(defaults = defaults) Isabelle_System.make_directory(file.dir) File.write_backup(file, "(* generated by Isabelle " + Date.now() + " *)\n\n" + prefs) } } class Options_Variable(init_options: Options) { private var _options = init_options def value: Options = synchronized { _options } def change(f: Options => Options): Unit = synchronized { _options = f(_options) } def += (name: String, x: String): Unit = change(options => options + Options.Spec(name, Some(x))) val bool: Options.Access_Variable[Boolean] = new Options.Access_Variable[Boolean](this, _.bool) val int: Options.Access_Variable[Int] = new Options.Access_Variable[Int](this, _.int) val real: Options.Access_Variable[Double] = new Options.Access_Variable[Double](this, _.real) val string: Options.Access_Variable[String] = new Options.Access_Variable[String](this, _.string) def seconds(name: String): Time = value.seconds(name) } diff --git a/src/Pure/Tools/build.scala b/src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala +++ b/src/Pure/Tools/build.scala @@ -1,682 +1,678 @@ /* Title: Pure/Tools/build.scala Author: Makarius Options: :folding=explicit: Command-line tools to build and manage Isabelle sessions. */ package isabelle import scala.collection.mutable import scala.util.matching.Regex object Build { /** "isabelle build" **/ /* results */ object Results { def apply(context: Build_Process.Context, results: Map[String, Process_Result]): Results = new Results(context.store, context.build_deps, results) } class Results private( val store: Sessions.Store, val deps: Sessions.Deps, results: Map[String, Process_Result] ) { def cache: Term.Cache = store.cache def sessions_ok: List[String] = (for { name <- deps.sessions_structure.build_topological_order.iterator result <- results.get(name) if result.ok } yield name).toList def info(name: String): Sessions.Info = deps.sessions_structure(name) def sessions: Set[String] = results.keySet def cancelled(name: String): Boolean = !results(name).defined def apply(name: String): Process_Result = results(name).strict val rc: Int = results.valuesIterator.map(_.strict.rc).foldLeft(Process_Result.RC.ok)(_ max _) def ok: Boolean = rc == Process_Result.RC.ok def unfinished: List[String] = sessions.iterator.filterNot(apply(_).ok).toList.sorted override def toString: String = rc.toString } /* engine */ class Engine(val name: String) extends Isabelle_System.Service { override def toString: String = name def init(build_context: Build_Process.Context, build_progress: Progress): Build_Process = new Build_Process(build_context, build_progress) } class Default_Engine extends Engine("") { override def toString: String = "" } lazy val engines: List[Engine] = Isabelle_System.make_services(classOf[Engine]) def get_engine(name: String): Engine = engines.find(_.name == name).getOrElse(error("Bad build engine " + quote(name))) /* options */ def hostname(options: Options): String = Isabelle_System.hostname(options.string("build_hostname")) def build_init(options: Options, cache: Term.Cache = Term.Cache.make()): Sessions.Store = { val build_options = options + "completion_limit=0" + "editor_tracing_messages=0" + ("pide_reports=" + options.bool("build_pide_reports")) val store = Sessions.store(build_options, cache = cache) Isabelle_Fonts.init() store } /* build */ def build( options: Options, selection: Sessions.Selection = Sessions.Selection.empty, browser_info: Browser_Info.Config = Browser_Info.Config.none, progress: Progress = new Progress, check_unknown_files: Boolean = false, build_heap: Boolean = false, clean_build: Boolean = false, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, infos: List[Sessions.Info] = Nil, numa_shuffling: Boolean = false, max_jobs: Int = 1, list_files: Boolean = false, check_keywords: Set[String] = Set.empty, fresh_build: Boolean = false, no_build: Boolean = false, soft_build: Boolean = false, export_files: Boolean = false, augment_options: String => List[Options.Spec] = _ => Nil, session_setup: (String, Session) => Unit = (_, _) => (), cache: Term.Cache = Term.Cache.make() ): Results = { val store = build_init(options, cache = cache) val build_options = store.options /* session selection and dependencies */ val full_sessions = Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos, augment_options = augment_options) val full_sessions_selection = full_sessions.imports_selection(selection) val build_deps = { val deps0 = Sessions.deps(full_sessions.selection(selection), progress = progress, inlined_files = true, list_files = list_files, check_keywords = check_keywords).check_errors if (soft_build && !fresh_build) { val outdated = deps0.sessions_structure.build_topological_order.flatMap(name => store.try_open_database(name) match { case Some(db) => using(db)(store.read_build(_, name)) match { case Some(build) if build.ok && build.sources == deps0.sources_shasum(name) => None case _ => Some(name) } case None => Some(name) }) Sessions.deps(full_sessions.selection(Sessions.Selection(sessions = outdated)), progress = progress, inlined_files = true).check_errors } else deps0 } /* check unknown files */ if (check_unknown_files) { val source_files = (for { (_, base) <- build_deps.session_bases.iterator (path, _) <- base.session_sources.iterator } yield path).toList Mercurial.check_files(source_files)._2 match { case Nil => case unknown_files => progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" + unknown_files.map(File.standard_path).sorted.mkString("\n ", "\n ", "")) } } /* build process and results */ val build_context = Build_Process.Context(store, build_deps, progress = progress, hostname = hostname(build_options), build_heap = build_heap, numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build, no_build = no_build, session_setup = session_setup, master = true) store.prepare_output() build_context.prepare_database() if (clean_build) { for (name <- full_sessions.imports_descendants(full_sessions_selection)) { val (relevant, ok) = store.clean_output(name) if (relevant) { if (ok) progress.echo("Cleaned " + name) else progress.echo(name + " FAILED to clean") } } } val results = Isabelle_Thread.uninterruptible { val engine = get_engine(build_options.string("build_engine")) using(engine.init(build_context, progress)) { build_process => val res = build_process.run() Results(build_context, res) } } if (export_files) { for (name <- full_sessions_selection.iterator if results(name).ok) { val info = results.info(name) if (info.export_files.nonEmpty) { progress.echo("Exporting " + info.name + " ...") for ((dir, prune, pats) <- info.export_files) { Export.export_files(store, name, info.dir + dir, progress = if (progress.verbose) progress else new Progress, export_prune = prune, export_patterns = pats) } } } } val presentation_sessions = results.sessions_ok.filter(name => browser_info.enabled(results.info(name))) if (presentation_sessions.nonEmpty && !progress.stopped) { Browser_Info.build(browser_info, results.store, results.deps, presentation_sessions, progress = progress) } if (!results.ok && (progress.verbose || !no_build)) { progress.echo("Unfinished session(s): " + commas(results.unfinished)) } results } /* build logic image */ def build_logic(options: Options, logic: String, progress: Progress = new Progress, build_heap: Boolean = false, dirs: List[Path] = Nil, fresh: Boolean = false, strict: Boolean = false ): Int = { val selection = Sessions.Selection.session(logic) val rc = if (!fresh && build(options, selection = selection, build_heap = build_heap, no_build = true, dirs = dirs).ok) Process_Result.RC.ok else { progress.echo("Build started for Isabelle/" + logic + " ...") build(options, selection = selection, progress = progress, build_heap = build_heap, fresh_build = fresh, dirs = dirs).rc } if (strict && rc != Process_Result.RC.ok) error("Failed to build Isabelle/" + logic) else rc } /* command-line wrapper */ val isabelle_tool1 = Isabelle_Tool("build", "build and manage Isabelle sessions", Scala_Project.here, { args => - val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")) - var base_sessions: List[String] = Nil var select_dirs: List[Path] = Nil var numa_shuffling = false var browser_info = Browser_Info.Config.none var requirements = false var soft_build = false var exclude_session_groups: List[String] = Nil var all_sessions = false var build_heap = false var clean_build = false var dirs: List[Path] = Nil var export_files = false var fresh_build = false var session_groups: List[String] = Nil var max_jobs = 1 var check_keywords: Set[String] = Set.empty var list_files = false var no_build = false - var options = Options.init(opts = build_options) + var options = Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS) var verbose = false var exclude_sessions: List[String] = Nil val getopts = Getopts(""" Usage: isabelle build [OPTIONS] [SESSIONS ...] Options are: -B NAME include session NAME and all descendants -D DIR include session directory and select its sessions -N cyclic shuffling of NUMA CPU nodes (performance tuning) -P DIR enable HTML/PDF presentation in directory (":" for default) -R refer to requirements of selected sessions -S soft build: only observe changes of sources, not heap images -X NAME exclude sessions from group NAME and all descendants -a select all sessions -b build heap images -c clean build -d DIR include session directory -e export files from session specification into file-system -f fresh build -g NAME select session group NAME -j INT maximum number of parallel jobs (default 1) -k KEYWORD check theory sources for conflicts with proposed keywords -l list session source files -n no build -- take existing session build databases -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose -x NAME exclude session NAME and all descendants Build and manage Isabelle sessions, depending on implicit settings: """ + Library.indent_lines(2, Build_Log.Settings.show()) + "\n", "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), "N" -> (_ => numa_shuffling = true), "P:" -> (arg => browser_info = Browser_Info.Config.make(arg)), "R" -> (_ => requirements = true), "S" -> (_ => soft_build = true), "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), "a" -> (_ => all_sessions = true), "b" -> (_ => build_heap = true), "c" -> (_ => clean_build = true), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "e" -> (_ => export_files = true), "f" -> (_ => fresh_build = true), "g:" -> (arg => session_groups = session_groups ::: List(arg)), "j:" -> (arg => max_jobs = Value.Int.parse(arg)), "k:" -> (arg => check_keywords = check_keywords + arg), "l" -> (_ => list_files = true), "n" -> (_ => no_build = true), "o:" -> (arg => options = options + arg), "v" -> (_ => verbose = true), "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) val sessions = getopts(args) val progress = new Console_Progress(verbose = verbose) val start_date = Date.now() progress.echo( "Started at " + Build_Log.print_date(start_date) + " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + hostname(options) +")", verbose = true) progress.echo(Build_Log.Settings.show() + "\n", verbose = true) val results = progress.interrupt_handler { build(options, selection = Sessions.Selection( requirements = requirements, all_sessions = all_sessions, base_sessions = base_sessions, exclude_session_groups = exclude_session_groups, exclude_sessions = exclude_sessions, session_groups = session_groups, sessions = sessions), browser_info = browser_info, progress = progress, check_unknown_files = Mercurial.is_repository(Path.ISABELLE_HOME), build_heap = build_heap, clean_build = clean_build, dirs = dirs, select_dirs = select_dirs, numa_shuffling = Host.numa_check(progress, numa_shuffling), max_jobs = max_jobs, list_files = list_files, check_keywords = check_keywords, fresh_build = fresh_build, no_build = no_build, soft_build = soft_build, export_files = export_files) } val stop_date = Date.now() val elapsed_time = stop_date.time - start_date.time progress.echo("\nFinished at " + Build_Log.print_date(stop_date), verbose = true) val total_timing = results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _). copy(elapsed = elapsed_time) progress.echo(total_timing.message_resources) sys.exit(results.rc) }) /** "isabelle build_worker" **/ /* build_worker */ def build_worker( options: Options, build_uuid: String, progress: Progress = new Progress, dirs: List[Path] = Nil, infos: List[Sessions.Info] = Nil, numa_shuffling: Boolean = false, max_jobs: Int = 1, session_setup: (String, Session) => Unit = (_, _) => (), cache: Term.Cache = Term.Cache.make() ): Results = { val store = build_init(options, cache = cache) val build_options = store.options progress.echo("build worker for " + build_uuid) progress.echo_warning("FIXME") ??? } /* command-line wrapper */ val isabelle_tool2 = Isabelle_Tool("build_worker", "external worker for session build process", Scala_Project.here, { args => - val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")) - var numa_shuffling = false var dirs: List[Path] = Nil var max_jobs = 1 - var options = Options.init(opts = build_options) + var options = Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS) var verbose = false var build_uuid = "" val getopts = Getopts(""" Usage: isabelle build_worker [OPTIONS] ...] Options are: -N cyclic shuffling of NUMA CPU nodes (performance tuning) -U UUID Universally Unique Identifier of the build process -d DIR include session directory -j INT maximum number of parallel jobs (default 1) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose Run as external worker for session build process, as identified via option -U UUID. """ + Library.indent_lines(2, Build_Log.Settings.show()) + "\n", "N" -> (_ => numa_shuffling = true), "U:" -> (arg => build_uuid = arg), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "j:" -> (arg => max_jobs = Value.Int.parse(arg)), "o:" -> (arg => options = options + arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() if (build_uuid.isEmpty) error("Missing UUID for build process (option -U)") val progress = new Console_Progress(verbose = verbose) val results = progress.interrupt_handler { build_worker(options, build_uuid, progress = progress, dirs = dirs, numa_shuffling = Host.numa_check(progress, numa_shuffling), max_jobs = max_jobs) } sys.exit(results.rc) }) /** "isabelle build_log" **/ /* theory markup/messages from session database */ def read_theory( theory_context: Export.Theory_Context, unicode_symbols: Boolean = false ): Option[Document.Snapshot] = { def decode_bytes(bytes: Bytes): String = Symbol.output(unicode_symbols, UTF8.decode_permissive(bytes)) def read(name: String): Export.Entry = theory_context(name, permissive = true) def read_xml(name: String): XML.Body = YXML.parse_body(decode_bytes(read(name).bytes), cache = theory_context.cache) def read_source_file(name: String): Sessions.Source_File = theory_context.session_context.source_file(name) for { id <- theory_context.document_id() (thy_file, blobs_files) <- theory_context.files(permissive = true) } yield { val master_dir = Path.explode(Url.strip_base_name(thy_file).getOrElse( error("Cannot determine theory master directory: " + quote(thy_file)))) val blobs = blobs_files.map { name => val path = Path.explode(name) val src_path = File.relative_path(master_dir, path).getOrElse(path) val file = read_source_file(name) val bytes = file.bytes val text = decode_bytes(bytes) val chunk = Symbol.Text_Chunk(text) Command.Blob(Document.Node.Name(name), src_path, Some((file.digest, chunk))) -> Document.Blobs.Item(bytes, text, chunk, changed = false) } val thy_source = decode_bytes(read_source_file(thy_file).bytes) val thy_xml = read_xml(Export.MARKUP) val blobs_xml = for (i <- (1 to blobs.length).toList) yield read_xml(Export.MARKUP + i) val markups_index = Command.Markup_Index.make(blobs.map(_._1)) val markups = Command.Markups.make( for ((index, xml) <- markups_index.zip(thy_xml :: blobs_xml)) yield index -> Markup_Tree.from_XML(xml)) val results = Command.Results.make( for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES)) yield i -> elem) val command = Command.unparsed(thy_source, theory = true, id = id, node_name = Document.Node.Name(thy_file, theory = theory_context.theory), blobs_info = Command.Blobs_Info.make(blobs), markups = markups, results = results) val doc_blobs = Document.Blobs.make(blobs) Document.State.init.snippet(command, doc_blobs) } } /* print messages */ def print_log( options: Options, sessions: List[String], theories: List[String] = Nil, message_head: List[Regex] = Nil, message_body: List[Regex] = Nil, progress: Progress = new Progress, margin: Double = Pretty.default_margin, breakgain: Double = Pretty.default_breakgain, metric: Pretty.Metric = Symbol.Metric, unicode_symbols: Boolean = false ): Unit = { val store = Sessions.store(options) val session = new Session(options, Resources.bootstrap) def check(filter: List[Regex], make_string: => String): Boolean = filter.isEmpty || { val s = Output.clean_yxml(make_string) filter.forall(r => r.findFirstIn(Output.clean_yxml(s)).nonEmpty) } def print(session_name: String): Unit = { using(Export.open_session_context0(store, session_name)) { session_context => val result = for { db <- session_context.session_db() theories = store.read_theories(db, session_name) errors = store.read_errors(db, session_name) info <- store.read_build(db, session_name) } yield (theories, errors, info.return_code) result match { case None => store.error_database(session_name) case Some((used_theories, errors, rc)) => theories.filterNot(used_theories.toSet) match { case Nil => case bad => error("Unknown theories " + commas_quote(bad)) } val print_theories = if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet) for (thy <- print_theories) { val thy_heading = "\nTheory " + quote(thy) + " (in " + session_name + ")" + ":" Build_Job.read_theory(session_context.theory(thy), unicode_symbols = unicode_symbols) match { case None => progress.echo(thy_heading + " MISSING") case Some(snapshot) => val rendering = new Rendering(snapshot, options, session) val messages = rendering.text_messages(Text.Range.full) .filter(message => progress.verbose || Protocol.is_exported(message.info)) if (messages.nonEmpty) { val line_document = Line.Document(snapshot.node.source) val buffer = new mutable.ListBuffer[String] for (Text.Info(range, elem) <- messages) { val line = line_document.position(range.start).line1 val pos = Position.Line_File(line, snapshot.node_name.node) def message_text: String = Protocol.message_text(elem, heading = true, pos = pos, margin = margin, breakgain = breakgain, metric = metric) val ok = check(message_head, Protocol.message_heading(elem, pos)) && check(message_body, XML.content(Pretty.unformatted(List(elem)))) if (ok) buffer += message_text } if (buffer.nonEmpty) { progress.echo(thy_heading) buffer.foreach(progress.echo(_)) } } } } if (errors.nonEmpty) { val msg = Symbol.output(unicode_symbols, cat_lines(errors)) progress.echo("\nBuild errors:\n" + Output.error_message_text(msg)) } if (rc != Process_Result.RC.ok) { progress.echo("\n" + Process_Result.RC.print_long(rc)) } } } } val errors = new mutable.ListBuffer[String] for (session_name <- sessions) { Exn.interruptible_capture(print(session_name)) match { case Exn.Res(_) => case Exn.Exn(exn) => errors += Exn.message(exn) } } if (errors.nonEmpty) error(cat_lines(errors.toList)) } /* command-line wrapper */ val isabelle_tool3 = Isabelle_Tool("build_log", "print messages from session build database", Scala_Project.here, { args => /* arguments */ var message_head = List.empty[Regex] var message_body = List.empty[Regex] var unicode_symbols = false var theories: List[String] = Nil var margin = Pretty.default_margin var options = Options.init() var verbose = false val getopts = Getopts(""" Usage: isabelle build_log [OPTIONS] [SESSIONS ...] Options are: -H REGEX filter messages by matching against head -M REGEX filter messages by matching against body -T NAME restrict to given theories (multiple options possible) -U output Unicode symbols -m MARGIN margin for pretty printing (default: """ + margin + """) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v print all messages, including information etc. Print messages from the session build database of the given sessions, without any checks against current sources nor session structure: results from old sessions or failed builds can be printed as well. Multiple options -H and -M are conjunctive: all given patterns need to match. Patterns match any substring, but ^ or $ may be used to match the start or end explicitly. """, "H:" -> (arg => message_head = message_head ::: List(arg.r)), "M:" -> (arg => message_body = message_body ::: List(arg.r)), "T:" -> (arg => theories = theories ::: List(arg)), "U" -> (_ => unicode_symbols = true), "m:" -> (arg => margin = Value.Double.parse(arg)), "o:" -> (arg => options = options + arg), "v" -> (_ => verbose = true)) val sessions = getopts(args) val progress = new Console_Progress(verbose = verbose) if (sessions.isEmpty) progress.echo_warning("No sessions to print") else { print_log(options, sessions, theories = theories, message_head = message_head, message_body = message_body, margin = margin, progress = progress, unicode_symbols = unicode_symbols) } }) } 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,334 +1,335 @@ /* 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 Help extends Server.Command("help") { override val command_body: Server.Command_Body = { case (context, ()) => context.command_list } } object Echo extends Server.Command("echo") { override val command_body: Server.Command_Body = { case (_, t) => t } } object Cancel extends Server.Command("cancel") { sealed case class Args(task: UUID.T) def unapply(json: JSON.T): Option[Args] = for { task <- JSON.uuid(json, "task") } yield Args(task) override val command_body: Server.Command_Body = { case (context, Cancel(args)) => context.cancel_task(args.task) } } object Shutdown extends Server.Command("shutdown") { override val command_body: Server.Command_Body = { case (context, ()) => context.server.shutdown() } } object Session_Build extends Server.Command("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) 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") } yield { Args(session, preferences = preferences, options = options, dirs = dirs, include_sessions = include_sessions) } def command( args: Args, progress: Progress = new Progress ) : (JSON.Object.T, Build.Results, Options, Sessions.Background) = { - val options = Options.init(prefs = args.preferences, opts = args.options) + val options = + Options.init(prefs = args.preferences, specs = args.options.map(Options.Spec.make)) val dirs = args.dirs.map(Path.explode) val session_background = Sessions.background(options, args.session, progress = progress, dirs = dirs, include_sessions = args.include_sessions).check_errors val results = Build.build(options, selection = Sessions.Selection.session(args.session), progress = progress, build_heap = true, dirs = dirs, infos = session_background.infos) val sessions_order = session_background.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, session_background) else { throw new Server.Error("Session build failed: " + Process_Result.RC.print(results.rc), results_json) } } override val command_body: Server.Command_Body = { case (context, Session_Build(args)) => context.make_task(task => Session_Build.command(args, progress = task.progress)._1) } } object Session_Start extends Server.Command("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, session_background) = try { Session_Build.command(args.build, progress = progress) } catch { case exn: Server.Error => error(exn.message) } val resources = Headless.Resources(options, session_background, 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" -> session.tmp_dir_name) (res, id -> session) } override val command_body: Server.Command_Body = { case (context, Session_Start(args)) => context.make_task { task => val (res, entry) = Session_Start.command(args, progress = task.progress, log = context.server.log) context.server.add_session(entry) res } } } object Session_Stop extends Server.Command("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: " + result.print_rc, result_json) } override val command_body: Server.Command_Body = { case (context, Session_Stop(id)) => context.make_task(_ => { val session = context.server.remove_session(id) Session_Stop.command(session)._1 }) } } object Use_Theories extends Server.Command("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(text: String): String = Symbol.output(args.unicode_symbols, text) 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 } } def show_message(tree: XML.Tree): Boolean = Protocol.is_exported(tree) || session.show_states && Protocol.is_state(tree) 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 show_message(tree) } yield output_message(tree, pos))) + ("exports" -> (if (args.export_pattern == "") Nil else { val matcher = Export.make_matcher(List(args.export_pattern)) for { entry <- snapshot.exports if matcher(entry.entry_name) } yield { val (base64, body) = entry.bytes.maybe_encode_base64 JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body) } })) })) (result_json, result) } override val command_body: Server.Command_Body = { case (context, Use_Theories(args)) => context.make_task { task => val session = context.server.the_session(args.session_id) Use_Theories.command(args, session, id = task.id, progress = task.progress)._1 } } } object Purge_Theories extends Server.Command("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)) } override val command_body: Server.Command_Body = { case (context, Purge_Theories(args)) => val session = context.server.the_session(args.session_id) command(args, session)._1 } } } class Server_Commands extends Server.Commands( Server_Commands.Help, Server_Commands.Echo, Server_Commands.Cancel, Server_Commands.Shutdown, Server_Commands.Session_Build, Server_Commands.Session_Start, Server_Commands.Session_Stop, Server_Commands.Use_Theories, Server_Commands.Purge_Theories)