src/Pure/Admin/ci_profile.scala
author wenzelm
Fri, 20 Apr 2018 11:41:09 +0200
changeset 68013 7a30a3cc2763
parent 65422 b606c98e6d10
child 68498 6855ebc61b4f
permissions -rw-r--r--
workaround for jdk-10.0.1;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64160
1eea419fab65 clarified files;
wenzelm
parents: 64115
diff changeset
     1
/*  Title:      Pure/Admin/ci_profile.scala
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     2
    Author:     Lars Hupel
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     3
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     4
Build profile for continuous integration services.
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     5
*/
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     6
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     7
package isabelle
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     8
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     9
64055
acd3e25975a2 proper imports;
wenzelm
parents: 63894
diff changeset
    10
import java.time.{Instant, ZoneId}
63472
Lars Hupel <lars.hupel@mytum.de>
parents: 63418
diff changeset
    11
import java.time.format.DateTimeFormatter
68013
7a30a3cc2763 workaround for jdk-10.0.1;
wenzelm
parents: 65422
diff changeset
    12
import java.util.{Properties => JProperties, Map => JMap}
63328
7a8515c58271 read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents: 63294
diff changeset
    13
7a8515c58271 read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents: 63294
diff changeset
    14
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    15
abstract class CI_Profile extends Isabelle_Tool.Body
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    16
{
63387
3395fe5e3893 more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents: 63385
diff changeset
    17
  private def build(options: Options): (Build.Results, Time) =
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    18
  {
64115
wenzelm
parents: 64081
diff changeset
    19
    val progress = new Console_Progress(verbose = true)
63387
3395fe5e3893 more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents: 63385
diff changeset
    20
    val start_time = Time.now()
3395fe5e3893 more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents: 63385
diff changeset
    21
    val results = progress.interrupt_handler {
65422
b606c98e6d10 tuned signature;
wenzelm
parents: 65419
diff changeset
    22
      Build.build(
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    23
        options = options,
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    24
        progress = progress,
64285
d7e0123a752b Jenkins: configurable clean build
Lars Hupel <lars.hupel@mytum.de>
parents: 64232
diff changeset
    25
        clean_build = clean,
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    26
        verbose = true,
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    27
        max_jobs = jobs,
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    28
        dirs = include,
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    29
        select_dirs = select,
64286
b2f7aa1c6b75 Jenkins: build in system mode again
Lars Hupel <lars.hupel@mytum.de>
parents: 64285
diff changeset
    30
        system_mode = true,
65419
457e4fbed731 explicit Sessions.Selection;
wenzelm
parents: 65415
diff changeset
    31
        selection = selection)
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    32
    }
63387
3395fe5e3893 more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents: 63385
diff changeset
    33
    val end_time = Time.now()
3395fe5e3893 more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents: 63385
diff changeset
    34
    (results, end_time - start_time)
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    35
  }
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    36
63328
7a8515c58271 read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents: 63294
diff changeset
    37
  private def load_properties(): JProperties =
7a8515c58271 read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents: 63294
diff changeset
    38
  {
7a8515c58271 read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents: 63294
diff changeset
    39
    val props = new JProperties()
63418
Lars Hupel <lars.hupel@mytum.de>
parents: 63401
diff changeset
    40
    val file_name = Isabelle_System.getenv("ISABELLE_CI_PROPERTIES")
Lars Hupel <lars.hupel@mytum.de>
parents: 63401
diff changeset
    41
Lars Hupel <lars.hupel@mytum.de>
parents: 63401
diff changeset
    42
    if (file_name != "")
Lars Hupel <lars.hupel@mytum.de>
parents: 63401
diff changeset
    43
    {
Lars Hupel <lars.hupel@mytum.de>
parents: 63401
diff changeset
    44
      val file = Path.explode(file_name).file
Lars Hupel <lars.hupel@mytum.de>
parents: 63401
diff changeset
    45
      if (file.exists())
Lars Hupel <lars.hupel@mytum.de>
parents: 63401
diff changeset
    46
        props.load(new java.io.FileReader(file))
Lars Hupel <lars.hupel@mytum.de>
parents: 63401
diff changeset
    47
      props
Lars Hupel <lars.hupel@mytum.de>
parents: 63401
diff changeset
    48
    }
Lars Hupel <lars.hupel@mytum.de>
parents: 63401
diff changeset
    49
    else
Lars Hupel <lars.hupel@mytum.de>
parents: 63401
diff changeset
    50
      props
63328
7a8515c58271 read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents: 63294
diff changeset
    51
  }
7a8515c58271 read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents: 63294
diff changeset
    52
63385
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    53
  private def compute_timing(results: Build.Results, group: Option[String]): Timing =
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    54
  {
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    55
    val timings = results.sessions.collect {
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    56
      case session if group.forall(results.info(session).groups.contains(_)) =>
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    57
        results(session).timing
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    58
    }
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    59
    (Timing.zero /: timings)(_ + _)
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    60
  }
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    61
63894
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
    62
  private def with_documents(options: Options): Options =
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
    63
  {
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
    64
    if (documents)
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
    65
      options
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
    66
        .bool.update("browser_info", true)
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
    67
        .string.update("document", "pdf")
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
    68
        .string.update("document_variants", "document:outline=/proof,/ML")
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
    69
    else
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
    70
      options
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
    71
  }
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
    72
63385
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    73
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    74
  final def hg_id(path: Path): String =
64232
367d83d6030e clarified hg.id operation, with explicit tip as default;
wenzelm
parents: 64217
diff changeset
    75
    Mercurial.repository(path).id()
63385
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    76
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    77
  final def print_section(title: String): Unit =
63349
6c889fe495a2 print statistics; tuned
Lars Hupel <lars.hupel@mytum.de>
parents: 63328
diff changeset
    78
    println(s"\n=== $title ===\n")
6c889fe495a2 print statistics; tuned
Lars Hupel <lars.hupel@mytum.de>
parents: 63328
diff changeset
    79
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    80
63385
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    81
  final val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME"))
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    82
  final val isabelle_id = hg_id(isabelle_home)
63472
Lars Hupel <lars.hupel@mytum.de>
parents: 63418
diff changeset
    83
  final val start_time = Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME)
63385
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    84
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    85
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    86
  override final def apply(args: List[String]): Unit =
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    87
  {
63349
6c889fe495a2 print statistics; tuned
Lars Hupel <lars.hupel@mytum.de>
parents: 63328
diff changeset
    88
    print_section("CONFIGURATION")
64081
38bb09ed965b more uniform treatment of settings;
wenzelm
parents: 64080
diff changeset
    89
    println(Build_Log.Settings.show())
63328
7a8515c58271 read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents: 63294
diff changeset
    90
    val props = load_properties()
68013
7a30a3cc2763 workaround for jdk-10.0.1;
wenzelm
parents: 65422
diff changeset
    91
    System.getProperties().asInstanceOf[JMap[AnyRef, AnyRef]].putAll(props)
63328
7a8515c58271 read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents: 63294
diff changeset
    92
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    93
    val options =
63894
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
    94
      with_documents(Options.init())
65056
002b4c8c366e clarified defaults;
wenzelm
parents: 64286
diff changeset
    95
        .int.update("parallel_proofs", 1)
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    96
        .int.update("threads", threads)
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    97
63349
6c889fe495a2 print statistics; tuned
Lars Hupel <lars.hupel@mytum.de>
parents: 63328
diff changeset
    98
    print_section("BUILD")
63472
Lars Hupel <lars.hupel@mytum.de>
parents: 63418
diff changeset
    99
    println(s"Build started at $start_time")
Lars Hupel <lars.hupel@mytum.de>
parents: 63418
diff changeset
   100
    println(s"Isabelle id $isabelle_id")
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   101
    pre_hook(args)
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   102
63472
Lars Hupel <lars.hupel@mytum.de>
parents: 63418
diff changeset
   103
    print_section("LOG")
63387
3395fe5e3893 more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents: 63385
diff changeset
   104
    val (results, elapsed_time) = build(options)
63349
6c889fe495a2 print statistics; tuned
Lars Hupel <lars.hupel@mytum.de>
parents: 63328
diff changeset
   105
6c889fe495a2 print statistics; tuned
Lars Hupel <lars.hupel@mytum.de>
parents: 63328
diff changeset
   106
    print_section("TIMING")
63385
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
   107
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
   108
    val groups = results.sessions.map(results.info).flatMap(_.groups)
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
   109
    for (group <- groups)
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
   110
      println(s"Group $group: " + compute_timing(results, Some(group)).message_resources)
63387
3395fe5e3893 more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents: 63385
diff changeset
   111
3395fe5e3893 more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents: 63385
diff changeset
   112
    val total_timing = compute_timing(results, None).copy(elapsed = elapsed_time)
3395fe5e3893 more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents: 63385
diff changeset
   113
    println("Overall: " + total_timing.message_resources)
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   114
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   115
    if (!results.ok) {
63349
6c889fe495a2 print statistics; tuned
Lars Hupel <lars.hupel@mytum.de>
parents: 63328
diff changeset
   116
      print_section("FAILED SESSIONS")
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   117
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   118
      for (name <- results.sessions) {
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   119
        if (results.cancelled(name)) {
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   120
          println(s"Session $name: CANCELLED")
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   121
        }
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   122
        else {
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   123
          val result = results(name)
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   124
          if (!result.ok)
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   125
            println(s"Session $name: FAILED ${result.rc}")
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   126
        }
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   127
      }
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   128
    }
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   129
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   130
    post_hook(results)
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   131
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   132
    System.exit(results.rc)
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   133
  }
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   134
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   135
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   136
  /* profile */
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   137
63894
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
   138
  def documents: Boolean = true
64285
d7e0123a752b Jenkins: configurable clean build
Lars Hupel <lars.hupel@mytum.de>
parents: 64232
diff changeset
   139
  def clean: Boolean = true
63894
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
   140
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   141
  def threads: Int
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   142
  def jobs: Int
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   143
  def include: List[Path]
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   144
  def select: List[Path]
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   145
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   146
  def pre_hook(args: List[String]): Unit
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   147
  def post_hook(results: Build.Results): Unit
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   148
65419
457e4fbed731 explicit Sessions.Selection;
wenzelm
parents: 65415
diff changeset
   149
  def selection: Sessions.Selection
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   150
}