/* Title: Pure/Build/build_ci.scala
Author: Fabian Huch, TU Munich
Module for automated (continuous integration) builds.
*/
package isabelle
import scala.collection.mutable
object Build_CI {
def section(title: String): String = "\n=== " + title + " ===\n"
/* mailing */
object Mail_System {
def try_open(options: Options): Option[Mail_System] =
Exn.capture(new Mail_System(options)) match {
case Exn.Res(res) if res.server.defined => Some(res)
case _ => None
}
}
class Mail_System private(options: Options) {
val from: Mail.Address = Mail.address(options.string("ci_mail_from"))
val to: Mail.Address = Mail.address(options.string("ci_mail_to"))
val server: Mail.Server =
new Mail.Server(Mail.address(options.string("ci_mail_sender")),
smtp_host = options.string("ci_mail_smtp_host"),
smtp_port = options.int("ci_mail_smtp_port"),
user = options.string("ci_mail_user"),
password = options.string("ci_mail_password"))
}
/** ci build jobs **/
/* hosts */
sealed trait Hosts {
def hosts_spec: String
def max_jobs: Option[Int]
def prefs: List[Options.Spec]
def numa_shuffling: Boolean
def build_cluster: Boolean
}
case class Local(host_spec: String, jobs: Int, threads: Int, numa_shuffling: Boolean = true)
extends Hosts {
def hosts_spec: String = host_spec
def max_jobs: Option[Int] = Some(jobs)
def prefs: List[Options.Spec] = List(Options.Spec.eq("threads", threads.toString))
def build_cluster: Boolean = false
}
case class Cluster(hosts_spec: String, numa_shuffling: Boolean = true) extends Hosts {
def max_jobs: Option[Int] = None
def prefs: List[Options.Spec] = Nil
def build_cluster: Boolean = true
}
/* build triggers */
sealed trait Trigger
case object On_Commit extends Trigger
object Timed {
def nightly(start_time: Time = Time.zero): Timed =
Timed { (before, now) =>
val start0 = before.midnight + start_time
val start1 = now.midnight + start_time
(before.time < start0.time && start0.time <= now.time) ||
(before.time < start1.time && start1.time <= now.time)
}
}
case class Timed(in_interval: (Date, Date) => Boolean) extends Trigger
/* build hooks */
trait Hook {
def pre(options: Options, progress: Progress): Unit = ()
def post(
options: Options,
url: Option[Url],
results: Build.Results,
progress: Progress
): Unit = ()
}
object none extends Hook
/* jobs */
sealed case class Job(
name: String,
description: String,
hosts: Hosts,
timeout: Time,
afp: Boolean = false,
selection: Sessions.Selection = Sessions.Selection.empty,
presentation: Boolean = false,
clean_build: Boolean = false,
select_dirs: List[Path] = Nil,
build_prefs: List[Options.Spec] = Nil,
hook: Hook = none,
extra_components: List[String] = Nil,
other_settings: List[String] = Nil,
trigger: Trigger = On_Commit,
verbose: Boolean = false
) {
override def toString: String = name
def afp_root: Option[Path] = if (!afp) None else Some(AFP.BASE)
def prefs: List[Options.Spec] = build_prefs ++ hosts.prefs ++ document_prefs
def document_prefs: List[Options.Spec] =
if (!presentation) Nil
else List(
Options.Spec.eq("browser_info", "true"),
Options.Spec.eq("document", "pdf"),
Options.Spec.eq("document_variants", "document:outline=/proof,/ML"))
def components: List[String] = (if (!afp) Nil else List("AFP")) ::: extra_components
}
private lazy val known_jobs: List[Job] =
Isabelle_System.make_services(classOf[Isabelle_CI_Jobs]).flatMap(_.jobs)
def show_jobs: String =
cat_lines(known_jobs.sortBy(_.name).map(job => job.name + " - " + job.description))
def the_job(name: String): Job = known_jobs.find(job => job.name == name) getOrElse
error("Unknown job " + quote(name))
/* concrete jobs */
val timing =
Job("benchmark",
description = "runs benchmark and timing sessions",
Local("benchmark", jobs = 1, threads = 6, numa_shuffling = false),
Time.hms(2, 0, 0),
selection = Sessions.Selection(session_groups = List("timing")),
clean_build = true,
select_dirs = List(Path.explode("~~/src/Benchmarks")),
trigger = Timed.nightly())
/* build ci */
def build_ci(
options: Options,
job: Job,
build_hosts: List[Build_Cluster.Host] = Nil,
url: Option[Url] = None,
progress: Progress = new Progress
): Unit = {
def return_code(f: => Unit): Int =
Exn.capture(f) match {
case Exn.Res(_) => Process_Result.RC.ok
case Exn.Exn(e) =>
progress.echo_error_message(e.getMessage)
Process_Result.RC.error
}
val mail_result =
return_code {
Mail_System.try_open(options).getOrElse(error("No mail configuration")).server.check()
}
val pre_result = return_code { job.hook.pre(options, progress) }
progress.echo(section("BUILD"))
val results = progress.interrupt_handler {
Build.build(
options ++ job.prefs,
build_hosts = build_hosts,
selection = job.selection,
progress = progress,
clean_build = job.clean_build,
afp_root = job.afp_root,
select_dirs = job.select_dirs,
numa_shuffling = job.hosts.numa_shuffling,
max_jobs = job.hosts.max_jobs)
}
val stop_date = progress.now()
val elapsed_time = stop_date - progress.start
progress.echo("\nFinished at " + Build_Log.print_date(stop_date))
progress.echo(section("TIMING"))
val total_timing =
results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _).
copy(elapsed = elapsed_time)
progress.echo(total_timing.message_resources)
val post_result = return_code { job.hook.post(options, url, results, progress) }
val rc = List(mail_result, pre_result, results.rc, post_result).max
if (rc != Process_Result.RC.ok) {
progress.echo(section("FAILED"))
if (mail_result != Process_Result.RC.ok) progress.echo("Mail: FAILED")
else {
val mail_system = Mail_System.try_open(options).get
val content =
"The job " + job.name + " failed. " + if_proper(url, " View the build at: " + url.get)
val mail = Mail("Build failed", List(mail_system.to), content, Some(mail_system.from))
mail_system.server.send(mail)
}
if (pre_result != Process_Result.RC.ok) progress.echo("Pre-hook: FAILED")
for (name <- results.sessions) {
if (results.cancelled(name)) progress.echo("Session " + name + ": CANCELLED")
else {
val result = results(name)
if (!result.ok) progress.echo("Session " + name + ": FAILED " + result.rc)
}
}
if (post_result != Process_Result.RC.ok) progress.echo("Post-hook: FAILED")
}
sys.exit(rc)
}
/* Isabelle tool wrapper */
val isabelle_tool = Isabelle_Tool("build_ci", "builds Isabelle jobs in ci environments",
Scala_Project.here,
{ args =>
var options = Options.init()
val build_hosts = new mutable.ListBuffer[Build_Cluster.Host]
var url: Option[Url] = None
val getopts = Getopts("""
Usage: isabelle build_ci [OPTIONS] JOB
Options are:
-H HOSTS host specifications of the form NAMES:PARAMETERS (separated by commas)
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-u URL build url
Runs Isabelle builds in ci environment. For cluster builds, build hosts must
be passed explicitly (no registry).
The following build jobs are available:
""" + Library.indent_lines(4, show_jobs) + "\n",
"H:" -> (arg => build_hosts ++= Build_Cluster.Host.parse(Registry.load(Nil), arg)),
"o:" -> (arg => options = options + arg),
"u:" -> (arg => url = Some(Url(arg))))
val more_args = getopts(args)
val job =
more_args match {
case job :: Nil => the_job(job)
case _ => getopts.usage()
}
val progress = new Console_Progress(verbose = job.verbose)
build_ci(options, job, url = url, build_hosts = build_hosts.toList, progress = progress)
})
}
class Isabelle_CI_Jobs(val jobs: Build_CI.Job*) extends Isabelle_System.Service
class CI_Jobs extends Isabelle_CI_Jobs(Build_CI.timing)