--- a/etc/options Mon Oct 07 14:31:46 2019 +0200
+++ b/etc/options Mon Oct 07 15:04:18 2019 +0200
@@ -225,9 +225,6 @@
option headless_load_limit : int = 100
-- "limit for loaded theories (0 = unlimited)"
-option dump_checkpoint : bool = false
- -- "mark individual theories to share common data in ML"
-
section "Miscellaneous Tools"
--- a/src/Doc/System/Sessions.thy Mon Oct 07 14:31:46 2019 +0200
+++ b/src/Doc/System/Sessions.thy Mon Oct 07 15:04:18 2019 +0200
@@ -546,7 +546,6 @@
Options are:
-A NAMES dump named aspects (default: ...)
-B NAME include session NAME and all descendants
- -C observe option dump_checkpoint for theories
-D DIR include session directory and select its sessions
-O DIR output directory for dumped files (default: "dump")
-R operate on requirements of selected sessions
@@ -583,11 +582,6 @@
\<^verbatim>\<open>isabelle.Dump.dump()\<close> takes aspects as user-defined operations on the
final PIDE state and document version. This allows to imitate Prover IDE
rendering under program control.
-
- \<^medskip> Option \<^verbatim>\<open>-C\<close> observes option \<^verbatim>\<open>dump_checkpoint\<close> within the
- \isakeyword{theories} specification of session ROOT definitions. This helps
- to structure the load process of large collections of theories, and thus
- reduce overall resource requirements.
\<close>
--- a/src/HOL/ROOT Mon Oct 07 14:31:46 2019 +0200
+++ b/src/HOL/ROOT Mon Oct 07 15:04:18 2019 +0200
@@ -6,9 +6,8 @@
"
options [strict_facts]
directories "../Tools"
- theories [dump_checkpoint]
+ theories
Main (global)
- theories
Complex_Main (global)
document_files
"root.bib"
--- a/src/Pure/General/graph.scala Mon Oct 07 14:31:46 2019 +0200
+++ b/src/Pure/General/graph.scala Mon Oct 07 15:04:18 2019 +0200
@@ -112,20 +112,25 @@
/* reachability */
/*reachable nodes with length of longest path*/
- def reachable_length(next: Key => Keys, xs: List[Key]): Map[Key, Int] =
+ def reachable_length(
+ count: Key => Int,
+ next: Key => Keys,
+ xs: List[Key]): Map[Key, Int] =
{
def reach(length: Int)(rs: Map[Key, Int], x: Key): Map[Key, Int] =
if (rs.get(x) match { case Some(n) => n >= length case None => false }) rs
- else ((rs + (x -> length)) /: next(x))(reach(length + 1))
+ else ((rs + (x -> length)) /: next(x))(reach(length + count(x)))
(Map.empty[Key, Int] /: xs)(reach(0))
}
- def node_height: Map[Key, Int] = reachable_length(imm_preds(_), maximals)
- def node_depth: Map[Key, Int] = reachable_length(imm_succs(_), minimals)
+ def node_height(count: Key => Int): Map[Key, Int] =
+ reachable_length(count, imm_preds(_), maximals)
+ def node_depth(count: Key => Int): Map[Key, Int] =
+ reachable_length(count, imm_succs(_), minimals)
/*reachable nodes with size limit*/
def reachable_limit(
limit: Int,
- count: Key => Boolean,
+ count: Key => Int,
next: Key => Keys,
xs: List[Key]): Keys =
{
@@ -133,7 +138,7 @@
{
val (n, rs) = res
if (rs.contains(x)) res
- else ((if (count(x)) n + 1 else n, rs + x) /: next(x))(reach _)
+ else ((n + count(x), rs + x) /: next(x))(reach _)
}
@tailrec def reachs(size: Int, rs: Keys, rest: List[Key]): Keys =
--- a/src/Pure/PIDE/headless.scala Mon Oct 07 14:31:46 2019 +0200
+++ b/src/Pure/PIDE/headless.scala Mon Oct 07 15:04:18 2019 +0200
@@ -44,82 +44,35 @@
(nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok })
}
- private type Load = (List[Document.Node.Name], Boolean)
- private val no_load: Load = (Nil, false)
+ private object Load_State
+ {
+ def finished: Load_State = Load_State(Nil, Nil, 0)
+ }
- private sealed abstract class Load_State
+ private case class Load_State(
+ pending: List[Document.Node.Name], rest: List[Document.Node.Name], load_limit: Int)
{
def next(
- limit: Int,
dep_graph: Document.Node.Name.Graph[Unit],
- finished: Document.Node.Name => Boolean): (Load, Load_State) =
+ finished: Document.Node.Name => Boolean): (List[Document.Node.Name], Load_State) =
{
- def make_pending(maximals: List[Document.Node.Name]): List[Document.Node.Name] =
+ def load_requirements(pending1: List[Document.Node.Name], rest1: List[Document.Node.Name])
+ : (List[Document.Node.Name], Load_State) =
{
- val pending = maximals.filterNot(finished)
- if (pending.isEmpty || pending.tail.isEmpty) pending
- else {
- val depth = dep_graph.node_depth
- pending.sortBy(node => - depth(node))
- }
+ val load_theories = dep_graph.all_preds(pending1).reverse.filterNot(finished)
+ (load_theories, Load_State(pending1, rest1, load_limit))
}
- def load_checkpoints(checkpoints: List[Document.Node.Name]): (Load, Load_State) =
- Load_Init(checkpoints).next(limit, dep_graph, finished)
-
- def load_requirements(
- pending: List[Document.Node.Name],
- checkpoints: List[Document.Node.Name] = Nil,
- share_common_data: Boolean = false): (Load, Load_State) =
- {
- if (pending.isEmpty) load_checkpoints(checkpoints)
- else if (limit == 0) {
- val requirements = dep_graph.all_preds(pending).reverse
- ((requirements, share_common_data), Load_Bulk(pending, Nil, checkpoints))
- }
- else {
- def count(node: Document.Node.Name): Boolean = !finished(node)
- val reachable = dep_graph.reachable_limit(limit, count _, dep_graph.imm_preds, pending)
- val (pending1, pending2) = pending.partition(reachable)
- val requirements = dep_graph.all_preds(pending1).reverse
- ((requirements, share_common_data), Load_Bulk(pending1, pending2, checkpoints))
- }
+ if (!pending.forall(finished)) (Nil, this)
+ else if (rest.isEmpty) (Nil, Load_State.finished)
+ else if (load_limit == 0) load_requirements(rest, Nil)
+ else {
+ val reachable = dep_graph.reachable_limit(load_limit, _ => 1, dep_graph.imm_preds, rest)
+ val (pending1, rest1) = rest.partition(reachable)
+ load_requirements(pending1, rest1)
}
-
- val result: (Load, Load_State) =
- this match {
- case Load_Init(Nil) =>
- val pending = make_pending(dep_graph.maximals)
- if (pending.isEmpty) (no_load, Load_Finished)
- else load_requirements(pending)
- case Load_Init(target :: checkpoints) =>
- val requirements = dep_graph.all_preds(List(target)).reverse
- ((requirements, false), Load_Target(target, checkpoints))
- case Load_Target(pending, checkpoints) if finished(pending) =>
- val dep_graph1 =
- if (checkpoints.isEmpty) dep_graph
- else dep_graph.exclude(dep_graph.all_succs(checkpoints).toSet)
- val dep_graph2 =
- dep_graph1.restrict(dep_graph.all_succs(List(pending)).toSet)
- val pending2 = make_pending(dep_graph.maximals.filter(dep_graph2.defined))
- load_requirements(pending2, checkpoints = checkpoints, share_common_data = true)
- case Load_Bulk(pending, remaining, checkpoints) if pending.forall(finished) =>
- load_requirements(remaining, checkpoints = checkpoints)
- case st => (no_load, st)
- }
-
- val ((load_theories, share_common_data), st1) = result
- ((load_theories.filterNot(finished), share_common_data), st1)
}
}
- private case class Load_Init(checkpoints: List[Document.Node.Name]) extends Load_State
- private case class Load_Target(
- pending: Document.Node.Name, checkpoints: List[Document.Node.Name]) extends Load_State
- private case class Load_Bulk(
- pending: List[Document.Node.Name],
- remaining: List[Document.Node.Name],
- checkpoints: List[Document.Node.Name]) extends Load_State
- private case object Load_Finished extends Load_State
class Session private[Headless](
session_name: String,
@@ -144,12 +97,6 @@
def default_watchdog_timeout: Time = session_options.seconds("headless_watchdog_timeout")
def default_commit_cleanup_delay: Time = session_options.seconds("headless_commit_cleanup_delay")
- def load_limit: Int =
- {
- val limit = session_options.int("headless_load_limit")
- if (limit == 0) Integer.MAX_VALUE else limit
- }
-
/* temporary directory */
@@ -225,7 +172,7 @@
}
def check(state: Document.State, version: Document.Version, beyond_limit: Boolean)
- : ((List[Document.Node.Name], Boolean), Use_Theories_State) =
+ : (List[Document.Node.Name], Use_Theories_State) =
{
val already_committed1 =
commit match {
@@ -273,9 +220,9 @@
}
else result
- val (load, load_state1) = load_state.next(load_limit, dep_graph, finished_theory(_))
+ val (load_theories, load_state1) = load_state.next(dep_graph, finished_theory(_))
- (load,
+ (load_theories,
copy(already_committed = already_committed1, result = result1, load_state = load_state1))
}
}
@@ -290,7 +237,6 @@
watchdog_timeout: Time = default_watchdog_timeout,
nodes_status_delay: Time = default_nodes_status_delay,
id: UUID.T = UUID.random(),
- 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,
@@ -311,25 +257,29 @@
val use_theories_state =
{
- val load_state =
- Load_Init(
- if (checkpoints.isEmpty) Nil
- else dependencies.theory_graph.topological_order.filter(checkpoints(_)))
- Synchronized(
- Use_Theories_State(dependencies.theory_graph, load_state, watchdog_timeout, commit))
+ val dep_graph = dependencies.theory_graph
+
+ val maximals = dep_graph.maximals
+ val rest =
+ if (maximals.isEmpty || maximals.tail.isEmpty) maximals
+ else {
+ val depth = dep_graph.node_depth(_ => 1)
+ maximals.sortBy(node => - depth(node))
+ }
+ val load_limit = if (commit.isDefined) session_options.int("headless_load_limit") else 0
+ val load_state = Load_State(Nil, rest, load_limit)
+
+ Synchronized(Use_Theories_State(dep_graph, load_state, watchdog_timeout, commit))
}
def check_state(beyond_limit: Boolean = false)
{
val state = session.get_state()
- for (version <- state.stable_tip_version) {
- val (load_theories, share_common_data) =
- 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)
- }
- }
+ for {
+ version <- state.stable_tip_version
+ 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, progress)
}
val check_progress =
@@ -649,7 +599,6 @@
theories: List[Document.Node.Name],
files: List[Document.Node.Name],
unicode_symbols: Boolean,
- share_common_data: Boolean,
progress: Progress)
{
val loaded_theories =
@@ -683,8 +632,7 @@
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,
- share_common_data = share_common_data)
+ session.update(doc_blobs1, theory_edits.flatMap(_._1) ::: file_edits.flatten)
st1.update_theories(theory_edits.map(_._2))
})
}
--- a/src/Pure/PIDE/resources.scala Mon Oct 07 14:31:46 2019 +0200
+++ b/src/Pure/PIDE/resources.scala Mon Oct 07 15:04:18 2019 +0200
@@ -165,13 +165,6 @@
} yield theory_node
}
- def dump_checkpoints(info: Sessions.Info): Set[Document.Node.Name] =
- (for {
- (options, thys) <- info.theories.iterator
- if options.bool("dump_checkpoint")
- (thy, _) <- thys.iterator
- } yield import_name(info, thy)).toSet
-
def complete_import_name(context_name: Document.Node.Name, s: String): List[String] =
{
val context_session = session_base.theory_qualifier(context_name)
@@ -262,10 +255,8 @@
previous: Document.Version,
doc_blobs: Document.Blobs,
edits: List[Document.Edit_Text],
- consolidate: List[Document.Node.Name],
- share_common_data: Boolean): Session.Change =
- Thy_Syntax.parse_change(
- resources, reparse_limit, previous, doc_blobs, edits, consolidate, share_common_data)
+ consolidate: List[Document.Node.Name]): Session.Change =
+ Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate)
def commit(change: Session.Change) { }
--- a/src/Pure/PIDE/session.scala Mon Oct 07 14:31:46 2019 +0200
+++ b/src/Pure/PIDE/session.scala Mon Oct 07 15:04:18 2019 +0200
@@ -53,7 +53,6 @@
deps_changed: Boolean,
doc_edits: List[Document.Edit_Command],
consolidate: List[Document.Node.Name],
- share_common_data: Boolean,
version: Document.Version)
case object Change_Flush
@@ -65,8 +64,7 @@
case class Statistics(props: Properties.T)
case class Global_Options(options: Options)
case object Caret_Focus
- case class Raw_Edits(
- doc_blobs: Document.Blobs, edits: List[Document.Edit_Text], share_common_data: Boolean)
+ case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
case class Build_Theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
case class Commands_Changed(
@@ -232,17 +230,15 @@
doc_blobs: Document.Blobs,
text_edits: List[Document.Edit_Text],
consolidate: List[Document.Node.Name],
- share_common_data: Boolean,
version_result: Promise[Document.Version])
private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true)
{
- case Text_Edits(previous, doc_blobs, text_edits, consolidate, share_common_data, version_result) =>
+ case Text_Edits(previous, doc_blobs, text_edits, consolidate, version_result) =>
val prev = previous.get_finished
val change =
Timing.timeit("parse_change", timing) {
- resources.parse_change(
- reparse_limit, prev, doc_blobs, text_edits, consolidate, share_common_data)
+ resources.parse_change(reparse_limit, prev, doc_blobs, text_edits, consolidate)
}
version_result.fulfill(change.version)
manager.send(change)
@@ -393,8 +389,7 @@
def handle_raw_edits(
doc_blobs: Document.Blobs = Document.Blobs.empty,
edits: List[Document.Edit_Text] = Nil,
- consolidate: List[Document.Node.Name] = Nil,
- share_common_data: Boolean = false)
+ consolidate: List[Document.Node.Name] = Nil)
//{{{
{
require(prover.defined)
@@ -405,9 +400,8 @@
val version = Future.promise[Document.Version]
global_state.change(_.continue_history(previous, edits, version))
- raw_edits.post(Session.Raw_Edits(doc_blobs, edits, share_common_data))
- change_parser.send(
- Text_Edits(previous, doc_blobs, edits, consolidate, share_common_data, version))
+ raw_edits.post(Session.Raw_Edits(doc_blobs, edits))
+ change_parser.send(Text_Edits(previous, doc_blobs, edits, consolidate, version))
}
//}}}
@@ -419,10 +413,6 @@
{
require(prover.defined)
- if (change.share_common_data) {
- prover.get.protocol_command("ML_Heap.share_common_data")
- }
-
// define commands
{
val id_commands = new mutable.ListBuffer[Command]
@@ -636,9 +626,8 @@
case Cancel_Exec(exec_id) if prover.defined =>
prover.get.cancel_exec(exec_id)
- case Session.Raw_Edits(doc_blobs, edits, share_common_data) if prover.defined =>
- handle_raw_edits(doc_blobs = doc_blobs, edits = edits,
- share_common_data = share_common_data)
+ case Session.Raw_Edits(doc_blobs, edits) if prover.defined =>
+ handle_raw_edits(doc_blobs = doc_blobs, edits = edits)
case Session.Dialog_Result(id, serial, result) if prover.defined =>
prover.get.dialog_result(serial, result)
@@ -744,12 +733,9 @@
def cancel_exec(exec_id: Document_ID.Exec)
{ manager.send(Cancel_Exec(exec_id)) }
- def update(
- doc_blobs: Document.Blobs,
- edits: List[Document.Edit_Text],
- share_common_data: Boolean = false)
+ def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
{
- if (edits.nonEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits, share_common_data))
+ if (edits.nonEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits))
}
def update_options(options: Options)
--- a/src/Pure/Thy/sessions.scala Mon Oct 07 14:31:46 2019 +0200
+++ b/src/Pure/Thy/sessions.scala Mon Oct 07 15:04:18 2019 +0200
@@ -54,7 +54,6 @@
global_theories: Map[String, String] = Map.empty,
loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
used_theories: List[(Document.Node.Name, Options)] = Nil,
- dump_checkpoints: Set[Document.Node.Name] = Set.empty,
known_theories: Map[String, Document.Node.Entry] = Map.empty,
known_loaded_files: Map[String, List[Path]] = Map.empty,
overall_syntax: Outer_Syntax = Outer_Syntax.empty,
@@ -98,12 +97,6 @@
def imported_sources(name: String): List[SHA1.Digest] =
session_bases(name).imported_sources.map(_._2)
- def dump_checkpoints: Set[Document.Node.Name] =
- (for {
- (_, base) <- session_bases.iterator
- name <- base.dump_checkpoints.iterator
- } yield name).toSet
-
def used_theories_condition(default_options: Options, progress: Progress = No_Progress)
: List[(Document.Node.Name, Options)] =
{
@@ -219,8 +212,6 @@
val dependencies = resources.session_dependencies(info)
- val dump_checkpoints = resources.dump_checkpoints(info)
-
val overall_syntax = dependencies.overall_syntax
val theory_files = dependencies.theories.map(_.path)
@@ -338,7 +329,6 @@
global_theories = sessions_structure.global_theories,
loaded_theories = dependencies.loaded_theories,
used_theories = used_theories,
- dump_checkpoints = dump_checkpoints,
known_theories = known_theories,
known_loaded_files = known_loaded_files,
overall_syntax = overall_syntax,
--- a/src/Pure/Thy/thy_syntax.scala Mon Oct 07 14:31:46 2019 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Mon Oct 07 15:04:18 2019 +0200
@@ -296,8 +296,7 @@
previous: Document.Version,
doc_blobs: Document.Blobs,
edits: List[Document.Edit_Text],
- consolidate: List[Document.Node.Name],
- share_common_data: Boolean): Session.Change =
+ consolidate: List[Document.Node.Name]): Session.Change =
{
val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)
@@ -358,7 +357,6 @@
}
Session.Change(
- previous, syntax_changed, syntax_changed.nonEmpty, doc_edits,
- consolidate, share_common_data, version)
+ previous, syntax_changed, syntax_changed.nonEmpty, doc_edits, consolidate, version)
}
}
--- a/src/Pure/Tools/dump.scala Mon Oct 07 14:31:46 2019 +0200
+++ b/src/Pure/Tools/dump.scala Mon Oct 07 15:04:18 2019 +0200
@@ -88,7 +88,6 @@
def apply(
options: Options,
logic: String,
- dump_checkpoints: Boolean = false,
aspects: List[Aspect] = Nil,
progress: Progress = No_Progress,
log: Logger = No_Logger,
@@ -96,15 +95,13 @@
select_dirs: List[Path] = Nil,
selection: Sessions.Selection = Sessions.Selection.empty): Session =
{
- new Session(
- options, logic, dump_checkpoints, aspects, progress, log, dirs, select_dirs, selection)
+ new Session(options, logic, aspects, progress, log, dirs, select_dirs, selection)
}
}
class Session private(
options: Options,
logic: String,
- dump_checkpoints: Boolean,
aspects: List[Aspect],
progress: Progress,
log: Logger,
@@ -215,7 +212,6 @@
session.use_theories(used_theories.map(_.theory),
unicode_symbols = unicode_symbols,
progress = progress,
- checkpoints = if (dump_checkpoints) deps.dump_checkpoints else Set.empty,
commit = Some(Consumer.apply _))
val bad_theories = Consumer.shutdown()
@@ -247,7 +243,6 @@
def dump(
options: Options,
logic: String,
- dump_checkpoints: Boolean = false,
aspects: List[Aspect] = Nil,
progress: Progress = No_Progress,
log: Logger = No_Logger,
@@ -257,9 +252,8 @@
selection: Sessions.Selection = Sessions.Selection.empty)
{
val session =
- Session(options, logic, dump_checkpoints = dump_checkpoints, aspects = aspects,
- progress = progress, log = log, dirs = dirs, select_dirs = select_dirs,
- selection = selection)
+ Session(options, logic, aspects = aspects, progress = progress, log = log, dirs = dirs,
+ select_dirs = select_dirs, selection = selection)
session.run((args: Args) =>
{
@@ -280,7 +274,6 @@
var aspects: List[Aspect] = known_aspects
var base_sessions: List[String] = Nil
var select_dirs: List[Path] = Nil
- var dump_checkpoints = false
var output_dir = default_output_dir
var requirements = false
var exclude_session_groups: List[String] = Nil
@@ -298,7 +291,6 @@
Options are:
-A NAMES dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
-B NAME include session NAME and all descendants
- -C observe option dump_checkpoint for theories
-D DIR include session directory and select its sessions
-O DIR output directory for dumped files (default: """ + default_output_dir + """)
-R operate on requirements of selected sessions
@@ -316,7 +308,6 @@
""" + Library.prefix_lines(" ", show_aspects) + "\n",
"A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
"B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
- "C" -> (_ => dump_checkpoints = true),
"D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
"O:" -> (arg => output_dir = Path.explode(arg)),
"R" -> (_ => requirements = true),
@@ -335,7 +326,6 @@
progress.interrupt_handler {
dump(options, logic,
- dump_checkpoints = dump_checkpoints,
aspects = aspects,
progress = progress,
dirs = dirs,