src/Pure/Admin/ci_profile.scala
author Lars Hupel <lars.hupel@mytum.de>
Thu, 04 Oct 2018 14:52:50 +0200
changeset 69120 9d3b41732fe0
parent 68498 6855ebc61b4f
child 69121 842958af0400
permissions -rw-r--r--
Jenkins: detect machine; adjust job parameters accordingly
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,
68498
6855ebc61b4f support NUMA shuffling in CI
Lars Hupel <lars.hupel@mytum.de>
parents: 68013
diff changeset
    27
        numa_shuffling = numa,
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    28
        max_jobs = jobs,
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    29
        dirs = include,
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    30
        select_dirs = select,
64286
b2f7aa1c6b75 Jenkins: build in system mode again
Lars Hupel <lars.hupel@mytum.de>
parents: 64285
diff changeset
    31
        system_mode = true,
65419
457e4fbed731 explicit Sessions.Selection;
wenzelm
parents: 65415
diff changeset
    32
        selection = selection)
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    33
    }
63387
3395fe5e3893 more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents: 63385
diff changeset
    34
    val end_time = Time.now()
3395fe5e3893 more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents: 63385
diff changeset
    35
    (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
    36
  }
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    37
63328
7a8515c58271 read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents: 63294
diff changeset
    38
  private def load_properties(): JProperties =
7a8515c58271 read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents: 63294
diff changeset
    39
  {
7a8515c58271 read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents: 63294
diff changeset
    40
    val props = new JProperties()
63418
Lars Hupel <lars.hupel@mytum.de>
parents: 63401
diff changeset
    41
    val file_name = Isabelle_System.getenv("ISABELLE_CI_PROPERTIES")
Lars Hupel <lars.hupel@mytum.de>
parents: 63401
diff changeset
    42
Lars Hupel <lars.hupel@mytum.de>
parents: 63401
diff changeset
    43
    if (file_name != "")
Lars Hupel <lars.hupel@mytum.de>
parents: 63401
diff changeset
    44
    {
Lars Hupel <lars.hupel@mytum.de>
parents: 63401
diff changeset
    45
      val file = Path.explode(file_name).file
Lars Hupel <lars.hupel@mytum.de>
parents: 63401
diff changeset
    46
      if (file.exists())
Lars Hupel <lars.hupel@mytum.de>
parents: 63401
diff changeset
    47
        props.load(new java.io.FileReader(file))
Lars Hupel <lars.hupel@mytum.de>
parents: 63401
diff changeset
    48
      props
Lars Hupel <lars.hupel@mytum.de>
parents: 63401
diff changeset
    49
    }
Lars Hupel <lars.hupel@mytum.de>
parents: 63401
diff changeset
    50
    else
Lars Hupel <lars.hupel@mytum.de>
parents: 63401
diff changeset
    51
      props
63328
7a8515c58271 read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents: 63294
diff changeset
    52
  }
7a8515c58271 read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents: 63294
diff changeset
    53
63385
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    54
  private def compute_timing(results: Build.Results, group: Option[String]): Timing =
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    55
  {
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    56
    val timings = results.sessions.collect {
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    57
      case session if group.forall(results.info(session).groups.contains(_)) =>
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    58
        results(session).timing
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    59
    }
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    60
    (Timing.zero /: timings)(_ + _)
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    61
  }
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    62
63894
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
    63
  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
    64
  {
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
    65
    if (documents)
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
    66
      options
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
    67
        .bool.update("browser_info", true)
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
    68
        .string.update("document", "pdf")
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
    69
        .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
    70
    else
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
    71
      options
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
    72
  }
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
    73
63385
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    74
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    75
  final def hg_id(path: Path): String =
64232
367d83d6030e clarified hg.id operation, with explicit tip as default;
wenzelm
parents: 64217
diff changeset
    76
    Mercurial.repository(path).id()
63385
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    77
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    78
  final def print_section(title: String): Unit =
63349
6c889fe495a2 print statistics; tuned
Lars Hupel <lars.hupel@mytum.de>
parents: 63328
diff changeset
    79
    println(s"\n=== $title ===\n")
6c889fe495a2 print statistics; tuned
Lars Hupel <lars.hupel@mytum.de>
parents: 63328
diff changeset
    80
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    81
63385
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    82
  final val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME"))
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    83
  final val isabelle_id = hg_id(isabelle_home)
63472
Lars Hupel <lars.hupel@mytum.de>
parents: 63418
diff changeset
    84
  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
    85
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
    86
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    87
  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
    88
  {
63349
6c889fe495a2 print statistics; tuned
Lars Hupel <lars.hupel@mytum.de>
parents: 63328
diff changeset
    89
    print_section("CONFIGURATION")
64081
38bb09ed965b more uniform treatment of settings;
wenzelm
parents: 64080
diff changeset
    90
    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
    91
    val props = load_properties()
68013
7a30a3cc2763 workaround for jdk-10.0.1;
wenzelm
parents: 65422
diff changeset
    92
    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
    93
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    94
    val options =
63894
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
    95
      with_documents(Options.init())
65056
002b4c8c366e clarified defaults;
wenzelm
parents: 64286
diff changeset
    96
        .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
    97
        .int.update("threads", threads)
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    98
69120
9d3b41732fe0 Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents: 68498
diff changeset
    99
    println(s"jobs = $jobs, threads = $threads, numa = $numa")
9d3b41732fe0 Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents: 68498
diff changeset
   100
63349
6c889fe495a2 print statistics; tuned
Lars Hupel <lars.hupel@mytum.de>
parents: 63328
diff changeset
   101
    print_section("BUILD")
63472
Lars Hupel <lars.hupel@mytum.de>
parents: 63418
diff changeset
   102
    println(s"Build started at $start_time")
Lars Hupel <lars.hupel@mytum.de>
parents: 63418
diff changeset
   103
    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
   104
    pre_hook(args)
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   105
63472
Lars Hupel <lars.hupel@mytum.de>
parents: 63418
diff changeset
   106
    print_section("LOG")
63387
3395fe5e3893 more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents: 63385
diff changeset
   107
    val (results, elapsed_time) = build(options)
63349
6c889fe495a2 print statistics; tuned
Lars Hupel <lars.hupel@mytum.de>
parents: 63328
diff changeset
   108
6c889fe495a2 print statistics; tuned
Lars Hupel <lars.hupel@mytum.de>
parents: 63328
diff changeset
   109
    print_section("TIMING")
63385
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
   110
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
   111
    val groups = results.sessions.map(results.info).flatMap(_.groups)
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
   112
    for (group <- groups)
Lars Hupel <lars.hupel@mytum.de>
parents: 63349
diff changeset
   113
      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
   114
3395fe5e3893 more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents: 63385
diff changeset
   115
    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
   116
    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
   117
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   118
    if (!results.ok) {
63349
6c889fe495a2 print statistics; tuned
Lars Hupel <lars.hupel@mytum.de>
parents: 63328
diff changeset
   119
      print_section("FAILED SESSIONS")
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   120
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   121
      for (name <- results.sessions) {
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   122
        if (results.cancelled(name)) {
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   123
          println(s"Session $name: CANCELLED")
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   124
        }
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   125
        else {
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   126
          val result = results(name)
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   127
          if (!result.ok)
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   128
            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
   129
        }
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   130
      }
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
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   133
    post_hook(results)
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
    System.exit(results.rc)
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   136
  }
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   137
69120
9d3b41732fe0 Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents: 68498
diff changeset
   138
  /* profile */
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   139
69120
9d3b41732fe0 Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents: 68498
diff changeset
   140
  def threads: Int = Isabelle_System.hostname() match {
9d3b41732fe0 Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents: 68498
diff changeset
   141
    case "hpcisabelle" => 8
9d3b41732fe0 Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents: 68498
diff changeset
   142
    case "lxcisa0" => 4
9d3b41732fe0 Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents: 68498
diff changeset
   143
    case _ => 2
9d3b41732fe0 Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents: 68498
diff changeset
   144
  }
9d3b41732fe0 Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents: 68498
diff changeset
   145
9d3b41732fe0 Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents: 68498
diff changeset
   146
  def jobs: Int = Isabelle_System.hostname() match {
9d3b41732fe0 Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents: 68498
diff changeset
   147
    case "hpcisabelle" => 8
9d3b41732fe0 Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents: 68498
diff changeset
   148
    case "lxcisa0" => 10
9d3b41732fe0 Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents: 68498
diff changeset
   149
    case _ => 2
9d3b41732fe0 Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents: 68498
diff changeset
   150
  }
9d3b41732fe0 Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents: 68498
diff changeset
   151
9d3b41732fe0 Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents: 68498
diff changeset
   152
  def numa: Boolean = Isabelle_System.hostname() == "hpcisabelle"
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   153
63894
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
   154
  def documents: Boolean = true
64285
d7e0123a752b Jenkins: configurable clean build
Lars Hupel <lars.hupel@mytum.de>
parents: 64232
diff changeset
   155
  def clean: Boolean = true
63894
7534eec7cfad benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents: 63685
diff changeset
   156
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   157
  def include: List[Path]
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   158
  def select: List[Path]
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   159
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   160
  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
   161
  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
   162
65419
457e4fbed731 explicit Sessions.Selection;
wenzelm
parents: 65415
diff changeset
   163
  def selection: Sessions.Selection
63288
e0513d6e4916 start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   164
}