diff --git a/src/Pure/Admin/build_doc.scala b/src/Pure/Admin/build_doc.scala --- a/src/Pure/Admin/build_doc.scala +++ b/src/Pure/Admin/build_doc.scala @@ -1,107 +1,108 @@ /* Title: Pure/Admin/build_doc.scala Author: Makarius Build Isabelle documentation. */ package isabelle import java.io.{File => JFile} object Build_Doc { /* build_doc */ def build_doc( options: Options, progress: Progress = new Progress, all_docs: Boolean = false, max_jobs: Int = 1, docs: List[String] = Nil): Int = { val sessions_structure = Sessions.load_structure(options) val selection = for { name <- sessions_structure.build_topological_order info = sessions_structure(name) if info.groups.contains("doc") doc = info.options.string("document_variants") if all_docs || docs.contains(doc) } yield (doc, name) val selected_docs = selection.map(_._1) val sessions = selection.map(_._2) docs.filter(doc => !selected_docs.contains(doc)) match { case Nil => case bad => error("No documentation session for " + commas_quote(bad)) } progress.echo("Build started for documentation " + commas_quote(selected_docs)) val res1 = - Build.build(options, Sessions.Selection(requirements = true, sessions = sessions), + Build.build(options, + selection = Sessions.Selection(requirements = true, sessions = sessions), progress = progress, build_heap = true, max_jobs = max_jobs) if (res1.ok) { Isabelle_System.with_tmp_dir("document_output")(output => { val res2 = Build.build( options.bool.update("browser_info", false). string.update("document", "pdf"). string.update("document_output", output.implode), - Sessions.Selection(sessions = sessions), + selection = Sessions.Selection(sessions = sessions), progress = progress, clean_build = true, max_jobs = max_jobs) if (res2.ok) { val doc_dir = Path.explode("~~/doc") for (doc <- selected_docs) { val name = Path.explode(doc + ".pdf") File.copy(output + name, doc_dir + name) } } res2.rc }) } else res1.rc } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_doc", "build Isabelle documentation", args => { var all_docs = false var max_jobs = 1 var options = Options.init() val getopts = Getopts(""" Usage: isabelle build_doc [OPTIONS] [DOCS ...] Options are: -a select all documentation sessions -j INT maximum number of parallel jobs (default 1) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) Build Isabelle documentation from documentation sessions with suitable document_variants entry. """, "a" -> (_ => all_docs = true), "j:" -> (arg => max_jobs = Value.Int.parse(arg)), "o:" -> (arg => options = options + arg)) val docs = getopts(args) if (!all_docs && docs.isEmpty) getopts.usage() val progress = new Console_Progress() val rc = progress.interrupt_handler { build_doc(options, progress, all_docs, max_jobs, docs) } sys.exit(rc) }) } diff --git a/src/Pure/Admin/ci_profile.scala b/src/Pure/Admin/ci_profile.scala --- a/src/Pure/Admin/ci_profile.scala +++ b/src/Pure/Admin/ci_profile.scala @@ -1,163 +1,163 @@ /* Title: Pure/Admin/ci_profile.scala Author: Lars Hupel Build profile for continuous integration services. */ package isabelle import java.time.{Instant, ZoneId} import java.time.format.DateTimeFormatter import java.util.{Properties => JProperties, Map => JMap} abstract class CI_Profile extends Isabelle_Tool.Body { private def build(options: Options): (Build.Results, Time) = { val progress = new Console_Progress(verbose = true) val start_time = Time.now() val results = progress.interrupt_handler { Build.build( options + "system_heaps", - selection, + selection = selection, progress = progress, clean_build = clean, verbose = true, numa_shuffling = numa, max_jobs = jobs, dirs = include, select_dirs = select) } val end_time = Time.now() (results, end_time - start_time) } private def load_properties(): JProperties = { val props = new JProperties() val file_name = Isabelle_System.getenv("ISABELLE_CI_PROPERTIES") if (file_name != "") { val file = Path.explode(file_name).file if (file.exists()) props.load(new java.io.FileReader(file)) props } else props } private def compute_timing(results: Build.Results, group: Option[String]): Timing = { val timings = results.sessions.collect { case session if group.forall(results.info(session).groups.contains(_)) => results(session).timing } (Timing.zero /: timings)(_ + _) } private def with_documents(options: Options): Options = { if (documents) options .bool.update("browser_info", true) .string.update("document", "pdf") .string.update("document_variants", "document:outline=/proof,/ML") else options } final def hg_id(path: Path): String = Mercurial.repository(path).id() final def print_section(title: String): Unit = println(s"\n=== $title ===\n") final val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME")) final val isabelle_id = hg_id(isabelle_home) final val start_time = Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME) override final def apply(args: List[String]): Unit = { print_section("CONFIGURATION") println(Build_Log.Settings.show()) val props = load_properties() System.getProperties().asInstanceOf[JMap[AnyRef, AnyRef]].putAll(props) val options = with_documents(Options.init()) .int.update("parallel_proofs", 1) .int.update("threads", threads) println(s"jobs = $jobs, threads = $threads, numa = $numa") print_section("BUILD") println(s"Build started at $start_time") println(s"Isabelle id $isabelle_id") pre_hook(args) print_section("LOG") val (results, elapsed_time) = build(options) print_section("TIMING") val groups = results.sessions.map(results.info).flatMap(_.groups) for (group <- groups) println(s"Group $group: " + compute_timing(results, Some(group)).message_resources) val total_timing = compute_timing(results, None).copy(elapsed = elapsed_time) println("Overall: " + total_timing.message_resources) if (!results.ok) { print_section("FAILED SESSIONS") for (name <- results.sessions) { if (results.cancelled(name)) { println(s"Session $name: CANCELLED") } else { val result = results(name) if (!result.ok) println(s"Session $name: FAILED ${result.rc}") } } } post_hook(results) System.exit(results.rc) } /* profile */ def threads: Int = Isabelle_System.hostname() match { case "hpcisabelle" => 8 case "lxcisa1" => 4 case _ => 2 } def jobs: Int = Isabelle_System.hostname() match { case "hpcisabelle" => 8 case "lxcisa1" => 10 case _ => 2 } def numa: Boolean = Isabelle_System.hostname() == "hpcisabelle" def documents: Boolean = true def clean: Boolean = true def include: List[Path] def select: List[Path] def pre_hook(args: List[String]): Unit def post_hook(results: Build.Results): Unit def selection: Sessions.Selection } 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,948 +1,948 @@ /* Title: Pure/Tools/build.scala Author: Makarius Options: :folding=explicit: Build and manage Isabelle sessions. */ package isabelle import scala.collection.{SortedSet, mutable} import scala.annotation.tailrec object Build { /** auxiliary **/ /* persistent build info */ sealed case class Session_Info( sources: String, input_heaps: List[String], output_heap: Option[String], return_code: Int) { def ok: Boolean = return_code == 0 } /* queue with scheduling information */ private object Queue { type Timings = (List[Properties.T], Double) def load_timings(progress: Progress, store: Sessions.Store, session_name: String): Timings = { val no_timings: Timings = (Nil, 0.0) store.access_database(session_name) match { case None => no_timings case Some(db) => def ignore_error(msg: String) = { progress.echo_warning("Ignoring bad database " + db + (if (msg == "") "" else "\n" + msg)) no_timings } try { val command_timings = store.read_command_timings(db, session_name) val session_timing = store.read_session_timing(db, session_name) match { case Markup.Elapsed(t) => t case _ => 0.0 } (command_timings, session_timing) } catch { case ERROR(msg) => ignore_error(msg) case exn: java.lang.Error => ignore_error(Exn.message(exn)) case _: XML.Error => ignore_error("") } finally { db.close } } } def make_session_timing(sessions_structure: Sessions.Structure, timing: Map[String, Double]) : Map[String, Double] = { val maximals = sessions_structure.build_graph.maximals.toSet def desc_timing(session_name: String): Double = { if (maximals.contains(session_name)) timing(session_name) else { val descendants = sessions_structure.build_descendants(List(session_name)).toSet val g = sessions_structure.build_graph.restrict(descendants) (0.0 :: g.maximals.flatMap(desc => { val ps = g.all_preds(List(desc)) if (ps.exists(p => !timing.isDefinedAt(p))) None else Some(ps.map(timing(_)).sum) })).max } } timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0) } def apply(progress: Progress, sessions_structure: Sessions.Structure, store: Sessions.Store) : Queue = { val graph = sessions_structure.build_graph val names = graph.keys val timings = names.map(name => (name, load_timings(progress, store, name))) val command_timings = timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil) val session_timing = make_session_timing(sessions_structure, timings.map({ case (name, (_, t)) => (name, t) }).toMap) object Ordering extends scala.math.Ordering[String] { def compare_timing(name1: String, name2: String): Int = { val t1 = session_timing(name1) val t2 = session_timing(name2) if (t1 == 0.0 || t2 == 0.0) 0 else t1 compare t2 } def compare(name1: String, name2: String): Int = compare_timing(name2, name1) match { case 0 => sessions_structure(name2).timeout compare sessions_structure(name1).timeout match { case 0 => name1 compare name2 case ord => ord } case ord => ord } } new Queue(graph, SortedSet(names: _*)(Ordering), command_timings) } } private class Queue( graph: Graph[String, Sessions.Info], order: SortedSet[String], val command_timings: String => List[Properties.T]) { def is_inner(name: String): Boolean = !graph.is_maximal(name) def is_empty: Boolean = graph.is_empty def - (name: String): Queue = new Queue(graph.del_node(name), order - name, // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!? command_timings) def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] = { val it = order.iterator.dropWhile(name => skip(name) || !graph.defined(name) // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!? || !graph.is_minimal(name)) if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) } else None } } /* PIDE protocol handler */ /* job: running prover process */ private class Job(progress: Progress, session_name: String, val info: Sessions.Info, deps: Sessions.Deps, store: Sessions.Store, do_store: Boolean, verbose: Boolean, val numa_node: Option[Int], command_timings: List[Properties.T]) { val options: Options = NUMA.policy_options(info.options, numa_node) private val sessions_structure = deps.sessions_structure private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf") graphview.Graph_File.write(options, graph_file, deps(session_name).session_graph_display) private val export_tmp_dir = Isabelle_System.tmp_dir("export") private val export_consumer = Export.consumer(store.open_database(session_name, output = true), cache = store.xz_cache) private val future_result: Future[Process_Result] = Future.thread("build", uninterruptible = true) { val parent = info.parent.getOrElse("") val base = deps(parent) val args_yxml = YXML.string_of_body( { import XML.Encode._ pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string, pair(string, pair(Path.encode, pair(list(pair(Options.encode, list(pair(string, properties)))), pair(list(pair(string, properties)), pair(list(pair(string, string)), pair(list(string), pair(list(pair(string, string)), pair(list(string), list(string)))))))))))))))))( (Symbol.codes, (command_timings, (verbose, (store.browser_info, (info.document_files, (File.standard_path(graph_file), (parent, (info.chapter, (session_name, (Path.current, (info.theories, (sessions_structure.session_positions, (sessions_structure.dest_session_directories, (base.doc_names, (base.global_theories.toList, (base.loaded_theories.keys, info.bibtex_entries.map(_.info)))))))))))))))))) }) val env = Isabelle_System.settings() + ("ISABELLE_EXPORT_TMP" -> File.standard_path(export_tmp_dir)) + ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString) val is_pure = Sessions.is_pure(session_name) val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil val eval_store = if (do_store) { (if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) ::: List("ML_Heap.save_child " + ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name)))) } else Nil if (options.bool("pide_session")) { val resources = new Resources(sessions_structure, deps(parent)) val session = new Session(options, resources) { override val xml_cache: XML.Cache = store.xml_cache override val xz_cache: XZ.Cache = store.xz_cache } val build_session_errors: Promise[List[String]] = Future.promise val stdout = new StringBuilder(1000) val messages = new mutable.ListBuffer[XML.Elem] val command_timings = new mutable.ListBuffer[Properties.T] val theory_timings = new mutable.ListBuffer[Properties.T] val runtime_statistics = new mutable.ListBuffer[Properties.T] val task_statistics = new mutable.ListBuffer[Properties.T] def fun( name: String, acc: mutable.ListBuffer[Properties.T], unapply: Properties.T => Option[Properties.T]): (String, Session.Protocol_Function) = { name -> ((msg: Prover.Protocol_Output) => unapply(msg.properties) match { case Some(props) => acc += props; true case _ => false }) } session.init_protocol_handler(new Session.Protocol_Handler { override def exit() { build_session_errors.cancel } private def build_session_finished(msg: Prover.Protocol_Output): Boolean = { val (rc, errors) = try { val (rc, errs) = { import XML.Decode._ pair(int, list(x => x))(Symbol.decode_yxml(msg.text)) } val errors = for (err <- errs) yield { val prt = Protocol_Message.expose_no_reports(err) Pretty.string_of(prt, metric = Symbol.Metric) } (rc, errors) } catch { case ERROR(err) => (2, List(err)) } session.protocol_command("Prover.stop", rc.toString) build_session_errors.fulfill(errors) true } private def loading_theory(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Markup.Loading_Theory(name) => progress.theory(Progress.Theory(name, session = session_name)) true case _ => false } private def export(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Protocol.Export(args) => export_consumer(session_name, args, msg.bytes) true case _ => false } val functions = List( Markup.Build_Session_Finished.name -> build_session_finished, Markup.Loading_Theory.name -> loading_theory, Markup.EXPORT -> export, fun(Markup.Command_Timing.name, command_timings, Markup.Command_Timing.unapply), fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply), fun(Markup.ML_Statistics.name, runtime_statistics, Markup.ML_Statistics.unapply), fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply)) }) session.all_messages += Session.Consumer[Any]("build_session_output") { case msg: Prover.Output => val message = msg.message if (msg.is_stdout) { stdout ++= Symbol.encode(XML.content(message)) } else if (Protocol.is_exported(message)) { messages += message } case _ => } val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store) val process = Isabelle_Process(session, options, sessions_structure, store, logic = parent, raw_ml_system = is_pure, use_prelude = use_prelude, eval_main = eval_main, cwd = info.dir.file, env = env) val errors = Isabelle_Thread.interrupt_handler(_ => process.terminate) { Exn.capture { process.await_startup } match { case Exn.Res(_) => session.protocol_command("build_session", args_yxml) build_session_errors.join_result case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn))) } } val process_result = Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown } val process_output = stdout.toString :: messages.toList.map(message => Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))) ::: command_timings.toList.map(Protocol.Command_Timing_Marker.apply) ::: theory_timings.toList.map(Protocol.Theory_Timing_Marker.apply) ::: runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) ::: task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) val result = process_result.output(process_output) errors match { case Exn.Res(Nil) => result case Exn.Res(errs) => result.error_rc.output( errs.flatMap(s => split_lines(Output.error_message_text(s))) ::: errs.map(Protocol.Error_Message_Marker.apply)) case Exn.Exn(Exn.Interrupt()) => if (result.ok) result.copy(rc = Exn.Interrupt.return_code) else result case Exn.Exn(exn) => throw exn } } else { val args_file = Isabelle_System.tmp_file("build") File.write(args_file, args_yxml) val eval_build = "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file)) val eval_main = Command_Line.ML_tool(eval_build :: eval_store) val process = ML_Process(options, deps.sessions_structure, store, logic = parent, raw_ml_system = is_pure, use_prelude = use_prelude, eval_main = eval_main, cwd = info.dir.file, env = env, cleanup = () => args_file.delete) Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.result( progress_stdout = { case Protocol.Loading_Theory_Marker(theory) => progress.theory(Progress.Theory(theory, session = session_name)) case Protocol.Export.Marker((args, path)) => val body = try { Bytes.read(path) } catch { case ERROR(msg) => error("Failed to read export " + quote(args.compound_name) + "\n" + msg) } path.file.delete export_consumer(session_name, args, body) case _ => }, progress_limit = options.int("process_output_limit") match { case 0 => None case m => Some(m * 1000000L) }, strict = false) } } } def terminate: Unit = future_result.cancel def is_finished: Boolean = future_result.is_finished private val timeout_request: Option[Event_Timer.Request] = { if (info.timeout > Time.zero) Some(Event_Timer.request(Time.now() + info.timeout) { terminate }) else None } def join: (Process_Result, Option[String]) = { val result0 = future_result.join val result1 = export_consumer.shutdown(close = true).map(Output.error_message_text) match { case Nil => result0 case errs => result0.errors(errs).error_rc } Isabelle_System.rm_tree(export_tmp_dir) if (result1.ok) Present.finish(progress, store.browser_info, graph_file, info, session_name) graph_file.delete val was_timeout = timeout_request match { case None => false case Some(request) => !request.cancel } val result2 = if (result1.interrupted) { if (was_timeout) result1.error(Output.error_message_text("Timeout")).was_timeout else result1.error(Output.error_message_text("Interrupt")) } else result1 val heap_digest = if (result2.ok && do_store && store.output_heap(session_name).is_file) Some(Sessions.write_heap_digest(store.output_heap(session_name))) else None (result2, heap_digest) } } /** build with results **/ class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)]) { def sessions: Set[String] = results.keySet def cancelled(name: String): Boolean = results(name)._1.isEmpty def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1)) def info(name: String): Sessions.Info = results(name)._2 val rc: Int = (0 /: results.iterator.map( { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _) def ok: Boolean = rc == 0 override def toString: String = rc.toString } def build( options: Options, - selection: Sessions.Selection, + selection: Sessions.Selection = Sessions.Selection.empty, 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, verbose: Boolean = false, export_files: Boolean = false): Results = { val build_options = options + "ML_statistics" + "completion_limit=0" + "editor_tracing_messages=0" + "pide_reports=false" val store = Sessions.store(build_options) Isabelle_Fonts.init() /* session selection and dependencies */ val full_sessions = Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos) def sources_stamp(deps: Sessions.Deps, session_name: String): String = { val digests = full_sessions(session_name).meta_digest :: deps.sources(session_name) ::: deps.imported_sources(session_name) SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString } val deps = { val deps0 = Sessions.deps(full_sessions.selection(selection), progress = progress, inlined_files = true, verbose = verbose, 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.access_database(name) match { case Some(db) => using(db)(store.read_build(_, name)) match { case Some(build) if build.ok && build.sources == sources_stamp(deps0, 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) <- deps.session_bases.iterator (path, _) <- base.sources.iterator } yield path).toList val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file) val unknown_files = Mercurial.check_files(source_files)._2. filterNot(path => exclude_files.contains(path.canonical_file)) if (unknown_files.nonEmpty) { progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" + unknown_files.map(path => path.expand.implode).sorted.mkString("\n ", "\n ", "")) } } /* main build process */ val queue = Queue(progress, deps.sessions_structure, store) store.prepare_output_dir() if (clean_build) { for (name <- full_sessions.imports_descendants(full_sessions.imports_selection(selection))) { val (relevant, ok) = store.clean_output(name) if (relevant) { if (ok) progress.echo("Cleaned " + name) else progress.echo(name + " FAILED to clean") } } } // scheduler loop case class Result( current: Boolean, heap_digest: Option[String], process: Option[Process_Result], info: Sessions.Info) { def ok: Boolean = process match { case None => false case Some(res) => res.rc == 0 } } def sleep() { Isabelle_Thread.interrupt_handler(_ => progress.stop) { Time.seconds(0.5).sleep } } val numa_nodes = new NUMA.Nodes(numa_shuffling) @tailrec def loop( pending: Queue, running: Map[String, (List[String], Job)], results: Map[String, Result]): Map[String, Result] = { def used_node(i: Int): Boolean = running.iterator.exists( { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i }) if (pending.is_empty) results else { if (progress.stopped) { for ((_, (_, job)) <- running) job.terminate } running.find({ case (_, (_, job)) => job.is_finished }) match { case Some((session_name, (input_heaps, job))) => //{{{ finish job val (process_result, heap_digest) = job.join val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test) val process_result_tail = { val tail = job.info.options.int("process_output_tail") process_result.copy( out_lines = "(see also " + store.output_log(session_name).file.toString + ")" :: (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0))) } // write log file if (process_result.ok) { File.write_gzip(store.output_log_gz(session_name), terminate_lines(log_lines)) } else File.write(store.output_log(session_name), terminate_lines(log_lines)) // write database { val build_log = Build_Log.Log_File(session_name, process_result.out_lines). parse_session_info( command_timings = true, theory_timings = true, ml_statistics = true, task_statistics = true) using(store.open_database(session_name, output = true))(db => store.write_session_info(db, session_name, build_log = if (process_result.timeout) build_log.error("Timeout") else build_log, build = Session_Info(sources_stamp(deps, session_name), input_heaps, heap_digest, process_result.rc))) } // messages process_result.err_lines.foreach(progress.echo) if (process_result.ok) progress.echo( "Finished " + session_name + " (" + process_result.timing.message_resources + ")") else { progress.echo(session_name + " FAILED") if (!process_result.interrupted) progress.echo(process_result_tail.out) } loop(pending - session_name, running - session_name, results + (session_name -> Result(false, heap_digest, Some(process_result_tail), job.info))) //}}} case None if running.size < (max_jobs max 1) => //{{{ check/start next job pending.dequeue(running.isDefinedAt) match { case Some((session_name, info)) => val ancestor_results = deps.sessions_structure.build_requirements(List(session_name)). filterNot(_ == session_name).map(results(_)) val ancestor_heaps = ancestor_results.flatMap(_.heap_digest) val do_store = build_heap || Sessions.is_pure(session_name) || queue.is_inner(session_name) val (current, heap_digest) = { store.access_database(session_name) match { case Some(db) => using(db)(store.read_build(_, session_name)) match { case Some(build) => val heap_digest = store.find_heap_digest(session_name) val current = !fresh_build && build.ok && build.sources == sources_stamp(deps, session_name) && build.input_heaps == ancestor_heaps && build.output_heap == heap_digest && !(do_store && heap_digest.isEmpty) (current, heap_digest) case None => (false, None) } case None => (false, None) } } val all_current = current && ancestor_results.forall(_.current) if (all_current) loop(pending - session_name, running, results + (session_name -> Result(true, heap_digest, Some(Process_Result(0)), info))) else if (no_build) { progress.echo_if(verbose, "Skipping " + session_name + " ...") loop(pending - session_name, running, results + (session_name -> Result(false, heap_digest, Some(Process_Result(1)), info))) } else if (ancestor_results.forall(_.ok) && !progress.stopped) { progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...") store.clean_output(session_name) using(store.open_database(session_name, output = true))( store.init_session_info(_, session_name)) val numa_node = numa_nodes.next(used_node) val job = new Job(progress, session_name, info, deps, store, do_store, verbose, numa_node, queue.command_timings(session_name)) loop(pending, running + (session_name -> (ancestor_heaps, job)), results) } else { progress.echo(session_name + " CANCELLED") loop(pending - session_name, running, results + (session_name -> Result(false, heap_digest, None, info))) } case None => sleep(); loop(pending, running, results) } ///}}} case None => sleep(); loop(pending, running, results) } } } /* build results */ val results0 = if (deps.is_empty) { progress.echo_warning("Nothing to build") Map.empty[String, Result] } else Isabelle_Thread.uninterruptible { loop(queue, Map.empty, Map.empty) } val results = new Results( (for ((name, result) <- results0.iterator) yield (name, (result.process, result.info))).toMap) if (export_files) { for (name <- full_sessions.imports_selection(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 (verbose) progress else new Progress, export_prune = prune, export_patterns = pats) } } } } if (results.rc != 0 && (verbose || !no_build)) { val unfinished = (for { name <- results.sessions.iterator if !results(name).ok } yield name).toList.sorted progress.echo("Unfinished session(s): " + commas(unfinished)) } /* global browser info */ if (!no_build) { val browser_chapters = (for { (name, result) <- results0.iterator if result.ok info = full_sessions(name) if info.options.bool("browser_info") } yield (info.chapter, (name, info.description))).toList.groupBy(_._1). map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty) for ((chapter, entries) <- browser_chapters) Present.update_chapter_index(store.browser_info, chapter, entries) if (browser_chapters.nonEmpty) Present.make_global_index(store.browser_info) } results } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", 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 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 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) -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 -- test dependencies only -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.prefix_lines(" ", 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), "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() if (verbose) { progress.echo( "Started at " + Build_Log.print_date(start_date) + " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")") progress.echo(Build_Log.Settings.show() + "\n") } val results = progress.interrupt_handler { build(options, - Sessions.Selection( + 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), progress = progress, check_unknown_files = Mercurial.is_repository(Path.explode("~~")), build_heap = build_heap, clean_build = clean_build, dirs = dirs, select_dirs = select_dirs, numa_shuffling = NUMA.enabled_warning(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, verbose = verbose, export_files = export_files) } val end_date = Date.now() val elapsed_time = end_date.time - start_date.time if (verbose) { progress.echo("\nFinished at " + Build_Log.print_date(end_date)) } val total_timing = (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _). copy(elapsed = elapsed_time) progress.echo(total_timing.message_resources) sys.exit(results.rc) }) /* 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, build_heap = build_heap, no_build = true, dirs = dirs).ok) 0 + if (!fresh && build(options, selection = selection, + build_heap = build_heap, no_build = true, dirs = dirs).ok) 0 else { progress.echo("Build started for Isabelle/" + logic + " ...") - Build.build(options, selection, progress = progress, build_heap = build_heap, - fresh_build = fresh, dirs = dirs).rc + Build.build(options, selection = selection, progress = progress, + build_heap = build_heap, fresh_build = fresh, dirs = dirs).rc } if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc } } 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,275 +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, Sessions.Selection.session(args.session), + Build.build(options, + selection = Sessions.Selection.session(args.session), progress = progress, build_heap = true, dirs = dirs, infos = base_info.infos, verbose = args.verbose) 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: " + 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: " + 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 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, Sessions.Selection.session(base_info.session), + Build.build(options, + selection = Sessions.Selection.session(base_info.session), build_heap = true, no_build = no_build, dirs = session_dirs, infos = base_info.infos) 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: " + 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/jedit_sessions.scala b/src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala +++ b/src/Tools/jEdit/src/jedit_sessions.scala @@ -1,151 +1,152 @@ /* Title: Tools/jEdit/src/jedit_sessions.scala Author: Makarius Isabelle/jEdit session information, based on implicit process environment and explicit options. */ package isabelle.jedit import isabelle._ import scala.swing.ComboBox import scala.swing.event.SelectionChanged object JEdit_Sessions { /* session options */ def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")).filterNot(p => p.implode == "-") def session_no_build(): Boolean = Isabelle_System.getenv("JEDIT_NO_BUILD") == "true" def session_options(options: Options): Options = { val options1 = Isabelle_System.getenv("JEDIT_BUILD_MODE") match { case "default" => options case mode => options.bool.update("system_heaps", mode == "system") } val options2 = Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match { case "" => options1 case s => options1.string.update("ML_process_policy", s) } options2 } def sessions_structure(options: Options, dirs: List[Path] = session_dirs()): Sessions.Structure = Sessions.load_structure(session_options(options), dirs = dirs) /* raw logic info */ private val jedit_logic_option = "jedit_logic" def logic_name(options: Options): String = Isabelle_System.default_logic( Isabelle_System.getenv("JEDIT_LOGIC"), options.string(jedit_logic_option)) def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR")) def logic_requirements: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_REQUIREMENTS") == "true" def logic_include_sessions: List[String] = space_explode(':', Isabelle_System.getenv("JEDIT_INCLUDE_SESSIONS")) def logic_info(options: Options): Option[Sessions.Info] = try { sessions_structure(options).get(logic_name(options)) } catch { case ERROR(_) => None } def logic_root(options: Options): Position.T = if (logic_requirements) logic_info(options).map(_.pos) getOrElse Position.none else Position.none /* logic selector */ private class Logic_Entry(val name: String, val description: String) { override def toString: String = description } def logic_selector(options: Options_Variable, autosave: Boolean): Option_Component = { GUI_Thread.require {} val session_list = { val sessions = sessions_structure(options.value) val (main_sessions, other_sessions) = sessions.imports_topological_order.partition(name => sessions(name).groups.contains("main")) main_sessions.sorted ::: other_sessions.sorted } val entries = new Logic_Entry("", "default (" + logic_name(options.value) + ")") :: session_list.map(name => new Logic_Entry(name, name)) val component = new ComboBox(entries) with Option_Component { name = jedit_logic_option val title = "Logic" def load: Unit = { val logic = options.string(jedit_logic_option) entries.find(_.name == logic) match { case Some(entry) => selection.item = entry case None => } } def save: Unit = options.string(jedit_logic_option) = selection.item.name } component.load() if (autosave) { component.listenTo(component.selection) component.reactions += { case SelectionChanged(_) => component.save() } } component.tooltip = "Logic session name (change requires restart)" component } /* session build process */ def session_base_info(options: Options): Sessions.Base_Info = Sessions.base_info(options, dirs = JEdit_Sessions.session_dirs(), include_sessions = logic_include_sessions, session = logic_name(options), session_ancestor = logic_ancestor, session_requirements = logic_requirements) def session_build( options: Options, progress: Progress = new Progress, no_build: Boolean = false): Int = { - Build.build(session_options(options), Sessions.Selection.session(PIDE.resources.session_name), + Build.build(session_options(options), + selection = Sessions.Selection.session(PIDE.resources.session_name), progress = progress, build_heap = true, no_build = no_build, dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos).rc } def session_start(options0: Options) { val session = PIDE.session val options = session_options(options0) val sessions_structure = PIDE.resources.session_base_info.sessions_structure val store = Sessions.store(options) session.phase_changed += PIDE.plugin.session_phase_changed Isabelle_Process(session, options, sessions_structure, store, logic = PIDE.resources.session_name, modes = (space_explode(',', options.string("jedit_print_mode")) ::: space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse) } }