--- a/Admin/isatest/settings/mac-poly-M4 Wed Jan 02 20:53:01 2013 +0100
+++ b/Admin/isatest/settings/mac-poly-M4 Wed Jan 02 22:16:16 2013 +0100
@@ -29,3 +29,5 @@
ISABELLE_FULL_TEST=true
+Z3_NON_COMMERCIAL="yes"
+
--- a/Admin/isatest/settings/mac-poly-M8 Wed Jan 02 20:53:01 2013 +0100
+++ b/Admin/isatest/settings/mac-poly-M8 Wed Jan 02 22:16:16 2013 +0100
@@ -29,3 +29,5 @@
ISABELLE_FULL_TEST=true
+Z3_NON_COMMERCIAL="yes"
+
--- a/src/Pure/Concurrent/future.ML Wed Jan 02 20:53:01 2013 +0100
+++ b/src/Pure/Concurrent/future.ML Wed Jan 02 22:16:16 2013 +0100
@@ -204,7 +204,7 @@
("workers_waiting", Markup.print_int waiting)] @
ML_Statistics.get ();
in
- Output.protocol_message (Markup.ML_statistics @ stats) ""
+ Output.protocol_message (Markup.ML_statistics :: stats) ""
handle Fail msg => warning msg
end
else ();
--- a/src/Pure/General/file.scala Wed Jan 02 20:53:01 2013 +0100
+++ b/src/Pure/General/file.scala Wed Jan 02 22:16:16 2013 +0100
@@ -8,8 +8,9 @@
import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
- InputStream, FileInputStream, BufferedReader, InputStreamReader, File => JFile}
-import java.util.zip.GZIPOutputStream
+ InputStream, FileInputStream, BufferedInputStream, BufferedReader, InputStreamReader,
+ File => JFile}
+import java.util.zip.{GZIPInputStream, GZIPOutputStream}
import scala.collection.mutable
@@ -54,10 +55,10 @@
}
def read(file: JFile): String = new String(read_bytes(file), UTF8.charset)
-
def read(path: Path): String = read(path.file)
- def read(reader: BufferedReader): String =
+
+ def read_stream(reader: BufferedReader): String =
{
val output = new StringBuilder(100)
var c = -1
@@ -66,8 +67,12 @@
output.toString
}
- def read(stream: InputStream): String =
- read(new BufferedReader(new InputStreamReader(stream, UTF8.charset)))
+ def read_stream(stream: InputStream): String =
+ read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset)))
+
+ def read_gzip(file: JFile): String =
+ read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file))))
+ def read_gzip(path: Path): String = read_gzip(path.file)
/* try_read */
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_statistics.scala Wed Jan 02 22:16:16 2013 +0100
@@ -0,0 +1,139 @@
+/* Title: Pure/ML/ml_statistics.ML
+ Author: Makarius
+
+ML runtime statistics.
+*/
+
+package isabelle
+
+
+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(stats: List[Properties.T]): ML_Statistics = new ML_Statistics(stats)
+ def apply(log: Path): ML_Statistics = apply(read_log(log))
+
+
+ /* standard fields */
+
+ val GC_fields = ("GCs", List("partial_GCs", "full_GCs"))
+
+ val heap_fields =
+ ("Heap", List("size_heap", "size_allocation", "size_allocation_free",
+ "size_heap_free_last_full_GC", "size_heap_free_last_GC"))
+
+ val threads_fields =
+ ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar",
+ "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal"))
+
+ val time_fields =
+ ("Time", List("time_GC_system", "time_GC_user", "time_non_GC_system", "time_non_GC_user"))
+
+ val tasks_fields =
+ ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
+
+ val workers_fields =
+ ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
+
+ val standard_fields =
+ List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields)
+
+
+ /* read properties from build log */
+
+ private val line_prefix = "\fML_statistics = "
+
+ private val syntax = Outer_Syntax.empty + "," + "(" + ")" + "[" + "]"
+
+ private object Parser extends Parse.Parser
+ {
+ private def stat: Parser[(String, String)] =
+ keyword("(") ~ string ~ keyword(",") ~ string ~ keyword(")") ^^
+ { case _ ~ x ~ _ ~ y ~ _ => (x, y) }
+ private def stats: Parser[Properties.T] =
+ keyword("[") ~> repsep(stat, keyword(",")) <~ keyword("]")
+
+ def parse_stats(s: String): Properties.T =
+ {
+ parse_all(stats, Token.reader(syntax.scan(s))) match {
+ case Success(result, _) => result
+ case bad => error(bad.toString)
+ }
+ }
+ }
+
+ def read_log(log: Path): List[Properties.T] =
+ for {
+ line <- split_lines(File.read_gzip(log))
+ if line.startsWith(line_prefix)
+ stats = line.substring(line_prefix.length)
+ } yield Parser.parse_stats(stats)
+}
+
+final class ML_Statistics private(val stats: List[Properties.T])
+{
+ val Now = new Properties.Double("now")
+
+ require(!stats.isEmpty && stats.forall(props => Now.unapply(props).isDefined))
+
+ val time_start = Now.unapply(stats.head).get
+ val duration = Now.unapply(stats.last).get - time_start
+
+ val fields: Set[String] =
+ SortedSet.empty[String] ++
+ (for (props <- stats.iterator; (x, _) <- props.iterator if x != Now.name)
+ yield x)
+
+ val content: List[ML_Statistics.Entry] =
+ stats.map(props => {
+ val time = Now.unapply(props).get - time_start
+ require(time >= 0.0)
+ val data =
+ SortedMap.empty[String, Double] ++
+ (for ((x, y) <- props.iterator if x != Now.name)
+ yield (x, java.lang.Double.parseDouble(y)))
+ ML_Statistics.Entry(time, data)
+ })
+
+
+ /* charts */
+
+ def chart(title: String, selected_fields: Iterable[String]): JFreeChart =
+ {
+ val data = new XYSeriesCollection
+
+ for {
+ field <- selected_fields.iterator
+ series = new XYSeries(field)
+ } {
+ content.foreach(entry => series.add(entry.time, entry.data(field)))
+ data.addSeries(series)
+ }
+
+ ChartFactory.createXYLineChart(title, "time", "value", data,
+ PlotOrientation.VERTICAL, true, true, true)
+ }
+
+ def chart_panel(title: String, selected_fields: Iterable[String]): ChartPanel =
+ new ChartPanel(chart(title, selected_fields))
+
+ def standard_frames: Unit =
+ for ((title, selected_fields) <- ML_Statistics.standard_fields) {
+ val c = chart(title, selected_fields)
+ Swing_Thread.later {
+ new Frame { contents = Component.wrap(new ChartPanel(c)); visible = true }
+ }
+ }
+}
+
--- a/src/Pure/PIDE/markup.ML Wed Jan 02 20:53:01 2013 +0100
+++ b/src/Pure/PIDE/markup.ML Wed Jan 02 22:16:16 2013 +0100
@@ -130,7 +130,7 @@
val removed_versions: Properties.T
val invoke_scala: string -> string -> Properties.T
val cancel_scala: string -> Properties.T
- val ML_statistics: Properties.T
+ val ML_statistics: string * string
val no_output: Output.output * Output.output
val default_output: T -> Output.output * Output.output
val add_mode: string -> (T -> Output.output * Output.output) -> unit
@@ -402,7 +402,7 @@
fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
-val ML_statistics = [(functionN, "ML_statistics")];
+val ML_statistics = (functionN, "ML_statistics");
--- a/src/Pure/ROOT Wed Jan 02 20:53:01 2013 +0100
+++ b/src/Pure/ROOT Wed Jan 02 22:16:16 2013 +0100
@@ -181,7 +181,6 @@
"Syntax/syntax_phases.ML"
"Syntax/syntax_trans.ML"
"Syntax/term_position.ML"
- "System/build.ML"
"System/command_line.ML"
"System/invoke_scala.ML"
"System/isabelle_process.ML"
@@ -201,6 +200,7 @@
"Thy/thy_load.ML"
"Thy/thy_output.ML"
"Thy/thy_syntax.ML"
+ "Tools/build.ML"
"Tools/named_thms.ML"
"Tools/legacy_xml_syntax.ML"
"assumption.ML"
--- a/src/Pure/ROOT.ML Wed Jan 02 20:53:01 2013 +0100
+++ b/src/Pure/ROOT.ML Wed Jan 02 22:16:16 2013 +0100
@@ -276,7 +276,6 @@
use "System/session.ML";
use "System/command_line.ML";
-use "System/build.ML";
use "System/system_channel.ML";
use "System/isabelle_process.ML";
use "System/invoke_scala.ML";
@@ -286,8 +285,8 @@
(* miscellaneous tools and packages for Pure Isabelle *)
+use "Tools/build.ML";
use "Tools/named_thms.ML";
-
use "Tools/legacy_xml_syntax.ML";
--- a/src/Pure/System/build.ML Wed Jan 02 20:53:01 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,100 +0,0 @@
-(* Title: Pure/System/build.ML
- Author: Makarius
-
-Build Isabelle sessions.
-*)
-
-signature BUILD =
-sig
- val build: string -> unit
-end;
-
-structure Build: BUILD =
-struct
-
-local
-
-fun no_document options =
- (case Options.string options "document" of "" => true | "false" => true | _ => false);
-
-fun use_thys options =
- Thy_Info.use_thys
- |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
- |> Unsynchronized.setmp print_mode
- (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
- |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
- |> Unsynchronized.setmp Goal.parallel_proofs_threshold
- (Options.int options "parallel_proofs_threshold")
- |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
- |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
- |> Unsynchronized.setmp Future.ML_statistics (Options.bool options "ML_statistics")
- |> no_document options ? Present.no_document
- |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
- |> Unsynchronized.setmp Toplevel.skip_proofs (Options.bool options "skip_proofs")
- |> Unsynchronized.setmp Printer.show_question_marks_default
- (Options.bool options "show_question_marks")
- |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")
- |> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short")
- |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique")
- |> Unsynchronized.setmp Thy_Output.display_default (Options.bool options "thy_output_display")
- |> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes")
- |> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent")
- |> Unsynchronized.setmp Thy_Output.source_default (Options.bool options "thy_output_source")
- |> Unsynchronized.setmp Thy_Output.break_default (Options.bool options "thy_output_break")
- |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
- |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
-
-fun use_theories (options, thys) =
- let val condition = space_explode "," (Options.string options "condition") in
- (case filter_out (can getenv_strict) condition of
- [] => use_thys options (map (rpair Position.none) thys)
- | conds =>
- Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
- " (undefined " ^ commas conds ^ ")\n"))
- end;
-
-in
-
-fun build args_file = Command_Line.tool (fn () =>
- let
- val (do_output, (options, (verbose, (browser_info, (parent_name,
- (name, theories)))))) =
- File.read (Path.explode args_file) |> YXML.parse_body |>
- let open XML.Decode in
- pair bool (pair Options.decode (pair bool (pair string (pair string
- (pair string ((list (pair Options.decode (list string)))))))))
- end;
-
- val document_variants =
- map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
- val _ =
- (case duplicates (op =) (map fst document_variants) of
- [] => ()
- | dups => error ("Duplicate document variants: " ^ commas_quote dups));
-
- val _ =
- Session.init do_output false
- (Options.bool options "browser_info") browser_info
- (Options.string options "document")
- (Options.bool options "document_graph")
- (Options.string options "document_output")
- document_variants
- parent_name name
- (false, "") ""
- verbose;
-
- val res1 =
- theories |>
- (List.app use_theories
- |> Session.with_timing name verbose
- |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
- |> Exn.capture);
- val res2 = Exn.capture Session.finish ();
- val _ = Par_Exn.release_all [res1, res2];
-
- val _ = if do_output then () else exit 0;
- in 0 end);
-
-end;
-
-end;
--- a/src/Pure/System/build.scala Wed Jan 02 20:53:01 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,750 +0,0 @@
-/* Title: Pure/System/build.scala
- Author: Makarius
- Options: :folding=explicit:collapseFolds=1:
-
-Build and manage Isabelle sessions.
-*/
-
-package isabelle
-
-
-import java.util.{Timer, TimerTask}
-import java.io.{BufferedInputStream, FileInputStream,
- BufferedReader, InputStreamReader, IOException}
-import java.util.zip.GZIPInputStream
-
-import scala.collection.SortedSet
-import scala.annotation.tailrec
-
-
-object Build
-{
- /** progress context **/
-
- class Progress {
- def echo(msg: String) {}
- def stopped: Boolean = false
- }
-
- object Ignore_Progress extends Progress
-
- object Console_Progress extends Progress {
- override def echo(msg: String) { java.lang.System.out.println(msg) }
- }
-
-
-
- /** session information **/
-
- // external version
- sealed case class Session_Entry(
- pos: Position.T,
- name: String,
- groups: List[String],
- path: String,
- parent: Option[String],
- description: String,
- options: List[Options.Spec],
- theories: List[(List[Options.Spec], List[String])],
- files: List[String])
-
- // internal version
- sealed case class Session_Info(
- select: Boolean,
- pos: Position.T,
- groups: List[String],
- dir: Path,
- parent: Option[String],
- description: String,
- options: Options,
- theories: List[(Options, List[Path])],
- files: List[Path],
- entry_digest: SHA1.Digest)
-
- def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
-
- def session_info(options: Options, select: Boolean, dir: Path, entry: Session_Entry)
- : (String, Session_Info) =
- try {
- val name = entry.name
-
- if (name == "") error("Bad session name")
- if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
- if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
-
- val session_options = options ++ entry.options
-
- val theories =
- entry.theories.map({ case (opts, thys) =>
- (session_options ++ opts, thys.map(Path.explode(_))) })
- val files = entry.files.map(Path.explode(_))
- val entry_digest = SHA1.digest((name, entry.parent, entry.options, entry.theories).toString)
-
- val info =
- Session_Info(select, entry.pos, entry.groups, dir + Path.explode(entry.path),
- entry.parent, entry.description, session_options, theories, files, entry_digest)
-
- (name, info)
- }
- catch {
- case ERROR(msg) =>
- error(msg + "\nThe error(s) above occurred in session entry " +
- quote(entry.name) + Position.here(entry.pos))
- }
-
-
- /* session tree */
-
- object Session_Tree
- {
- def apply(infos: Seq[(String, Session_Info)]): Session_Tree =
- {
- val graph1 =
- (Graph.string[Session_Info] /: infos) {
- case (graph, (name, info)) =>
- if (graph.defined(name))
- error("Duplicate session " + quote(name) + Position.here(info.pos))
- else graph.new_node(name, info)
- }
- val graph2 =
- (graph1 /: graph1.entries) {
- case (graph, (name, (info, _))) =>
- info.parent match {
- case None => graph
- case Some(parent) =>
- if (!graph.defined(parent))
- error("Bad parent session " + quote(parent) + " for " +
- quote(name) + Position.here(info.pos))
-
- try { graph.add_edge_acyclic(parent, name) }
- catch {
- case exn: Graph.Cycles[_] =>
- error(cat_lines(exn.cycles.map(cycle =>
- "Cyclic session dependency of " +
- cycle.map(c => quote(c.toString)).mkString(" via "))) +
- Position.here(info.pos))
- }
- }
- }
- new Session_Tree(graph2)
- }
- }
-
- final class Session_Tree private(val graph: Graph[String, Session_Info])
- extends PartialFunction[String, Session_Info]
- {
- def apply(name: String): Session_Info = graph.get_node(name)
- def isDefinedAt(name: String): Boolean = graph.defined(name)
-
- def selection(requirements: Boolean, all_sessions: Boolean,
- session_groups: List[String], sessions: List[String]): (List[String], Session_Tree) =
- {
- val bad_sessions = sessions.filterNot(isDefinedAt(_))
- if (!bad_sessions.isEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
-
- val pre_selected =
- {
- if (all_sessions) graph.keys.toList
- else {
- val select_group = session_groups.toSet
- val select = sessions.toSet
- (for {
- (name, (info, _)) <- graph.entries
- if info.select || select(name) || apply(name).groups.exists(select_group)
- } yield name).toList
- }
- }
- val selected =
- if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
- else pre_selected
-
- val tree1 = new Session_Tree(graph.restrict(graph.all_preds(selected).toSet))
- (selected, tree1)
- }
-
- def topological_order: List[(String, Session_Info)] =
- graph.topological_order.map(name => (name, apply(name)))
-
- override def toString: String = graph.entries.map(_._1).toList.sorted.mkString(",")
- }
-
-
- /* parser */
-
- private val SESSION = "session"
- private val IN = "in"
- private val DESCRIPTION = "description"
- private val OPTIONS = "options"
- private val THEORIES = "theories"
- private val FILES = "files"
-
- lazy val root_syntax =
- Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
- (SESSION, Keyword.THY_DECL) + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
-
- private object Parser extends Parse.Parser
- {
- def session_entry(pos: Position.T): Parser[Session_Entry] =
- {
- val session_name = atom("session name", _.is_name)
-
- val option =
- name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
- val options = keyword("[") ~> rep1sep(option, keyword(",")) <~ keyword("]")
-
- val theories =
- keyword(THEORIES) ~! ((options | success(Nil)) ~ rep(theory_name)) ^^
- { case _ ~ (x ~ y) => (x, y) }
-
- command(SESSION) ~!
- (session_name ~
- ((keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
- ((keyword(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
- (keyword("=") ~!
- (opt(session_name ~! keyword("+") ^^ { case x ~ _ => x }) ~
- ((keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
- ((keyword(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
- rep1(theories) ~
- ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil))))) ^^
- { case _ ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h))) =>
- Session_Entry(pos, a, b, c, d, e, f, g, h) }
- }
-
- def parse_entries(root: Path): List[Session_Entry] =
- {
- val toks = root_syntax.scan(File.read(root))
- parse_all(rep(session_entry(root.position)), Token.reader(toks, root.implode)) match {
- case Success(result, _) => result
- case bad => error(bad.toString)
- }
- }
- }
-
-
- /* find sessions within certain directories */
-
- private val ROOT = Path.explode("ROOT")
- private val ROOTS = Path.explode("ROOTS")
-
- private def is_session_dir(dir: Path): Boolean =
- (dir + ROOT).is_file || (dir + ROOTS).is_file
-
- private def check_session_dir(dir: Path): Path =
- if (is_session_dir(dir)) dir
- else error("Bad session root directory: " + dir.toString)
-
- def find_sessions(options: Options, more_dirs: List[(Boolean, Path)]): Session_Tree =
- {
- def find_dir(select: Boolean, dir: Path): List[(String, Session_Info)] =
- find_root(select, dir) ::: find_roots(select, dir)
-
- def find_root(select: Boolean, dir: Path): List[(String, Session_Info)] =
- {
- val root = dir + ROOT
- if (root.is_file) Parser.parse_entries(root).map(session_info(options, select, dir, _))
- else Nil
- }
-
- def find_roots(select: Boolean, dir: Path): List[(String, Session_Info)] =
- {
- val roots = dir + ROOTS
- if (roots.is_file) {
- for {
- line <- split_lines(File.read(roots))
- if !(line == "" || line.startsWith("#"))
- dir1 =
- try { check_session_dir(dir + Path.explode(line)) }
- catch {
- case ERROR(msg) =>
- error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
- }
- info <- find_dir(select, dir1)
- } yield info
- }
- else Nil
- }
-
- val default_dirs = Isabelle_System.components().filter(is_session_dir(_)).map((false, _))
-
- more_dirs foreach { case (_, dir) => check_session_dir(dir) }
-
- Session_Tree(
- for {
- (select, dir) <- default_dirs ::: more_dirs
- info <- find_dir(select, dir)
- } yield info)
- }
-
-
-
- /** build **/
-
- /* queue */
-
- object Queue
- {
- def apply(tree: Session_Tree): Queue =
- {
- val graph = tree.graph
-
- def outdegree(name: String): Int = graph.imm_succs(name).size
- def timeout(name: String): Double = tree(name).options.real("timeout")
-
- object Ordering extends scala.math.Ordering[String]
- {
- def compare(name1: String, name2: String): Int =
- outdegree(name2) compare outdegree(name1) match {
- case 0 =>
- timeout(name2) compare timeout(name1) match {
- case 0 => name1 compare name2
- case ord => ord
- }
- case ord => ord
- }
- }
-
- new Queue(graph, SortedSet(graph.keys.toList: _*)(Ordering))
- }
- }
-
- final class Queue private(graph: Graph[String, Session_Info], order: SortedSet[String])
- {
- def is_inner(name: String): Boolean = !graph.is_maximal(name)
-
- def is_empty: Boolean = graph.is_empty
-
- def - (name: String): Queue = new Queue(graph.del_node(name), order - name)
-
- def dequeue(skip: String => Boolean): Option[(String, Session_Info)] =
- {
- val it = order.iterator.dropWhile(name => skip(name) || !graph.is_minimal(name))
- if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) }
- else None
- }
- }
-
-
- /* source dependencies and static content */
-
- sealed case class Session_Content(
- loaded_theories: Set[String],
- syntax: Outer_Syntax,
- sources: List[(Path, SHA1.Digest)],
- errors: List[String])
- {
- def check_errors: Session_Content =
- {
- if (errors.isEmpty) this
- else error(cat_lines(errors))
- }
- }
-
- sealed case class Deps(deps: Map[String, Session_Content])
- {
- def is_empty: Boolean = deps.isEmpty
- def apply(name: String): Session_Content = deps(name)
- def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
- }
-
- def dependencies(progress: Build.Progress, inlined_files: Boolean,
- verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps =
- Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
- { case (deps, (name, info)) =>
- val (preloaded, parent_syntax, parent_errors) =
- info.parent match {
- case None =>
- (Set.empty[String], Outer_Syntax.init_pure(), Nil)
- case Some(parent_name) =>
- val parent = deps(parent_name)
- (parent.loaded_theories, parent.syntax, parent.errors)
- }
- val thy_info = new Thy_Info(new Thy_Load(preloaded, parent_syntax))
-
- if (verbose || list_files) {
- val groups =
- if (info.groups.isEmpty) ""
- else info.groups.mkString(" (", " ", ")")
- progress.echo("Session " + name + groups)
- }
-
- val thy_deps =
- thy_info.dependencies(inlined_files,
- info.theories.map(_._2).flatten.
- map(thy => Thy_Load.path_node_name(info.dir + Thy_Load.thy_path(thy))))
-
- val loaded_theories = thy_deps.loaded_theories
- val syntax = thy_deps.make_syntax
-
- val all_files =
- (thy_deps.deps.map({ case dep =>
- val thy = Path.explode(dep.name.node)
- val uses = dep.join_header.uses.map(p =>
- Path.explode(dep.name.dir) + Path.explode(p._1))
- thy :: uses
- }).flatten ::: info.files.map(file => info.dir + file)).map(_.expand)
-
- if (list_files)
- progress.echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _)))
-
- val sources =
- try { all_files.map(p => (p, SHA1.digest(p.file))) }
- catch {
- case ERROR(msg) =>
- error(msg + "\nThe error(s) above occurred in session " +
- quote(name) + Position.here(info.pos))
- }
- val errors = parent_errors ::: thy_deps.deps.map(dep => dep.join_header.errors).flatten
-
- deps + (name -> Session_Content(loaded_theories, syntax, sources, errors))
- }))
-
- def session_content(inlined_files: Boolean, dirs: List[Path], session: String): Session_Content =
- {
- val options = Options.init()
- val (_, tree) =
- find_sessions(options, dirs.map((false, _))).selection(false, false, Nil, List(session))
- dependencies(Build.Ignore_Progress, inlined_files, false, false, tree)(session)
- }
-
- def outer_syntax(session: String): Outer_Syntax =
- session_content(false, Nil, session).check_errors.syntax
-
-
- /* jobs */
-
- private class Job(name: String, info: Session_Info, output: Path, do_output: Boolean,
- verbose: Boolean, browser_info: Path)
- {
- // global browser info dir
- if (info.options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file)
- {
- browser_info.file.mkdirs()
- File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
- browser_info + Path.explode("isabelle.gif"))
- File.write(browser_info + Path.explode("index.html"),
- File.read(Path.explode("~~/lib/html/library_index_header.template")) +
- File.read(Path.explode("~~/lib/html/library_index_content.template")) +
- File.read(Path.explode("~~/lib/html/library_index_footer.template")))
- }
-
- def output_path: Option[Path] = if (do_output) Some(output) else None
-
- private val parent = info.parent.getOrElse("")
-
- private val args_file = File.tmp_file("args")
- File.write(args_file, YXML.string_of_body(
- if (is_pure(name)) Options.encode(info.options)
- else
- {
- import XML.Encode._
- pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
- pair(string, list(pair(Options.encode, list(Path.encode)))))))))(
- (do_output, (info.options, (verbose, (browser_info, (parent,
- (name, info.theories)))))))
- }))
-
- private val env =
- Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output),
- (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
- Isabelle_System.posix_path(args_file.getPath))
-
- private val script =
- if (is_pure(name)) {
- if (do_output) "./build " + name + " \"$OUTPUT\""
- else """ rm -f "$OUTPUT"; ./build """ + name
- }
- else {
- """
- . "$ISABELLE_HOME/lib/scripts/timestart.bash"
- """ +
- (if (do_output)
- """
- "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT"
- """
- else
- """
- rm -f "$OUTPUT"; "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT"
- """) +
- """
- RC="$?"
-
- . "$ISABELLE_HOME/lib/scripts/timestop.bash"
-
- if [ "$RC" -eq 0 ]; then
- echo "Finished $TARGET ($TIMES_REPORT)" >&2
- fi
-
- exit "$RC"
- """
- }
-
- private val (thread, result) =
- Simple_Thread.future("build") { Isabelle_System.bash_env(info.dir.file, env, script) }
-
- def terminate: Unit = thread.interrupt
- def is_finished: Boolean = result.is_finished
-
- @volatile private var timeout = false
- private val time = info.options.seconds("timeout")
- private val timer: Option[Timer] =
- if (time.seconds > 0.0) {
- val t = new Timer("build", true)
- t.schedule(new TimerTask { def run = { terminate; timeout = true } }, time.ms)
- Some(t)
- }
- else None
-
- def join: (String, String, Int) = {
- val (out, err, rc) = result.join
- args_file.delete
- timer.map(_.cancel())
-
- val err1 =
- if (rc == 130)
- (if (err.isEmpty || err.endsWith("\n")) err else err + "\n") +
- (if (timeout) "*** Timeout\n" else "*** Interrupt\n")
- else err
- (out, err1, rc)
- }
- }
-
-
- /* log files and corresponding heaps */
-
- private val LOG = Path.explode("log")
- private def log(name: String): Path = LOG + Path.basic(name)
- private def log_gz(name: String): Path = log(name).ext("gz")
-
- private def sources_stamp(digests: List[SHA1.Digest]): String =
- digests.map(_.toString).sorted.mkString("sources: ", " ", "")
-
- private val no_heap: String = "heap: -"
-
- private def heap_stamp(heap: Option[Path]): String =
- {
- "heap: " +
- (heap match {
- case Some(path) =>
- val file = path.file
- if (file.isFile) file.length.toString + " " + file.lastModified.toString
- else "-"
- case None => "-"
- })
- }
-
- private def read_stamps(path: Path): Option[(String, String, String)] =
- if (path.is_file) {
- val stream = new GZIPInputStream (new BufferedInputStream(new FileInputStream(path.file)))
- val reader = new BufferedReader(new InputStreamReader(stream, UTF8.charset))
- val (s, h1, h2) =
- try { (reader.readLine, reader.readLine, reader.readLine) }
- finally { reader.close }
- if (s != null && s.startsWith("sources: ") &&
- h1 != null && h1.startsWith("heap: ") &&
- h2 != null && h2.startsWith("heap: ")) Some((s, h1, h2))
- else None
- }
- else None
-
-
- /* build */
-
- def build(
- progress: Build.Progress,
- options: Options,
- requirements: Boolean = false,
- all_sessions: Boolean = false,
- build_heap: Boolean = false,
- clean_build: Boolean = false,
- more_dirs: List[(Boolean, Path)] = Nil,
- session_groups: List[String] = Nil,
- max_jobs: Int = 1,
- list_files: Boolean = false,
- no_build: Boolean = false,
- system_mode: Boolean = false,
- verbose: Boolean = false,
- sessions: List[String] = Nil): Int =
- {
- val full_tree = find_sessions(options, more_dirs)
- val (selected, selected_tree) =
- full_tree.selection(requirements, all_sessions, session_groups, sessions)
-
- val deps = dependencies(progress, true, verbose, list_files, selected_tree)
- val queue = Queue(selected_tree)
-
- def make_stamp(name: String): String =
- sources_stamp(selected_tree(name).entry_digest :: deps.sources(name))
-
- val (input_dirs, output_dir, browser_info) =
- if (system_mode) {
- val output_dir = Path.explode("~~/heaps/$ML_IDENTIFIER")
- (List(output_dir), output_dir, Path.explode("~~/browser_info"))
- }
- else {
- val output_dir = Path.explode("$ISABELLE_OUTPUT")
- (output_dir :: Isabelle_System.find_logics_dirs(), output_dir,
- Path.explode("$ISABELLE_BROWSER_INFO"))
- }
-
- // prepare log dir
- (output_dir + LOG).file.mkdirs()
-
- // optional cleanup
- if (clean_build) {
- for (name <- full_tree.graph.all_succs(selected)) {
- val files =
- List(Path.basic(name), log(name), log_gz(name)).map(output_dir + _).filter(_.is_file)
- if (!files.isEmpty) progress.echo("Cleaning " + name + " ...")
- if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete")
- }
- }
-
- // scheduler loop
- case class Result(current: Boolean, heap: String, rc: Int)
-
- def sleep(): Unit = Thread.sleep(500)
-
- @tailrec def loop(
- pending: Queue,
- running: Map[String, (String, Job)],
- results: Map[String, Result]): Map[String, Result] =
- {
- if (pending.is_empty) results
- else if (progress.stopped) {
- for ((_, (_, job)) <- running) job.terminate
- sleep(); loop(pending, running, results)
- }
- else
- running.find({ case (_, (_, job)) => job.is_finished }) match {
- case Some((name, (parent_heap, job))) =>
- //{{{ finish job
-
- val (out, err, rc) = job.join
- progress.echo(Library.trim_line(err))
-
- val heap =
- if (rc == 0) {
- (output_dir + log(name)).file.delete
-
- val sources = make_stamp(name)
- val heap = heap_stamp(job.output_path)
- File.write_gzip(output_dir + log_gz(name),
- sources + "\n" + parent_heap + "\n" + heap + "\n" + out)
-
- heap
- }
- else {
- (output_dir + Path.basic(name)).file.delete
- (output_dir + log_gz(name)).file.delete
-
- File.write(output_dir + log(name), out)
- progress.echo(name + " FAILED")
- if (rc != 130) {
- progress.echo("(see also " + (output_dir + log(name)).file.toString + ")")
- val lines = split_lines(out)
- val tail = lines.drop(lines.length - 20 max 0)
- progress.echo("\n" + cat_lines(tail))
- }
-
- no_heap
- }
- loop(pending - name, running - name, results + (name -> Result(false, heap, rc)))
- //}}}
- case None if (running.size < (max_jobs max 1)) =>
- //{{{ check/start next job
- pending.dequeue(running.isDefinedAt(_)) match {
- case Some((name, info)) =>
- val parent_result =
- info.parent match {
- case None => Result(true, no_heap, 0)
- case Some(parent) => results(parent)
- }
- val output = output_dir + Path.basic(name)
- val do_output = build_heap || queue.is_inner(name)
-
- val (current, heap) =
- {
- input_dirs.find(dir => (dir + log_gz(name)).is_file) match {
- case Some(dir) =>
- read_stamps(dir + log_gz(name)) match {
- case Some((s, h1, h2)) =>
- val heap = heap_stamp(Some(dir + Path.basic(name)))
- (s == make_stamp(name) && h1 == parent_result.heap && h2 == heap &&
- !(do_output && heap == no_heap), heap)
- case None => (false, no_heap)
- }
- case None => (false, no_heap)
- }
- }
- val all_current = current && parent_result.current
-
- if (all_current)
- loop(pending - name, running, results + (name -> Result(true, heap, 0)))
- else if (no_build) {
- if (verbose) progress.echo("Skipping " + name + " ...")
- loop(pending - name, running, results + (name -> Result(false, heap, 1)))
- }
- else if (parent_result.rc == 0) {
- progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
- val job = new Job(name, info, output, do_output, verbose, browser_info)
- loop(pending, running + (name -> (parent_result.heap, job)), results)
- }
- else {
- progress.echo(name + " CANCELLED")
- loop(pending - name, running, results + (name -> Result(false, heap, 1)))
- }
- case None => sleep(); loop(pending, running, results)
- }
- ///}}}
- case None => sleep(); loop(pending, running, results)
- }
- }
-
- val results =
- if (deps.is_empty) {
- progress.echo("### Nothing to build")
- Map.empty
- }
- else loop(queue, Map.empty, Map.empty)
-
- val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
- if (rc != 0 && (verbose || !no_build)) {
- val unfinished =
- (for ((name, res) <- results.iterator if res.rc != 0) yield name).toList
- .sorted(scala.math.Ordering.String) // FIXME scala-2.10.0-RC1
- progress.echo("Unfinished session(s): " + commas(unfinished))
- }
- rc
- }
-
-
- /* command line entry point */
-
- def main(args: Array[String])
- {
- Command_Line.tool {
- args.toList match {
- case
- Properties.Value.Boolean(requirements) ::
- Properties.Value.Boolean(all_sessions) ::
- Properties.Value.Boolean(build_heap) ::
- Properties.Value.Boolean(clean_build) ::
- Properties.Value.Int(max_jobs) ::
- Properties.Value.Boolean(list_files) ::
- Properties.Value.Boolean(no_build) ::
- Properties.Value.Boolean(system_mode) ::
- Properties.Value.Boolean(verbose) ::
- Command_Line.Chunks(select_dirs, include_dirs, session_groups, build_options, sessions) =>
- val options = (Options.init() /: build_options)(_ + _)
- val dirs =
- select_dirs.map(d => (true, Path.explode(d))) :::
- include_dirs.map(d => (false, Path.explode(d)))
- build(Build.Console_Progress, options, requirements, all_sessions, build_heap,
- clean_build, dirs, session_groups, max_jobs, list_files, no_build, system_mode,
- verbose, sessions)
- case _ => error("Bad arguments:\n" + cat_lines(args))
- }
- }
- }
-}
-
--- a/src/Pure/System/build_dialog.scala Wed Jan 02 20:53:01 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,135 +0,0 @@
-/* Title: Pure/System/build_dialog.scala
- Author: Makarius
-
-Dialog for session build process.
-*/
-
-package isabelle
-
-
-import java.awt.{GraphicsEnvironment, Point, Font}
-
-import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
- BorderPanel, MainFrame, TextArea, SwingApplication}
-import scala.swing.event.ButtonClicked
-
-
-object Build_Dialog
-{
- def main(args: Array[String]) =
- {
- Platform.init_laf()
- try {
- args.toList match {
- case
- logic_option ::
- logic ::
- Properties.Value.Boolean(system_mode) ::
- include_dirs =>
- val more_dirs = include_dirs.map(s => ((false, Path.explode(s))))
-
- val options = Options.init()
- val session =
- Isabelle_System.default_logic(logic,
- if (logic_option != "") options.string(logic_option) else "")
-
- if (Build.build(Build.Ignore_Progress, options, build_heap = true, no_build = true,
- more_dirs = more_dirs, sessions = List(session)) == 0) sys.exit(0)
- else
- Swing_Thread.later {
- val top = build_dialog(options, system_mode, more_dirs, session)
- top.pack()
-
- val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
- top.location =
- new Point(point.x - top.size.width / 2, point.y - top.size.height / 2)
-
- top.visible = true
- }
- case _ => error("Bad arguments:\n" + cat_lines(args))
- }
- }
- catch {
- case exn: Throwable =>
- Library.error_dialog(null, "Isabelle build failure",
- Library.scrollable_text(Exn.message(exn)))
- sys.exit(2)
- }
- }
-
-
- def build_dialog(
- options: Options,
- system_mode: Boolean,
- more_dirs: List[(Boolean, Path)],
- session: String): MainFrame = new MainFrame
- {
- /* GUI state */
-
- private var is_stopped = false
- private var return_code = 0
-
-
- /* text */
-
- val text = new TextArea {
- font = new Font("SansSerif", Font.PLAIN, 14)
- editable = false
- columns = 40
- rows = 10
- }
-
- val progress = new Build.Progress
- {
- override def echo(msg: String): Unit = Swing_Thread.now { text.append(msg + "\n") }
- override def stopped: Boolean =
- Swing_Thread.now { val b = is_stopped; is_stopped = false; b }
- }
-
-
- /* action button */
-
- var button_action: () => Unit = (() => is_stopped = true)
- val button = new Button("Cancel") {
- reactions += { case ButtonClicked(_) => button_action() }
- }
- def button_exit(rc: Int)
- {
- button.text = if (rc == 0) "OK" else "Exit"
- button_action = (() => sys.exit(rc))
- button.peer.getRootPane.setDefaultButton(button.peer)
- }
-
- val action_panel = new FlowPanel(FlowPanel.Alignment.Center)(button)
-
-
- /* layout panel */
-
- val layout_panel = new BorderPanel
- layout_panel.layout(new ScrollPane(text)) = BorderPanel.Position.Center
- layout_panel.layout(action_panel) = BorderPanel.Position.South
-
- contents = layout_panel
-
-
- /* main build */
-
- title = "Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")"
- progress.echo("Build started for Isabelle/" + session + " ...")
-
- default_thread_pool.submit(() => {
- val (out, rc) =
- try {
- ("",
- Build.build(progress, options, build_heap = true, more_dirs = more_dirs,
- system_mode = system_mode, sessions = List(session)))
- }
- catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) }
- Swing_Thread.now {
- progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
- button_exit(rc)
- }
- })
- }
-}
-
--- a/src/Pure/System/invoke_scala.ML Wed Jan 02 20:53:01 2013 +0100
+++ b/src/Pure/System/invoke_scala.ML Wed Jan 02 22:16:16 2013 +0100
@@ -2,8 +2,6 @@
Author: Makarius
JVM method invocation service via Isabelle/Scala.
-
-TODO: proper cancellation!
*)
signature INVOKE_SCALA =
--- a/src/Pure/System/isabelle_system.scala Wed Jan 02 20:53:01 2013 +0100
+++ b/src/Pure/System/isabelle_system.scala Wed Jan 02 22:16:16 2013 +0100
@@ -232,7 +232,7 @@
private def process_output(proc: Process): (String, Int) =
{
proc.getOutputStream.close
- val output = File.read(proc.getInputStream)
+ val output = File.read_stream(proc.getInputStream)
val rc =
try { proc.waitFor }
finally {
@@ -336,8 +336,8 @@
val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file.getPath))
proc.stdin.close
- val (_, stdout) = Simple_Thread.future("bash_stdout") { File.read(proc.stdout) }
- val (_, stderr) = Simple_Thread.future("bash_stderr") { File.read(proc.stderr) }
+ val (_, stdout) = Simple_Thread.future("bash_stdout") { File.read_stream(proc.stdout) }
+ val (_, stderr) = Simple_Thread.future("bash_stderr") { File.read_stream(proc.stderr) }
val rc =
try { proc.join }
--- a/src/Pure/System/main.scala Wed Jan 02 20:53:01 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-/* Title: Pure/System/main.scala
- Author: Makarius
-
-Default Isabelle application wrapper.
-*/
-
-package isabelle
-
-import scala.swing.TextArea
-
-
-object Main
-{
- def main(args: Array[String])
- {
- val (out, rc) =
- try {
- Platform.init_laf()
- Isabelle_System.init()
- Isabelle_System.isabelle_tool("jedit", args: _*)
- }
- catch { case exn: Throwable => (Exn.message(exn), 2) }
-
- if (rc != 0)
- Library.dialog(null, "Isabelle", "Isabelle output",
- Library.scrollable_text(out + "\nReturn code: " + rc))
-
- sys.exit(rc)
- }
-}
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/build.ML Wed Jan 02 22:16:16 2013 +0100
@@ -0,0 +1,117 @@
+(* Title: Pure/Tools/build.ML
+ Author: Makarius
+
+Build Isabelle sessions.
+*)
+
+signature BUILD =
+sig
+ val build: string -> unit
+end;
+
+structure Build: BUILD =
+struct
+
+(* protocol messages *)
+
+fun ML_statistics (function :: stats) "" =
+ if function = Markup.ML_statistics then SOME stats
+ else NONE
+ | ML_statistics _ _ = NONE;
+
+fun protocol_message props output =
+ (case ML_statistics props output of
+ SOME stats =>
+ writeln ("\f" ^ #2 Markup.ML_statistics ^ " = " ^ ML_Syntax.print_properties stats)
+ | NONE => raise Fail "Undefined Output.protocol_message");
+
+
+(* build *)
+
+local
+
+fun no_document options =
+ (case Options.string options "document" of "" => true | "false" => true | _ => false);
+
+fun use_thys options =
+ Thy_Info.use_thys
+ |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
+ |> Unsynchronized.setmp print_mode
+ (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
+ |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
+ |> Unsynchronized.setmp Goal.parallel_proofs_threshold
+ (Options.int options "parallel_proofs_threshold")
+ |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
+ |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
+ |> Unsynchronized.setmp Future.ML_statistics (Options.bool options "ML_statistics")
+ |> no_document options ? Present.no_document
+ |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
+ |> Unsynchronized.setmp Toplevel.skip_proofs (Options.bool options "skip_proofs")
+ |> Unsynchronized.setmp Printer.show_question_marks_default
+ (Options.bool options "show_question_marks")
+ |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")
+ |> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short")
+ |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique")
+ |> Unsynchronized.setmp Thy_Output.display_default (Options.bool options "thy_output_display")
+ |> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes")
+ |> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent")
+ |> Unsynchronized.setmp Thy_Output.source_default (Options.bool options "thy_output_source")
+ |> Unsynchronized.setmp Thy_Output.break_default (Options.bool options "thy_output_break")
+ |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
+ |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
+
+fun use_theories (options, thys) =
+ let val condition = space_explode "," (Options.string options "condition") in
+ (case filter_out (can getenv_strict) condition of
+ [] => use_thys options (map (rpair Position.none) thys)
+ | conds =>
+ Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
+ " (undefined " ^ commas conds ^ ")\n"))
+ end;
+
+in
+
+fun build args_file = Command_Line.tool (fn () =>
+ let
+ val (do_output, (options, (verbose, (browser_info, (parent_name,
+ (name, theories)))))) =
+ File.read (Path.explode args_file) |> YXML.parse_body |>
+ let open XML.Decode in
+ pair bool (pair Options.decode (pair bool (pair string (pair string
+ (pair string ((list (pair Options.decode (list string)))))))))
+ end;
+
+ val document_variants =
+ map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
+ val _ =
+ (case duplicates (op =) (map fst document_variants) of
+ [] => ()
+ | dups => error ("Duplicate document variants: " ^ commas_quote dups));
+
+ val _ =
+ Session.init do_output false
+ (Options.bool options "browser_info") browser_info
+ (Options.string options "document")
+ (Options.bool options "document_graph")
+ (Options.string options "document_output")
+ document_variants
+ parent_name name
+ (false, "") ""
+ verbose;
+
+ val res1 =
+ theories |>
+ (List.app use_theories
+ |> Session.with_timing name verbose
+ |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
+ |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
+ |> Exn.capture);
+ val res2 = Exn.capture Session.finish ();
+ val _ = Par_Exn.release_all [res1, res2];
+
+ val _ = if do_output then () else exit 0;
+ in 0 end);
+
+end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/build.scala Wed Jan 02 22:16:16 2013 +0100
@@ -0,0 +1,750 @@
+/* Title: Pure/Tools/build.scala
+ Author: Makarius
+ Options: :folding=explicit:collapseFolds=1:
+
+Build and manage Isabelle sessions.
+*/
+
+package isabelle
+
+
+import java.util.{Timer, TimerTask}
+import java.io.{BufferedInputStream, FileInputStream,
+ BufferedReader, InputStreamReader, IOException}
+import java.util.zip.GZIPInputStream
+
+import scala.collection.SortedSet
+import scala.annotation.tailrec
+
+
+object Build
+{
+ /** progress context **/
+
+ class Progress {
+ def echo(msg: String) {}
+ def stopped: Boolean = false
+ }
+
+ object Ignore_Progress extends Progress
+
+ object Console_Progress extends Progress {
+ override def echo(msg: String) { java.lang.System.out.println(msg) }
+ }
+
+
+
+ /** session information **/
+
+ // external version
+ sealed case class Session_Entry(
+ pos: Position.T,
+ name: String,
+ groups: List[String],
+ path: String,
+ parent: Option[String],
+ description: String,
+ options: List[Options.Spec],
+ theories: List[(List[Options.Spec], List[String])],
+ files: List[String])
+
+ // internal version
+ sealed case class Session_Info(
+ select: Boolean,
+ pos: Position.T,
+ groups: List[String],
+ dir: Path,
+ parent: Option[String],
+ description: String,
+ options: Options,
+ theories: List[(Options, List[Path])],
+ files: List[Path],
+ entry_digest: SHA1.Digest)
+
+ def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
+
+ def session_info(options: Options, select: Boolean, dir: Path, entry: Session_Entry)
+ : (String, Session_Info) =
+ try {
+ val name = entry.name
+
+ if (name == "") error("Bad session name")
+ if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
+ if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
+
+ val session_options = options ++ entry.options
+
+ val theories =
+ entry.theories.map({ case (opts, thys) =>
+ (session_options ++ opts, thys.map(Path.explode(_))) })
+ val files = entry.files.map(Path.explode(_))
+ val entry_digest = SHA1.digest((name, entry.parent, entry.options, entry.theories).toString)
+
+ val info =
+ Session_Info(select, entry.pos, entry.groups, dir + Path.explode(entry.path),
+ entry.parent, entry.description, session_options, theories, files, entry_digest)
+
+ (name, info)
+ }
+ catch {
+ case ERROR(msg) =>
+ error(msg + "\nThe error(s) above occurred in session entry " +
+ quote(entry.name) + Position.here(entry.pos))
+ }
+
+
+ /* session tree */
+
+ object Session_Tree
+ {
+ def apply(infos: Seq[(String, Session_Info)]): Session_Tree =
+ {
+ val graph1 =
+ (Graph.string[Session_Info] /: infos) {
+ case (graph, (name, info)) =>
+ if (graph.defined(name))
+ error("Duplicate session " + quote(name) + Position.here(info.pos))
+ else graph.new_node(name, info)
+ }
+ val graph2 =
+ (graph1 /: graph1.entries) {
+ case (graph, (name, (info, _))) =>
+ info.parent match {
+ case None => graph
+ case Some(parent) =>
+ if (!graph.defined(parent))
+ error("Bad parent session " + quote(parent) + " for " +
+ quote(name) + Position.here(info.pos))
+
+ try { graph.add_edge_acyclic(parent, name) }
+ catch {
+ case exn: Graph.Cycles[_] =>
+ error(cat_lines(exn.cycles.map(cycle =>
+ "Cyclic session dependency of " +
+ cycle.map(c => quote(c.toString)).mkString(" via "))) +
+ Position.here(info.pos))
+ }
+ }
+ }
+ new Session_Tree(graph2)
+ }
+ }
+
+ final class Session_Tree private(val graph: Graph[String, Session_Info])
+ extends PartialFunction[String, Session_Info]
+ {
+ def apply(name: String): Session_Info = graph.get_node(name)
+ def isDefinedAt(name: String): Boolean = graph.defined(name)
+
+ def selection(requirements: Boolean, all_sessions: Boolean,
+ session_groups: List[String], sessions: List[String]): (List[String], Session_Tree) =
+ {
+ val bad_sessions = sessions.filterNot(isDefinedAt(_))
+ if (!bad_sessions.isEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
+
+ val pre_selected =
+ {
+ if (all_sessions) graph.keys.toList
+ else {
+ val select_group = session_groups.toSet
+ val select = sessions.toSet
+ (for {
+ (name, (info, _)) <- graph.entries
+ if info.select || select(name) || apply(name).groups.exists(select_group)
+ } yield name).toList
+ }
+ }
+ val selected =
+ if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
+ else pre_selected
+
+ val tree1 = new Session_Tree(graph.restrict(graph.all_preds(selected).toSet))
+ (selected, tree1)
+ }
+
+ def topological_order: List[(String, Session_Info)] =
+ graph.topological_order.map(name => (name, apply(name)))
+
+ override def toString: String = graph.entries.map(_._1).toList.sorted.mkString(",")
+ }
+
+
+ /* parser */
+
+ private val SESSION = "session"
+ private val IN = "in"
+ private val DESCRIPTION = "description"
+ private val OPTIONS = "options"
+ private val THEORIES = "theories"
+ private val FILES = "files"
+
+ lazy val root_syntax =
+ Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
+ (SESSION, Keyword.THY_DECL) + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
+
+ private object Parser extends Parse.Parser
+ {
+ def session_entry(pos: Position.T): Parser[Session_Entry] =
+ {
+ val session_name = atom("session name", _.is_name)
+
+ val option =
+ name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
+ val options = keyword("[") ~> rep1sep(option, keyword(",")) <~ keyword("]")
+
+ val theories =
+ keyword(THEORIES) ~! ((options | success(Nil)) ~ rep(theory_name)) ^^
+ { case _ ~ (x ~ y) => (x, y) }
+
+ command(SESSION) ~!
+ (session_name ~
+ ((keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
+ ((keyword(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
+ (keyword("=") ~!
+ (opt(session_name ~! keyword("+") ^^ { case x ~ _ => x }) ~
+ ((keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
+ ((keyword(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
+ rep1(theories) ~
+ ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil))))) ^^
+ { case _ ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h))) =>
+ Session_Entry(pos, a, b, c, d, e, f, g, h) }
+ }
+
+ def parse_entries(root: Path): List[Session_Entry] =
+ {
+ val toks = root_syntax.scan(File.read(root))
+ parse_all(rep(session_entry(root.position)), Token.reader(toks, root.implode)) match {
+ case Success(result, _) => result
+ case bad => error(bad.toString)
+ }
+ }
+ }
+
+
+ /* find sessions within certain directories */
+
+ private val ROOT = Path.explode("ROOT")
+ private val ROOTS = Path.explode("ROOTS")
+
+ private def is_session_dir(dir: Path): Boolean =
+ (dir + ROOT).is_file || (dir + ROOTS).is_file
+
+ private def check_session_dir(dir: Path): Path =
+ if (is_session_dir(dir)) dir
+ else error("Bad session root directory: " + dir.toString)
+
+ def find_sessions(options: Options, more_dirs: List[(Boolean, Path)]): Session_Tree =
+ {
+ def find_dir(select: Boolean, dir: Path): List[(String, Session_Info)] =
+ find_root(select, dir) ::: find_roots(select, dir)
+
+ def find_root(select: Boolean, dir: Path): List[(String, Session_Info)] =
+ {
+ val root = dir + ROOT
+ if (root.is_file) Parser.parse_entries(root).map(session_info(options, select, dir, _))
+ else Nil
+ }
+
+ def find_roots(select: Boolean, dir: Path): List[(String, Session_Info)] =
+ {
+ val roots = dir + ROOTS
+ if (roots.is_file) {
+ for {
+ line <- split_lines(File.read(roots))
+ if !(line == "" || line.startsWith("#"))
+ dir1 =
+ try { check_session_dir(dir + Path.explode(line)) }
+ catch {
+ case ERROR(msg) =>
+ error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
+ }
+ info <- find_dir(select, dir1)
+ } yield info
+ }
+ else Nil
+ }
+
+ val default_dirs = Isabelle_System.components().filter(is_session_dir(_)).map((false, _))
+
+ more_dirs foreach { case (_, dir) => check_session_dir(dir) }
+
+ Session_Tree(
+ for {
+ (select, dir) <- default_dirs ::: more_dirs
+ info <- find_dir(select, dir)
+ } yield info)
+ }
+
+
+
+ /** build **/
+
+ /* queue */
+
+ object Queue
+ {
+ def apply(tree: Session_Tree): Queue =
+ {
+ val graph = tree.graph
+
+ def outdegree(name: String): Int = graph.imm_succs(name).size
+ def timeout(name: String): Double = tree(name).options.real("timeout")
+
+ object Ordering extends scala.math.Ordering[String]
+ {
+ def compare(name1: String, name2: String): Int =
+ outdegree(name2) compare outdegree(name1) match {
+ case 0 =>
+ timeout(name2) compare timeout(name1) match {
+ case 0 => name1 compare name2
+ case ord => ord
+ }
+ case ord => ord
+ }
+ }
+
+ new Queue(graph, SortedSet(graph.keys.toList: _*)(Ordering))
+ }
+ }
+
+ final class Queue private(graph: Graph[String, Session_Info], order: SortedSet[String])
+ {
+ def is_inner(name: String): Boolean = !graph.is_maximal(name)
+
+ def is_empty: Boolean = graph.is_empty
+
+ def - (name: String): Queue = new Queue(graph.del_node(name), order - name)
+
+ def dequeue(skip: String => Boolean): Option[(String, Session_Info)] =
+ {
+ val it = order.iterator.dropWhile(name => skip(name) || !graph.is_minimal(name))
+ if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) }
+ else None
+ }
+ }
+
+
+ /* source dependencies and static content */
+
+ sealed case class Session_Content(
+ loaded_theories: Set[String],
+ syntax: Outer_Syntax,
+ sources: List[(Path, SHA1.Digest)],
+ errors: List[String])
+ {
+ def check_errors: Session_Content =
+ {
+ if (errors.isEmpty) this
+ else error(cat_lines(errors))
+ }
+ }
+
+ sealed case class Deps(deps: Map[String, Session_Content])
+ {
+ def is_empty: Boolean = deps.isEmpty
+ def apply(name: String): Session_Content = deps(name)
+ def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
+ }
+
+ def dependencies(progress: Build.Progress, inlined_files: Boolean,
+ verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps =
+ Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
+ { case (deps, (name, info)) =>
+ val (preloaded, parent_syntax, parent_errors) =
+ info.parent match {
+ case None =>
+ (Set.empty[String], Outer_Syntax.init_pure(), Nil)
+ case Some(parent_name) =>
+ val parent = deps(parent_name)
+ (parent.loaded_theories, parent.syntax, parent.errors)
+ }
+ val thy_info = new Thy_Info(new Thy_Load(preloaded, parent_syntax))
+
+ if (verbose || list_files) {
+ val groups =
+ if (info.groups.isEmpty) ""
+ else info.groups.mkString(" (", " ", ")")
+ progress.echo("Session " + name + groups)
+ }
+
+ val thy_deps =
+ thy_info.dependencies(inlined_files,
+ info.theories.map(_._2).flatten.
+ map(thy => Thy_Load.path_node_name(info.dir + Thy_Load.thy_path(thy))))
+
+ val loaded_theories = thy_deps.loaded_theories
+ val syntax = thy_deps.make_syntax
+
+ val all_files =
+ (thy_deps.deps.map({ case dep =>
+ val thy = Path.explode(dep.name.node)
+ val uses = dep.join_header.uses.map(p =>
+ Path.explode(dep.name.dir) + Path.explode(p._1))
+ thy :: uses
+ }).flatten ::: info.files.map(file => info.dir + file)).map(_.expand)
+
+ if (list_files)
+ progress.echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _)))
+
+ val sources =
+ try { all_files.map(p => (p, SHA1.digest(p.file))) }
+ catch {
+ case ERROR(msg) =>
+ error(msg + "\nThe error(s) above occurred in session " +
+ quote(name) + Position.here(info.pos))
+ }
+ val errors = parent_errors ::: thy_deps.deps.map(dep => dep.join_header.errors).flatten
+
+ deps + (name -> Session_Content(loaded_theories, syntax, sources, errors))
+ }))
+
+ def session_content(inlined_files: Boolean, dirs: List[Path], session: String): Session_Content =
+ {
+ val options = Options.init()
+ val (_, tree) =
+ find_sessions(options, dirs.map((false, _))).selection(false, false, Nil, List(session))
+ dependencies(Build.Ignore_Progress, inlined_files, false, false, tree)(session)
+ }
+
+ def outer_syntax(session: String): Outer_Syntax =
+ session_content(false, Nil, session).check_errors.syntax
+
+
+ /* jobs */
+
+ private class Job(name: String, info: Session_Info, output: Path, do_output: Boolean,
+ verbose: Boolean, browser_info: Path)
+ {
+ // global browser info dir
+ if (info.options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file)
+ {
+ browser_info.file.mkdirs()
+ File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
+ browser_info + Path.explode("isabelle.gif"))
+ File.write(browser_info + Path.explode("index.html"),
+ File.read(Path.explode("~~/lib/html/library_index_header.template")) +
+ File.read(Path.explode("~~/lib/html/library_index_content.template")) +
+ File.read(Path.explode("~~/lib/html/library_index_footer.template")))
+ }
+
+ def output_path: Option[Path] = if (do_output) Some(output) else None
+
+ private val parent = info.parent.getOrElse("")
+
+ private val args_file = File.tmp_file("args")
+ File.write(args_file, YXML.string_of_body(
+ if (is_pure(name)) Options.encode(info.options)
+ else
+ {
+ import XML.Encode._
+ pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
+ pair(string, list(pair(Options.encode, list(Path.encode)))))))))(
+ (do_output, (info.options, (verbose, (browser_info, (parent,
+ (name, info.theories)))))))
+ }))
+
+ private val env =
+ Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output),
+ (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
+ Isabelle_System.posix_path(args_file.getPath))
+
+ private val script =
+ if (is_pure(name)) {
+ if (do_output) "./build " + name + " \"$OUTPUT\""
+ else """ rm -f "$OUTPUT"; ./build """ + name
+ }
+ else {
+ """
+ . "$ISABELLE_HOME/lib/scripts/timestart.bash"
+ """ +
+ (if (do_output)
+ """
+ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT"
+ """
+ else
+ """
+ rm -f "$OUTPUT"; "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT"
+ """) +
+ """
+ RC="$?"
+
+ . "$ISABELLE_HOME/lib/scripts/timestop.bash"
+
+ if [ "$RC" -eq 0 ]; then
+ echo "Finished $TARGET ($TIMES_REPORT)" >&2
+ fi
+
+ exit "$RC"
+ """
+ }
+
+ private val (thread, result) =
+ Simple_Thread.future("build") { Isabelle_System.bash_env(info.dir.file, env, script) }
+
+ def terminate: Unit = thread.interrupt
+ def is_finished: Boolean = result.is_finished
+
+ @volatile private var timeout = false
+ private val time = info.options.seconds("timeout")
+ private val timer: Option[Timer] =
+ if (time.seconds > 0.0) {
+ val t = new Timer("build", true)
+ t.schedule(new TimerTask { def run = { terminate; timeout = true } }, time.ms)
+ Some(t)
+ }
+ else None
+
+ def join: (String, String, Int) = {
+ val (out, err, rc) = result.join
+ args_file.delete
+ timer.map(_.cancel())
+
+ val err1 =
+ if (rc == 130)
+ (if (err.isEmpty || err.endsWith("\n")) err else err + "\n") +
+ (if (timeout) "*** Timeout\n" else "*** Interrupt\n")
+ else err
+ (out, err1, rc)
+ }
+ }
+
+
+ /* log files and corresponding heaps */
+
+ private val LOG = Path.explode("log")
+ private def log(name: String): Path = LOG + Path.basic(name)
+ private def log_gz(name: String): Path = log(name).ext("gz")
+
+ private def sources_stamp(digests: List[SHA1.Digest]): String =
+ digests.map(_.toString).sorted.mkString("sources: ", " ", "")
+
+ private val no_heap: String = "heap: -"
+
+ private def heap_stamp(heap: Option[Path]): String =
+ {
+ "heap: " +
+ (heap match {
+ case Some(path) =>
+ val file = path.file
+ if (file.isFile) file.length.toString + " " + file.lastModified.toString
+ else "-"
+ case None => "-"
+ })
+ }
+
+ private def read_stamps(path: Path): Option[(String, String, String)] =
+ if (path.is_file) {
+ val stream = new GZIPInputStream (new BufferedInputStream(new FileInputStream(path.file)))
+ val reader = new BufferedReader(new InputStreamReader(stream, UTF8.charset))
+ val (s, h1, h2) =
+ try { (reader.readLine, reader.readLine, reader.readLine) }
+ finally { reader.close }
+ if (s != null && s.startsWith("sources: ") &&
+ h1 != null && h1.startsWith("heap: ") &&
+ h2 != null && h2.startsWith("heap: ")) Some((s, h1, h2))
+ else None
+ }
+ else None
+
+
+ /* build */
+
+ def build(
+ progress: Build.Progress,
+ options: Options,
+ requirements: Boolean = false,
+ all_sessions: Boolean = false,
+ build_heap: Boolean = false,
+ clean_build: Boolean = false,
+ more_dirs: List[(Boolean, Path)] = Nil,
+ session_groups: List[String] = Nil,
+ max_jobs: Int = 1,
+ list_files: Boolean = false,
+ no_build: Boolean = false,
+ system_mode: Boolean = false,
+ verbose: Boolean = false,
+ sessions: List[String] = Nil): Int =
+ {
+ val full_tree = find_sessions(options, more_dirs)
+ val (selected, selected_tree) =
+ full_tree.selection(requirements, all_sessions, session_groups, sessions)
+
+ val deps = dependencies(progress, true, verbose, list_files, selected_tree)
+ val queue = Queue(selected_tree)
+
+ def make_stamp(name: String): String =
+ sources_stamp(selected_tree(name).entry_digest :: deps.sources(name))
+
+ val (input_dirs, output_dir, browser_info) =
+ if (system_mode) {
+ val output_dir = Path.explode("~~/heaps/$ML_IDENTIFIER")
+ (List(output_dir), output_dir, Path.explode("~~/browser_info"))
+ }
+ else {
+ val output_dir = Path.explode("$ISABELLE_OUTPUT")
+ (output_dir :: Isabelle_System.find_logics_dirs(), output_dir,
+ Path.explode("$ISABELLE_BROWSER_INFO"))
+ }
+
+ // prepare log dir
+ (output_dir + LOG).file.mkdirs()
+
+ // optional cleanup
+ if (clean_build) {
+ for (name <- full_tree.graph.all_succs(selected)) {
+ val files =
+ List(Path.basic(name), log(name), log_gz(name)).map(output_dir + _).filter(_.is_file)
+ if (!files.isEmpty) progress.echo("Cleaning " + name + " ...")
+ if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete")
+ }
+ }
+
+ // scheduler loop
+ case class Result(current: Boolean, heap: String, rc: Int)
+
+ def sleep(): Unit = Thread.sleep(500)
+
+ @tailrec def loop(
+ pending: Queue,
+ running: Map[String, (String, Job)],
+ results: Map[String, Result]): Map[String, Result] =
+ {
+ if (pending.is_empty) results
+ else if (progress.stopped) {
+ for ((_, (_, job)) <- running) job.terminate
+ sleep(); loop(pending, running, results)
+ }
+ else
+ running.find({ case (_, (_, job)) => job.is_finished }) match {
+ case Some((name, (parent_heap, job))) =>
+ //{{{ finish job
+
+ val (out, err, rc) = job.join
+ progress.echo(Library.trim_line(err))
+
+ val heap =
+ if (rc == 0) {
+ (output_dir + log(name)).file.delete
+
+ val sources = make_stamp(name)
+ val heap = heap_stamp(job.output_path)
+ File.write_gzip(output_dir + log_gz(name),
+ sources + "\n" + parent_heap + "\n" + heap + "\n" + out)
+
+ heap
+ }
+ else {
+ (output_dir + Path.basic(name)).file.delete
+ (output_dir + log_gz(name)).file.delete
+
+ File.write(output_dir + log(name), out)
+ progress.echo(name + " FAILED")
+ if (rc != 130) {
+ progress.echo("(see also " + (output_dir + log(name)).file.toString + ")")
+ val lines = split_lines(out)
+ val tail = lines.drop(lines.length - 20 max 0)
+ progress.echo("\n" + cat_lines(tail))
+ }
+
+ no_heap
+ }
+ loop(pending - name, running - name, results + (name -> Result(false, heap, rc)))
+ //}}}
+ case None if (running.size < (max_jobs max 1)) =>
+ //{{{ check/start next job
+ pending.dequeue(running.isDefinedAt(_)) match {
+ case Some((name, info)) =>
+ val parent_result =
+ info.parent match {
+ case None => Result(true, no_heap, 0)
+ case Some(parent) => results(parent)
+ }
+ val output = output_dir + Path.basic(name)
+ val do_output = build_heap || queue.is_inner(name)
+
+ val (current, heap) =
+ {
+ input_dirs.find(dir => (dir + log_gz(name)).is_file) match {
+ case Some(dir) =>
+ read_stamps(dir + log_gz(name)) match {
+ case Some((s, h1, h2)) =>
+ val heap = heap_stamp(Some(dir + Path.basic(name)))
+ (s == make_stamp(name) && h1 == parent_result.heap && h2 == heap &&
+ !(do_output && heap == no_heap), heap)
+ case None => (false, no_heap)
+ }
+ case None => (false, no_heap)
+ }
+ }
+ val all_current = current && parent_result.current
+
+ if (all_current)
+ loop(pending - name, running, results + (name -> Result(true, heap, 0)))
+ else if (no_build) {
+ if (verbose) progress.echo("Skipping " + name + " ...")
+ loop(pending - name, running, results + (name -> Result(false, heap, 1)))
+ }
+ else if (parent_result.rc == 0) {
+ progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
+ val job = new Job(name, info, output, do_output, verbose, browser_info)
+ loop(pending, running + (name -> (parent_result.heap, job)), results)
+ }
+ else {
+ progress.echo(name + " CANCELLED")
+ loop(pending - name, running, results + (name -> Result(false, heap, 1)))
+ }
+ case None => sleep(); loop(pending, running, results)
+ }
+ ///}}}
+ case None => sleep(); loop(pending, running, results)
+ }
+ }
+
+ val results =
+ if (deps.is_empty) {
+ progress.echo("### Nothing to build")
+ Map.empty
+ }
+ else loop(queue, Map.empty, Map.empty)
+
+ val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
+ if (rc != 0 && (verbose || !no_build)) {
+ val unfinished =
+ (for ((name, res) <- results.iterator if res.rc != 0) yield name).toList
+ .sorted(scala.math.Ordering.String) // FIXME scala-2.10.0-RC1
+ progress.echo("Unfinished session(s): " + commas(unfinished))
+ }
+ rc
+ }
+
+
+ /* command line entry point */
+
+ def main(args: Array[String])
+ {
+ Command_Line.tool {
+ args.toList match {
+ case
+ Properties.Value.Boolean(requirements) ::
+ Properties.Value.Boolean(all_sessions) ::
+ Properties.Value.Boolean(build_heap) ::
+ Properties.Value.Boolean(clean_build) ::
+ Properties.Value.Int(max_jobs) ::
+ Properties.Value.Boolean(list_files) ::
+ Properties.Value.Boolean(no_build) ::
+ Properties.Value.Boolean(system_mode) ::
+ Properties.Value.Boolean(verbose) ::
+ Command_Line.Chunks(select_dirs, include_dirs, session_groups, build_options, sessions) =>
+ val options = (Options.init() /: build_options)(_ + _)
+ val dirs =
+ select_dirs.map(d => (true, Path.explode(d))) :::
+ include_dirs.map(d => (false, Path.explode(d)))
+ build(Build.Console_Progress, options, requirements, all_sessions, build_heap,
+ clean_build, dirs, session_groups, max_jobs, list_files, no_build, system_mode,
+ verbose, sessions)
+ case _ => error("Bad arguments:\n" + cat_lines(args))
+ }
+ }
+ }
+}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/build_dialog.scala Wed Jan 02 22:16:16 2013 +0100
@@ -0,0 +1,135 @@
+/* Title: Pure/Tools/build_dialog.scala
+ Author: Makarius
+
+Dialog for session build process.
+*/
+
+package isabelle
+
+
+import java.awt.{GraphicsEnvironment, Point, Font}
+
+import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
+ BorderPanel, MainFrame, TextArea, SwingApplication}
+import scala.swing.event.ButtonClicked
+
+
+object Build_Dialog
+{
+ def main(args: Array[String]) =
+ {
+ Platform.init_laf()
+ try {
+ args.toList match {
+ case
+ logic_option ::
+ logic ::
+ Properties.Value.Boolean(system_mode) ::
+ include_dirs =>
+ val more_dirs = include_dirs.map(s => ((false, Path.explode(s))))
+
+ val options = Options.init()
+ val session =
+ Isabelle_System.default_logic(logic,
+ if (logic_option != "") options.string(logic_option) else "")
+
+ if (Build.build(Build.Ignore_Progress, options, build_heap = true, no_build = true,
+ more_dirs = more_dirs, sessions = List(session)) == 0) sys.exit(0)
+ else
+ Swing_Thread.later {
+ val top = build_dialog(options, system_mode, more_dirs, session)
+ top.pack()
+
+ val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
+ top.location =
+ new Point(point.x - top.size.width / 2, point.y - top.size.height / 2)
+
+ top.visible = true
+ }
+ case _ => error("Bad arguments:\n" + cat_lines(args))
+ }
+ }
+ catch {
+ case exn: Throwable =>
+ Library.error_dialog(null, "Isabelle build failure",
+ Library.scrollable_text(Exn.message(exn)))
+ sys.exit(2)
+ }
+ }
+
+
+ def build_dialog(
+ options: Options,
+ system_mode: Boolean,
+ more_dirs: List[(Boolean, Path)],
+ session: String): MainFrame = new MainFrame
+ {
+ /* GUI state */
+
+ private var is_stopped = false
+ private var return_code = 0
+
+
+ /* text */
+
+ val text = new TextArea {
+ font = new Font("SansSerif", Font.PLAIN, 14)
+ editable = false
+ columns = 40
+ rows = 10
+ }
+
+ val progress = new Build.Progress
+ {
+ override def echo(msg: String): Unit = Swing_Thread.now { text.append(msg + "\n") }
+ override def stopped: Boolean =
+ Swing_Thread.now { val b = is_stopped; is_stopped = false; b }
+ }
+
+
+ /* action button */
+
+ var button_action: () => Unit = (() => is_stopped = true)
+ val button = new Button("Cancel") {
+ reactions += { case ButtonClicked(_) => button_action() }
+ }
+ def button_exit(rc: Int)
+ {
+ button.text = if (rc == 0) "OK" else "Exit"
+ button_action = (() => sys.exit(rc))
+ button.peer.getRootPane.setDefaultButton(button.peer)
+ }
+
+ val action_panel = new FlowPanel(FlowPanel.Alignment.Center)(button)
+
+
+ /* layout panel */
+
+ val layout_panel = new BorderPanel
+ layout_panel.layout(new ScrollPane(text)) = BorderPanel.Position.Center
+ layout_panel.layout(action_panel) = BorderPanel.Position.South
+
+ contents = layout_panel
+
+
+ /* main build */
+
+ title = "Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")"
+ progress.echo("Build started for Isabelle/" + session + " ...")
+
+ default_thread_pool.submit(() => {
+ val (out, rc) =
+ try {
+ ("",
+ Build.build(progress, options, build_heap = true, more_dirs = more_dirs,
+ system_mode = system_mode, sessions = List(session)))
+ }
+ catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) }
+ Swing_Thread.now {
+ progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
+ button_exit(rc)
+ }
+ })
+ }
+}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/main.scala Wed Jan 02 22:16:16 2013 +0100
@@ -0,0 +1,31 @@
+/* Title: Pure/Tools/main.scala
+ Author: Makarius
+
+Default Isabelle application wrapper.
+*/
+
+package isabelle
+
+import scala.swing.TextArea
+
+
+object Main
+{
+ def main(args: Array[String])
+ {
+ val (out, rc) =
+ try {
+ Platform.init_laf()
+ Isabelle_System.init()
+ Isabelle_System.isabelle_tool("jedit", args: _*)
+ }
+ catch { case exn: Throwable => (Exn.message(exn), 2) }
+
+ if (rc != 0)
+ Library.dialog(null, "Isabelle", "Isabelle output",
+ Library.scrollable_text(out + "\nReturn code: " + rc))
+
+ sys.exit(rc)
+ }
+}
+
--- a/src/Pure/build-jars Wed Jan 02 20:53:01 2013 +0100
+++ b/src/Pure/build-jars Wed Jan 02 22:16:16 2013 +0100
@@ -30,6 +30,7 @@
Isar/outer_syntax.scala
Isar/parse.scala
Isar/token.scala
+ ML/ml_statistics.scala
PIDE/command.scala
PIDE/document.scala
PIDE/markup.scala
@@ -38,8 +39,6 @@
PIDE/text.scala
PIDE/xml.scala
PIDE/yxml.scala
- System/build.scala
- System/build_dialog.scala
System/color_value.scala
System/command_line.scala
System/event_bus.scala
@@ -50,7 +49,6 @@
System/isabelle_process.scala
System/isabelle_system.scala
System/jfx_thread.scala
- System/main.scala
System/options.scala
System/platform.scala
System/session.scala
@@ -63,6 +61,9 @@
Thy/thy_info.scala
Thy/thy_load.scala
Thy/thy_syntax.scala
+ Tools/build.scala
+ Tools/build_dialog.scala
+ Tools/main.scala
library.scala
package.scala
term.scala
@@ -125,6 +126,15 @@
[ "$#" -ne 0 ] && usage
+## dependencies
+
+declare -a JFREECHART_JARS=()
+for NAME in $JFREECHART_JAR_NAMES
+do
+ JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$JFREECHART_HOME/lib/$NAME"
+done
+
+
## build
TARGET_DIR="$ISABELLE_HOME/lib/classes"
@@ -181,18 +191,23 @@
JFXRT="$ISABELLE_JDK_HOME/jre/lib/jfxrt.jar"
- if [ "$TEST_PIDE" = true ]; then
- isabelle_scala scalac $SCALAC_OPTIONS \
- -classpath "$(jvmpath "$JFXRT:classes")" "${PIDE_SOURCES[@]}" || \
- fail "Failed to compile PIDE sources"
- isabelle_scala scalac $SCALAC_OPTIONS \
- -classpath "$(jvmpath "$JFXRT:classes")" "${PURE_SOURCES[@]}" || \
- fail "Failed to compile Pure sources"
- else
- isabelle_scala scalac $SCALAC_OPTIONS \
- -classpath "$(jvmpath "$JFXRT:classes")" "${PIDE_SOURCES[@]}" "${PURE_SOURCES[@]}" || \
- fail "Failed to compile sources"
- fi
+ (
+ for X in "$JFXRT" "${JFREECHART_JARS[@]}" classes
+ do
+ CLASSPATH="$CLASSPATH:$X"
+ done
+ CLASSPATH="$(jvmpath "$CLASSPATH")"
+
+ if [ "$TEST_PIDE" = true ]; then
+ isabelle_scala scalac $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" || \
+ fail "Failed to compile PIDE sources"
+ isabelle_scala scalac $SCALAC_OPTIONS "${PURE_SOURCES[@]}" || \
+ fail "Failed to compile Pure sources"
+ else
+ isabelle_scala scalac $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" "${PURE_SOURCES[@]}" || \
+ fail "Failed to compile sources"
+ fi
+ )
mkdir -p "$TARGET_DIR/ext" || fail "Failed to create directory $TARGET_DIR/ext"