explicit indication of Admin tools;
authorwenzelm
Wed Oct 12 10:22:34 2016 +0200 (2016-10-12)
changeset 641612b1128e95dfb
parent 64160 1eea419fab65
child 64162 03057a8fdd1f
explicit indication of Admin tools;
src/Pure/Admin/build_doc.scala
src/Pure/Admin/build_stats.scala
src/Pure/Admin/check_sources.scala
src/Pure/Admin/remote_dmg.scala
src/Pure/System/isabelle_system.scala
src/Pure/System/isabelle_tool.scala
src/Pure/Tools/build_doc.scala
src/Pure/Tools/build_stats.scala
src/Pure/Tools/check_sources.scala
src/Pure/Tools/remote_dmg.scala
src/Pure/build-jars
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Admin/build_doc.scala	Wed Oct 12 10:22:34 2016 +0200
     1.3 @@ -0,0 +1,107 @@
     1.4 +/*  Title:      Pure/Admin/build_doc.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Build Isabelle documentation.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +import java.io.{File => JFile}
    1.14 +
    1.15 +
    1.16 +object Build_Doc
    1.17 +{
    1.18 +  /* build_doc */
    1.19 +
    1.20 +  def build_doc(
    1.21 +    options: Options,
    1.22 +    progress: Progress = Ignore_Progress,
    1.23 +    all_docs: Boolean = false,
    1.24 +    max_jobs: Int = 1,
    1.25 +    system_mode: Boolean = false,
    1.26 +    docs: List[String] = Nil): Int =
    1.27 +  {
    1.28 +    val selection =
    1.29 +      for {
    1.30 +        (name, info) <- Sessions.load(options).topological_order
    1.31 +        if info.groups.contains("doc")
    1.32 +        doc = info.options.string("document_variants")
    1.33 +        if all_docs || docs.contains(doc)
    1.34 +      } yield (doc, name)
    1.35 +
    1.36 +    val selected_docs = selection.map(_._1)
    1.37 +    val sessions = selection.map(_._2)
    1.38 +
    1.39 +    docs.filter(doc => !selected_docs.contains(doc)) match {
    1.40 +      case Nil =>
    1.41 +      case bad => error("No documentation session for " + commas_quote(bad))
    1.42 +    }
    1.43 +
    1.44 +    progress.echo("Build started for documentation " + commas_quote(selected_docs))
    1.45 +
    1.46 +    val res1 =
    1.47 +      Build.build(options, progress, requirements = true, build_heap = true,
    1.48 +        max_jobs = max_jobs, system_mode = system_mode, sessions = sessions)
    1.49 +    if (res1.ok) {
    1.50 +      Isabelle_System.with_tmp_dir("document_output")(output =>
    1.51 +        {
    1.52 +          val res2 =
    1.53 +            Build.build(
    1.54 +              options.bool.update("browser_info", false).
    1.55 +                string.update("document", "pdf").
    1.56 +                string.update("document_output", File.standard_path(output)),
    1.57 +              progress, clean_build = true, max_jobs = max_jobs, system_mode = system_mode,
    1.58 +              sessions = sessions)
    1.59 +          if (res2.ok) {
    1.60 +            val doc_dir = Path.explode("$ISABELLE_HOME/doc").file
    1.61 +            for (doc <- selected_docs) {
    1.62 +              val name = doc + ".pdf"
    1.63 +              File.copy(new JFile(output, name), new JFile(doc_dir, name))
    1.64 +            }
    1.65 +          }
    1.66 +          res2.rc
    1.67 +        })
    1.68 +    }
    1.69 +    else res1.rc
    1.70 +  }
    1.71 +
    1.72 +
    1.73 +  /* Isabelle tool wrapper */
    1.74 +
    1.75 +  val isabelle_tool =
    1.76 +    Isabelle_Tool("build_doc", "build Isabelle documentation", args =>
    1.77 +    {
    1.78 +      var all_docs = false
    1.79 +      var max_jobs = 1
    1.80 +      var system_mode = false
    1.81 +
    1.82 +      val getopts =
    1.83 +        Getopts("""
    1.84 +Usage: isabelle build_doc [OPTIONS] [DOCS ...]"
    1.85 +
    1.86 +  Options are:
    1.87 +    -a           select all documentation sessions
    1.88 +    -j INT       maximum number of parallel jobs (default 1)
    1.89 +    -s           system build mode
    1.90 +
    1.91 +  Build Isabelle documentation from documentation sessions with
    1.92 +  suitable document_variants entry.
    1.93 +""",
    1.94 +        "a" -> (_ => all_docs = true),
    1.95 +        "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
    1.96 +        "s" -> (_ => system_mode = true))
    1.97 +
    1.98 +      val docs = getopts(args)
    1.99 +
   1.100 +      if (!all_docs && docs.isEmpty) getopts.usage()
   1.101 +
   1.102 +      val options = Options.init()
   1.103 +      val progress = new Console_Progress()
   1.104 +      val rc =
   1.105 +        progress.interrupt_handler {
   1.106 +          build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
   1.107 +        }
   1.108 +      sys.exit(rc)
   1.109 +    }, admin = true)
   1.110 +}
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Admin/build_stats.scala	Wed Oct 12 10:22:34 2016 +0200
     2.3 @@ -0,0 +1,191 @@
     2.4 +/*  Title:      Pure/Admin/build_stats.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Statistics from session build output.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +
    2.13 +object Build_Stats
    2.14 +{
    2.15 +  /* presentation */
    2.16 +
    2.17 +  private val default_history_length = 100
    2.18 +  private val default_size = (800, 600)
    2.19 +  private val default_only_sessions = Set.empty[String]
    2.20 +  private val default_elapsed_threshold = Time.zero
    2.21 +  private val default_ml_timing: Option[Boolean] = None
    2.22 +
    2.23 +  def present_job(job: String, dir: Path,
    2.24 +    history_length: Int = default_history_length,
    2.25 +    size: (Int, Int) = default_size,
    2.26 +    only_sessions: Set[String] = default_only_sessions,
    2.27 +    elapsed_threshold: Time = default_elapsed_threshold,
    2.28 +    ml_timing: Option[Boolean] = default_ml_timing): List[String] =
    2.29 +  {
    2.30 +    val job_infos = CI_API.build_job_builds(job).sortBy(_.timestamp).reverse.take(history_length)
    2.31 +    if (job_infos.isEmpty) error("No build infos for job " + quote(job))
    2.32 +
    2.33 +    val all_infos =
    2.34 +      Par_List.map((job_info: CI_API.Job_Info) =>
    2.35 +        (job_info.timestamp / 1000, job_info.read_main_log.parse_build_info), job_infos)
    2.36 +    val all_sessions =
    2.37 +      (Set.empty[String] /: all_infos)(
    2.38 +        { case (s, (_, info)) => s ++ info.sessions.keySet })
    2.39 +
    2.40 +    def check_threshold(info: Build_Log.Build_Info, session: String): Boolean =
    2.41 +    {
    2.42 +      val t = info.timing(session)
    2.43 +      !t.is_zero && t.elapsed >= elapsed_threshold
    2.44 +    }
    2.45 +
    2.46 +    val sessions =
    2.47 +      for {
    2.48 +        session <- (if (only_sessions.isEmpty) all_sessions else all_sessions & only_sessions)
    2.49 +        if all_infos.filter({ case (_, info) => check_threshold(info, session) }).length >= 3
    2.50 +      } yield session
    2.51 +
    2.52 +    Isabelle_System.mkdirs(dir)
    2.53 +    for (session <- sessions) {
    2.54 +      Isabelle_System.with_tmp_file(session, "png") { data_file =>
    2.55 +        Isabelle_System.with_tmp_file(session, "gnuplot") { plot_file =>
    2.56 +          val data =
    2.57 +            for { (t, info) <- all_infos if info.finished(session) }
    2.58 +            yield {
    2.59 +              val timing1 = info.timing(session)
    2.60 +              val timing2 = info.ml_timing(session)
    2.61 +              List(t.toString,
    2.62 +                timing1.elapsed.minutes,
    2.63 +                timing1.cpu.minutes,
    2.64 +                timing2.elapsed.minutes,
    2.65 +                timing2.cpu.minutes,
    2.66 +                timing2.gc.minutes).mkString(" ")
    2.67 +            }
    2.68 +          File.write(data_file, cat_lines(data))
    2.69 +
    2.70 +          val plots1 =
    2.71 +            List(
    2.72 +              """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
    2.73 +              """ using 1:3 smooth csplines title "cpu time" """,
    2.74 +              """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
    2.75 +              """ using 1:2 smooth csplines title "elapsed time" """)
    2.76 +          val plots2 =
    2.77 +            List(
    2.78 +              """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
    2.79 +              """ using 1:5 smooth csplines title "ML cpu time" """,
    2.80 +              """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
    2.81 +              """ using 1:4 smooth csplines title "ML elapsed time" """,
    2.82 +              """ using 1:6 smooth sbezier title "ML gc time (smooth)" """,
    2.83 +              """ using 1:6 smooth csplines title "ML gc time" """)
    2.84 +          val plots =
    2.85 +            ml_timing match {
    2.86 +              case None => plots1
    2.87 +              case Some(false) => plots1 ::: plots2
    2.88 +              case Some(true) => plots2
    2.89 +            }
    2.90 +
    2.91 +          val data_file_name = File.standard_path(data_file.getAbsolutePath)
    2.92 +          File.write(plot_file, """
    2.93 +set terminal png size """ + size._1 + "," + size._2 + """
    2.94 +set output """ + quote(File.standard_path(dir + Path.basic(session + ".png"))) + """
    2.95 +set xdata time
    2.96 +set timefmt "%s"
    2.97 +set format x "%d-%b"
    2.98 +set xlabel """ + quote(session) + """ noenhanced
    2.99 +set key left top
   2.100 +plot [] [0:] """ + plots.map(s => quote(data_file_name) + " " + s).mkString(", ") + "\n")
   2.101 +          val result = Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(plot_file))
   2.102 +          if (result.rc != 0) {
   2.103 +            Output.error_message("Session " + session + ": gnuplot error")
   2.104 +            result.print
   2.105 +          }
   2.106 +        }
   2.107 +      }
   2.108 +    }
   2.109 +
   2.110 +    sessions.toList.sorted
   2.111 +  }
   2.112 +
   2.113 +
   2.114 +  /* Isabelle tool wrapper */
   2.115 +
   2.116 +  private val html_header = """<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
   2.117 +<html>
   2.118 +<head><title>Performance statistics from session build output</title></head>
   2.119 +<body>
   2.120 +"""
   2.121 +  private val html_footer = """
   2.122 +</body>
   2.123 +</html>
   2.124 +"""
   2.125 +
   2.126 +  val isabelle_tool =
   2.127 +    Isabelle_Tool("build_stats", "present statistics from session build output", args =>
   2.128 +    {
   2.129 +      var target_dir = Path.explode("stats")
   2.130 +      var ml_timing = default_ml_timing
   2.131 +      var only_sessions = default_only_sessions
   2.132 +      var elapsed_threshold = default_elapsed_threshold
   2.133 +      var history_length = default_history_length
   2.134 +      var size = default_size
   2.135 +
   2.136 +      val getopts = Getopts("""
   2.137 +Usage: isabelle build_stats [OPTIONS] [JOBS ...]
   2.138 +
   2.139 +  Options are:
   2.140 +    -D DIR       target directory (default "stats")
   2.141 +    -M           only ML timing
   2.142 +    -S SESSIONS  only given SESSIONS (comma separated)
   2.143 +    -T THRESHOLD only sessions with elapsed time >= THRESHOLD (minutes)
   2.144 +    -l LENGTH    length of history (default 100)
   2.145 +    -m           include ML timing
   2.146 +    -s WxH       size of PNG image (default 800x600)
   2.147 +
   2.148 +  Present statistics from session build output of the given JOBS, from Jenkins
   2.149 +  continuous build service specified as URL via ISABELLE_JENKINS_ROOT.
   2.150 +""",
   2.151 +        "D:" -> (arg => target_dir = Path.explode(arg)),
   2.152 +        "M" -> (_ => ml_timing = Some(true)),
   2.153 +        "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
   2.154 +        "T:" -> (arg => elapsed_threshold = Time.minutes(Value.Double.parse(arg))),
   2.155 +        "l:" -> (arg => history_length = Value.Int.parse(arg)),
   2.156 +        "m" -> (_ => ml_timing = Some(false)),
   2.157 +        "s:" -> (arg =>
   2.158 +          space_explode('x', arg).map(Value.Int.parse(_)) match {
   2.159 +            case List(w, h) if w > 0 && h > 0 => size = (w, h)
   2.160 +            case _ => error("Error bad PNG image size: " + quote(arg))
   2.161 +          }))
   2.162 +
   2.163 +      val jobs = getopts(args)
   2.164 +      val all_jobs = CI_API.build_jobs()
   2.165 +      val bad_jobs = jobs.filterNot(all_jobs.contains(_)).sorted
   2.166 +
   2.167 +      if (jobs.isEmpty)
   2.168 +        error("No build jobs given. Available jobs: " + all_jobs.sorted.mkString(" "))
   2.169 +
   2.170 +      if (bad_jobs.nonEmpty)
   2.171 +        error("Unknown build jobs: " + bad_jobs.mkString(" ") +
   2.172 +          "\nAvailable jobs: " + all_jobs.sorted.mkString(" "))
   2.173 +
   2.174 +      for (job <- jobs) {
   2.175 +        val dir = target_dir + Path.basic(job)
   2.176 +        Output.writeln(dir.implode)
   2.177 +        val sessions =
   2.178 +          present_job(job, dir, history_length, size, only_sessions, elapsed_threshold, ml_timing)
   2.179 +        File.write(dir + Path.basic("index.html"),
   2.180 +          html_header + "\n<h1>" + HTML.output(job) + "</h1>\n" +
   2.181 +          cat_lines(
   2.182 +            sessions.map(session =>
   2.183 +              """<br/><img src=""" + quote(HTML.output(session + ".png")) + """><br/>""")) +
   2.184 +          "\n" + html_footer)
   2.185 +      }
   2.186 +
   2.187 +      File.write(target_dir + Path.basic("index.html"),
   2.188 +        html_header + "\n<ul>\n" +
   2.189 +        cat_lines(
   2.190 +          jobs.map(job => """<li> <a href=""" + quote(HTML.output(job + "/index.html")) + """>""" +
   2.191 +            HTML.output(job) + """</a> </li>""")) +
   2.192 +        "\n</ul>\n" + html_footer)
   2.193 +  }, admin = true)
   2.194 +}
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Admin/check_sources.scala	Wed Oct 12 10:22:34 2016 +0200
     3.3 @@ -0,0 +1,72 @@
     3.4 +/*  Title:      Pure/Admin/check_sources.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Some sanity checks for Isabelle sources.
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +
    3.13 +object Check_Sources
    3.14 +{
    3.15 +  def check_file(path: Path)
    3.16 +  {
    3.17 +    val file_name = path.implode
    3.18 +    val file_pos = path.position
    3.19 +    def line_pos(i: Int) = Position.Line_File(i + 1, file_name)
    3.20 +
    3.21 +    val content = File.read(path)
    3.22 +
    3.23 +    for { (line, i) <- split_lines(content).iterator.zipWithIndex }
    3.24 +    {
    3.25 +      try {
    3.26 +        Symbol.decode_strict(line)
    3.27 +
    3.28 +        for { c <- Word.codepoint_iterator(line); if c > 128 && !Character.isAlphabetic(c) }
    3.29 +        {
    3.30 +          Output.warning("Suspicious Unicode character " + quote(Word.codepoint(c)) +
    3.31 +            Position.here(line_pos(i)))
    3.32 +        }
    3.33 +      }
    3.34 +      catch { case ERROR(msg) => Output.warning(msg + Position.here(line_pos(i))) }
    3.35 +
    3.36 +      if (line.contains('\t'))
    3.37 +        Output.warning("TAB character" + Position.here(line_pos(i)))
    3.38 +    }
    3.39 +
    3.40 +    if (content.contains('\r'))
    3.41 +      Output.warning("CR character" + Position.here(file_pos))
    3.42 +
    3.43 +    if (Word.bidi_detect(content))
    3.44 +      Output.warning("Bidirectional Unicode text " + Position.here(file_pos))
    3.45 +  }
    3.46 +
    3.47 +  def check_hg(root: Path)
    3.48 +  {
    3.49 +    Output.writeln("Checking " + root + " ...")
    3.50 +    using(Mercurial.open_repository(root)) { hg =>
    3.51 +      for {
    3.52 +        file <- hg.manifest()
    3.53 +        if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
    3.54 +      } check_file(root + Path.explode(file))
    3.55 +    }
    3.56 +  }
    3.57 +
    3.58 +
    3.59 +  /* Isabelle tool wrapper */
    3.60 +
    3.61 +  val isabelle_tool =
    3.62 +    Isabelle_Tool("check_sources", "some sanity checks for Isabelle sources", args =>
    3.63 +    {
    3.64 +      val getopts = Getopts("""
    3.65 +Usage: isabelle check_sources [ROOT_DIRS...]
    3.66 +
    3.67 +  Check .thy, .ML, ROOT files from manifest of Mercurial ROOT_DIRS.
    3.68 +""")
    3.69 +
    3.70 +      val specs = getopts(args)
    3.71 +      if (specs.isEmpty) getopts.usage()
    3.72 +
    3.73 +      for (root <- specs) check_hg(Path.explode(root))
    3.74 +    }, admin = true)
    3.75 +}
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/Admin/remote_dmg.scala	Wed Oct 12 10:22:34 2016 +0200
     4.3 @@ -0,0 +1,65 @@
     4.4 +/*  Title:      Pure/Admin/remote_dmg.scala
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Build dmg on remote Mac OS X system.
     4.8 +*/
     4.9 +
    4.10 +package isabelle
    4.11 +
    4.12 +
    4.13 +object Remote_DMG
    4.14 +{
    4.15 +  def remote_dmg(session: SSH.Session, tar_gz_file: Path, dmg_file: Path, volume_name: String = "")
    4.16 +  {
    4.17 +    session.with_tmp_dir(remote_dir =>
    4.18 +      using(session.sftp())(sftp =>
    4.19 +        {
    4.20 +          val cd = "cd " + File.bash_string(remote_dir) + "; "
    4.21 +
    4.22 +          sftp.write_file(remote_dir + "/dmg.tar.gz", tar_gz_file)
    4.23 +          session.execute(cd + "mkdir root && tar -C root -xzf dmg.tar.gz").check
    4.24 +          session.execute(
    4.25 +            cd + "hdiutil create -srcfolder root" +
    4.26 +              (if (volume_name == "") "" else " -volname " + File.bash_string(volume_name)) +
    4.27 +              " dmg.dmg").check
    4.28 +          sftp.read_file(remote_dir + "/dmg.dmg", dmg_file)
    4.29 +        }))
    4.30 +  }
    4.31 +
    4.32 +
    4.33 +  /* Isabelle tool wrapper */
    4.34 +
    4.35 +  val isabelle_tool =
    4.36 +    Isabelle_Tool("remote_dmg", "build dmg on remote Mac OS X system", args =>
    4.37 +    {
    4.38 +      Command_Line.tool0 {
    4.39 +        var port = SSH.default_port
    4.40 +        var volume_name = ""
    4.41 +
    4.42 +        val getopts = Getopts("""
    4.43 +Usage: isabelle remote_dmg [OPTIONS] USER@HOST TAR_GZ_FILE DMG_FILE
    4.44 +
    4.45 +  Options are:
    4.46 +    -p PORT      alternative SSH port (default: """ + SSH.default_port + """)
    4.47 +    -V NAME      specify volume name
    4.48 +
    4.49 +  Turn the contents of a tar.gz file into a dmg file -- produced on a remote
    4.50 +  Mac OS X system.
    4.51 +""",
    4.52 +          "p:" -> (arg => port = Value.Int.parse(arg)),
    4.53 +          "V:" -> (arg => volume_name = arg))
    4.54 +
    4.55 +        val more_args = getopts(args)
    4.56 +        val (user, host, tar_gz_file, dmg_file) =
    4.57 +          more_args match {
    4.58 +            case List(SSH.User_Host(user, host), tar_gz_file, dmg_file) =>
    4.59 +              (user, host, Path.explode(tar_gz_file), Path.explode(dmg_file))
    4.60 +            case _ => getopts.usage()
    4.61 +          }
    4.62 +
    4.63 +        val ssh = SSH.init(Options.init)
    4.64 +        using(ssh.open_session(user = user, host = host, port = port))(
    4.65 +          remote_dmg(_, tar_gz_file, dmg_file, volume_name))
    4.66 +      }
    4.67 +    }, admin = true)
    4.68 +}
     5.1 --- a/src/Pure/System/isabelle_system.scala	Wed Oct 12 09:38:20 2016 +0200
     5.2 +++ b/src/Pure/System/isabelle_system.scala	Wed Oct 12 10:22:34 2016 +0200
     5.3 @@ -324,6 +324,11 @@
     5.4  
     5.5    /** Isabelle resources **/
     5.6  
     5.7 +  /* repository clone with Admin */
     5.8 +
     5.9 +  def admin(): Boolean = Path.explode("~~/Admin").is_dir
    5.10 +
    5.11 +
    5.12    /* components */
    5.13  
    5.14    def components(): List[Path] =
     6.1 --- a/src/Pure/System/isabelle_tool.scala	Wed Oct 12 09:38:20 2016 +0200
     6.2 +++ b/src/Pure/System/isabelle_tool.scala	Wed Oct 12 10:22:34 2016 +0200
     6.3 @@ -113,11 +113,12 @@
     6.4        Update_Theorems.isabelle_tool)
     6.5  
     6.6    private def list_internal(): List[(String, String)] =
     6.7 -    for (tool <- internal_tools.toList) yield (tool.name, tool.description)
     6.8 +    for (tool <- internal_tools.toList if tool.accessible)
     6.9 +      yield (tool.name, tool.description)
    6.10  
    6.11    private def find_internal(name: String): Option[List[String] => Unit] =
    6.12      internal_tools.collectFirst({
    6.13 -      case tool if tool.name == name =>
    6.14 +      case tool if tool.name == name && tool.accessible =>
    6.15          args => Command_Line.tool0 { tool.body(args) }
    6.16        })
    6.17  
    6.18 @@ -148,4 +149,8 @@
    6.19    }
    6.20  }
    6.21  
    6.22 -sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit)
    6.23 +sealed case class Isabelle_Tool(
    6.24 +  name: String, description: String, body: List[String] => Unit, admin: Boolean = false)
    6.25 +{
    6.26 +  def accessible: Boolean = !admin || Isabelle_System.admin()
    6.27 +}
     7.1 --- a/src/Pure/Tools/build_doc.scala	Wed Oct 12 09:38:20 2016 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,106 +0,0 @@
     7.4 -/*  Title:      Pure/Tools/build_doc.scala
     7.5 -    Author:     Makarius
     7.6 -
     7.7 -Build Isabelle documentation.
     7.8 -*/
     7.9 -
    7.10 -package isabelle
    7.11 -
    7.12 -
    7.13 -import java.io.{File => JFile}
    7.14 -
    7.15 -
    7.16 -object Build_Doc
    7.17 -{
    7.18 -  /* build_doc */
    7.19 -
    7.20 -  def build_doc(
    7.21 -    options: Options,
    7.22 -    progress: Progress = Ignore_Progress,
    7.23 -    all_docs: Boolean = false,
    7.24 -    max_jobs: Int = 1,
    7.25 -    system_mode: Boolean = false,
    7.26 -    docs: List[String] = Nil): Int =
    7.27 -  {
    7.28 -    val selection =
    7.29 -      for {
    7.30 -        (name, info) <- Sessions.load(options).topological_order
    7.31 -        if info.groups.contains("doc")
    7.32 -        doc = info.options.string("document_variants")
    7.33 -        if all_docs || docs.contains(doc)
    7.34 -      } yield (doc, name)
    7.35 -
    7.36 -    val selected_docs = selection.map(_._1)
    7.37 -    val sessions = selection.map(_._2)
    7.38 -
    7.39 -    docs.filter(doc => !selected_docs.contains(doc)) match {
    7.40 -      case Nil =>
    7.41 -      case bad => error("No documentation session for " + commas_quote(bad))
    7.42 -    }
    7.43 -
    7.44 -    progress.echo("Build started for documentation " + commas_quote(selected_docs))
    7.45 -
    7.46 -    val res1 =
    7.47 -      Build.build(options, progress, requirements = true, build_heap = true,
    7.48 -        max_jobs = max_jobs, system_mode = system_mode, sessions = sessions)
    7.49 -    if (res1.ok) {
    7.50 -      Isabelle_System.with_tmp_dir("document_output")(output =>
    7.51 -        {
    7.52 -          val res2 =
    7.53 -            Build.build(
    7.54 -              options.bool.update("browser_info", false).
    7.55 -                string.update("document", "pdf").
    7.56 -                string.update("document_output", File.standard_path(output)),
    7.57 -              progress, clean_build = true, max_jobs = max_jobs, system_mode = system_mode,
    7.58 -              sessions = sessions)
    7.59 -          if (res2.ok) {
    7.60 -            val doc_dir = Path.explode("$ISABELLE_HOME/doc").file
    7.61 -            for (doc <- selected_docs) {
    7.62 -              val name = doc + ".pdf"
    7.63 -              File.copy(new JFile(output, name), new JFile(doc_dir, name))
    7.64 -            }
    7.65 -          }
    7.66 -          res2.rc
    7.67 -        })
    7.68 -    }
    7.69 -    else res1.rc
    7.70 -  }
    7.71 -
    7.72 -
    7.73 -  /* Isabelle tool wrapper */
    7.74 -
    7.75 -  val isabelle_tool = Isabelle_Tool("build_doc", "build Isabelle documentation", args =>
    7.76 -  {
    7.77 -    var all_docs = false
    7.78 -    var max_jobs = 1
    7.79 -    var system_mode = false
    7.80 -
    7.81 -    val getopts =
    7.82 -      Getopts("""
    7.83 -Usage: isabelle build_doc [OPTIONS] [DOCS ...]"
    7.84 -
    7.85 -  Options are:
    7.86 -    -a           select all documentation sessions
    7.87 -    -j INT       maximum number of parallel jobs (default 1)
    7.88 -    -s           system build mode
    7.89 -
    7.90 -  Build Isabelle documentation from documentation sessions with
    7.91 -  suitable document_variants entry.
    7.92 -""",
    7.93 -      "a" -> (_ => all_docs = true),
    7.94 -      "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
    7.95 -      "s" -> (_ => system_mode = true))
    7.96 -
    7.97 -    val docs = getopts(args)
    7.98 -
    7.99 -    if (!all_docs && docs.isEmpty) getopts.usage()
   7.100 -
   7.101 -    val options = Options.init()
   7.102 -    val progress = new Console_Progress()
   7.103 -    val rc =
   7.104 -      progress.interrupt_handler {
   7.105 -        build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
   7.106 -      }
   7.107 -    sys.exit(rc)
   7.108 -  })
   7.109 -}
     8.1 --- a/src/Pure/Tools/build_stats.scala	Wed Oct 12 09:38:20 2016 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,191 +0,0 @@
     8.4 -/*  Title:      Pure/Tools/build_stats.scala
     8.5 -    Author:     Makarius
     8.6 -
     8.7 -Statistics from session build output.
     8.8 -*/
     8.9 -
    8.10 -package isabelle
    8.11 -
    8.12 -
    8.13 -object Build_Stats
    8.14 -{
    8.15 -  /* presentation */
    8.16 -
    8.17 -  private val default_history_length = 100
    8.18 -  private val default_size = (800, 600)
    8.19 -  private val default_only_sessions = Set.empty[String]
    8.20 -  private val default_elapsed_threshold = Time.zero
    8.21 -  private val default_ml_timing: Option[Boolean] = None
    8.22 -
    8.23 -  def present_job(job: String, dir: Path,
    8.24 -    history_length: Int = default_history_length,
    8.25 -    size: (Int, Int) = default_size,
    8.26 -    only_sessions: Set[String] = default_only_sessions,
    8.27 -    elapsed_threshold: Time = default_elapsed_threshold,
    8.28 -    ml_timing: Option[Boolean] = default_ml_timing): List[String] =
    8.29 -  {
    8.30 -    val job_infos = CI_API.build_job_builds(job).sortBy(_.timestamp).reverse.take(history_length)
    8.31 -    if (job_infos.isEmpty) error("No build infos for job " + quote(job))
    8.32 -
    8.33 -    val all_infos =
    8.34 -      Par_List.map((job_info: CI_API.Job_Info) =>
    8.35 -        (job_info.timestamp / 1000, job_info.read_main_log.parse_build_info), job_infos)
    8.36 -    val all_sessions =
    8.37 -      (Set.empty[String] /: all_infos)(
    8.38 -        { case (s, (_, info)) => s ++ info.sessions.keySet })
    8.39 -
    8.40 -    def check_threshold(info: Build_Log.Build_Info, session: String): Boolean =
    8.41 -    {
    8.42 -      val t = info.timing(session)
    8.43 -      !t.is_zero && t.elapsed >= elapsed_threshold
    8.44 -    }
    8.45 -
    8.46 -    val sessions =
    8.47 -      for {
    8.48 -        session <- (if (only_sessions.isEmpty) all_sessions else all_sessions & only_sessions)
    8.49 -        if all_infos.filter({ case (_, info) => check_threshold(info, session) }).length >= 3
    8.50 -      } yield session
    8.51 -
    8.52 -    Isabelle_System.mkdirs(dir)
    8.53 -    for (session <- sessions) {
    8.54 -      Isabelle_System.with_tmp_file(session, "png") { data_file =>
    8.55 -        Isabelle_System.with_tmp_file(session, "gnuplot") { plot_file =>
    8.56 -          val data =
    8.57 -            for { (t, info) <- all_infos if info.finished(session) }
    8.58 -            yield {
    8.59 -              val timing1 = info.timing(session)
    8.60 -              val timing2 = info.ml_timing(session)
    8.61 -              List(t.toString,
    8.62 -                timing1.elapsed.minutes,
    8.63 -                timing1.cpu.minutes,
    8.64 -                timing2.elapsed.minutes,
    8.65 -                timing2.cpu.minutes,
    8.66 -                timing2.gc.minutes).mkString(" ")
    8.67 -            }
    8.68 -          File.write(data_file, cat_lines(data))
    8.69 -
    8.70 -          val plots1 =
    8.71 -            List(
    8.72 -              """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
    8.73 -              """ using 1:3 smooth csplines title "cpu time" """,
    8.74 -              """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
    8.75 -              """ using 1:2 smooth csplines title "elapsed time" """)
    8.76 -          val plots2 =
    8.77 -            List(
    8.78 -              """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
    8.79 -              """ using 1:5 smooth csplines title "ML cpu time" """,
    8.80 -              """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
    8.81 -              """ using 1:4 smooth csplines title "ML elapsed time" """,
    8.82 -              """ using 1:6 smooth sbezier title "ML gc time (smooth)" """,
    8.83 -              """ using 1:6 smooth csplines title "ML gc time" """)
    8.84 -          val plots =
    8.85 -            ml_timing match {
    8.86 -              case None => plots1
    8.87 -              case Some(false) => plots1 ::: plots2
    8.88 -              case Some(true) => plots2
    8.89 -            }
    8.90 -
    8.91 -          val data_file_name = File.standard_path(data_file.getAbsolutePath)
    8.92 -          File.write(plot_file, """
    8.93 -set terminal png size """ + size._1 + "," + size._2 + """
    8.94 -set output """ + quote(File.standard_path(dir + Path.basic(session + ".png"))) + """
    8.95 -set xdata time
    8.96 -set timefmt "%s"
    8.97 -set format x "%d-%b"
    8.98 -set xlabel """ + quote(session) + """ noenhanced
    8.99 -set key left top
   8.100 -plot [] [0:] """ + plots.map(s => quote(data_file_name) + " " + s).mkString(", ") + "\n")
   8.101 -          val result = Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(plot_file))
   8.102 -          if (result.rc != 0) {
   8.103 -            Output.error_message("Session " + session + ": gnuplot error")
   8.104 -            result.print
   8.105 -          }
   8.106 -        }
   8.107 -      }
   8.108 -    }
   8.109 -
   8.110 -    sessions.toList.sorted
   8.111 -  }
   8.112 -
   8.113 -
   8.114 -  /* Isabelle tool wrapper */
   8.115 -
   8.116 -  private val html_header = """<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
   8.117 -<html>
   8.118 -<head><title>Performance statistics from session build output</title></head>
   8.119 -<body>
   8.120 -"""
   8.121 -  private val html_footer = """
   8.122 -</body>
   8.123 -</html>
   8.124 -"""
   8.125 -
   8.126 -  val isabelle_tool =
   8.127 -    Isabelle_Tool("build_stats", "present statistics from session build output", args =>
   8.128 -    {
   8.129 -      var target_dir = Path.explode("stats")
   8.130 -      var ml_timing = default_ml_timing
   8.131 -      var only_sessions = default_only_sessions
   8.132 -      var elapsed_threshold = default_elapsed_threshold
   8.133 -      var history_length = default_history_length
   8.134 -      var size = default_size
   8.135 -
   8.136 -      val getopts = Getopts("""
   8.137 -Usage: isabelle build_stats [OPTIONS] [JOBS ...]
   8.138 -
   8.139 -  Options are:
   8.140 -    -D DIR       target directory (default "stats")
   8.141 -    -M           only ML timing
   8.142 -    -S SESSIONS  only given SESSIONS (comma separated)
   8.143 -    -T THRESHOLD only sessions with elapsed time >= THRESHOLD (minutes)
   8.144 -    -l LENGTH    length of history (default 100)
   8.145 -    -m           include ML timing
   8.146 -    -s WxH       size of PNG image (default 800x600)
   8.147 -
   8.148 -  Present statistics from session build output of the given JOBS, from Jenkins
   8.149 -  continuous build service specified as URL via ISABELLE_JENKINS_ROOT.
   8.150 -""",
   8.151 -        "D:" -> (arg => target_dir = Path.explode(arg)),
   8.152 -        "M" -> (_ => ml_timing = Some(true)),
   8.153 -        "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
   8.154 -        "T:" -> (arg => elapsed_threshold = Time.minutes(Value.Double.parse(arg))),
   8.155 -        "l:" -> (arg => history_length = Value.Int.parse(arg)),
   8.156 -        "m" -> (_ => ml_timing = Some(false)),
   8.157 -        "s:" -> (arg =>
   8.158 -          space_explode('x', arg).map(Value.Int.parse(_)) match {
   8.159 -            case List(w, h) if w > 0 && h > 0 => size = (w, h)
   8.160 -            case _ => error("Error bad PNG image size: " + quote(arg))
   8.161 -          }))
   8.162 -
   8.163 -      val jobs = getopts(args)
   8.164 -      val all_jobs = CI_API.build_jobs()
   8.165 -      val bad_jobs = jobs.filterNot(all_jobs.contains(_)).sorted
   8.166 -
   8.167 -      if (jobs.isEmpty)
   8.168 -        error("No build jobs given. Available jobs: " + all_jobs.sorted.mkString(" "))
   8.169 -
   8.170 -      if (bad_jobs.nonEmpty)
   8.171 -        error("Unknown build jobs: " + bad_jobs.mkString(" ") +
   8.172 -          "\nAvailable jobs: " + all_jobs.sorted.mkString(" "))
   8.173 -
   8.174 -      for (job <- jobs) {
   8.175 -        val dir = target_dir + Path.basic(job)
   8.176 -        Output.writeln(dir.implode)
   8.177 -        val sessions =
   8.178 -          present_job(job, dir, history_length, size, only_sessions, elapsed_threshold, ml_timing)
   8.179 -        File.write(dir + Path.basic("index.html"),
   8.180 -          html_header + "\n<h1>" + HTML.output(job) + "</h1>\n" +
   8.181 -          cat_lines(
   8.182 -            sessions.map(session =>
   8.183 -              """<br/><img src=""" + quote(HTML.output(session + ".png")) + """><br/>""")) +
   8.184 -          "\n" + html_footer)
   8.185 -      }
   8.186 -
   8.187 -      File.write(target_dir + Path.basic("index.html"),
   8.188 -        html_header + "\n<ul>\n" +
   8.189 -        cat_lines(
   8.190 -          jobs.map(job => """<li> <a href=""" + quote(HTML.output(job + "/index.html")) + """>""" +
   8.191 -            HTML.output(job) + """</a> </li>""")) +
   8.192 -        "\n</ul>\n" + html_footer)
   8.193 -  })
   8.194 -}
     9.1 --- a/src/Pure/Tools/check_sources.scala	Wed Oct 12 09:38:20 2016 +0200
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,72 +0,0 @@
     9.4 -/*  Title:      Pure/Tools/check_sources.scala
     9.5 -    Author:     Makarius
     9.6 -
     9.7 -Some sanity checks for Isabelle sources.
     9.8 -*/
     9.9 -
    9.10 -package isabelle
    9.11 -
    9.12 -
    9.13 -object Check_Sources
    9.14 -{
    9.15 -  def check_file(path: Path)
    9.16 -  {
    9.17 -    val file_name = path.implode
    9.18 -    val file_pos = path.position
    9.19 -    def line_pos(i: Int) = Position.Line_File(i + 1, file_name)
    9.20 -
    9.21 -    val content = File.read(path)
    9.22 -
    9.23 -    for { (line, i) <- split_lines(content).iterator.zipWithIndex }
    9.24 -    {
    9.25 -      try {
    9.26 -        Symbol.decode_strict(line)
    9.27 -
    9.28 -        for { c <- Word.codepoint_iterator(line); if c > 128 && !Character.isAlphabetic(c) }
    9.29 -        {
    9.30 -          Output.warning("Suspicious Unicode character " + quote(Word.codepoint(c)) +
    9.31 -            Position.here(line_pos(i)))
    9.32 -        }
    9.33 -      }
    9.34 -      catch { case ERROR(msg) => Output.warning(msg + Position.here(line_pos(i))) }
    9.35 -
    9.36 -      if (line.contains('\t'))
    9.37 -        Output.warning("TAB character" + Position.here(line_pos(i)))
    9.38 -    }
    9.39 -
    9.40 -    if (content.contains('\r'))
    9.41 -      Output.warning("CR character" + Position.here(file_pos))
    9.42 -
    9.43 -    if (Word.bidi_detect(content))
    9.44 -      Output.warning("Bidirectional Unicode text " + Position.here(file_pos))
    9.45 -  }
    9.46 -
    9.47 -  def check_hg(root: Path)
    9.48 -  {
    9.49 -    Output.writeln("Checking " + root + " ...")
    9.50 -    using(Mercurial.open_repository(root)) { hg =>
    9.51 -      for {
    9.52 -        file <- hg.manifest()
    9.53 -        if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
    9.54 -      } check_file(root + Path.explode(file))
    9.55 -    }
    9.56 -  }
    9.57 -
    9.58 -
    9.59 -  /* Isabelle tool wrapper */
    9.60 -
    9.61 -  val isabelle_tool =
    9.62 -    Isabelle_Tool("check_sources", "some sanity checks for Isabelle sources", args =>
    9.63 -    {
    9.64 -      val getopts = Getopts("""
    9.65 -Usage: isabelle check_sources [ROOT_DIRS...]
    9.66 -
    9.67 -  Check .thy, .ML, ROOT files from manifest of Mercurial ROOT_DIRS.
    9.68 -""")
    9.69 -
    9.70 -      val specs = getopts(args)
    9.71 -      if (specs.isEmpty) getopts.usage()
    9.72 -
    9.73 -      for (root <- specs) check_hg(Path.explode(root))
    9.74 -    })
    9.75 -}
    10.1 --- a/src/Pure/Tools/remote_dmg.scala	Wed Oct 12 09:38:20 2016 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,64 +0,0 @@
    10.4 -/*  Title:      Pure/Tools/remote_dmg.scala
    10.5 -    Author:     Makarius
    10.6 -
    10.7 -Build dmg on remote Mac OS X system.
    10.8 -*/
    10.9 -
   10.10 -package isabelle
   10.11 -
   10.12 -
   10.13 -object Remote_DMG
   10.14 -{
   10.15 -  def remote_dmg(session: SSH.Session, tar_gz_file: Path, dmg_file: Path, volume_name: String = "")
   10.16 -  {
   10.17 -    session.with_tmp_dir(remote_dir =>
   10.18 -      using(session.sftp())(sftp =>
   10.19 -        {
   10.20 -          val cd = "cd " + File.bash_string(remote_dir) + "; "
   10.21 -
   10.22 -          sftp.write_file(remote_dir + "/dmg.tar.gz", tar_gz_file)
   10.23 -          session.execute(cd + "mkdir root && tar -C root -xzf dmg.tar.gz").check
   10.24 -          session.execute(
   10.25 -            cd + "hdiutil create -srcfolder root" +
   10.26 -              (if (volume_name == "") "" else " -volname " + File.bash_string(volume_name)) +
   10.27 -              " dmg.dmg").check
   10.28 -          sftp.read_file(remote_dir + "/dmg.dmg", dmg_file)
   10.29 -        }))
   10.30 -  }
   10.31 -
   10.32 -
   10.33 -  /* Isabelle tool wrapper */
   10.34 -
   10.35 -  val isabelle_tool = Isabelle_Tool("remote_dmg", "build dmg on remote Mac OS X system", args =>
   10.36 -  {
   10.37 -    Command_Line.tool0 {
   10.38 -      var port = SSH.default_port
   10.39 -      var volume_name = ""
   10.40 -
   10.41 -      val getopts = Getopts("""
   10.42 -Usage: isabelle remote_dmg [OPTIONS] USER@HOST TAR_GZ_FILE DMG_FILE
   10.43 -
   10.44 -  Options are:
   10.45 -    -p PORT      alternative SSH port (default: """ + SSH.default_port + """)
   10.46 -    -V NAME      specify volume name
   10.47 -
   10.48 -  Turn the contents of a tar.gz file into a dmg file -- produced on a remote
   10.49 -  Mac OS X system.
   10.50 -""",
   10.51 -        "p:" -> (arg => port = Value.Int.parse(arg)),
   10.52 -        "V:" -> (arg => volume_name = arg))
   10.53 -
   10.54 -      val more_args = getopts(args)
   10.55 -      val (user, host, tar_gz_file, dmg_file) =
   10.56 -        more_args match {
   10.57 -          case List(SSH.User_Host(user, host), tar_gz_file, dmg_file) =>
   10.58 -            (user, host, Path.explode(tar_gz_file), Path.explode(dmg_file))
   10.59 -          case _ => getopts.usage()
   10.60 -        }
   10.61 -
   10.62 -      val ssh = SSH.init(Options.init)
   10.63 -      using(ssh.open_session(user = user, host = host, port = port))(
   10.64 -        remote_dmg(_, tar_gz_file, dmg_file, volume_name))
   10.65 -    }
   10.66 -  })
   10.67 -}
    11.1 --- a/src/Pure/build-jars	Wed Oct 12 09:38:20 2016 +0200
    11.2 +++ b/src/Pure/build-jars	Wed Oct 12 10:22:34 2016 +0200
    11.3 @@ -9,11 +9,15 @@
    11.4  ## sources
    11.5  
    11.6  declare -a SOURCES=(
    11.7 +  Admin/build_doc.scala
    11.8    Admin/build_history.scala
    11.9    Admin/build_log.scala
   11.10 +  Admin/build_stats.scala
   11.11 +  Admin/check_sources.scala
   11.12    Admin/ci_api.scala
   11.13    Admin/ci_profile.scala
   11.14    Admin/isabelle_cronjob.scala
   11.15 +  Admin/remote_dmg.scala
   11.16    Concurrent/consumer_thread.scala
   11.17    Concurrent/counter.scala
   11.18    Concurrent/event_timer.scala
   11.19 @@ -113,10 +117,7 @@
   11.20    Thy/thy_syntax.scala
   11.21    Tools/bibtex.scala
   11.22    Tools/build.scala
   11.23 -  Tools/build_doc.scala
   11.24 -  Tools/build_stats.scala
   11.25    Tools/check_keywords.scala
   11.26 -  Tools/check_sources.scala
   11.27    Tools/debugger.scala
   11.28    Tools/doc.scala
   11.29    Tools/main.scala
   11.30 @@ -125,7 +126,6 @@
   11.31    Tools/ml_statistics.scala
   11.32    Tools/news.scala
   11.33    Tools/print_operation.scala
   11.34 -  Tools/remote_dmg.scala
   11.35    Tools/simplifier_trace.scala
   11.36    Tools/task_statistics.scala
   11.37    Tools/update_cartouches.scala