--- 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" +
--- 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))
--- 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 */
--- 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
--- 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])
--- 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
--- 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),
--- 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 =