Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/Pure/Build/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 8 kB

Quelle build_ci.scala Sprache: Scala

/*  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.hms(0, 17, 0)): Timed = Timed(Date.Daily(start))
    def weekly(day: Date.Day = Date.Day.sun, start: Time = Time.hms(0, 17, 0)): Timed =
      Timed(Date.Weekly(day, Date.Daily(start)))
  }

  case class Timed(cycle: Date.Cycle) extends Trigger {
    def next(previous: Date, now: Date): Boolean = cycle.next(previous).time < cycle.next(now).time
  }

  /* 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)

quality96%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.