# HG changeset patch
# User paulson
# Date 1530021092 -3600
# Node ID e3e742b9eed458c56a98d4e8f9edd6e2202ce0d4
# Parent 6855ebc61b4f38e2baf3b22fa731406e70dc0f53# Parent d4312962161ab8862595ab6e5f0e7508fbef8b9e
merged
diff -r d4312962161a -r e3e742b9eed4 Admin/jenkins/build/ci_build_stats.scala
--- 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"""
-
-Performance statistics from session build output
-
- Generated at $start_time
-"""
-
- val html_footer = """
-
-
-"""
-
- 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 =>
- "" +
- "
" + HTML.output(session) + "
" +
- "
\n"))
-
- val toc =
- cat_lines(
- sessions.map(session =>
- "" +
- HTML.output(session) + "\n"))
-
- val html =
- html_header + "\n" + HTML.output(job) + "
\n" + "\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\n" + html_footer)
- }
-
-}
diff -r d4312962161a -r e3e742b9eed4 src/Pure/Admin/ci_profile.scala
--- 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
diff -r d4312962161a -r e3e742b9eed4 src/Pure/General/graph.scala
--- 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)
diff -r d4312962161a -r e3e742b9eed4 src/Pure/PIDE/document.scala
--- 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 =