# HG changeset patch # User wenzelm # Date 1567627279 -7200 # Node ID cce7a95f6e0ff9d8f81a78db2c480669d35769d2 # Parent 93a7a85de31218ddc608172f8bdc5a7dc6823ec2# Parent f7c5b30fc4326e161675a65f207e86f9bed178ec merged diff -r 93a7a85de312 -r cce7a95f6e0f src/HOL/ROOT --- a/src/HOL/ROOT Wed Sep 04 16:34:45 2019 +0100 +++ b/src/HOL/ROOT Wed Sep 04 22:01:19 2019 +0200 @@ -734,7 +734,7 @@ ATP_Problem_Import session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" + - theories + theories [dump_checkpoint] Probability document_files "root.tex" @@ -745,7 +745,7 @@ Measure_Not_CCC session "HOL-Nominal" in Nominal = "HOL-Library" + - theories + theories [dump_checkpoint] Nominal session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" + diff -r 93a7a85de312 -r cce7a95f6e0f src/Pure/General/graph.scala --- a/src/Pure/General/graph.scala Wed Sep 04 16:34:45 2019 +0100 +++ b/src/Pure/General/graph.scala Wed Sep 04 22:01:19 2019 +0200 @@ -14,8 +14,17 @@ object Graph { class Duplicate[Key](val key: Key) extends Exception + { + override def toString: String = "Graph.Duplicate(" + key.toString + ")" + } class Undefined[Key](val key: Key) extends Exception + { + override def toString: String = "Graph.Undefined(" + key.toString + ")" + } class Cycles[Key](val cycles: List[List[Key]]) extends Exception + { + override def toString: String = cycles.mkString("Graph.Cycles(", ",\n", ")") + } def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] = new Graph[Key, A](SortedMap.empty(ord)) diff -r 93a7a85de312 -r cce7a95f6e0f src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Wed Sep 04 16:34:45 2019 +0100 +++ b/src/Pure/PIDE/document.scala Wed Sep 04 22:01:19 2019 +0200 @@ -76,6 +76,13 @@ type Edit_Text = Edit[Text.Edit, Text.Perspective] type Edit_Command = Edit[Command.Edit, Command.Perspective] + type Theory_Graph[A] = Graph[Node.Name, A] + + def theory_graph[A]( + entries: List[((Node.Name, A), List[Node.Name])], + permissive: Boolean = false): Theory_Graph[A] = + Graph.make(entries, symmetric = true, permissive = permissive)(Node.Name.Theory_Ordering) + object Node { /* header and name */ diff -r 93a7a85de312 -r cce7a95f6e0f src/Pure/PIDE/document_status.scala --- a/src/Pure/PIDE/document_status.scala Wed Sep 04 16:34:45 2019 +0100 +++ b/src/Pure/PIDE/document_status.scala Wed Sep 04 22:01:19 2019 +0200 @@ -244,6 +244,12 @@ node_status <- get(name) } yield (name, node_status)).toList + def consolidated(name: Document.Node.Name): Boolean = + rep.get(name) match { + case Some(st) => st.consolidated + case None => false + } + def quasi_consolidated(name: Document.Node.Name): Boolean = rep.get(name) match { case Some(st) => st.quasi_consolidated diff -r 93a7a85de312 -r cce7a95f6e0f src/Pure/PIDE/headless.scala --- a/src/Pure/PIDE/headless.scala Wed Sep 04 16:34:45 2019 +0100 +++ b/src/Pure/PIDE/headless.scala Wed Sep 04 22:01:19 2019 +0200 @@ -44,6 +44,62 @@ (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok }) } + private object Checkpoints_State + { + object Status extends Enumeration + { + val INIT, LOADED, LOADED_DESCENDANTS = Value + } + + def init(nodes: List[Document.Node.Name]): Checkpoints_State = + Checkpoints_State(Status.INIT, nodes) + + val last: Checkpoints_State = + Checkpoints_State(Status.LOADED_DESCENDANTS, Nil) + } + + private sealed case class Checkpoints_State( + status: Checkpoints_State.Status.Value, + nodes: List[Document.Node.Name]) + { + def next( + dep_graph: Document.Theory_Graph[Unit], + finished: Document.Node.Name => Boolean): (List[Document.Node.Name], Checkpoints_State) = + { + import Checkpoints_State.Status + + def descendants: List[Document.Node.Name] = + nodes match { + case Nil => dep_graph.topological_order + case current :: rest => + val dep_graph1 = + if (rest.isEmpty) dep_graph + else { + val exclude = dep_graph.all_succs(rest).toSet + dep_graph.restrict(name => !exclude(name)) + } + dep_graph1.all_succs(List(current)) + } + + def requirements: List[Document.Node.Name] = + dep_graph.all_preds(nodes.headOption.toList).reverse + + val (load_theories, st1) = + (status, nodes) match { + case (Status.INIT, Nil) => + (descendants, Checkpoints_State.last) + case (Status.INIT, current :: _) => + (requirements, copy(status = Status.LOADED)) + case (Status.LOADED, current :: rest) if finished(current) => + (descendants, copy(status = Status.LOADED_DESCENDANTS)) + case (Status.LOADED_DESCENDANTS, _ :: rest) if descendants.forall(finished) => + Checkpoints_State.init(rest).next(dep_graph, finished) + case _ => (Nil, this) + } + (load_theories.filterNot(finished), st1) + } + } + class Session private[Headless]( session_name: String, _session_options: => Options, @@ -52,6 +108,10 @@ session => + private def loaded_theory(name: Document.Node.Name): Boolean = + resources.session_base.loaded_theory(name.theory) + + /* options */ def default_check_delay: Time = session_options.seconds("headless_check_delay") @@ -81,69 +141,88 @@ /* theories */ private sealed case class Use_Theories_State( + dependencies: resources.Dependencies[Unit], + checkpoints_state: Checkpoints_State, + watchdog_timeout: Time, + commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit], last_update: Time = Time.now(), nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty, already_committed: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty, - result: Promise[Use_Theories_Result] = Future.promise[Use_Theories_Result]) + result: Option[Exn.Result[Use_Theories_Result]] = None) { + def dep_graph: Document.Theory_Graph[Unit] = dependencies.theory_graph + def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State = copy(last_update = Time.now(), nodes_status = new_nodes_status) - def watchdog(watchdog_timeout: Time): Boolean = + def watchdog: Boolean = watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout - def cancel_result { result.cancel } - def finished_result: Boolean = result.is_finished - def await_result { result.join_result } - def join_result: Use_Theories_Result = result.join - def check_result( - state: Document.State, - version: Document.Version, - dep_theories: List[Document.Node.Name], - beyond_limit: Boolean, - watchdog_timeout: Time, - commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit]) - : Use_Theories_State = + def finished_result: Boolean = result.isDefined + + def join_result: Option[(Exn.Result[Use_Theories_Result], Use_Theories_State)] = + if (finished_result) Some((result.get, this)) else None + + def cancel_result: Use_Theories_State = + if (finished_result) this else copy(result = Some(Exn.Exn(Exn.Interrupt()))) + + def clean: Set[Document.Node.Name] = + already_committed.keySet -- checkpoints_state.nodes + + def check(state: Document.State, version: Document.Version, beyond_limit: Boolean) + : (List[Document.Node.Name], Use_Theories_State) = { val already_committed1 = - if (commit.isDefined) { - (already_committed /: dep_theories)({ case (committed, name) => - def parents_committed: Boolean = - version.nodes(name).header.imports.forall(parent => - resources.session_base.loaded_theory(parent) || committed.isDefinedAt(parent)) - if (!committed.isDefinedAt(name) && parents_committed && - state.node_consolidated(version, name)) - { - val snapshot = stable_snapshot(state, version, name) - val status = Document_Status.Node_Status.make(state, version, name) - commit.get.apply(snapshot, status) - committed + (name -> status) - } - else committed - }) + commit match { + case None => already_committed + case Some(commit_fn) => + (already_committed /: dep_graph.topological_order)( + { case (committed, name) => + def parents_committed: Boolean = + version.nodes(name).header.imports.forall(parent => + loaded_theory(parent) || committed.isDefinedAt(parent)) + if (!committed.isDefinedAt(name) && parents_committed && + state.node_consolidated(version, name)) + { + val snapshot = stable_snapshot(state, version, name) + val status = Document_Status.Node_Status.make(state, version, name) + commit_fn(snapshot, status) + committed + (name -> status) + } + else committed + }) } - else already_committed - if (beyond_limit || watchdog(watchdog_timeout) || - dep_theories.forall(name => - already_committed1.isDefinedAt(name) || - state.node_consolidated(version, name) || - nodes_status.quasi_consolidated(name))) - { - val nodes = - for (name <- dep_theories) - yield { (name -> Document_Status.Node_Status.make(state, version, name)) } - val nodes_committed = - for { - name <- dep_theories - status <- already_committed1.get(name) - } yield (name -> status) + val result1 = + if (!finished_result && + (beyond_limit || watchdog || + dep_graph.keys_iterator.forall(name => + already_committed1.isDefinedAt(name) || + state.node_consolidated(version, name) || + nodes_status.quasi_consolidated(name)))) + { + val nodes = + (for (name <- dep_graph.keys_iterator) + yield { (name -> Document_Status.Node_Status.make(state, version, name)) }).toList + val nodes_committed = + (for { + name <- dep_graph.keys_iterator + status <- already_committed1.get(name) + } yield (name -> status)).toList + Some(Exn.Res(new Use_Theories_Result(state, version, nodes, nodes_committed))) + } + else result - try { result.fulfill(new Use_Theories_Result(state, version, nodes, nodes_committed)) } - catch { case _: IllegalStateException => } - } + val (load_theories, checkpoints_state1) = + checkpoints_state.next(dep_graph, + name => + loaded_theory(name) || + already_committed1.isDefinedAt(name) || + nodes_status.consolidated(name)) - copy(already_committed = already_committed1) + (load_theories, + copy(already_committed = already_committed1, result = result1, + checkpoints_state = checkpoints_state1)) } } @@ -158,6 +237,7 @@ nodes_status_delay: Time = default_nodes_status_delay, id: UUID.T = UUID.random(), share_common_data: Boolean = false, + checkpoints: Set[Document.Node.Name] = Set.empty, // commit: must not block, must not fail commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None, commit_cleanup_delay: Time = default_commit_cleanup_delay, @@ -171,20 +251,29 @@ resources.dependencies(import_names, progress = progress).check_errors } val dep_theories = dependencies.theories + val dep_theories_set = dep_theories.toSet val dep_files = dependencies.loaded_files(false).flatMap(_._2). map(path => Document.Node.Name(resources.append("", path))) - val use_theories_state = Synchronized(Use_Theories_State()) + val use_theories_state = + { + val checkpoints_state = + Checkpoints_State.init( + if (checkpoints.isEmpty) Nil + else dependencies.theory_graph.topological_order.filter(checkpoints(_))) + Synchronized(Use_Theories_State(dependencies, checkpoints_state, watchdog_timeout, commit)) + } - def check_result_state(beyond_limit: Boolean = false) + def check_state(beyond_limit: Boolean = false) { val state = session.current_state() - state.stable_tip_version match { - case Some(version) => - use_theories_state.change( - _.check_result(state, version, dep_theories, beyond_limit, watchdog_timeout, commit)) - case None => + for (version <- state.stable_tip_version) { + val load_theories = use_theories_state.change_result(_.check(state, version, beyond_limit)) + if (load_theories.nonEmpty) { + resources.load_theories( + session, id, load_theories, dep_files, unicode_symbols, share_common_data, progress) + } } } @@ -193,10 +282,10 @@ var check_count = 0 Event_Timer.request(Time.now(), repeat = Some(check_delay)) { - if (progress.stopped) use_theories_state.value.cancel_result + if (progress.stopped) use_theories_state.change(_.cancel_result) else { check_count += 1 - check_result_state(check_limit > 0 && check_count > check_limit) + check_state(check_limit > 0 && check_count > check_limit) } } } @@ -210,12 +299,9 @@ val delay_commit_clean = Standard_Thread.delay_first(commit_cleanup_delay max Time.zero) { - val clean = use_theories_state.value.already_committed.keySet - resources.clean_theories(session, id, clean) + resources.clean_theories(session, id, use_theories_state.value.clean) } - val dep_theories_set = dep_theories.toSet - Session.Consumer[Session.Commands_Changed](getClass.getName) { case changed => if (changed.nodes.exists(dep_theories_set)) { @@ -251,7 +337,7 @@ theory_progress.foreach(progress.theory(_)) - check_result_state() + check_state() if (commit.isDefined && commit_cleanup_delay > Time.zero) { if (use_theories_state.value.finished_result) @@ -264,9 +350,8 @@ try { session.commands_changed += consumer - resources.load_theories( - session, id, dep_theories, dep_files, unicode_symbols, share_common_data, progress) - use_theories_state.value.await_result + check_state() + use_theories_state.guarded_access(_.join_result) check_progress.cancel } finally { @@ -274,7 +359,7 @@ resources.unload_theories(session, id, dep_theories) } - use_theories_state.value.join_result + Exn.release(use_theories_state.guarded_access(_.join_result)) } def purge_theories( @@ -393,13 +478,10 @@ /* theories */ - lazy val theory_graph: Graph[Document.Node.Name, Unit] = - { - val entries = + lazy val theory_graph: Document.Theory_Graph[Unit] = + Document.theory_graph( for ((name, theory) <- theories.toList) - yield ((name, ()), theory.node_header.imports.filter(theories.isDefinedAt(_))) - Graph.make(entries, symmetric = true)(Document.Node.Name.Theory_Ordering) - } + yield ((name, ()), theory.node_header.imports.filter(theories.isDefinedAt(_)))) def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name) @@ -424,13 +506,13 @@ copy(theories = theories -- remove) } - def unload_theories(session: Session, id: UUID.T, dep_theories: List[Document.Node.Name]) + def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]) : State = { - val st1 = remove_required(id, dep_theories) + val st1 = remove_required(id, theories) val theory_edits = for { - node_name <- dep_theories + node_name <- theories theory <- st1.theories.get(node_name) } yield { @@ -470,7 +552,8 @@ frontier(base1, front ++ add) } } - frontier(theory_graph.maximals.filter(clean), Set.empty) + if (clean.isEmpty) Set.empty + else frontier(theory_graph.maximals.filter(clean), Set.empty) } } } @@ -523,14 +606,14 @@ def load_theories( session: Session, id: UUID.T, - dep_theories: List[Document.Node.Name], - dep_files: List[Document.Node.Name], + theories: List[Document.Node.Name], + files: List[Document.Node.Name], unicode_symbols: Boolean, share_common_data: Boolean, progress: Progress) { val loaded_theories = - for (node_name <- dep_theories) + for (node_name <- theories) yield { val path = node_name.path if (!node_name.is_theory) error("Not a theory file: " + path) @@ -547,7 +630,7 @@ state.change(st => { - val (doc_blobs1, st1) = st.insert_required(id, dep_theories).update_blobs(dep_files) + val (doc_blobs1, st1) = st.insert_required(id, theories).update_blobs(files) val theory_edits = for (theory <- loaded_theories) yield { @@ -557,7 +640,7 @@ (edits, (node_name, theory1)) } val file_edits = - for { node_name <- dep_files if doc_blobs1.changed(node_name) } + for { node_name <- files if doc_blobs1.changed(node_name) } yield st1.blob_edits(node_name, st.blobs.get(node_name)) session.update(doc_blobs1, theory_edits.flatMap(_._1) ::: file_edits.flatten, @@ -566,9 +649,9 @@ }) } - def unload_theories(session: Session, id: UUID.T, dep_theories: List[Document.Node.Name]) + def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]) { - state.change(_.unload_theories(session, id, dep_theories)) + state.change(_.unload_theories(session, id, theories)) } def clean_theories(session: Session, id: UUID.T, clean: Set[Document.Node.Name]) diff -r 93a7a85de312 -r cce7a95f6e0f src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Wed Sep 04 16:34:45 2019 +0100 +++ b/src/Pure/PIDE/resources.scala Wed Sep 04 22:01:19 2019 +0200 @@ -135,12 +135,12 @@ def import_name(info: Sessions.Info, s: String): Document.Node.Name = import_name(info.name, info.dir.implode, s) - def dump_checkpoint(info: Sessions.Info): List[Document.Node.Name] = - for { - (options, thys) <- info.theories + def dump_checkpoints(info: Sessions.Info): Set[Document.Node.Name] = + (for { + (options, thys) <- info.theories.iterator if options.bool("dump_checkpoint") - (thy, _) <- thys - } yield import_name(info, thy) + (thy, _) <- thys.iterator + } yield import_name(info, thy)).toSet def standard_import(base: Sessions.Base, qualifier: String, dir: String, s: String): String = { @@ -338,6 +338,21 @@ case errs => error(cat_lines(errs)) } + lazy val theory_graph: Document.Theory_Graph[Unit] = + { + val regular = theories.toSet + val irregular = + (for { + entry <- entries.iterator + imp <- entry.header.imports + if !regular(imp) + } yield imp).toSet + + Document.theory_graph( + irregular.toList.map(name => ((name, ()), Nil)) ::: + entries.map(entry => ((entry.name, ()), entry.header.imports))) + } + lazy val loaded_theories: Graph[String, Outer_Syntax] = (session_base.loaded_theories /: entries)({ case (graph, entry) => val name = entry.name.theory diff -r 93a7a85de312 -r cce7a95f6e0f src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Wed Sep 04 16:34:45 2019 +0100 +++ b/src/Pure/Thy/sessions.scala Wed Sep 04 22:01:19 2019 +0200 @@ -119,13 +119,10 @@ def theory_names: List[Document.Node.Name] = theories.iterator.map(p => p._2.name).toList - lazy val theory_graph: Graph[Document.Node.Name, Unit] = - { - val entries = + lazy val theory_graph: Document.Theory_Graph[Unit] = + Document.theory_graph( for ((_, entry) <- theories.toList) - yield ((entry.name, ()), entry.header.imports.map(imp => theories(imp.theory).name)) - Graph.make(entries, symmetric = true)(Document.Node.Name.Theory_Ordering) - } + yield ((entry.name, ()), entry.header.imports.map(imp => theories(imp.theory).name))) def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] = { @@ -148,7 +145,7 @@ global_theories: Map[String, String] = Map.empty, loaded_theories: Graph[String, Outer_Syntax] = Graph.string, used_theories: List[((Document.Node.Name, Options), List[Document.Node.Name])] = Nil, - dump_checkpoint: List[Document.Node.Name] = Nil, + dump_checkpoints: Set[Document.Node.Name] = Set.empty, known: Known = Known.empty, overall_syntax: Outer_Syntax = Outer_Syntax.empty, imported_sources: List[(Path, SHA1.Digest)] = Nil, @@ -201,40 +198,40 @@ def imported_sources(name: String): List[SHA1.Digest] = session_bases(name).imported_sources.map(_._2) - def dump_checkpoint: List[Document.Node.Name] = + def dump_checkpoints: Set[Document.Node.Name] = (for { (_, base) <- session_bases.iterator - name <- base.dump_checkpoint.iterator - } yield name).toList + name <- base.dump_checkpoints.iterator + } yield name).toSet - def used_theories_condition(default_options: Options, progress: Progress = No_Progress) - : Graph[Document.Node.Name, Options] = + def used_theories_condition( + default_options: Options, progress: Progress = No_Progress): Document.Theory_Graph[Options] = { val default_skip_proofs = default_options.bool("skip_proofs") - val used = - for { - session_name <- sessions_structure.build_topological_order - entry @ ((name, options), _) <- session_bases(session_name).used_theories - if { - def warn(msg: String): Unit = - progress.echo_warning("Skipping theory " + name + " (" + msg + ")") + Document.theory_graph( + permissive = true, + entries = + for { + session_name <- sessions_structure.build_topological_order + entry @ ((name, options), _) <- session_bases(session_name).used_theories + if { + def warn(msg: String): Unit = + progress.echo_warning("Skipping theory " + name + " (" + msg + ")") - val conditions = - space_explode(',', options.string("condition")). - filter(cond => Isabelle_System.getenv(cond) == "") - if (conditions.nonEmpty) { - warn("undefined " + conditions.mkString(", ")) - false + val conditions = + space_explode(',', options.string("condition")). + filter(cond => Isabelle_System.getenv(cond) == "") + if (conditions.nonEmpty) { + warn("undefined " + conditions.mkString(", ")) + false + } + else if (default_skip_proofs && !options.bool("skip_proofs")) { + warn("option skip_proofs") + false + } + else true } - else if (default_skip_proofs && !options.bool("skip_proofs")) { - warn("option skip_proofs") - false - } - else true - } - } yield entry - Graph.make[Document.Node.Name, Options](used, symmetric = true, permissive = true)( - Document.Node.Name.Theory_Ordering) + } yield entry) } def sources(name: String): List[SHA1.Digest] = @@ -311,7 +308,7 @@ val dependencies = resources.session_dependencies(info) - val dump_checkpoint = resources.dump_checkpoint(info) + val dump_checkpoints = resources.dump_checkpoints(info) val overall_syntax = dependencies.overall_syntax @@ -393,7 +390,7 @@ global_theories = global_theories, loaded_theories = dependencies.loaded_theories, used_theories = used_theories, - dump_checkpoint = dump_checkpoint, + dump_checkpoints = dump_checkpoints, known = known, overall_syntax = overall_syntax, imported_sources = check_sources(imported_files), diff -r 93a7a85de312 -r cce7a95f6e0f src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Wed Sep 04 16:34:45 2019 +0100 +++ b/src/Pure/Tools/dump.scala Wed Sep 04 22:01:19 2019 +0200 @@ -206,24 +206,16 @@ } - // run + // synchronous body try { - val dump_checkpoint = deps.dump_checkpoint.toSet - def commit(snapshot: Document.Snapshot, status: Document_Status.Node_Status) - { - if (dump_checkpoint(snapshot.node_name)) { - session.protocol_command("ML_Heap.share_common_data") - } - Consumer.apply(snapshot, status) - } - val use_theories_result = session.use_theories(used_theories.map(_.theory), unicode_symbols = unicode_symbols, share_common_data = true, progress = progress, - commit = Some(commit _)) + checkpoints = deps.dump_checkpoints, + commit = Some(Consumer.apply _)) val bad_theories = Consumer.shutdown() val bad_msgs =