--- a/etc/options Fri Dec 28 19:00:25 2018 +0100
+++ b/etc/options Fri Dec 28 19:06:33 2018 +0100
@@ -144,7 +144,7 @@
-- "ML process command prefix (process policy)"
-section "Editor Reactivity"
+section "Editor Session"
public option editor_load_delay : real = 0.5
-- "delay for file load operations (new buffers etc.)"
@@ -195,6 +195,24 @@
-- "dynamic presentation while editing"
+section "Headless Session"
+
+option headless_check_delay : real = 0.5
+ -- "delay for theory status check during PIDE processing (seconds)"
+
+option headless_check_limit : int = 0
+ -- "maximum number of theory status checks (0 = unlimited)"
+
+option headless_nodes_status_delay : real = -1
+ -- "delay for overall nodes status check during PIDE processing (seconds, disabled for < 0)"
+
+option headless_watchdog_timeout : real = 600
+ -- "watchdog timeout for PIDE processing of broken theories (seconds, 0 = disabled)"
+
+option headless_commit_cleanup_delay : real = 60
+ -- "delay for cleanup of already imported theories (seconds, 0 = disabled)"
+
+
section "Miscellaneous Tools"
public option find_theorems_limit : int = 40
--- a/src/Pure/PIDE/headless.scala Fri Dec 28 19:00:25 2018 +0100
+++ b/src/Pure/PIDE/headless.scala Fri Dec 28 19:06:33 2018 +0100
@@ -84,18 +84,21 @@
(nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok })
}
- val default_check_delay = Time.seconds(0.5)
- val default_nodes_status_delay = Time.seconds(-1.0)
- val default_commit_cleanup_delay = Time.seconds(60.0)
- val default_watchdog_timeout = Time.seconds(600.0)
+ class Session private[Headless](
+ session_name: String,
+ _session_options: => Options,
+ override val resources: Resources) extends isabelle.Session(_session_options, resources)
+ {
+ session =>
- class Session private[Headless](
- session_name: String,
- session_options: Options,
- override val resources: Resources) extends isabelle.Session(session_options, resources)
- {
- session =>
+ /* options */
+
+ def default_check_delay: Time = session_options.seconds("headless_check_delay")
+ def default_check_limit: Int = session_options.int("headless_check_limit")
+ def default_nodes_status_delay: Time = session_options.seconds("headless_nodes_status_delay")
+ def default_watchdog_timeout: Time = session_options.seconds("headless_watchdog_timeout")
+ def default_commit_cleanup_delay: Time = session_options.seconds("headless_commit_cleanup_delay")
/* temporary directory */
@@ -190,7 +193,7 @@
qualifier: String = Sessions.DRAFT,
master_dir: String = "",
check_delay: Time = default_check_delay,
- check_limit: Int = 0,
+ check_limit: Int = default_check_limit,
watchdog_timeout: Time = default_watchdog_timeout,
nodes_status_delay: Time = default_nodes_status_delay,
id: UUID.T = UUID.random(),
--- a/src/Pure/Thy/sessions.scala Fri Dec 28 19:00:25 2018 +0100
+++ b/src/Pure/Thy/sessions.scala Fri Dec 28 19:06:33 2018 +0100
@@ -660,6 +660,8 @@
val build_graph: Graph[String, Info],
val imports_graph: Graph[String, Info])
{
+ sessions_structure =>
+
def build_graph_display: Graph_Display.Graph = Graph_Display.make_graph(build_graph)
def imports_graph_display: Graph_Display.Graph = Graph_Display.make_graph(imports_graph)
@@ -737,13 +739,48 @@
new Structure(restrict(build_graph), restrict(imports_graph))
}
- def selection_deps(sel: Selection,
+ def selection_deps(
+ options: Options,
+ selection: Selection,
progress: Progress = No_Progress,
+ uniform_session: Boolean = false,
+ loading_sessions: Boolean = false,
inlined_files: Boolean = false,
verbose: Boolean = false): Deps =
{
- Sessions.deps(selection(sel), global_theories,
- progress = progress, inlined_files = inlined_files, verbose = verbose)
+ val selection1 =
+ if (uniform_session) {
+ val sessions_structure1 = sessions_structure.selection(selection)
+
+ val default_record_proofs = options.int("record_proofs")
+ val sessions_record_proofs =
+ for {
+ name <- sessions_structure1.build_topological_order
+ info <- sessions_structure1.get(name)
+ if info.options.int("record_proofs") > default_record_proofs
+ } yield name
+
+ val excluded =
+ for (name <- sessions_structure1.build_descendants(sessions_record_proofs))
+ yield {
+ progress.echo_warning("Skipping session " + name + " (option record_proofs)")
+ name
+ }
+
+ selection.copy(exclude_sessions = excluded ::: selection.exclude_sessions)
+ }
+ else selection
+
+ val deps =
+ Sessions.deps(sessions_structure.selection(selection1), global_theories,
+ progress = progress, inlined_files = inlined_files, verbose = verbose)
+
+ if (loading_sessions) {
+ val selection_size = deps.sessions_structure.build_graph.size
+ if (selection_size > 1) progress.echo("Loading " + selection_size + " sessions ...")
+ }
+
+ deps
}
def build_selection(sel: Selection): List[String] = selected(build_graph, sel)
--- a/src/Pure/Tools/dump.scala Fri Dec 28 19:00:25 2018 +0100
+++ b/src/Pure/Tools/dump.scala Fri Dec 28 19:06:33 2018 +0100
@@ -39,7 +39,7 @@
override def toString: String = name
}
- val known_aspects =
+ val known_aspects: List[Aspect] =
List(
Aspect("markup", "PIDE markup (YXML format)",
{ case args =>
@@ -73,43 +73,22 @@
error("Unknown aspect " + quote(name))
- /* dump */
-
- val default_output_dir: Path = Path.explode("dump")
+ /* session */
- def make_options(options: Options, aspects: List[Aspect]): Options =
- {
- val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options
- val options1 =
- options0 + "completion_limit=0" + "ML_statistics=false" +
- "parallel_proofs=0" + "editor_tracing_messages=0"
- (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
- }
-
- def dump(options: Options, logic: String,
- aspects: List[Aspect] = Nil,
+ def session(dump_options: Options, logic: String,
+ consume: (Sessions.Deps, Document.Snapshot, Document_Status.Node_Status) => Unit,
progress: Progress = No_Progress,
log: Logger = No_Logger,
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
- output_dir: Path = default_output_dir,
- verbose: Boolean = false,
- commit_cleanup_delay: Time = Headless.default_commit_cleanup_delay,
- watchdog_timeout: Time = Headless.default_watchdog_timeout,
system_mode: Boolean = false,
selection: Sessions.Selection = Sessions.Selection.empty): Boolean =
{
- if (Build.build_logic(options, logic, build_heap = true, progress = progress,
- dirs = dirs ::: select_dirs, system_mode = system_mode) != 0) error(logic + " FAILED")
-
- val dump_options = make_options(options, aspects)
-
-
/* dependencies */
val deps =
Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs).
- selection_deps(selection)
+ selection_deps(dump_options, selection, uniform_session = true, loading_sessions = true)
val include_sessions =
deps.sessions_structure.imports_topological_order
@@ -130,11 +109,7 @@
consume = (args: (Document.Snapshot, Document_Status.Node_Status)) =>
{
val (snapshot, node_status) = args
- if (node_status.ok) {
- val aspect_args =
- Aspect_Args(dump_options, progress, deps, output_dir, snapshot, node_status)
- aspects.foreach(_.operation(aspect_args))
- }
+ if (node_status.ok) consume(deps, snapshot, node_status)
else {
consumer_ok.change(_ => false)
for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree)) {
@@ -156,18 +131,14 @@
}
- /* session */
+ /* run session */
val session =
Headless.start_session(dump_options, logic, session_dirs = dirs ::: select_dirs,
include_sessions = include_sessions, progress = progress, log = log)
val use_theories_result =
- session.use_theories(use_theories,
- progress = progress,
- commit = Some(Consumer.apply _),
- commit_cleanup_delay = commit_cleanup_delay,
- watchdog_timeout = watchdog_timeout)
+ session.use_theories(use_theories, progress = progress, commit = Some(Consumer.apply _))
session.stop()
@@ -182,6 +153,48 @@
}
+ /* dump */
+
+ val default_output_dir: Path = Path.explode("dump")
+
+ def make_options(options: Options, aspects: List[Aspect] = Nil): Options =
+ {
+ val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options
+ val options1 =
+ options0 + "completion_limit=0" + "ML_statistics=false" +
+ "parallel_proofs=0" + "editor_tracing_messages=0"
+ (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
+ }
+
+ def dump(options: Options, logic: String,
+ aspects: List[Aspect] = Nil,
+ progress: Progress = No_Progress,
+ log: Logger = No_Logger,
+ dirs: List[Path] = Nil,
+ select_dirs: List[Path] = Nil,
+ output_dir: Path = default_output_dir,
+ system_mode: Boolean = false,
+ selection: Sessions.Selection = Sessions.Selection.empty): Boolean =
+ {
+ if (Build.build_logic(options, logic, build_heap = true, progress = progress,
+ dirs = dirs ::: select_dirs, system_mode = system_mode) != 0) error(logic + " FAILED")
+
+ val dump_options = make_options(options, aspects)
+
+ def consume(
+ deps: Sessions.Deps,
+ snapshot: Document.Snapshot,
+ node_status: Document_Status.Node_Status)
+ {
+ val aspect_args = Aspect_Args(dump_options, progress, deps, output_dir, snapshot, node_status)
+ aspects.foreach(_.operation(aspect_args))
+ }
+
+ session(dump_options, logic, consume _,
+ progress = progress, log = log, dirs = dirs, select_dirs = select_dirs, selection = selection)
+ }
+
+
/* Isabelle tool wrapper */
val isabelle_tool =
@@ -189,11 +202,9 @@
{
var aspects: List[Aspect] = known_aspects
var base_sessions: List[String] = Nil
- var commit_cleanup_delay = Headless.default_commit_cleanup_delay
var select_dirs: List[Path] = Nil
var output_dir = default_output_dir
var requirements = false
- var watchdog_timeout = Headless.default_watchdog_timeout
var exclude_session_groups: List[String] = Nil
var all_sessions = false
var dirs: List[Path] = Nil
@@ -210,13 +221,9 @@
Options are:
-A NAMES dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
-B NAME include session NAME and all descendants
- -C SECONDS delay for cleaning of already dumped theories (0 = disabled, default: """ +
- Value.Seconds(Headless.default_commit_cleanup_delay) + """)
-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
- -W SECONDS watchdog timeout for PIDE processing (0 = disabled, default: """ +
- Value.Seconds(Headless.default_watchdog_timeout) + """)
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
-d DIR include session directory
@@ -232,11 +239,9 @@
""" + 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:" -> (arg => commit_cleanup_delay = Value.Seconds.parse(arg)),
"D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
"O:" -> (arg => output_dir = Path.explode(arg)),
"R" -> (_ => requirements = true),
- "W:" -> (arg => watchdog_timeout = Value.Seconds.parse(arg)),
"X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
"a" -> (_ => all_sessions = true),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
@@ -259,9 +264,6 @@
dirs = dirs,
select_dirs = select_dirs,
output_dir = output_dir,
- commit_cleanup_delay = commit_cleanup_delay,
- watchdog_timeout = watchdog_timeout,
- verbose = verbose,
selection = Sessions.Selection(
requirements = requirements,
all_sessions = all_sessions,
--- a/src/Pure/Tools/imports.scala Fri Dec 28 19:00:25 2018 +0100
+++ b/src/Pure/Tools/imports.scala Fri Dec 28 19:06:33 2018 +0100
@@ -101,7 +101,7 @@
{
val deps =
Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs).
- selection_deps(selection, progress = progress, verbose = verbose).check_errors
+ selection_deps(options, selection, progress = progress, verbose = verbose).check_errors
val root_keywords = Sessions.root_syntax.keywords
--- a/src/Pure/Tools/server_commands.scala Fri Dec 28 19:00:25 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala Fri Dec 28 19:06:33 2018 +0100
@@ -158,10 +158,11 @@
pretty_margin: Double = Pretty.default_margin,
unicode_symbols: Boolean = false,
export_pattern: String = "",
- check_delay: Time = Headless.default_check_delay,
- check_limit: Int = 0,
- watchdog_timeout: Time = Headless.default_watchdog_timeout,
- nodes_status_delay: Time = Headless.default_nodes_status_delay)
+ 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 {
@@ -171,18 +172,17 @@
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_default(json, "check_delay", Headless.default_check_delay)
- check_limit <- JSON.int_default(json, "check_limit")
- watchdog_timeout <-
- JSON.seconds_default(json, "watchdog_timeout", Headless.default_watchdog_timeout)
- nodes_status_delay <-
- JSON.seconds_default(json, "nodes_status_delay", Headless.default_nodes_status_delay)
+ 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)
+ nodes_status_delay = nodes_status_delay, commit_cleanup_delay = commit_cleanup_delay)
}
def command(args: Args,
@@ -192,9 +192,12 @@
{
val result =
session.use_theories(args.theories, master_dir = args.master_dir,
- check_delay = args.check_delay, check_limit = args.check_limit,
- watchdog_timeout = args.watchdog_timeout,
- nodes_status_delay = args.nodes_status_delay,
+ 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 =