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