merged
authorpaulson
Tue, 26 Jun 2018 14:51:32 +0100
changeset 68500 e3e742b9eed4
parent 68498 6855ebc61b4f (diff)
parent 68499 d4312962161a (current diff)
child 68501 8a8f98c84df3
merged
--- a/Admin/jenkins/build/ci_build_stats.scala	Tue Jun 26 14:51:18 2018 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-// FIXME obsolete
-
-object stats extends isabelle.Isabelle_Tool.Body {
-
-  import isabelle._
-  import java.time._
-  import java.time.format.DateTimeFormatter
-
-
-  val start_time = Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME)
-
-  val target_dir = Path.explode("stats")
-  val jobs = List("isabelle-nightly-benchmark", "isabelle-nightly-slow")
-
-  val html_header = s"""<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
-<html>
-<head><title>Performance statistics from session build output</title></head>
-<body>
-  <p>Generated at $start_time</p>
-"""
-
-  val html_footer = """
-</body>
-</html>
-"""
-
-  def generate(job: String): Unit = {
-    println(s"=== $job ===")
-
-    val dir = target_dir + Path.basic(job)
-    val sessions: List[String] = Nil
-
-    val sections =
-      cat_lines(
-        sessions.map(session =>
-          "<p id=" + quote("session_" + HTML.output(session)) + ">" +
-          "<h2>" + HTML.output(session) + "</h2>" +
-          "<img src=" + quote(HTML.output(session + ".png")) + "></p>\n"))
-
-    val toc =
-      cat_lines(
-        sessions.map(session =>
-          "<li><a href=" + quote("#session_" + HTML.output(session)) + ">" +
-          HTML.output(session) + "</a></li>\n"))
-
-    val html =
-      html_header + "\n<h1>" + HTML.output(job) + "</h1>\n" + "<div><ul>" + toc + "</ul></div>\n" +
-      sections + html_footer
-
-    File.write(dir + Path.basic("index.html"), html)
-  }
-
-  override final def apply(args: List[String]): Unit = {
-    jobs.foreach(generate)
-
-    File.write(target_dir + Path.basic("index.html"),
-      html_header + "\n<ul>\n" +
-      cat_lines(
-        jobs.map(job => """<li> <a href=""" + quote(HTML.output(job + "/index.html")) + """>""" +
-          HTML.output(job) + """</a> </li>""")) +
-      "\n</ul>\n" + html_footer)
-  }
-
-}
--- a/src/Pure/Admin/ci_profile.scala	Tue Jun 26 14:51:18 2018 +0100
+++ b/src/Pure/Admin/ci_profile.scala	Tue Jun 26 14:51:32 2018 +0100
@@ -24,6 +24,7 @@
         progress = progress,
         clean_build = clean,
         verbose = true,
+        numa_shuffling = numa,
         max_jobs = jobs,
         dirs = include,
         select_dirs = select,
@@ -137,6 +138,7 @@
 
   def documents: Boolean = true
   def clean: Boolean = true
+  def numa: Boolean = false
 
   def threads: Int
   def jobs: Int
--- a/src/Pure/General/graph.scala	Tue Jun 26 14:51:18 2018 +0100
+++ b/src/Pure/General/graph.scala	Tue Jun 26 14:51:32 2018 +0100
@@ -68,6 +68,7 @@
   def defined(x: Key): Boolean = rep.isDefinedAt(x)
   def domain: Set[Key] = rep.keySet
 
+  def size: Int = rep.size
   def iterator: Iterator[(Key, Entry)] = rep.iterator
 
   def keys_iterator: Iterator[Key] = iterator.map(_._1)
--- a/src/Pure/PIDE/document.scala	Tue Jun 26 14:51:18 2018 +0100
+++ b/src/Pure/PIDE/document.scala	Tue Jun 26 14:51:32 2018 +0100
@@ -669,6 +669,16 @@
     /*intermediate state between remove_versions/removed_versions*/
     removing_versions: Boolean = false)
   {
+    override def toString: String =
+      "State(versions = " + versions.size +
+      ", blobs = " + blobs.size +
+      ", commands = " + commands.size +
+      ", execs = " + execs.size +
+      ", assignments = " + assignments.size +
+      ", commands_redirection = " + commands_redirection.size +
+      ", history = " + history.undo_list.size +
+      ", removing_versions = " + removing_versions + ")"
+
     private def fail[A]: A = throw new State.Fail(this)
 
     def define_version(version: Version, assignment: State.Assignment): State =