# HG changeset patch
# User wenzelm
# Date 1476260554 -7200
# Node ID 2b1128e95dfbf854a49d0fa55e3513a11ee9c529
# Parent 1eea419fab65117898c360475d744575ec67d47b
explicit indication of Admin tools;
diff -r 1eea419fab65 -r 2b1128e95dfb src/Pure/Admin/build_doc.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_doc.scala Wed Oct 12 10:22:34 2016 +0200
@@ -0,0 +1,107 @@
+/* Title: Pure/Admin/build_doc.scala
+ Author: Makarius
+
+Build Isabelle documentation.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile}
+
+
+object Build_Doc
+{
+ /* build_doc */
+
+ def build_doc(
+ options: Options,
+ progress: Progress = Ignore_Progress,
+ all_docs: Boolean = false,
+ max_jobs: Int = 1,
+ system_mode: Boolean = false,
+ docs: List[String] = Nil): Int =
+ {
+ val selection =
+ for {
+ (name, info) <- Sessions.load(options).topological_order
+ if info.groups.contains("doc")
+ doc = info.options.string("document_variants")
+ if all_docs || docs.contains(doc)
+ } yield (doc, name)
+
+ val selected_docs = selection.map(_._1)
+ val sessions = selection.map(_._2)
+
+ docs.filter(doc => !selected_docs.contains(doc)) match {
+ case Nil =>
+ case bad => error("No documentation session for " + commas_quote(bad))
+ }
+
+ progress.echo("Build started for documentation " + commas_quote(selected_docs))
+
+ val res1 =
+ Build.build(options, progress, requirements = true, build_heap = true,
+ max_jobs = max_jobs, system_mode = system_mode, sessions = sessions)
+ if (res1.ok) {
+ Isabelle_System.with_tmp_dir("document_output")(output =>
+ {
+ val res2 =
+ Build.build(
+ options.bool.update("browser_info", false).
+ string.update("document", "pdf").
+ string.update("document_output", File.standard_path(output)),
+ progress, clean_build = true, max_jobs = max_jobs, system_mode = system_mode,
+ sessions = sessions)
+ if (res2.ok) {
+ val doc_dir = Path.explode("$ISABELLE_HOME/doc").file
+ for (doc <- selected_docs) {
+ val name = doc + ".pdf"
+ File.copy(new JFile(output, name), new JFile(doc_dir, name))
+ }
+ }
+ res2.rc
+ })
+ }
+ else res1.rc
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("build_doc", "build Isabelle documentation", args =>
+ {
+ var all_docs = false
+ var max_jobs = 1
+ var system_mode = false
+
+ val getopts =
+ Getopts("""
+Usage: isabelle build_doc [OPTIONS] [DOCS ...]"
+
+ Options are:
+ -a select all documentation sessions
+ -j INT maximum number of parallel jobs (default 1)
+ -s system build mode
+
+ Build Isabelle documentation from documentation sessions with
+ suitable document_variants entry.
+""",
+ "a" -> (_ => all_docs = true),
+ "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
+ "s" -> (_ => system_mode = true))
+
+ val docs = getopts(args)
+
+ if (!all_docs && docs.isEmpty) getopts.usage()
+
+ val options = Options.init()
+ val progress = new Console_Progress()
+ val rc =
+ progress.interrupt_handler {
+ build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
+ }
+ sys.exit(rc)
+ }, admin = true)
+}
diff -r 1eea419fab65 -r 2b1128e95dfb src/Pure/Admin/build_stats.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_stats.scala Wed Oct 12 10:22:34 2016 +0200
@@ -0,0 +1,191 @@
+/* Title: Pure/Admin/build_stats.scala
+ Author: Makarius
+
+Statistics from session build output.
+*/
+
+package isabelle
+
+
+object Build_Stats
+{
+ /* presentation */
+
+ private val default_history_length = 100
+ private val default_size = (800, 600)
+ private val default_only_sessions = Set.empty[String]
+ private val default_elapsed_threshold = Time.zero
+ private val default_ml_timing: Option[Boolean] = None
+
+ def present_job(job: String, dir: Path,
+ history_length: Int = default_history_length,
+ size: (Int, Int) = default_size,
+ only_sessions: Set[String] = default_only_sessions,
+ elapsed_threshold: Time = default_elapsed_threshold,
+ ml_timing: Option[Boolean] = default_ml_timing): List[String] =
+ {
+ val job_infos = CI_API.build_job_builds(job).sortBy(_.timestamp).reverse.take(history_length)
+ if (job_infos.isEmpty) error("No build infos for job " + quote(job))
+
+ val all_infos =
+ Par_List.map((job_info: CI_API.Job_Info) =>
+ (job_info.timestamp / 1000, job_info.read_main_log.parse_build_info), job_infos)
+ val all_sessions =
+ (Set.empty[String] /: all_infos)(
+ { case (s, (_, info)) => s ++ info.sessions.keySet })
+
+ def check_threshold(info: Build_Log.Build_Info, session: String): Boolean =
+ {
+ val t = info.timing(session)
+ !t.is_zero && t.elapsed >= elapsed_threshold
+ }
+
+ val sessions =
+ for {
+ session <- (if (only_sessions.isEmpty) all_sessions else all_sessions & only_sessions)
+ if all_infos.filter({ case (_, info) => check_threshold(info, session) }).length >= 3
+ } yield session
+
+ Isabelle_System.mkdirs(dir)
+ for (session <- sessions) {
+ Isabelle_System.with_tmp_file(session, "png") { data_file =>
+ Isabelle_System.with_tmp_file(session, "gnuplot") { plot_file =>
+ val data =
+ for { (t, info) <- all_infos if info.finished(session) }
+ yield {
+ val timing1 = info.timing(session)
+ val timing2 = info.ml_timing(session)
+ List(t.toString,
+ timing1.elapsed.minutes,
+ timing1.cpu.minutes,
+ timing2.elapsed.minutes,
+ timing2.cpu.minutes,
+ timing2.gc.minutes).mkString(" ")
+ }
+ File.write(data_file, cat_lines(data))
+
+ val plots1 =
+ List(
+ """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
+ """ using 1:3 smooth csplines title "cpu time" """,
+ """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
+ """ using 1:2 smooth csplines title "elapsed time" """)
+ val plots2 =
+ List(
+ """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
+ """ using 1:5 smooth csplines title "ML cpu time" """,
+ """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
+ """ using 1:4 smooth csplines title "ML elapsed time" """,
+ """ using 1:6 smooth sbezier title "ML gc time (smooth)" """,
+ """ using 1:6 smooth csplines title "ML gc time" """)
+ val plots =
+ ml_timing match {
+ case None => plots1
+ case Some(false) => plots1 ::: plots2
+ case Some(true) => plots2
+ }
+
+ val data_file_name = File.standard_path(data_file.getAbsolutePath)
+ File.write(plot_file, """
+set terminal png size """ + size._1 + "," + size._2 + """
+set output """ + quote(File.standard_path(dir + Path.basic(session + ".png"))) + """
+set xdata time
+set timefmt "%s"
+set format x "%d-%b"
+set xlabel """ + quote(session) + """ noenhanced
+set key left top
+plot [] [0:] """ + plots.map(s => quote(data_file_name) + " " + s).mkString(", ") + "\n")
+ val result = Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(plot_file))
+ if (result.rc != 0) {
+ Output.error_message("Session " + session + ": gnuplot error")
+ result.print
+ }
+ }
+ }
+ }
+
+ sessions.toList.sorted
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ private val html_header = """
+
+Performance statistics from session build output
+
+"""
+ private val html_footer = """
+
+
+"""
+
+ val isabelle_tool =
+ Isabelle_Tool("build_stats", "present statistics from session build output", args =>
+ {
+ var target_dir = Path.explode("stats")
+ var ml_timing = default_ml_timing
+ var only_sessions = default_only_sessions
+ var elapsed_threshold = default_elapsed_threshold
+ var history_length = default_history_length
+ var size = default_size
+
+ val getopts = Getopts("""
+Usage: isabelle build_stats [OPTIONS] [JOBS ...]
+
+ Options are:
+ -D DIR target directory (default "stats")
+ -M only ML timing
+ -S SESSIONS only given SESSIONS (comma separated)
+ -T THRESHOLD only sessions with elapsed time >= THRESHOLD (minutes)
+ -l LENGTH length of history (default 100)
+ -m include ML timing
+ -s WxH size of PNG image (default 800x600)
+
+ Present statistics from session build output of the given JOBS, from Jenkins
+ continuous build service specified as URL via ISABELLE_JENKINS_ROOT.
+""",
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "M" -> (_ => ml_timing = Some(true)),
+ "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
+ "T:" -> (arg => elapsed_threshold = Time.minutes(Value.Double.parse(arg))),
+ "l:" -> (arg => history_length = Value.Int.parse(arg)),
+ "m" -> (_ => ml_timing = Some(false)),
+ "s:" -> (arg =>
+ space_explode('x', arg).map(Value.Int.parse(_)) match {
+ case List(w, h) if w > 0 && h > 0 => size = (w, h)
+ case _ => error("Error bad PNG image size: " + quote(arg))
+ }))
+
+ val jobs = getopts(args)
+ val all_jobs = CI_API.build_jobs()
+ val bad_jobs = jobs.filterNot(all_jobs.contains(_)).sorted
+
+ if (jobs.isEmpty)
+ error("No build jobs given. Available jobs: " + all_jobs.sorted.mkString(" "))
+
+ if (bad_jobs.nonEmpty)
+ error("Unknown build jobs: " + bad_jobs.mkString(" ") +
+ "\nAvailable jobs: " + all_jobs.sorted.mkString(" "))
+
+ for (job <- jobs) {
+ val dir = target_dir + Path.basic(job)
+ Output.writeln(dir.implode)
+ val sessions =
+ present_job(job, dir, history_length, size, only_sessions, elapsed_threshold, ml_timing)
+ File.write(dir + Path.basic("index.html"),
+ html_header + "\n" + HTML.output(job) + "
\n" +
+ cat_lines(
+ sessions.map(session =>
+ """
![]()
""")) +
+ "\n" + html_footer)
+ }
+
+ File.write(target_dir + Path.basic("index.html"),
+ html_header + "\n\n" + html_footer)
+ }, admin = true)
+}
diff -r 1eea419fab65 -r 2b1128e95dfb src/Pure/Admin/check_sources.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/check_sources.scala Wed Oct 12 10:22:34 2016 +0200
@@ -0,0 +1,72 @@
+/* Title: Pure/Admin/check_sources.scala
+ Author: Makarius
+
+Some sanity checks for Isabelle sources.
+*/
+
+package isabelle
+
+
+object Check_Sources
+{
+ def check_file(path: Path)
+ {
+ val file_name = path.implode
+ val file_pos = path.position
+ def line_pos(i: Int) = Position.Line_File(i + 1, file_name)
+
+ val content = File.read(path)
+
+ for { (line, i) <- split_lines(content).iterator.zipWithIndex }
+ {
+ try {
+ Symbol.decode_strict(line)
+
+ for { c <- Word.codepoint_iterator(line); if c > 128 && !Character.isAlphabetic(c) }
+ {
+ Output.warning("Suspicious Unicode character " + quote(Word.codepoint(c)) +
+ Position.here(line_pos(i)))
+ }
+ }
+ catch { case ERROR(msg) => Output.warning(msg + Position.here(line_pos(i))) }
+
+ if (line.contains('\t'))
+ Output.warning("TAB character" + Position.here(line_pos(i)))
+ }
+
+ if (content.contains('\r'))
+ Output.warning("CR character" + Position.here(file_pos))
+
+ if (Word.bidi_detect(content))
+ Output.warning("Bidirectional Unicode text " + Position.here(file_pos))
+ }
+
+ def check_hg(root: Path)
+ {
+ Output.writeln("Checking " + root + " ...")
+ using(Mercurial.open_repository(root)) { hg =>
+ for {
+ file <- hg.manifest()
+ if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
+ } check_file(root + Path.explode(file))
+ }
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("check_sources", "some sanity checks for Isabelle sources", args =>
+ {
+ val getopts = Getopts("""
+Usage: isabelle check_sources [ROOT_DIRS...]
+
+ Check .thy, .ML, ROOT files from manifest of Mercurial ROOT_DIRS.
+""")
+
+ val specs = getopts(args)
+ if (specs.isEmpty) getopts.usage()
+
+ for (root <- specs) check_hg(Path.explode(root))
+ }, admin = true)
+}
diff -r 1eea419fab65 -r 2b1128e95dfb src/Pure/Admin/remote_dmg.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/remote_dmg.scala Wed Oct 12 10:22:34 2016 +0200
@@ -0,0 +1,65 @@
+/* Title: Pure/Admin/remote_dmg.scala
+ Author: Makarius
+
+Build dmg on remote Mac OS X system.
+*/
+
+package isabelle
+
+
+object Remote_DMG
+{
+ def remote_dmg(session: SSH.Session, tar_gz_file: Path, dmg_file: Path, volume_name: String = "")
+ {
+ session.with_tmp_dir(remote_dir =>
+ using(session.sftp())(sftp =>
+ {
+ val cd = "cd " + File.bash_string(remote_dir) + "; "
+
+ sftp.write_file(remote_dir + "/dmg.tar.gz", tar_gz_file)
+ session.execute(cd + "mkdir root && tar -C root -xzf dmg.tar.gz").check
+ session.execute(
+ cd + "hdiutil create -srcfolder root" +
+ (if (volume_name == "") "" else " -volname " + File.bash_string(volume_name)) +
+ " dmg.dmg").check
+ sftp.read_file(remote_dir + "/dmg.dmg", dmg_file)
+ }))
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("remote_dmg", "build dmg on remote Mac OS X system", args =>
+ {
+ Command_Line.tool0 {
+ var port = SSH.default_port
+ var volume_name = ""
+
+ val getopts = Getopts("""
+Usage: isabelle remote_dmg [OPTIONS] USER@HOST TAR_GZ_FILE DMG_FILE
+
+ Options are:
+ -p PORT alternative SSH port (default: """ + SSH.default_port + """)
+ -V NAME specify volume name
+
+ Turn the contents of a tar.gz file into a dmg file -- produced on a remote
+ Mac OS X system.
+""",
+ "p:" -> (arg => port = Value.Int.parse(arg)),
+ "V:" -> (arg => volume_name = arg))
+
+ val more_args = getopts(args)
+ val (user, host, tar_gz_file, dmg_file) =
+ more_args match {
+ case List(SSH.User_Host(user, host), tar_gz_file, dmg_file) =>
+ (user, host, Path.explode(tar_gz_file), Path.explode(dmg_file))
+ case _ => getopts.usage()
+ }
+
+ val ssh = SSH.init(Options.init)
+ using(ssh.open_session(user = user, host = host, port = port))(
+ remote_dmg(_, tar_gz_file, dmg_file, volume_name))
+ }
+ }, admin = true)
+}
diff -r 1eea419fab65 -r 2b1128e95dfb src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala Wed Oct 12 09:38:20 2016 +0200
+++ b/src/Pure/System/isabelle_system.scala Wed Oct 12 10:22:34 2016 +0200
@@ -324,6 +324,11 @@
/** Isabelle resources **/
+ /* repository clone with Admin */
+
+ def admin(): Boolean = Path.explode("~~/Admin").is_dir
+
+
/* components */
def components(): List[Path] =
diff -r 1eea419fab65 -r 2b1128e95dfb src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala Wed Oct 12 09:38:20 2016 +0200
+++ b/src/Pure/System/isabelle_tool.scala Wed Oct 12 10:22:34 2016 +0200
@@ -113,11 +113,12 @@
Update_Theorems.isabelle_tool)
private def list_internal(): List[(String, String)] =
- for (tool <- internal_tools.toList) yield (tool.name, tool.description)
+ for (tool <- internal_tools.toList if tool.accessible)
+ yield (tool.name, tool.description)
private def find_internal(name: String): Option[List[String] => Unit] =
internal_tools.collectFirst({
- case tool if tool.name == name =>
+ case tool if tool.name == name && tool.accessible =>
args => Command_Line.tool0 { tool.body(args) }
})
@@ -148,4 +149,8 @@
}
}
-sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit)
+sealed case class Isabelle_Tool(
+ name: String, description: String, body: List[String] => Unit, admin: Boolean = false)
+{
+ def accessible: Boolean = !admin || Isabelle_System.admin()
+}
diff -r 1eea419fab65 -r 2b1128e95dfb src/Pure/Tools/build_doc.scala
--- a/src/Pure/Tools/build_doc.scala Wed Oct 12 09:38:20 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,106 +0,0 @@
-/* Title: Pure/Tools/build_doc.scala
- Author: Makarius
-
-Build Isabelle documentation.
-*/
-
-package isabelle
-
-
-import java.io.{File => JFile}
-
-
-object Build_Doc
-{
- /* build_doc */
-
- def build_doc(
- options: Options,
- progress: Progress = Ignore_Progress,
- all_docs: Boolean = false,
- max_jobs: Int = 1,
- system_mode: Boolean = false,
- docs: List[String] = Nil): Int =
- {
- val selection =
- for {
- (name, info) <- Sessions.load(options).topological_order
- if info.groups.contains("doc")
- doc = info.options.string("document_variants")
- if all_docs || docs.contains(doc)
- } yield (doc, name)
-
- val selected_docs = selection.map(_._1)
- val sessions = selection.map(_._2)
-
- docs.filter(doc => !selected_docs.contains(doc)) match {
- case Nil =>
- case bad => error("No documentation session for " + commas_quote(bad))
- }
-
- progress.echo("Build started for documentation " + commas_quote(selected_docs))
-
- val res1 =
- Build.build(options, progress, requirements = true, build_heap = true,
- max_jobs = max_jobs, system_mode = system_mode, sessions = sessions)
- if (res1.ok) {
- Isabelle_System.with_tmp_dir("document_output")(output =>
- {
- val res2 =
- Build.build(
- options.bool.update("browser_info", false).
- string.update("document", "pdf").
- string.update("document_output", File.standard_path(output)),
- progress, clean_build = true, max_jobs = max_jobs, system_mode = system_mode,
- sessions = sessions)
- if (res2.ok) {
- val doc_dir = Path.explode("$ISABELLE_HOME/doc").file
- for (doc <- selected_docs) {
- val name = doc + ".pdf"
- File.copy(new JFile(output, name), new JFile(doc_dir, name))
- }
- }
- res2.rc
- })
- }
- else res1.rc
- }
-
-
- /* Isabelle tool wrapper */
-
- val isabelle_tool = Isabelle_Tool("build_doc", "build Isabelle documentation", args =>
- {
- var all_docs = false
- var max_jobs = 1
- var system_mode = false
-
- val getopts =
- Getopts("""
-Usage: isabelle build_doc [OPTIONS] [DOCS ...]"
-
- Options are:
- -a select all documentation sessions
- -j INT maximum number of parallel jobs (default 1)
- -s system build mode
-
- Build Isabelle documentation from documentation sessions with
- suitable document_variants entry.
-""",
- "a" -> (_ => all_docs = true),
- "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
- "s" -> (_ => system_mode = true))
-
- val docs = getopts(args)
-
- if (!all_docs && docs.isEmpty) getopts.usage()
-
- val options = Options.init()
- val progress = new Console_Progress()
- val rc =
- progress.interrupt_handler {
- build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
- }
- sys.exit(rc)
- })
-}
diff -r 1eea419fab65 -r 2b1128e95dfb src/Pure/Tools/build_stats.scala
--- a/src/Pure/Tools/build_stats.scala Wed Oct 12 09:38:20 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,191 +0,0 @@
-/* Title: Pure/Tools/build_stats.scala
- Author: Makarius
-
-Statistics from session build output.
-*/
-
-package isabelle
-
-
-object Build_Stats
-{
- /* presentation */
-
- private val default_history_length = 100
- private val default_size = (800, 600)
- private val default_only_sessions = Set.empty[String]
- private val default_elapsed_threshold = Time.zero
- private val default_ml_timing: Option[Boolean] = None
-
- def present_job(job: String, dir: Path,
- history_length: Int = default_history_length,
- size: (Int, Int) = default_size,
- only_sessions: Set[String] = default_only_sessions,
- elapsed_threshold: Time = default_elapsed_threshold,
- ml_timing: Option[Boolean] = default_ml_timing): List[String] =
- {
- val job_infos = CI_API.build_job_builds(job).sortBy(_.timestamp).reverse.take(history_length)
- if (job_infos.isEmpty) error("No build infos for job " + quote(job))
-
- val all_infos =
- Par_List.map((job_info: CI_API.Job_Info) =>
- (job_info.timestamp / 1000, job_info.read_main_log.parse_build_info), job_infos)
- val all_sessions =
- (Set.empty[String] /: all_infos)(
- { case (s, (_, info)) => s ++ info.sessions.keySet })
-
- def check_threshold(info: Build_Log.Build_Info, session: String): Boolean =
- {
- val t = info.timing(session)
- !t.is_zero && t.elapsed >= elapsed_threshold
- }
-
- val sessions =
- for {
- session <- (if (only_sessions.isEmpty) all_sessions else all_sessions & only_sessions)
- if all_infos.filter({ case (_, info) => check_threshold(info, session) }).length >= 3
- } yield session
-
- Isabelle_System.mkdirs(dir)
- for (session <- sessions) {
- Isabelle_System.with_tmp_file(session, "png") { data_file =>
- Isabelle_System.with_tmp_file(session, "gnuplot") { plot_file =>
- val data =
- for { (t, info) <- all_infos if info.finished(session) }
- yield {
- val timing1 = info.timing(session)
- val timing2 = info.ml_timing(session)
- List(t.toString,
- timing1.elapsed.minutes,
- timing1.cpu.minutes,
- timing2.elapsed.minutes,
- timing2.cpu.minutes,
- timing2.gc.minutes).mkString(" ")
- }
- File.write(data_file, cat_lines(data))
-
- val plots1 =
- List(
- """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
- """ using 1:3 smooth csplines title "cpu time" """,
- """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
- """ using 1:2 smooth csplines title "elapsed time" """)
- val plots2 =
- List(
- """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
- """ using 1:5 smooth csplines title "ML cpu time" """,
- """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
- """ using 1:4 smooth csplines title "ML elapsed time" """,
- """ using 1:6 smooth sbezier title "ML gc time (smooth)" """,
- """ using 1:6 smooth csplines title "ML gc time" """)
- val plots =
- ml_timing match {
- case None => plots1
- case Some(false) => plots1 ::: plots2
- case Some(true) => plots2
- }
-
- val data_file_name = File.standard_path(data_file.getAbsolutePath)
- File.write(plot_file, """
-set terminal png size """ + size._1 + "," + size._2 + """
-set output """ + quote(File.standard_path(dir + Path.basic(session + ".png"))) + """
-set xdata time
-set timefmt "%s"
-set format x "%d-%b"
-set xlabel """ + quote(session) + """ noenhanced
-set key left top
-plot [] [0:] """ + plots.map(s => quote(data_file_name) + " " + s).mkString(", ") + "\n")
- val result = Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(plot_file))
- if (result.rc != 0) {
- Output.error_message("Session " + session + ": gnuplot error")
- result.print
- }
- }
- }
- }
-
- sessions.toList.sorted
- }
-
-
- /* Isabelle tool wrapper */
-
- private val html_header = """
-
-Performance statistics from session build output
-
-"""
- private val html_footer = """
-
-
-"""
-
- val isabelle_tool =
- Isabelle_Tool("build_stats", "present statistics from session build output", args =>
- {
- var target_dir = Path.explode("stats")
- var ml_timing = default_ml_timing
- var only_sessions = default_only_sessions
- var elapsed_threshold = default_elapsed_threshold
- var history_length = default_history_length
- var size = default_size
-
- val getopts = Getopts("""
-Usage: isabelle build_stats [OPTIONS] [JOBS ...]
-
- Options are:
- -D DIR target directory (default "stats")
- -M only ML timing
- -S SESSIONS only given SESSIONS (comma separated)
- -T THRESHOLD only sessions with elapsed time >= THRESHOLD (minutes)
- -l LENGTH length of history (default 100)
- -m include ML timing
- -s WxH size of PNG image (default 800x600)
-
- Present statistics from session build output of the given JOBS, from Jenkins
- continuous build service specified as URL via ISABELLE_JENKINS_ROOT.
-""",
- "D:" -> (arg => target_dir = Path.explode(arg)),
- "M" -> (_ => ml_timing = Some(true)),
- "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
- "T:" -> (arg => elapsed_threshold = Time.minutes(Value.Double.parse(arg))),
- "l:" -> (arg => history_length = Value.Int.parse(arg)),
- "m" -> (_ => ml_timing = Some(false)),
- "s:" -> (arg =>
- space_explode('x', arg).map(Value.Int.parse(_)) match {
- case List(w, h) if w > 0 && h > 0 => size = (w, h)
- case _ => error("Error bad PNG image size: " + quote(arg))
- }))
-
- val jobs = getopts(args)
- val all_jobs = CI_API.build_jobs()
- val bad_jobs = jobs.filterNot(all_jobs.contains(_)).sorted
-
- if (jobs.isEmpty)
- error("No build jobs given. Available jobs: " + all_jobs.sorted.mkString(" "))
-
- if (bad_jobs.nonEmpty)
- error("Unknown build jobs: " + bad_jobs.mkString(" ") +
- "\nAvailable jobs: " + all_jobs.sorted.mkString(" "))
-
- for (job <- jobs) {
- val dir = target_dir + Path.basic(job)
- Output.writeln(dir.implode)
- val sessions =
- present_job(job, dir, history_length, size, only_sessions, elapsed_threshold, ml_timing)
- File.write(dir + Path.basic("index.html"),
- html_header + "\n" + HTML.output(job) + "
\n" +
- cat_lines(
- sessions.map(session =>
- """
![]()
""")) +
- "\n" + html_footer)
- }
-
- File.write(target_dir + Path.basic("index.html"),
- html_header + "\n\n" + html_footer)
- })
-}
diff -r 1eea419fab65 -r 2b1128e95dfb src/Pure/Tools/check_sources.scala
--- a/src/Pure/Tools/check_sources.scala Wed Oct 12 09:38:20 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-/* Title: Pure/Tools/check_sources.scala
- Author: Makarius
-
-Some sanity checks for Isabelle sources.
-*/
-
-package isabelle
-
-
-object Check_Sources
-{
- def check_file(path: Path)
- {
- val file_name = path.implode
- val file_pos = path.position
- def line_pos(i: Int) = Position.Line_File(i + 1, file_name)
-
- val content = File.read(path)
-
- for { (line, i) <- split_lines(content).iterator.zipWithIndex }
- {
- try {
- Symbol.decode_strict(line)
-
- for { c <- Word.codepoint_iterator(line); if c > 128 && !Character.isAlphabetic(c) }
- {
- Output.warning("Suspicious Unicode character " + quote(Word.codepoint(c)) +
- Position.here(line_pos(i)))
- }
- }
- catch { case ERROR(msg) => Output.warning(msg + Position.here(line_pos(i))) }
-
- if (line.contains('\t'))
- Output.warning("TAB character" + Position.here(line_pos(i)))
- }
-
- if (content.contains('\r'))
- Output.warning("CR character" + Position.here(file_pos))
-
- if (Word.bidi_detect(content))
- Output.warning("Bidirectional Unicode text " + Position.here(file_pos))
- }
-
- def check_hg(root: Path)
- {
- Output.writeln("Checking " + root + " ...")
- using(Mercurial.open_repository(root)) { hg =>
- for {
- file <- hg.manifest()
- if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
- } check_file(root + Path.explode(file))
- }
- }
-
-
- /* Isabelle tool wrapper */
-
- val isabelle_tool =
- Isabelle_Tool("check_sources", "some sanity checks for Isabelle sources", args =>
- {
- val getopts = Getopts("""
-Usage: isabelle check_sources [ROOT_DIRS...]
-
- Check .thy, .ML, ROOT files from manifest of Mercurial ROOT_DIRS.
-""")
-
- val specs = getopts(args)
- if (specs.isEmpty) getopts.usage()
-
- for (root <- specs) check_hg(Path.explode(root))
- })
-}
diff -r 1eea419fab65 -r 2b1128e95dfb src/Pure/Tools/remote_dmg.scala
--- a/src/Pure/Tools/remote_dmg.scala Wed Oct 12 09:38:20 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-/* Title: Pure/Tools/remote_dmg.scala
- Author: Makarius
-
-Build dmg on remote Mac OS X system.
-*/
-
-package isabelle
-
-
-object Remote_DMG
-{
- def remote_dmg(session: SSH.Session, tar_gz_file: Path, dmg_file: Path, volume_name: String = "")
- {
- session.with_tmp_dir(remote_dir =>
- using(session.sftp())(sftp =>
- {
- val cd = "cd " + File.bash_string(remote_dir) + "; "
-
- sftp.write_file(remote_dir + "/dmg.tar.gz", tar_gz_file)
- session.execute(cd + "mkdir root && tar -C root -xzf dmg.tar.gz").check
- session.execute(
- cd + "hdiutil create -srcfolder root" +
- (if (volume_name == "") "" else " -volname " + File.bash_string(volume_name)) +
- " dmg.dmg").check
- sftp.read_file(remote_dir + "/dmg.dmg", dmg_file)
- }))
- }
-
-
- /* Isabelle tool wrapper */
-
- val isabelle_tool = Isabelle_Tool("remote_dmg", "build dmg on remote Mac OS X system", args =>
- {
- Command_Line.tool0 {
- var port = SSH.default_port
- var volume_name = ""
-
- val getopts = Getopts("""
-Usage: isabelle remote_dmg [OPTIONS] USER@HOST TAR_GZ_FILE DMG_FILE
-
- Options are:
- -p PORT alternative SSH port (default: """ + SSH.default_port + """)
- -V NAME specify volume name
-
- Turn the contents of a tar.gz file into a dmg file -- produced on a remote
- Mac OS X system.
-""",
- "p:" -> (arg => port = Value.Int.parse(arg)),
- "V:" -> (arg => volume_name = arg))
-
- val more_args = getopts(args)
- val (user, host, tar_gz_file, dmg_file) =
- more_args match {
- case List(SSH.User_Host(user, host), tar_gz_file, dmg_file) =>
- (user, host, Path.explode(tar_gz_file), Path.explode(dmg_file))
- case _ => getopts.usage()
- }
-
- val ssh = SSH.init(Options.init)
- using(ssh.open_session(user = user, host = host, port = port))(
- remote_dmg(_, tar_gz_file, dmg_file, volume_name))
- }
- })
-}
diff -r 1eea419fab65 -r 2b1128e95dfb src/Pure/build-jars
--- a/src/Pure/build-jars Wed Oct 12 09:38:20 2016 +0200
+++ b/src/Pure/build-jars Wed Oct 12 10:22:34 2016 +0200
@@ -9,11 +9,15 @@
## sources
declare -a SOURCES=(
+ Admin/build_doc.scala
Admin/build_history.scala
Admin/build_log.scala
+ Admin/build_stats.scala
+ Admin/check_sources.scala
Admin/ci_api.scala
Admin/ci_profile.scala
Admin/isabelle_cronjob.scala
+ Admin/remote_dmg.scala
Concurrent/consumer_thread.scala
Concurrent/counter.scala
Concurrent/event_timer.scala
@@ -113,10 +117,7 @@
Thy/thy_syntax.scala
Tools/bibtex.scala
Tools/build.scala
- Tools/build_doc.scala
- Tools/build_stats.scala
Tools/check_keywords.scala
- Tools/check_sources.scala
Tools/debugger.scala
Tools/doc.scala
Tools/main.scala
@@ -125,7 +126,6 @@
Tools/ml_statistics.scala
Tools/news.scala
Tools/print_operation.scala
- Tools/remote_dmg.scala
Tools/simplifier_trace.scala
Tools/task_statistics.scala
Tools/update_cartouches.scala