# HG changeset patch # User wenzelm # Date 1494792436 -7200 # Node ID d081671d4a876b9a23bcc2d3d26b2ba795d5ecae # Parent 8ee1799fb07674ec29500230c29aa08ed49415d8# Parent 30c2d78b5d3817d4a903ef4b375e6079bcf9abf8 merged diff -r 8ee1799fb076 -r d081671d4a87 etc/isabelle.css --- a/etc/isabelle.css Sun May 14 13:55:51 2017 +0200 +++ b/etc/isabelle.css Sun May 14 22:07:16 2017 +0200 @@ -16,6 +16,16 @@ src: url('fonts/Vacuous.ttf') format('truetype'); } + +/* standard document markup */ + +dt { + float: left; + clear: left; + padding-right: 0.5em; + font-weight: bold; +} + body { background-color: #FFFFFF; } .head { background-color: #FFFFFF; } @@ -65,4 +75,3 @@ .comment { color: #CC0000; } .improper { color: #FF5050; } .bad { background-color: #FF6A6A; } - diff -r 8ee1799fb076 -r d081671d4a87 src/HOL/Analysis/Great_Picard.thy --- a/src/HOL/Analysis/Great_Picard.thy Sun May 14 13:55:51 2017 +0200 +++ b/src/HOL/Analysis/Great_Picard.thy Sun May 14 22:07:16 2017 +0200 @@ -614,7 +614,7 @@ qed -subsection\The Arzelà–Ascoli theorem\ +subsection\The Arzelà--Ascoli theorem\ lemma subsequence_diagonalization_lemma: fixes P :: "nat \ (nat \ 'a) \ bool" diff -r 8ee1799fb076 -r d081671d4a87 src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala Sun May 14 13:55:51 2017 +0200 +++ b/src/Pure/Admin/build_release.scala Sun May 14 22:07:16 2017 +0200 @@ -123,21 +123,18 @@ info.all_bundles.find(name => (release_info.dist_dir + Path.explode(name)).is_file) } yield (bundle, info) - Isabelle_System.mkdirs(dir) - val afp_link = HTML.link("https://bitbucket.org/isa-afp/afp-devel/commits/" + afp_rev, HTML.text("AFP/" + afp_rev)) - File.write(dir + Path.explode("index.html"), - HTML.output_document( - List(HTML.title(release_info.name)), - List( - HTML.chapter(release_info.name + " (" + release_id + ")"), - HTML.itemize( - website_platform_bundles.map({ case (bundle, info) => - List(HTML.link(bundle, HTML.text(info.platform_description))) }))) ::: - (if (afp_rev == "") Nil else List(HTML.par(HTML.text("See also ") ::: List(afp_link)))))) + HTML.write_document(dir, "index.html", + List(HTML.title(release_info.name)), + List( + HTML.chapter(release_info.name + " (" + release_id + ")"), + HTML.itemize( + website_platform_bundles.map({ case (bundle, info) => + List(HTML.link(bundle, HTML.text(info.platform_description))) }))) ::: + (if (afp_rev == "") Nil else List(HTML.par(HTML.text("See also ") ::: List(afp_link))))) for ((bundle, _) <- website_platform_bundles) File.copy(release_info.dist_dir + Path.explode(bundle), dir) diff -r 8ee1799fb076 -r d081671d4a87 src/Pure/Admin/build_status.scala --- a/src/Pure/Admin/build_status.scala Sun May 14 13:55:51 2017 +0200 +++ b/src/Pure/Admin/build_status.scala Sun May 14 22:07:16 2017 +0200 @@ -203,18 +203,16 @@ def clean_name(name: String): String = name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString) - Isabelle_System.mkdirs(target_dir) - File.write(target_dir + Path.basic("index.html"), - HTML.output_document( - List(HTML.title("Isabelle build status")), - List(HTML.chapter("Isabelle build status"), - HTML.par( - List(HTML.itemize( - List(HTML.bold(HTML.text("status date: ")) :: HTML.text(data.date.toString))))), - HTML.par( - List(HTML.itemize(data.entries.map({ case data_entry => - List(HTML.link(clean_name(data_entry.name) + "/index.html", - HTML.text(data_entry.name))) }))))))) + HTML.write_document(target_dir, "index.html", + List(HTML.title("Isabelle build status")), + List(HTML.chapter("Isabelle build status"), + HTML.par( + List(HTML.description( + List(HTML.text("status date:") -> HTML.text(data.date.toString))))), + HTML.par( + List(HTML.itemize(data.entries.map({ case data_entry => + List(HTML.link(clean_name(data_entry.name) + "/index.html", + HTML.text(data_entry.name))) })))))) for (data_entry <- data.entries) { val data_name = data_entry.name @@ -308,36 +306,35 @@ } }, data_entry.sessions).toMap - File.write(dir + Path.basic("index.html"), - HTML.output_document( - List(HTML.title("Isabelle build status for " + data_name)), - HTML.chapter("Isabelle build status for " + data_name) :: - HTML.par( - List(HTML.itemize( - List( - HTML.bold(HTML.text("status date: ")) :: HTML.text(data.date.toString), - HTML.bold(HTML.text("build host: ")) :: HTML.text(commas(data_entry.hosts)))))) :: - HTML.par( - List(HTML.itemize( - data_entry.sessions.map(session => - HTML.link("#session_" + session.name, HTML.text(session.name)) :: - HTML.text(" (" + session.timing.message_resources + ")"))))) :: - data_entry.sessions.flatMap(session => + HTML.write_document(dir, "index.html", + List(HTML.title("Isabelle build status for " + data_name)), + HTML.chapter("Isabelle build status for " + data_name) :: + HTML.par( + List(HTML.description( List( - HTML.section(session.name) + HTML.id("session_" + session.name), - HTML.par( - HTML.itemize(List( - HTML.bold(HTML.text("timing: ")) :: HTML.text(session.timing.message_resources), - HTML.bold(HTML.text("ML timing: ")) :: - HTML.text(session.ml_timing.message_resources)) ::: - proper_string(session.isabelle_version).map(s => - HTML.bold(HTML.text("Isabelle version: ")) :: HTML.text(s)).toList ::: - proper_string(session.afp_version).map(s => - HTML.bold(HTML.text("AFP version: ")) :: HTML.text(s)).toList) :: - session_plots.getOrElse(session.name, Nil).map(plot_name => - HTML.image(plot_name) + - HTML.width(image_width / 2) + - HTML.height(image_height / 2))))))) + HTML.text("status date:") -> HTML.text(data.date.toString), + HTML.text("build host:") -> HTML.text(commas(data_entry.hosts)))))) :: + HTML.par( + List(HTML.itemize( + data_entry.sessions.map(session => + HTML.link("#session_" + session.name, HTML.text(session.name)) :: + HTML.text(" (" + session.timing.message_resources + ")"))))) :: + data_entry.sessions.flatMap(session => + List( + HTML.section(session.name) + HTML.id("session_" + session.name), + HTML.par( + HTML.description( + List( + HTML.text("timing:") -> HTML.text(session.timing.message_resources), + HTML.text("ML timing:") -> HTML.text(session.ml_timing.message_resources)) ::: + proper_string(session.isabelle_version).map(s => + HTML.text("Isabelle version:") -> HTML.text(s)).toList ::: + proper_string(session.afp_version).map(s => + HTML.text("AFP version:") -> HTML.text(s)).toList) :: + session_plots.getOrElse(session.name, Nil).map(plot_name => + HTML.image(plot_name) + + HTML.width(image_width / 2) + + HTML.height(image_height / 2)))))) } } diff -r 8ee1799fb076 -r d081671d4a87 src/Pure/Admin/check_sources.scala --- a/src/Pure/Admin/check_sources.scala Sun May 14 13:55:51 2017 +0200 +++ b/src/Pure/Admin/check_sources.scala Sun May 14 22:07:16 2017 +0200 @@ -49,7 +49,7 @@ Output.writeln("Checking " + root + " ...") val hg = Mercurial.repository(root) for { - file <- hg.manifest() + file <- hg.known_files() if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT") } check_file(root + Path.explode(file)) } @@ -63,7 +63,7 @@ val getopts = Getopts(""" Usage: isabelle check_sources [ROOT_DIRS...] - Check .thy, .ML, ROOT files from manifest of Mercurial ROOT_DIRS. + Check .thy, .ML, ROOT against known files of Mercurial ROOT_DIRS. """) val specs = getopts(args) diff -r 8ee1799fb076 -r d081671d4a87 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Sun May 14 13:55:51 2017 +0200 +++ b/src/Pure/Admin/isabelle_cronjob.scala Sun May 14 22:07:16 2017 +0200 @@ -105,8 +105,9 @@ user: String = "", port: Int = 0, shared_home: Boolean = true, + historic: Boolean = false, history: Int = 0, - historic: Boolean = false, + history_base: String = "build_history_base", options: String = "", args: String = "", detect: SQL.Source = "") @@ -119,14 +120,24 @@ def profile: Build_Status.Profile = Build_Status.Profile(description, history, sql) - def pick(options: Options, rev: String = ""): Option[String] = + def history_base_filter(hg: Mercurial.Repository): Set[String] = + { + val rev0 = hg.id(history_base) + val graph = hg.graph() + (rev0 :: graph.all_succs(List(rev0))).toSet + } + + def pick(options: Options, rev: String = "", filter: String => Boolean = (_: String) => true) + : Option[String] = { val store = Build_Log.store(options) using(store.open_database())(db => { def pick_days(days: Int): Option[String] = { - val items = recent_items(db, days = days, rev = rev, sql = sql) + val items = + recent_items(db, days = days, rev = rev, sql = sql). + filter(item => filter(item.isabelle_version)) def runs = unknown_runs(items) val known_rev = @@ -145,8 +156,8 @@ } pick_days(options.int("build_log_history") max history) orElse - pick_days(100) orElse - pick_days(1000) + pick_days(200) orElse + pick_days(2000) }) } } @@ -164,13 +175,14 @@ val remote_builds: List[List[Remote_Build]] = { List( - List(Remote_Build("Poly/ML 5.7 Linux", "lxbroy8", history = 90, historic = true, + List(Remote_Build("Poly/ML 5.7 Linux", "lxbroy8", historic = true, history = 90, + history_base = "37074e22e8be", options = "-m32 -B -M1x2,2 -t polyml-5.7 -e 'init_component /home/isabelle/contrib/polyml-5.7'", args = "-N -g timing", detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7"))), List(Remote_Build("Linux A", "lxbroy9", options = "-m32 -B -M1x2,2", args = "-N -g timing")), - List(Remote_Build("Linux B", "lxbroy10", history = 90, historic = true, + List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90, options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")), List( Remote_Build("Mac OS X 10.9 Mavericks", "macbroy2", options = "-m32 -M8", args = "-a", @@ -366,14 +378,17 @@ val main_start_date = Date.now() File.write(main_state_file, main_start_date + " " + log_service.hostname) - val rev = Mercurial.repository(isabelle_repos).id() + val hg = Mercurial.repository(isabelle_repos) + val rev = hg.id() run(main_start_date, Logger_Task("isabelle_cronjob", logger => run_now( SEQ(List(build_release, build_history_base, PAR(remote_builds.map(seq => - SEQ(seq.flatMap(r => r.pick(logger.options, rev).map(remote_build_history(_, r)))))), + SEQ(seq.flatMap(r => + r.pick(logger.options, rev, r.history_base_filter(hg)). + map(remote_build_history(_, r)))))), Logger_Task("jenkins_logs", _ => Jenkins.download_logs(jenkins_jobs, main_dir)), Logger_Task("build_log_database", logger => Isabelle_Devel.build_log_database(logger.options)), diff -r 8ee1799fb076 -r d081671d4a87 src/Pure/Admin/isabelle_devel.scala --- a/src/Pure/Admin/isabelle_devel.scala Sun May 14 13:55:51 2017 +0200 +++ b/src/Pure/Admin/isabelle_devel.scala Sun May 14 22:07:16 2017 +0200 @@ -25,27 +25,25 @@ { val header = "Isabelle Development Resources" - Isabelle_System.mkdirs(root) - File.write(root + Path.explode("index.html"), - HTML.output_document( - List(HTML.title(header)), - List(HTML.chapter(header), - HTML.itemize( - List( - HTML.text("Isabelle nightly ") ::: - List(HTML.link(RELEASE_SNAPSHOT, HTML.text("release snapshot"))) ::: - HTML.text(" (for all platforms)"), + HTML.write_document(root, "index.html", + List(HTML.title(header)), + List(HTML.chapter(header), + HTML.itemize( + List( + HTML.text("Isabelle nightly ") ::: + List(HTML.link(RELEASE_SNAPSHOT, HTML.text("release snapshot"))) ::: + HTML.text(" (for all platforms)"), - HTML.text("Isabelle ") ::: - List(HTML.link(BUILD_STATUS + "/index.html", HTML.text("build status"))) ::: - HTML.text(" information"), + HTML.text("Isabelle ") ::: + List(HTML.link(BUILD_STATUS + "/index.html", HTML.text("build status"))) ::: + HTML.text(" information"), - HTML.text("Database with recent ") ::: - List(HTML.link(BUILD_LOG_DB, HTML.text("build log"))) ::: - HTML.text(" information (e.g. for ") ::: - List(HTML.link("http://sqlitebrowser.org", - List(HTML.code(HTML.text("sqlitebrowser"))))) ::: - HTML.text(")")))))) + HTML.text("Database with recent ") ::: + List(HTML.link(BUILD_LOG_DB, HTML.text("build log"))) ::: + HTML.text(" information (e.g. for ") ::: + List(HTML.link("http://sqlitebrowser.org", + List(HTML.code(HTML.text("sqlitebrowser"))))) ::: + HTML.text(")"))))) } diff -r 8ee1799fb076 -r d081671d4a87 src/Pure/General/exn.scala --- a/src/Pure/General/exn.scala Sun May 14 13:55:51 2017 +0200 +++ b/src/Pure/General/exn.scala Sun May 14 22:07:16 2017 +0200 @@ -20,7 +20,7 @@ } override def hashCode: Int = message.hashCode - override def toString: String = "\n" + Output.error_text(message) + override def toString: String = "\n" + Output.error_message_text(message) } object ERROR diff -r 8ee1799fb076 -r d081671d4a87 src/Pure/General/http.scala --- a/src/Pure/General/http.scala Sun May 14 13:55:51 2017 +0200 +++ b/src/Pure/General/http.scala Sun May 14 22:07:16 2017 +0200 @@ -77,7 +77,7 @@ case Exn.Res(None) => http.write_response(404, Response.empty) case Exn.Exn(ERROR(msg)) => - http.write_response(500, Response.text(Output.error_text(msg))) + http.write_response(500, Response.text(Output.error_message_text(msg))) case Exn.Exn(exn) => throw exn } else http.write_response(400, Response.empty) diff -r 8ee1799fb076 -r d081671d4a87 src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Sun May 14 13:55:51 2017 +0200 +++ b/src/Pure/General/mercurial.scala Sun May 14 22:07:16 2017 +0200 @@ -10,6 +10,9 @@ import java.io.{File => JFile} +import scala.annotation.tailrec +import scala.collection.mutable + object Mercurial { @@ -68,7 +71,7 @@ case Some(ssh) => ssh.is_dir(root) } if (present) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg } - else clone_repository(source, root, options = "--noupdate", ssh = ssh) + else clone_repository(source, root, options = "--pull --noupdate", ssh = ssh) } class Repository private[Mercurial](root_path: Path, ssh: Option[SSH.Session]) @@ -96,7 +99,7 @@ def command(name: String, args: String = "", options: String = ""): Process_Result = { val cmdline = - "\"${HG:-hg}\"" + + "\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") + (if (name == "clone") "" else " --repository " + File.bash_path(root)) + " --noninteractive " + name + " " + options + " " + args ssh match { @@ -137,5 +140,50 @@ hg.command("update", opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check } + + def known_files(): List[String] = + hg.command("status", options = "--modified --added --clean --no-status").check.out_lines + + def graph(): Graph[String, Unit] = + { + val Node = """^node: (\w{12}) (\w{12}) (\w{12})""".r + val log_result = + log(template = """node: {node|short} {p1node|short} {p2node|short}\n""") + (Graph.string[Unit] /: split_lines(log_result)) { + case (graph, Node(x, y, z)) => + val deps = List(y, z).filterNot(s => s.forall(_ == '0')) + val graph1 = (graph /: (x :: deps))(_.default_node(_, ())) + (graph1 /: deps)({ case (g, dep) => g.add_edge(dep, x) }) + case (graph, _) => graph + } + } + } + + + /* unknown files */ + + def unknown_files(files: List[Path], ssh: Option[SSH.Session] = None): List[Path] = + { + val unknown = new mutable.ListBuffer[Path] + + @tailrec def check(paths: List[Path]) + { + paths match { + case path :: rest => + find_repository(path, ssh) match { + case None => unknown += path; check(rest) + case Some(hg) => + val known = + hg.known_files().iterator.map(name => + (hg.root + Path.explode(name)).canonical_file).toSet + if (!known(path.canonical_file)) unknown += path + check(rest.filterNot(p => known(p.canonical_file))) + } + case Nil => + } + } + + check(files) + unknown.toList } } diff -r 8ee1799fb076 -r d081671d4a87 src/Pure/General/output.scala --- a/src/Pure/General/output.scala Sun May 14 13:55:51 2017 +0200 +++ b/src/Pure/General/output.scala Sun May 14 22:07:16 2017 +0200 @@ -14,8 +14,12 @@ catch { case ERROR(_) => msg } def writeln_text(msg: String): String = clean_yxml(msg) - def warning_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("### " + _)) - def error_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("*** " + _)) + + def warning_text(msg: String): String = + cat_lines(split_lines(clean_yxml(msg)).map("### " + _)) + + def error_message_text(msg: String): String = + cat_lines(split_lines(clean_yxml(msg)).map("*** " + _)) def writeln(msg: String, stdout: Boolean = false) { @@ -36,8 +40,8 @@ def error_message(msg: String, stdout: Boolean = false) { if (msg != "") { - if (stdout) Console.println(error_text(msg)) - else Console.err.println(error_text(msg)) + if (stdout) Console.println(error_message_text(msg)) + else Console.err.println(error_message_text(msg)) } } } diff -r 8ee1799fb076 -r d081671d4a87 src/Pure/General/path.scala --- a/src/Pure/General/path.scala Sun May 14 13:55:51 2017 +0200 +++ b/src/Pure/General/path.scala Sun May 14 22:07:16 2017 +0200 @@ -211,4 +211,6 @@ def file: JFile = File.platform_file(this) def is_file: Boolean = file.isFile def is_dir: Boolean = file.isDirectory + + def canonical_file: JFile = file.getCanonicalFile } diff -r 8ee1799fb076 -r d081671d4a87 src/Pure/System/numa.scala --- a/src/Pure/System/numa.scala Sun May 14 13:55:51 2017 +0200 +++ b/src/Pure/System/numa.scala Sun May 14 22:07:16 2017 +0200 @@ -42,7 +42,7 @@ /* shuffling of CPU nodes */ - def enabled_warning(enabled: Boolean): Boolean = + def enabled_warning(progress: Progress, enabled: Boolean): Boolean = { def warning = if (nodes().length < 2) Some("no NUMA nodes available") @@ -51,7 +51,7 @@ enabled && (warning match { - case Some(s) => Output.warning("Shuffling of CPU nodes is disabled: " + s); false + case Some(s) => progress.echo_warning("Shuffling of CPU nodes is disabled: " + s); false case _ => true }) } diff -r 8ee1799fb076 -r d081671d4a87 src/Pure/System/progress.scala --- a/src/Pure/System/progress.scala Sun May 14 13:55:51 2017 +0200 +++ b/src/Pure/System/progress.scala Sun May 14 22:07:16 2017 +0200 @@ -16,6 +16,9 @@ def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) } def theory(session: String, theory: String) {} + def echo_warning(msg: String) { echo(Output.warning_text(msg)) } + def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) } + def stopped: Boolean = false override def toString: String = if (stopped) "Progress(stopped)" else "Progress" diff -r 8ee1799fb076 -r d081671d4a87 src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Sun May 14 13:55:51 2017 +0200 +++ b/src/Pure/Thy/html.scala Sun May 14 22:07:16 2017 +0200 @@ -58,6 +58,10 @@ /* output XML as HTML */ + private val structural_elements = + Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6", + "ul", "ol", "dl", "li", "dt", "dd") + def output(body: XML.Body, s: StringBuilder) { def attrib(p: (String, String)): Unit = @@ -69,9 +73,11 @@ case XML.Elem(markup, Nil) => s ++= "<"; elem(markup); s ++= "/>" case XML.Elem(markup, ts) => - s ++= "\n<"; elem(markup); s ++= ">" + if (structural_elements(markup.name)) s += '\n' + s ++= "<"; elem(markup); s ++= ">" ts.foreach(tree) - s ++= "\n" + s ++= "" + if (structural_elements(markup.name)) s += '\n' case XML.Text(txt) => output(txt, s) } body.foreach(tree) @@ -142,13 +148,32 @@ XML.Elem(Markup("meta", List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil) - def output_document(head: XML.Body, body: XML.Body): String = + def head_css(css: String): XML.Elem = + XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> css)), Nil) + + def output_document(head: XML.Body, body: XML.Body, css: String = "isabelle.css"): String = cat_lines( List(header, - output(XML.elem("head", head_meta :: head)), + output(XML.elem("head", head_meta :: (if (css == "") Nil else List(head_css(css))) ::: head)), output(XML.elem("body", body)))) + /* document directory */ + + def init_dir(dir: Path) + { + Isabelle_System.mkdirs(dir) + File.copy(Path.explode("~~/etc/isabelle.css"), dir) + } + + def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body, + css: String = "isabelle.css") + { + init_dir(dir) + File.write(dir + Path.basic(name), output_document(head, body, css)) + } + + /* Isabelle document */ def begin_document(title: String): String = diff -r 8ee1799fb076 -r d081671d4a87 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Sun May 14 13:55:51 2017 +0200 +++ b/src/Pure/Thy/sessions.scala Sun May 14 22:07:16 2017 +0200 @@ -37,9 +37,9 @@ def local_theories_iterator = { - val local_path = local_dir.file.getCanonicalFile.toPath + val local_path = local_dir.canonical_file.toPath theories.iterator.filter(name => - Path.explode(name.node).file.getCanonicalFile.toPath.startsWith(local_path)) + Path.explode(name.node).canonical_file.toPath.startsWith(local_path)) } val known_theories = @@ -60,7 +60,7 @@ (Map.empty[JFile, List[Document.Node.Name]] /: (bases_iterator(true) ++ bases_iterator(false) ++ theories.iterator))({ case (known, name) => - val file = Path.explode(name.node).file.getCanonicalFile + val file = Path.explode(name.node).canonical_file val theories1 = known.getOrElse(file, Nil) if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory)) known diff -r 8ee1799fb076 -r d081671d4a87 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sun May 14 13:55:51 2017 +0200 +++ b/src/Pure/Tools/build.scala Sun May 14 22:07:16 2017 +0200 @@ -34,7 +34,8 @@ private object Queue { - def load_timings(store: Sessions.Store, name: String): (List[Properties.T], Double) = + def load_timings(progress: Progress, store: Sessions.Store, name: String) + : (List[Properties.T], Double) = { val no_timings: (List[Properties.T], Double) = (Nil, 0.0) @@ -43,7 +44,7 @@ case Some(database) => def ignore_error(msg: String) = { - Output.warning("Ignoring bad database: " + + progress.echo_warning("Ignoring bad database: " + database.expand + (if (msg == "") "" else "\n" + msg)) no_timings } @@ -63,12 +64,12 @@ } } - def apply(sessions: Sessions.T, store: Sessions.Store): Queue = + def apply(progress: Progress, sessions: Sessions.T, store: Sessions.Store): Queue = { val graph = sessions.build_graph val names = graph.keys - val timings = names.map(name => (name, load_timings(store, name))) + val timings = names.map(name => (name, load_timings(progress, store, name))) val command_timings = Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil) val session_timing = @@ -245,7 +246,7 @@ case msg => result.copy( rc = result.rc max 1, - out_lines = result.out_lines ::: split_lines(Output.error_text(msg))) + out_lines = result.out_lines ::: split_lines(Output.error_message_text(msg))) } } else { @@ -309,8 +310,8 @@ timeout_request.foreach(_.cancel) if (result.interrupted) { - if (was_timeout) result.error(Output.error_text("Timeout")).was_timeout - else result.error(Output.error_text("Interrupt")) + if (was_timeout) result.error(Output.error_message_text("Timeout")).was_timeout + else result.error(Output.error_message_text("Interrupt")) } else result } @@ -337,6 +338,7 @@ def build( options: Options, progress: Progress = No_Progress, + check_unknown_files: Boolean = false, build_heap: Boolean = false, clean_build: Boolean = false, dirs: List[Path] = Nil, @@ -376,11 +378,24 @@ def sources_stamp(name: String): List[String] = (selected_sessions(name).meta_digest :: deps.sources(name)).map(_.toString).sorted + if (check_unknown_files) { + val source_files = + (for { + (_, base) <- deps.session_bases.iterator + (path, _) <- base.sources.iterator + } yield path).toList + val unknown_files = Mercurial.unknown_files(source_files) + if (unknown_files.nonEmpty) { + progress.echo_warning("Unknown files (not part of a Mercurial repository):" + + unknown_files.map(path => path.expand.implode).sorted.mkString("\n ", "\n ", "")) + } + } + /* main build process */ val store = Sessions.store(system_mode) - val queue = Queue(selected_sessions, store) + val queue = Queue(progress, selected_sessions, store) store.prepare_output() @@ -551,7 +566,7 @@ val results0 = if (deps.is_empty) { - progress.echo(Output.warning_text("Nothing to build")) + progress.echo_warning("Nothing to build") Map.empty[String, Result] } else loop(queue, Map.empty, Map.empty) @@ -679,11 +694,12 @@ val results = progress.interrupt_handler { build(options, progress, + check_unknown_files = Mercurial.is_repository(Path.explode("~~")), build_heap = build_heap, clean_build = clean_build, dirs = dirs, select_dirs = select_dirs, - numa_shuffling = NUMA.enabled_warning(numa_shuffling), + numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling), max_jobs = max_jobs, list_files = list_files, check_keywords = check_keywords, diff -r 8ee1799fb076 -r d081671d4a87 src/Pure/Tools/check_keywords.scala --- a/src/Pure/Tools/check_keywords.scala Sun May 14 13:55:51 2017 +0200 +++ b/src/Pure/Tools/check_keywords.scala Sun May 14 22:07:16 2017 +0200 @@ -46,9 +46,8 @@ }, parallel_args).flatten for ((tok, pos) <- bad) { - progress.echo(Output.warning_text( - "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) + - Position.here(pos))) + progress.echo_warning( + "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) + Position.here(pos)) } } } diff -r 8ee1799fb076 -r d081671d4a87 src/Pure/Tools/imports.scala --- a/src/Pure/Tools/imports.scala Sun May 14 13:55:51 2017 +0200 +++ b/src/Pure/Tools/imports.scala Sun May 14 22:07:16 2017 +0200 @@ -12,17 +12,18 @@ object Imports { - /* manifest */ + /* repository files */ - def manifest_files(start: Path, pred: JFile => Boolean = _ => true): List[JFile] = + def repository_files(progress: Progress, start: Path, pred: JFile => Boolean = _ => true) + : List[JFile] = Mercurial.find_repository(start) match { case None => - Output.warning("Ignoring directory " + start + " (no Mercurial repository)") + progress.echo_warning("Ignoring directory " + start + " (no Mercurial repository)") Nil case Some(hg) => - val start_path = start.file.getCanonicalFile.toPath + val start_path = start.canonical_file.toPath for { - name <- hg.manifest() + name <- hg.known_files() file = (hg.root + Path.explode(name)).file if pred(file) && file.getCanonicalFile.toPath.startsWith(start_path) } yield file @@ -45,7 +46,7 @@ { val file = pos match { - case Position.File(file) => Path.explode(file).file.getCanonicalFile + case Position.File(file) => Path.explode(file).canonical_file case _ => error("Missing file in position" + Position.here(pos)) } @@ -72,7 +73,7 @@ def imports( options: Options, operation_imports: Boolean = false, - operation_manifest: Boolean = false, + operation_repository_files: Boolean = false, operation_update: Boolean = false, progress: Progress = No_Progress, selection: Sessions.Selection = Sessions.Selection.empty, @@ -116,12 +117,12 @@ }) } - if (operation_manifest) { - progress.echo("\nManifest check:") + if (operation_repository_files) { + progress.echo("\nMercurial files check:") val unused_files = for { (_, dir) <- Sessions.directories(dirs, select_dirs) - file <- manifest_files(dir, file => file.getName.endsWith(".thy")) + file <- repository_files(progress, dir, file => file.getName.endsWith(".thy")) if deps.all_known.get_file(file).isEmpty } yield file unused_files.foreach(file => progress.echo("unused file " + quote(file.toString))) @@ -211,7 +212,7 @@ { var select_dirs: List[Path] = Nil var operation_imports = false - var operation_manifest = false + var operation_repository_files = false var requirements = false var operation_update = false var exclude_session_groups: List[String] = Nil @@ -228,7 +229,7 @@ Options are: -D DIR include session directory and select its sessions -I operation: report potential session imports - -M operation: Mercurial manifest check for imported theory files + -M operation: Mercurial files check for imported theory files -R operate on requirements of selected sessions -U operation: update theory imports to use session qualifiers -X NAME exclude sessions from group NAME and all descendants @@ -244,7 +245,7 @@ """, "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), "I" -> (_ => operation_imports = true), - "M" -> (_ => operation_manifest = true), + "M" -> (_ => operation_repository_files = true), "R" -> (_ => requirements = true), "U" -> (_ => operation_update = true), "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), @@ -256,7 +257,7 @@ "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) val sessions = getopts(args) - if (args.isEmpty || !(operation_imports || operation_manifest || operation_update)) + if (args.isEmpty || !(operation_imports || operation_repository_files || operation_update)) getopts.usage() val selection = @@ -266,7 +267,7 @@ val progress = new Console_Progress(verbose = verbose) imports(options, operation_imports = operation_imports, - operation_manifest = operation_manifest, operation_update = operation_update, + operation_repository_files = operation_repository_files, operation_update = operation_update, progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs, verbose = verbose) }) diff -r 8ee1799fb076 -r d081671d4a87 src/Tools/VSCode/src/channel.scala --- a/src/Tools/VSCode/src/channel.scala Sun May 14 13:55:51 2017 +0200 +++ b/src/Tools/VSCode/src/channel.scala Sun May 14 22:07:16 2017 +0200 @@ -110,6 +110,8 @@ def make_progress(verbose: Boolean = false): Progress = new Progress { override def echo(msg: String): Unit = log_writeln(msg) + override def echo_warning(msg: String): Unit = log_warning(msg) + override def echo_error_message(msg: String): Unit = log_error_message(msg) override def theory(session: String, theory: String): Unit = if (verbose) echo(session + ": theory " + theory) } diff -r 8ee1799fb076 -r d081671d4a87 src/Tools/jEdit/src/session_build.scala --- a/src/Tools/jEdit/src/session_build.scala Sun May 14 13:55:51 2017 +0200 +++ b/src/Tools/jEdit/src/session_build.scala Sun May 14 22:07:16 2017 +0200 @@ -173,7 +173,7 @@ try { ("", JEdit_Sessions.session_build(options, progress = progress)) } catch { case exn: Throwable => - (Output.error_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2)) + (Output.error_message_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2)) } progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))