# HG changeset patch # User wenzelm # Date 1546020393 -3600 # Node ID 8e7134f1f5853921023b406c5bb0bc2251d520be # Parent 0563419bf022c8388b3ca280ccde0a79255e4f2e# Parent fa94f2b2a8775c310bd190f0f156c9d2a16102ab merged; diff -r 0563419bf022 -r 8e7134f1f585 etc/options --- 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 diff -r 0563419bf022 -r 8e7134f1f585 src/Pure/PIDE/headless.scala --- 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(), diff -r 0563419bf022 -r 8e7134f1f585 src/Pure/Thy/sessions.scala --- 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) diff -r 0563419bf022 -r 8e7134f1f585 src/Pure/Tools/dump.scala --- 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, diff -r 0563419bf022 -r 8e7134f1f585 src/Pure/Tools/imports.scala --- 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 diff -r 0563419bf022 -r 8e7134f1f585 src/Pure/Tools/server_commands.scala --- 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 =