src/Pure/Tools/ci_profile.scala
author wenzelm
Fri Oct 07 11:10:17 2016 +0200 (2016-10-07)
changeset 64079 ff26032b7f2a
parent 64055 acd3e25975a2
child 64080 2e5c0bd708af
permissions -rw-r--r--
tuned;
     1 /*  Title:      Pure/Tools/ci_profile.scala
     2     Author:     Lars Hupel
     3 
     4 Build profile for continuous integration services.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.time.{Instant, ZoneId}
    11 import java.time.format.DateTimeFormatter
    12 import java.util.{Properties => JProperties}
    13 
    14 
    15 abstract class CI_Profile extends Isabelle_Tool.Body
    16 {
    17   private def build(options: Options): (Build.Results, Time) =
    18   {
    19     val progress = new Console_Progress(true)
    20     val start_time = Time.now()
    21     val results = progress.interrupt_handler {
    22       Build.build_selection(
    23         options = options,
    24         progress = progress,
    25         clean_build = true,
    26         verbose = true,
    27         max_jobs = jobs,
    28         dirs = include,
    29         select_dirs = select,
    30         system_mode = true,
    31         selection = select_sessions _)
    32     }
    33     val end_time = Time.now()
    34     (results, end_time - start_time)
    35   }
    36 
    37   private def load_properties(): JProperties =
    38   {
    39     val props = new JProperties()
    40     val file_name = Isabelle_System.getenv("ISABELLE_CI_PROPERTIES")
    41 
    42     if (file_name != "")
    43     {
    44       val file = Path.explode(file_name).file
    45       if (file.exists())
    46         props.load(new java.io.FileReader(file))
    47       props
    48     }
    49     else
    50       props
    51   }
    52 
    53   private def compute_timing(results: Build.Results, group: Option[String]): Timing =
    54   {
    55     val timings = results.sessions.collect {
    56       case session if group.forall(results.info(session).groups.contains(_)) =>
    57         results(session).timing
    58     }
    59     (Timing.zero /: timings)(_ + _)
    60   }
    61 
    62   private def with_documents(options: Options): Options =
    63   {
    64     if (documents)
    65       options
    66         .bool.update("browser_info", true)
    67         .string.update("document", "pdf")
    68         .string.update("document_variants", "document:outline=/proof,/ML")
    69     else
    70       options
    71   }
    72 
    73 
    74   final def hg_id(path: Path): String =
    75     Isabelle_System.hg("id -i", path.file).out
    76 
    77   final def print_section(title: String): Unit =
    78     println(s"\n=== $title ===\n")
    79 
    80 
    81   final val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME"))
    82   final val isabelle_id = hg_id(isabelle_home)
    83   final val start_time = Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME)
    84 
    85 
    86   override final def apply(args: List[String]): Unit =
    87   {
    88     print_section("CONFIGURATION")
    89     Build.ml_settings.foreach(a => println(a + "=" + quote(Isabelle_System.getenv(a))))
    90     val props = load_properties()
    91     System.getProperties().putAll(props)
    92 
    93     val options =
    94       with_documents(Options.init())
    95         .int.update("parallel_proofs", 2)
    96         .int.update("threads", threads)
    97 
    98     print_section("BUILD")
    99     println(s"Build started at $start_time")
   100     println(s"Isabelle id $isabelle_id")
   101     pre_hook(args)
   102 
   103     print_section("LOG")
   104     val (results, elapsed_time) = build(options)
   105 
   106     print_section("TIMING")
   107 
   108     val groups = results.sessions.map(results.info).flatMap(_.groups)
   109     for (group <- groups)
   110       println(s"Group $group: " + compute_timing(results, Some(group)).message_resources)
   111 
   112     val total_timing = compute_timing(results, None).copy(elapsed = elapsed_time)
   113     println("Overall: " + total_timing.message_resources)
   114 
   115     if (!results.ok) {
   116       print_section("FAILED SESSIONS")
   117 
   118       for (name <- results.sessions) {
   119         if (results.cancelled(name)) {
   120           println(s"Session $name: CANCELLED")
   121         }
   122         else {
   123           val result = results(name)
   124           if (!result.ok)
   125             println(s"Session $name: FAILED ${result.rc}")
   126         }
   127       }
   128     }
   129 
   130     post_hook(results)
   131 
   132     System.exit(results.rc)
   133   }
   134 
   135 
   136   /* profile */
   137 
   138   def documents: Boolean = true
   139 
   140   def threads: Int
   141   def jobs: Int
   142   def include: List[Path]
   143   def select: List[Path]
   144 
   145   def pre_hook(args: List[String]): Unit
   146   def post_hook(results: Build.Results): Unit
   147 
   148   def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree)
   149 }