--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_console.scala Thu Apr 13 12:27:57 2017 +0200
@@ -0,0 +1,135 @@
+/* Title: Pure/ML/ml_console.scala
+ Author: Makarius
+
+The raw ML process in interactive mode.
+*/
+
+package isabelle
+
+
+import java.io.{IOException, BufferedReader, InputStreamReader}
+
+
+object ML_Console
+{
+ /* command line entry point */
+
+ def main(args: Array[String])
+ {
+ Command_Line.tool {
+ var dirs: List[Path] = Nil
+ var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
+ var modes: List[String] = Nil
+ var no_build = false
+ var options = Options.init()
+ var raw_ml_system = false
+ var system_mode = false
+
+ val getopts = Getopts("""
+Usage: isabelle console [OPTIONS]
+
+ Options are:
+ -d DIR include session directory
+ -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
+ -m MODE add print mode for output
+ -n no build of session image on startup
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -r bootstrap from raw Poly/ML
+ -s system build mode for session image
+
+ Build a logic session image and run the raw Isabelle ML process
+ in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" +
+ quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """.
+""",
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "l:" -> (arg => logic = arg),
+ "m:" -> (arg => modes = arg :: modes),
+ "n" -> (arg => no_build = true),
+ "o:" -> (arg => options = options + arg),
+ "r" -> (_ => raw_ml_system = true),
+ "s" -> (_ => system_mode = true))
+
+ val more_args = getopts(args)
+ if (!more_args.isEmpty) getopts.usage()
+
+
+ // build
+ if (!no_build && !raw_ml_system &&
+ !Build.build(options = options, build_heap = true, no_build = true,
+ dirs = dirs, system_mode = system_mode, sessions = List(logic)).ok)
+ {
+ val progress = new Console_Progress()
+ progress.echo("Build started for Isabelle/" + logic + " ...")
+ progress.interrupt_handler {
+ val res =
+ Build.build(options = options, progress = progress, build_heap = true,
+ dirs = dirs, system_mode = system_mode, sessions = List(logic))
+ if (!res.ok) sys.exit(res.rc)
+ }
+ }
+
+ // process loop
+ val process =
+ ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true,
+ modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
+ raw_ml_system = raw_ml_system, store = Sessions.store(system_mode),
+ session_base =
+ if (raw_ml_system) None
+ else Some(Sessions.session_base(options, logic, dirs)))
+ val process_output = Future.thread[Unit]("process_output") {
+ try {
+ var result = new StringBuilder(100)
+ var finished = false
+ while (!finished) {
+ var c = -1
+ var done = false
+ while (!done && (result.length == 0 || process.stdout.ready)) {
+ c = process.stdout.read
+ if (c >= 0) result.append(c.asInstanceOf[Char])
+ else done = true
+ }
+ if (result.length > 0) {
+ System.out.print(result.toString)
+ System.out.flush()
+ result.length = 0
+ }
+ else {
+ process.stdout.close()
+ finished = true
+ }
+ }
+ }
+ catch { case e: IOException => case Exn.Interrupt() => }
+ }
+ val process_input = Future.thread[Unit]("process_input") {
+ val reader = new BufferedReader(new InputStreamReader(System.in))
+ POSIX_Interrupt.handler { process.interrupt } {
+ try {
+ var finished = false
+ while (!finished) {
+ reader.readLine() match {
+ case null =>
+ process.stdin.close()
+ finished = true
+ case line =>
+ process.stdin.write(line)
+ process.stdin.write("\n")
+ process.stdin.flush()
+ }
+ }
+ }
+ catch { case e: IOException => case Exn.Interrupt() => }
+ }
+ }
+ val process_result = Future.thread[Int]("process_result") {
+ val rc = process.join
+ process_input.cancel
+ rc
+ }
+
+ process_output.join
+ process_input.join
+ process_result.join
+ }
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_process.scala Thu Apr 13 12:27:57 2017 +0200
@@ -0,0 +1,194 @@
+/* Title: Pure/ML/ml_process.scala
+ Author: Makarius
+
+The raw ML process.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile}
+
+
+object ML_Process
+{
+ def apply(options: Options,
+ logic: String = "",
+ args: List[String] = Nil,
+ dirs: List[Path] = Nil,
+ modes: List[String] = Nil,
+ raw_ml_system: Boolean = false,
+ cwd: JFile = null,
+ env: Map[String, String] = Isabelle_System.settings(),
+ redirect: Boolean = false,
+ cleanup: () => Unit = () => (),
+ channel: Option[System_Channel] = None,
+ sessions: Option[Sessions.T] = None,
+ session_base: Option[Sessions.Base] = None,
+ store: Sessions.Store = Sessions.store()): Bash.Process =
+ {
+ val logic_name = Isabelle_System.default_logic(logic)
+ val heaps: List[String] =
+ if (raw_ml_system) Nil
+ else {
+ val selection = Sessions.Selection(sessions = List(logic_name))
+ val (_, selected_sessions) =
+ sessions.getOrElse(Sessions.load(options, dirs)).selection(selection)
+ (selected_sessions.build_ancestors(logic_name) ::: List(logic_name)).
+ map(a => File.platform_path(store.heap(a)))
+ }
+
+ val eval_init =
+ if (heaps.isEmpty) {
+ List(
+ """
+ fun chapter (_: string) = ();
+ fun section (_: string) = ();
+ fun subsection (_: string) = ();
+ fun subsubsection (_: string) = ();
+ fun paragraph (_: string) = ();
+ fun subparagraph (_: string) = ();
+ val ML_file = PolyML.use;
+ """,
+ if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6")
+ """
+ structure FixedInt = IntInf;
+ structure RunCall =
+ struct
+ open RunCall
+ val loadWord: word * word -> word =
+ run_call2 RuntimeCalls.POLY_SYS_load_word;
+ val storeWord: word * word * word -> unit =
+ run_call3 RuntimeCalls.POLY_SYS_assign_word;
+ end;
+ """
+ else "",
+ if (Platform.is_windows)
+ "fun exit 0 = OS.Process.exit OS.Process.success" +
+ " | exit 1 = OS.Process.exit OS.Process.failure" +
+ " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
+ else
+ "fun exit rc = Posix.Process.exit (Word8.fromInt rc)",
+ "PolyML.Compiler.prompt1 := \"Poly/ML> \"",
+ "PolyML.Compiler.prompt2 := \"Poly/ML# \"")
+ }
+ else
+ List(
+ "(PolyML.SaveState.loadHierarchy " +
+ ML_Syntax.print_list(ML_Syntax.print_string0)(heaps) +
+ "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
+ ML_Syntax.print_string0(": " + logic_name + "\n") +
+ "); OS.Process.exit OS.Process.failure)")
+
+ val eval_modes =
+ if (modes.isEmpty) Nil
+ else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string0)(modes))
+
+ // options
+ val isabelle_process_options = Isabelle_System.tmp_file("options")
+ File.write(isabelle_process_options, YXML.string_of_body(options.encode))
+ val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
+ val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
+
+ // session base
+ val eval_session_base =
+ session_base match {
+ case None => Nil
+ case Some(base) =>
+ def print_table(table: List[(String, String)]): String =
+ ML_Syntax.print_list(
+ ML_Syntax.print_pair(
+ ML_Syntax.print_string, ML_Syntax.print_string))(table)
+ List("Resources.set_session_base {default_qualifier = \"\"" +
+ ", global_theories = " + print_table(base.global_theories.toList) +
+ ", loaded_theories = " + print_table(base.loaded_theories.toList) +
+ ", known_theories = " + print_table(base.dest_known_theories) + "}")
+ }
+
+ // process
+ val eval_process =
+ if (heaps.isEmpty)
+ List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")))
+ else
+ channel match {
+ case None =>
+ List("Isabelle_Process.init_options ()")
+ case Some(ch) =>
+ List("Isabelle_Process.init_protocol " + ML_Syntax.print_string0(ch.server_name))
+ }
+
+ // ISABELLE_TMP
+ val isabelle_tmp = Isabelle_System.tmp_dir("process")
+ val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp))
+
+ val ml_runtime_options =
+ {
+ val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS"))
+ if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options
+ else ml_options ::: List("--gcthreads", options.int("threads").toString)
+ }
+
+ // bash
+ val bash_args =
+ ml_runtime_options :::
+ (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process).
+ map(eval => List("--eval", eval)).flatten ::: args
+
+ Bash.process(
+ "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
+ Bash.strings(bash_args),
+ cwd = cwd,
+ env =
+ Isabelle_System.library_path(env ++ env_options ++ env_tmp,
+ Isabelle_System.getenv_strict("ML_HOME")),
+ redirect = redirect,
+ cleanup = () =>
+ {
+ isabelle_process_options.delete
+ Isabelle_System.rm_tree(isabelle_tmp)
+ cleanup()
+ })
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args =>
+ {
+ var dirs: List[Path] = Nil
+ var eval_args: List[String] = Nil
+ var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
+ var modes: List[String] = Nil
+ var options = Options.init()
+
+ val getopts = Getopts("""
+Usage: isabelle process [OPTIONS]
+
+ Options are:
+ -T THEORY load theory
+ -d DIR include session directory
+ -e ML_EXPR evaluate ML expression on startup
+ -f ML_FILE evaluate ML file on startup
+ -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
+ -m MODE add print mode for output
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+
+ Run the raw Isabelle ML process in batch mode.
+""",
+ "T:" -> (arg =>
+ eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))),
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
+ "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
+ "l:" -> (arg => logic = arg),
+ "m:" -> (arg => modes = arg :: modes),
+ "o:" -> (arg => options = options + arg))
+
+ val more_args = getopts(args)
+ if (args.isEmpty || !more_args.isEmpty) getopts.usage()
+
+ val rc = ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
+ result().print_stdout.rc
+ sys.exit(rc)
+ })
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_statistics.scala Thu Apr 13 12:27:57 2017 +0200
@@ -0,0 +1,151 @@
+/* Title: Pure/ML/ml_statistics.scala
+ Author: Makarius
+
+ML runtime statistics.
+*/
+
+package isabelle
+
+
+import scala.collection.mutable
+import scala.collection.immutable.{SortedSet, SortedMap}
+import scala.swing.{Frame, Component}
+
+import org.jfree.data.xy.{XYSeries, XYSeriesCollection}
+import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory}
+import org.jfree.chart.plot.PlotOrientation
+
+
+object ML_Statistics
+{
+ /* content interpretation */
+
+ final case class Entry(time: Double, data: Map[String, Double])
+
+ def apply(session_name: String, ml_statistics: List[Properties.T]): ML_Statistics =
+ new ML_Statistics(session_name, ml_statistics)
+
+ val empty = apply("", Nil)
+
+
+ /* standard fields */
+
+ type Fields = (String, Iterable[String])
+
+ val tasks_fields: Fields =
+ ("Future tasks",
+ List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive", "tasks_urgent"))
+
+ val workers_fields: Fields =
+ ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
+
+ val GC_fields: Fields =
+ ("GCs", List("partial_GCs", "full_GCs"))
+
+ val heap_fields: Fields =
+ ("Heap", List("size_heap", "size_allocation", "size_allocation_free",
+ "size_heap_free_last_full_GC", "size_heap_free_last_GC"))
+
+ val threads_fields: Fields =
+ ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar",
+ "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal"))
+
+ val time_fields: Fields =
+ ("Time", List("time_CPU", "time_GC"))
+
+ val speed_fields: Fields =
+ ("Speed", List("speed_CPU", "speed_GC"))
+
+
+ val all_fields: List[Fields] =
+ List(tasks_fields, workers_fields, GC_fields, heap_fields, threads_fields,
+ time_fields, speed_fields)
+
+ val main_fields: List[Fields] =
+ List(tasks_fields, workers_fields, heap_fields)
+}
+
+final class ML_Statistics private(val session_name: String, val ml_statistics: List[Properties.T])
+{
+ val Now = new Properties.Double("now")
+ def now(props: Properties.T): Double = Now.unapply(props).get
+
+ require(ml_statistics.forall(props => Now.unapply(props).isDefined))
+
+ val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head)
+ val duration = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.last) - time_start
+
+ val fields: Set[String] =
+ SortedSet.empty[String] ++
+ (for (props <- ml_statistics.iterator; (x, _) <- props.iterator if x != Now.name)
+ yield x)
+
+ val content: List[ML_Statistics.Entry] =
+ {
+ var last_edge = Map.empty[String, (Double, Double, Double)]
+ val result = new mutable.ListBuffer[ML_Statistics.Entry]
+ for (props <- ml_statistics) {
+ val time = now(props) - time_start
+ require(time >= 0.0)
+
+ // rising edges -- relative speed
+ val speeds =
+ for ((key, value) <- props; a <- Library.try_unprefix("time", key)) yield {
+ val (x0, y0, s0) = last_edge.getOrElse(a, (0.0, 0.0, 0.0))
+
+ val x1 = time
+ val y1 = java.lang.Double.parseDouble(value)
+ val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0)
+
+ val b = ("speed" + a).intern
+ if (y1 > y0) { last_edge += (a -> (x1, y1, s1)); (b, s1) } else (b, s0)
+ }
+
+ val data =
+ SortedMap.empty[String, Double] ++ speeds ++
+ (for ((x, y) <- props.iterator if x != Now.name)
+ yield (x, java.lang.Double.parseDouble(y)))
+ result += ML_Statistics.Entry(time, data)
+ }
+ result.toList
+ }
+
+
+ /* charts */
+
+ def update_data(data: XYSeriesCollection, selected_fields: Iterable[String])
+ {
+ data.removeAllSeries
+ for {
+ field <- selected_fields.iterator
+ series = new XYSeries(field)
+ } {
+ content.foreach(entry => series.add(entry.time, entry.data(field)))
+ data.addSeries(series)
+ }
+ }
+
+ def chart(title: String, selected_fields: Iterable[String]): JFreeChart =
+ {
+ val data = new XYSeriesCollection
+ update_data(data, selected_fields)
+
+ ChartFactory.createXYLineChart(title, "time", "value", data,
+ PlotOrientation.VERTICAL, true, true, true)
+ }
+
+ def chart(fields: ML_Statistics.Fields): JFreeChart =
+ chart(fields._1, fields._2)
+
+ def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.main_fields): Unit =
+ fields.map(chart(_)).foreach(c =>
+ GUI_Thread.later {
+ new Frame {
+ iconImage = GUI.isabelle_image()
+ title = session_name
+ contents = Component.wrap(new ChartPanel(c))
+ visible = true
+ }
+ })
+}
+
--- a/src/Pure/Tools/ml_console.scala Thu Apr 13 12:19:28 2017 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,135 +0,0 @@
-/* Title: Pure/Tools/ml_console.scala
- Author: Makarius
-
-The raw ML process in interactive mode.
-*/
-
-package isabelle
-
-
-import java.io.{IOException, BufferedReader, InputStreamReader}
-
-
-object ML_Console
-{
- /* command line entry point */
-
- def main(args: Array[String])
- {
- Command_Line.tool {
- var dirs: List[Path] = Nil
- var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
- var modes: List[String] = Nil
- var no_build = false
- var options = Options.init()
- var raw_ml_system = false
- var system_mode = false
-
- val getopts = Getopts("""
-Usage: isabelle console [OPTIONS]
-
- Options are:
- -d DIR include session directory
- -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
- -m MODE add print mode for output
- -n no build of session image on startup
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -r bootstrap from raw Poly/ML
- -s system build mode for session image
-
- Build a logic session image and run the raw Isabelle ML process
- in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" +
- quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """.
-""",
- "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
- "l:" -> (arg => logic = arg),
- "m:" -> (arg => modes = arg :: modes),
- "n" -> (arg => no_build = true),
- "o:" -> (arg => options = options + arg),
- "r" -> (_ => raw_ml_system = true),
- "s" -> (_ => system_mode = true))
-
- val more_args = getopts(args)
- if (!more_args.isEmpty) getopts.usage()
-
-
- // build
- if (!no_build && !raw_ml_system &&
- !Build.build(options = options, build_heap = true, no_build = true,
- dirs = dirs, system_mode = system_mode, sessions = List(logic)).ok)
- {
- val progress = new Console_Progress()
- progress.echo("Build started for Isabelle/" + logic + " ...")
- progress.interrupt_handler {
- val res =
- Build.build(options = options, progress = progress, build_heap = true,
- dirs = dirs, system_mode = system_mode, sessions = List(logic))
- if (!res.ok) sys.exit(res.rc)
- }
- }
-
- // process loop
- val process =
- ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true,
- modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
- raw_ml_system = raw_ml_system, store = Sessions.store(system_mode),
- session_base =
- if (raw_ml_system) None
- else Some(Sessions.session_base(options, logic, dirs)))
- val process_output = Future.thread[Unit]("process_output") {
- try {
- var result = new StringBuilder(100)
- var finished = false
- while (!finished) {
- var c = -1
- var done = false
- while (!done && (result.length == 0 || process.stdout.ready)) {
- c = process.stdout.read
- if (c >= 0) result.append(c.asInstanceOf[Char])
- else done = true
- }
- if (result.length > 0) {
- System.out.print(result.toString)
- System.out.flush()
- result.length = 0
- }
- else {
- process.stdout.close()
- finished = true
- }
- }
- }
- catch { case e: IOException => case Exn.Interrupt() => }
- }
- val process_input = Future.thread[Unit]("process_input") {
- val reader = new BufferedReader(new InputStreamReader(System.in))
- POSIX_Interrupt.handler { process.interrupt } {
- try {
- var finished = false
- while (!finished) {
- reader.readLine() match {
- case null =>
- process.stdin.close()
- finished = true
- case line =>
- process.stdin.write(line)
- process.stdin.write("\n")
- process.stdin.flush()
- }
- }
- }
- catch { case e: IOException => case Exn.Interrupt() => }
- }
- }
- val process_result = Future.thread[Int]("process_result") {
- val rc = process.join
- process_input.cancel
- rc
- }
-
- process_output.join
- process_input.join
- process_result.join
- }
- }
-}
--- a/src/Pure/Tools/ml_process.scala Thu Apr 13 12:19:28 2017 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,194 +0,0 @@
-/* Title: Pure/Tools/ml_process.scala
- Author: Makarius
-
-The raw ML process.
-*/
-
-package isabelle
-
-
-import java.io.{File => JFile}
-
-
-object ML_Process
-{
- def apply(options: Options,
- logic: String = "",
- args: List[String] = Nil,
- dirs: List[Path] = Nil,
- modes: List[String] = Nil,
- raw_ml_system: Boolean = false,
- cwd: JFile = null,
- env: Map[String, String] = Isabelle_System.settings(),
- redirect: Boolean = false,
- cleanup: () => Unit = () => (),
- channel: Option[System_Channel] = None,
- sessions: Option[Sessions.T] = None,
- session_base: Option[Sessions.Base] = None,
- store: Sessions.Store = Sessions.store()): Bash.Process =
- {
- val logic_name = Isabelle_System.default_logic(logic)
- val heaps: List[String] =
- if (raw_ml_system) Nil
- else {
- val selection = Sessions.Selection(sessions = List(logic_name))
- val (_, selected_sessions) =
- sessions.getOrElse(Sessions.load(options, dirs)).selection(selection)
- (selected_sessions.build_ancestors(logic_name) ::: List(logic_name)).
- map(a => File.platform_path(store.heap(a)))
- }
-
- val eval_init =
- if (heaps.isEmpty) {
- List(
- """
- fun chapter (_: string) = ();
- fun section (_: string) = ();
- fun subsection (_: string) = ();
- fun subsubsection (_: string) = ();
- fun paragraph (_: string) = ();
- fun subparagraph (_: string) = ();
- val ML_file = PolyML.use;
- """,
- if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6")
- """
- structure FixedInt = IntInf;
- structure RunCall =
- struct
- open RunCall
- val loadWord: word * word -> word =
- run_call2 RuntimeCalls.POLY_SYS_load_word;
- val storeWord: word * word * word -> unit =
- run_call3 RuntimeCalls.POLY_SYS_assign_word;
- end;
- """
- else "",
- if (Platform.is_windows)
- "fun exit 0 = OS.Process.exit OS.Process.success" +
- " | exit 1 = OS.Process.exit OS.Process.failure" +
- " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
- else
- "fun exit rc = Posix.Process.exit (Word8.fromInt rc)",
- "PolyML.Compiler.prompt1 := \"Poly/ML> \"",
- "PolyML.Compiler.prompt2 := \"Poly/ML# \"")
- }
- else
- List(
- "(PolyML.SaveState.loadHierarchy " +
- ML_Syntax.print_list(ML_Syntax.print_string0)(heaps) +
- "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
- ML_Syntax.print_string0(": " + logic_name + "\n") +
- "); OS.Process.exit OS.Process.failure)")
-
- val eval_modes =
- if (modes.isEmpty) Nil
- else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string0)(modes))
-
- // options
- val isabelle_process_options = Isabelle_System.tmp_file("options")
- File.write(isabelle_process_options, YXML.string_of_body(options.encode))
- val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
- val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
-
- // session base
- val eval_session_base =
- session_base match {
- case None => Nil
- case Some(base) =>
- def print_table(table: List[(String, String)]): String =
- ML_Syntax.print_list(
- ML_Syntax.print_pair(
- ML_Syntax.print_string, ML_Syntax.print_string))(table)
- List("Resources.set_session_base {default_qualifier = \"\"" +
- ", global_theories = " + print_table(base.global_theories.toList) +
- ", loaded_theories = " + print_table(base.loaded_theories.toList) +
- ", known_theories = " + print_table(base.dest_known_theories) + "}")
- }
-
- // process
- val eval_process =
- if (heaps.isEmpty)
- List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")))
- else
- channel match {
- case None =>
- List("Isabelle_Process.init_options ()")
- case Some(ch) =>
- List("Isabelle_Process.init_protocol " + ML_Syntax.print_string0(ch.server_name))
- }
-
- // ISABELLE_TMP
- val isabelle_tmp = Isabelle_System.tmp_dir("process")
- val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp))
-
- val ml_runtime_options =
- {
- val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS"))
- if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options
- else ml_options ::: List("--gcthreads", options.int("threads").toString)
- }
-
- // bash
- val bash_args =
- ml_runtime_options :::
- (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process).
- map(eval => List("--eval", eval)).flatten ::: args
-
- Bash.process(
- "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
- Bash.strings(bash_args),
- cwd = cwd,
- env =
- Isabelle_System.library_path(env ++ env_options ++ env_tmp,
- Isabelle_System.getenv_strict("ML_HOME")),
- redirect = redirect,
- cleanup = () =>
- {
- isabelle_process_options.delete
- Isabelle_System.rm_tree(isabelle_tmp)
- cleanup()
- })
- }
-
-
- /* Isabelle tool wrapper */
-
- val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args =>
- {
- var dirs: List[Path] = Nil
- var eval_args: List[String] = Nil
- var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
- var modes: List[String] = Nil
- var options = Options.init()
-
- val getopts = Getopts("""
-Usage: isabelle process [OPTIONS]
-
- Options are:
- -T THEORY load theory
- -d DIR include session directory
- -e ML_EXPR evaluate ML expression on startup
- -f ML_FILE evaluate ML file on startup
- -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
- -m MODE add print mode for output
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-
- Run the raw Isabelle ML process in batch mode.
-""",
- "T:" -> (arg =>
- eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))),
- "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
- "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
- "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
- "l:" -> (arg => logic = arg),
- "m:" -> (arg => modes = arg :: modes),
- "o:" -> (arg => options = options + arg))
-
- val more_args = getopts(args)
- if (args.isEmpty || !more_args.isEmpty) getopts.usage()
-
- val rc = ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
- result().print_stdout.rc
- sys.exit(rc)
- })
-}
--- a/src/Pure/Tools/ml_statistics.scala Thu Apr 13 12:19:28 2017 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,151 +0,0 @@
-/* Title: Pure/Tools/ml_statistics.scala
- Author: Makarius
-
-ML runtime statistics.
-*/
-
-package isabelle
-
-
-import scala.collection.mutable
-import scala.collection.immutable.{SortedSet, SortedMap}
-import scala.swing.{Frame, Component}
-
-import org.jfree.data.xy.{XYSeries, XYSeriesCollection}
-import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory}
-import org.jfree.chart.plot.PlotOrientation
-
-
-object ML_Statistics
-{
- /* content interpretation */
-
- final case class Entry(time: Double, data: Map[String, Double])
-
- def apply(session_name: String, ml_statistics: List[Properties.T]): ML_Statistics =
- new ML_Statistics(session_name, ml_statistics)
-
- val empty = apply("", Nil)
-
-
- /* standard fields */
-
- type Fields = (String, Iterable[String])
-
- val tasks_fields: Fields =
- ("Future tasks",
- List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive", "tasks_urgent"))
-
- val workers_fields: Fields =
- ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
-
- val GC_fields: Fields =
- ("GCs", List("partial_GCs", "full_GCs"))
-
- val heap_fields: Fields =
- ("Heap", List("size_heap", "size_allocation", "size_allocation_free",
- "size_heap_free_last_full_GC", "size_heap_free_last_GC"))
-
- val threads_fields: Fields =
- ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar",
- "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal"))
-
- val time_fields: Fields =
- ("Time", List("time_CPU", "time_GC"))
-
- val speed_fields: Fields =
- ("Speed", List("speed_CPU", "speed_GC"))
-
-
- val all_fields: List[Fields] =
- List(tasks_fields, workers_fields, GC_fields, heap_fields, threads_fields,
- time_fields, speed_fields)
-
- val main_fields: List[Fields] =
- List(tasks_fields, workers_fields, heap_fields)
-}
-
-final class ML_Statistics private(val session_name: String, val ml_statistics: List[Properties.T])
-{
- val Now = new Properties.Double("now")
- def now(props: Properties.T): Double = Now.unapply(props).get
-
- require(ml_statistics.forall(props => Now.unapply(props).isDefined))
-
- val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head)
- val duration = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.last) - time_start
-
- val fields: Set[String] =
- SortedSet.empty[String] ++
- (for (props <- ml_statistics.iterator; (x, _) <- props.iterator if x != Now.name)
- yield x)
-
- val content: List[ML_Statistics.Entry] =
- {
- var last_edge = Map.empty[String, (Double, Double, Double)]
- val result = new mutable.ListBuffer[ML_Statistics.Entry]
- for (props <- ml_statistics) {
- val time = now(props) - time_start
- require(time >= 0.0)
-
- // rising edges -- relative speed
- val speeds =
- for ((key, value) <- props; a <- Library.try_unprefix("time", key)) yield {
- val (x0, y0, s0) = last_edge.getOrElse(a, (0.0, 0.0, 0.0))
-
- val x1 = time
- val y1 = java.lang.Double.parseDouble(value)
- val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0)
-
- val b = ("speed" + a).intern
- if (y1 > y0) { last_edge += (a -> (x1, y1, s1)); (b, s1) } else (b, s0)
- }
-
- val data =
- SortedMap.empty[String, Double] ++ speeds ++
- (for ((x, y) <- props.iterator if x != Now.name)
- yield (x, java.lang.Double.parseDouble(y)))
- result += ML_Statistics.Entry(time, data)
- }
- result.toList
- }
-
-
- /* charts */
-
- def update_data(data: XYSeriesCollection, selected_fields: Iterable[String])
- {
- data.removeAllSeries
- for {
- field <- selected_fields.iterator
- series = new XYSeries(field)
- } {
- content.foreach(entry => series.add(entry.time, entry.data(field)))
- data.addSeries(series)
- }
- }
-
- def chart(title: String, selected_fields: Iterable[String]): JFreeChart =
- {
- val data = new XYSeriesCollection
- update_data(data, selected_fields)
-
- ChartFactory.createXYLineChart(title, "time", "value", data,
- PlotOrientation.VERTICAL, true, true, true)
- }
-
- def chart(fields: ML_Statistics.Fields): JFreeChart =
- chart(fields._1, fields._2)
-
- def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.main_fields): Unit =
- fields.map(chart(_)).foreach(c =>
- GUI_Thread.later {
- new Frame {
- iconImage = GUI.isabelle_image()
- title = session_name
- contents = Component.wrap(new ChartPanel(c))
- visible = true
- }
- })
-}
-
--- a/src/Pure/build-jars Thu Apr 13 12:19:28 2017 +0200
+++ b/src/Pure/build-jars Thu Apr 13 12:27:57 2017 +0200
@@ -82,7 +82,10 @@
Isar/outer_syntax.scala
Isar/parse.scala
Isar/token.scala
+ ML/ml_console.scala
ML/ml_lex.scala
+ ML/ml_process.scala
+ ML/ml_statistics.scala
ML/ml_syntax.scala
PIDE/command.scala
PIDE/command_span.scala
@@ -133,9 +136,6 @@
Tools/debugger.scala
Tools/doc.scala
Tools/main.scala
- Tools/ml_console.scala
- Tools/ml_process.scala
- Tools/ml_statistics.scala
Tools/print_operation.scala
Tools/profiling_report.scala
Tools/simplifier_trace.scala