diff --git a/admin/jenkins/ci_build_afp.scala b/admin/jenkins/ci_build_afp.scala
--- a/admin/jenkins/ci_build_afp.scala
+++ b/admin/jenkins/ci_build_afp.scala
@@ -1,46 +1,43 @@
-object profile extends isabelle.CI_Profile
-{
+object profile extends isabelle.CI_Profile {
import isabelle._
import java.io.FileReader
import scala.sys.process._
import org.apache.commons.configuration2._
override def clean = false
val afp = Path.explode("$ISABELLE_HOME/afp")
val afp_thys = afp + Path.explode("thys")
val afp_id = hg_id(afp)
val status_file = Path.explode("$ISABELLE_HOME/status.json").file
val deps_file = Path.explode("$ISABELLE_HOME/dependencies.json").file
def can_send_mails = System.getProperties().containsKey("mail.smtp.host")
def include = List(afp_thys)
def select = Nil
- def pre_hook(args: List[String]) =
- {
+ def pre_hook(args: List[String]) = {
println(s"AFP id $afp_id")
if (status_file.exists())
status_file.delete()
Result.ok
}
- def post_hook(results: Build.Results) =
- {
+ def post_hook(results: Build.Results) = {
print_section("DEPENDENCIES")
println("Generating dependencies file ...")
val result = Isabelle_System.bash("isabelle afp_dependencies")
result.check
println("Writing dependencies file ...")
File.write(deps_file, result.out)
print_section("COMPLETED")
Result.ok
}
def selection =
Sessions.Selection(
session_groups = List("AFP"),
exclude_session_groups = List("slow"))
}
diff --git a/admin/jenkins/ci_build_all.scala b/admin/jenkins/ci_build_all.scala
--- a/admin/jenkins/ci_build_all.scala
+++ b/admin/jenkins/ci_build_all.scala
@@ -1,275 +1,262 @@
-object profile extends isabelle.CI_Profile
-{
+object profile extends isabelle.CI_Profile {
import isabelle._
import java.io.FileReader
import scala.sys.process._
import org.apache.commons.configuration2._
override def clean = false
val afp = Path.explode("$AFP_BASE")
val afp_thys = afp + Path.explode("thys")
val afp_id = hg_id(afp)
- sealed abstract class Status(val str: String)
- {
+ sealed abstract class Status(val str: String) {
def merge(that: Status): Status = (this, that) match {
case (Ok, s) => s
case (Failed, s) => Failed
case (Skipped, Failed) => Failed
case (Skipped, s) => Skipped
}
}
- object Status
- {
+ object Status {
def merge(statuses: List[Status]): Status =
statuses.foldLeft(Ok: Status)(_ merge _)
def from_results(results: Build.Results, session: String): Status =
if (results.cancelled(session))
Skipped
else if (results(session).ok)
Ok
else
Failed
}
case object Ok extends Status("ok")
case object Skipped extends Status("skipped")
case object Failed extends Status("failed")
case class Mail(subject: String, recipients: List[String], text: String) {
import java.util._
import javax.mail._
import javax.mail.internet._
import javax.activation._
def send(): Unit = {
val user = System.getProperty("mail.smtp.user")
val sender = System.getProperty("mail.smtp.from")
val password = System.getProperty("mail.smtp.password")
System.setProperty("mail.smtp.ssl.protocols", "TLSv1.2")
val authenticator = new Authenticator() {
override def getPasswordAuthentication() =
new PasswordAuthentication(user, password)
}
val session = Session.getDefaultInstance(System.getProperties(), authenticator)
val message = new MimeMessage(session)
message.setFrom(new InternetAddress("ci@isabelle.systems", "Isabelle/Jenkins"))
message.setSender(new InternetAddress(sender))
message.setSubject(subject)
message.setText(text, "UTF-8")
message.setSentDate(new java.util.Date())
recipients.foreach { recipient =>
message.addRecipient(Message.RecipientType.TO, new InternetAddress(recipient))
}
try {
Transport.send(message)
}
catch {
case ex: MessagingException => println(s"Sending mail failed: ${ex.getMessage}")
}
}
}
- class Metadata(ini: INIConfiguration)
- {
+ class Metadata(ini: INIConfiguration) {
- def maintainers(entry: String): List[String] =
- {
+ def maintainers(entry: String): List[String] = {
val config = ini.getSection(entry)
val raw =
if (config.containsKey("notify"))
config.getString("notify")
else
""
List(raw.split(','): _*).map(_.trim).filterNot(_.isEmpty)
}
- def entry_of_session(info: Sessions.Info): Option[String] =
- {
+ def entry_of_session(info: Sessions.Info): Option[String] = {
val afp_path = afp_thys.canonical_file.toPath
val session_path = info.dir.canonical_file.toPath
if (session_path.startsWith(afp_path))
Some(afp_path.relativize(session_path).getName(0).toFile.getName)
else
None
}
def notify(name: String, result: Process_Result, info: Sessions.Info): Unit =
entry_of_session(info).foreach { entry =>
val mails = maintainers(entry)
val text =
s"""|The build for the session
| $name,
|belonging to the AFP entry
| $entry
|failed.
|
|You are receiving this mail because you are the maintainer of that AFP
|entry.
|
|The following information might help you with resolving the problem.
|
|Build log: ${Isabelle_System.getenv("BUILD_URL")}
|Isabelle ID: $isabelle_id
|AFP ID: $afp_id
|Timeout? ${result.timeout}
|Exit code: ${result.rc}
|
|Last 50 lines from stdout (if available):
|
|${result.out_lines.takeRight(50).mkString("\n")}
|
|Last 50 lines from stderr (if available):
|
|${result.err_lines.takeRight(50).mkString("\n")}
|""".stripMargin
val subject = s"Build of AFP entry $entry failed"
if (mails.isEmpty)
println(s"Entry $entry: WARNING no maintainers specified")
else
Mail(text = text, subject = subject, recipients = mails).send()
}
def group_by_entry(results: Build.Results): Map[Option[String], List[String]] =
results.sessions.toList.map { name =>
entry_of_session(results.info(name)) -> name
}.groupBy(_._1).view.mapValues(_.map(_._2)).toMap
- def status_as_json(status: Map[Option[String], Status]): String =
- {
+ def status_as_json(status: Map[Option[String], Status]): String = {
val entries_strings = status.collect {
case (Some(entry), status) =>
s"""{"entry": "$entry", "status": "${status.str}"}"""
}
val entries_string = entries_strings.mkString("[", ",\n", "]")
s"""
{"build_data":
{"isabelle_id": "$isabelle_id",
"afp_id": "$afp_id",
"time": "$start_time",
"url": "${Isabelle_System.getenv("BUILD_URL")}",
"job": "${Isabelle_System.getenv("JOB_NAME")}"
},
"entries":
$entries_string
}
"""
}
- def status_as_html(status: Map[Option[String], Status]): String =
- {
+ def status_as_html(status: Map[Option[String], Status]): String = {
val entries_strings = status.collect {
case (None, Failed) =>
s"
Distribution"
case (Some(entry), Failed) =>
s"""$entry"""
}
if (entries_strings.isEmpty)
""
else
entries_strings.mkString("Failed entries: ")
}
}
val status_file = Path.explode("$ISABELLE_HOME/status.json").file
val report_file = Path.explode("$ISABELLE_HOME/report.html").file
val deps_file = Path.explode("$ISABELLE_HOME/dependencies.json").file
def can_send_mails = System.getProperties().containsKey("mail.smtp.host")
def include = List(afp_thys)
def select = Nil
- def pre_hook(args: List[String]) =
- {
+ def pre_hook(args: List[String]) = {
println(s"AFP id $afp_id")
if (status_file.exists())
status_file.delete()
if (report_file.exists())
report_file.delete()
File.write(report_file, "")
if (!can_send_mails) {
println(s"Mail configuration not found.")
Result.error
} else {
Result.ok
}
}
- def post_hook(results: Build.Results) =
- {
+ def post_hook(results: Build.Results) = {
print_section("DEPENDENCIES")
println("Generating dependencies file ...")
val result = Isabelle_System.bash("isabelle afp_dependencies")
result.check
println("Writing dependencies file ...")
File.write(deps_file, result.out)
val metadata = {
val path = afp + Path.explode("metadata/metadata")
val ini = new INIConfiguration()
if (path.is_file) {
val reader = new FileReader(path.file)
ini.read(reader)
reader.close()
}
new Metadata(ini)
}
val status =
metadata.group_by_entry(results).view.mapValues { sessions =>
Status.merge(sessions.map(Status.from_results(results, _)))
}.toMap
print_section("REPORT")
println("Writing report file ...")
File.write(report_file, metadata.status_as_html(status))
print_section("SITEGEN")
println("Writing status file ...")
File.write(status_file, metadata.status_as_json(status))
println("Running sitegen ...")
val script = afp + Path.explode("admin/sitegen-devel")
val sitegen_rc = List(script.file.toString, status_file.toString, deps_file.toString).!
- if (sitegen_rc > 0)
- {
+ if (sitegen_rc > 0) {
println("sitegen failed")
}
- if (!results.ok)
- {
+ if (!results.ok) {
print_section("NOTIFICATIONS")
- for (name <- results.sessions)
- {
+ for (name <- results.sessions) {
val result = results(name)
if (!result.ok && !results.cancelled(name) && can_send_mails)
metadata.notify(name, result, results.info(name))
}
}
print_section("COMPLETED")
Result(sitegen_rc)
}
def selection =
Sessions.Selection(
all_sessions = true,
exclude_session_groups = List("slow"))
}
diff --git a/admin/jenkins/ci_build_mac.scala b/admin/jenkins/ci_build_mac.scala
--- a/admin/jenkins/ci_build_mac.scala
+++ b/admin/jenkins/ci_build_mac.scala
@@ -1,27 +1,25 @@
-object profile extends isabelle.CI_Profile
-{
+object profile extends isabelle.CI_Profile {
import isabelle._
val afp = Path.explode("$ISABELLE_HOME/afp")
val afp_thys = afp + Path.explode("thys")
override def threads = 8
override def jobs = 1
def include = List(afp_thys)
def select = Nil
- def pre_hook(args: List[String]) =
- {
+ def pre_hook(args: List[String]) = {
println(s"Build for AFP id ${hg_id(afp)}")
Result.ok
}
def post_hook(results: Build.Results) = Result.ok
def selection = Sessions.Selection(
all_sessions = true,
exclude_sessions = List("HOL-Proofs", "HOL-ODE-Numerics", "Linear_Programming", "HOL-Nominal-Examples", "HOL-Analysis"),
exclude_session_groups = List("slow"))
}
diff --git a/admin/jenkins/ci_build_slow.scala b/admin/jenkins/ci_build_slow.scala
--- a/admin/jenkins/ci_build_slow.scala
+++ b/admin/jenkins/ci_build_slow.scala
@@ -1,24 +1,21 @@
-object profile extends isabelle.CI_Profile
-{
+object profile extends isabelle.CI_Profile {
import isabelle._
val afp = Path.explode("$ISABELLE_HOME/afp")
val afp_thys = afp + Path.explode("thys")
override def threads = 8
override def jobs = 1
def include = List(afp_thys)
def select = Nil
- def pre_hook(args: List[String]) =
- {
+ def pre_hook(args: List[String]) = {
println(s"Build for AFP id ${hg_id(afp)}")
Result.ok
}
def post_hook(results: Build.Results) = Result.ok
def selection = Sessions.Selection(session_groups = List("slow"))
-
}
diff --git a/admin/jenkins/ci_build_testboard.scala b/admin/jenkins/ci_build_testboard.scala
--- a/admin/jenkins/ci_build_testboard.scala
+++ b/admin/jenkins/ci_build_testboard.scala
@@ -1,121 +1,113 @@
-object profile extends isabelle.CI_Profile
-{
+object profile extends isabelle.CI_Profile {
import isabelle._
import java.io.FileReader
import scala.sys.process._
import org.apache.commons.configuration2._
override def clean = false
val afp = Path.explode("$AFP_BASE")
val afp_thys = afp + Path.explode("thys")
val afp_id = hg_id(afp)
- sealed abstract class Status(val str: String)
- {
+ sealed abstract class Status(val str: String) {
def merge(that: Status): Status = (this, that) match {
case (Ok, s) => s
case (Failed, s) => Failed
case (Skipped, Failed) => Failed
case (Skipped, s) => Skipped
}
}
- object Status
- {
+ object Status {
def merge(statuses: List[Status]): Status =
statuses.foldLeft(Ok: Status)(_ merge _)
def from_results(results: Build.Results, session: String): Status =
if (results.cancelled(session))
Skipped
else if (results(session).ok)
Ok
else
Failed
}
case object Ok extends Status("ok")
case object Skipped extends Status("skipped")
case object Failed extends Status("failed")
- class Metadata(ini: INIConfiguration)
- {
+ class Metadata(ini: INIConfiguration) {
- def entry_of_session(info: Sessions.Info): Option[String] =
- {
+ def entry_of_session(info: Sessions.Info): Option[String] = {
val afp_path = afp_thys.canonical_file.toPath
val session_path = info.dir.canonical_file.toPath
if (session_path.startsWith(afp_path))
Some(afp_path.relativize(session_path).getName(0).toFile.getName)
else
None
}
def group_by_entry(results: Build.Results): Map[Option[String], List[String]] =
results.sessions.toList.map { name =>
entry_of_session(results.info(name)) -> name
}.groupBy(_._1).view.mapValues(_.map(_._2)).toMap
- def status_as_html(status: Map[Option[String], Status]): String =
- {
+ def status_as_html(status: Map[Option[String], Status]): String = {
val entries_strings = status.collect {
case (None, Failed) =>
s"Distribution"
case (Some(entry), Failed) =>
s"""$entry"""
}
if (entries_strings.isEmpty)
""
else
entries_strings.mkString("Failed entries: ")
}
}
val report_file = Path.explode("$ISABELLE_HOME/report.html").file
def include = List(afp_thys)
def select = Nil
- def pre_hook(args: List[String]) =
- {
+ def pre_hook(args: List[String]) = {
println(s"AFP id $afp_id")
if (report_file.exists())
report_file.delete()
File.write(report_file, "")
Result.ok
}
- def post_hook(results: Build.Results) =
- {
+ def post_hook(results: Build.Results) = {
val metadata = {
val path = afp + Path.explode("metadata/metadata")
val ini = new INIConfiguration()
if (path.is_file) {
val reader = new FileReader(path.file)
ini.read(reader)
reader.close()
}
new Metadata(ini)
}
val status =
metadata.group_by_entry(results).view.mapValues { sessions =>
Status.merge(sessions.map(Status.from_results(results, _)))
}.toMap
print_section("REPORT")
println("Writing report file ...")
File.write(report_file, metadata.status_as_html(status))
print_section("COMPLETED")
Result.ok
}
def selection =
Sessions.Selection(
all_sessions = true,
exclude_session_groups = List("slow"))
}
diff --git a/tools/afp_check_roots.scala b/tools/afp_check_roots.scala
--- a/tools/afp_check_roots.scala
+++ b/tools/afp_check_roots.scala
@@ -1,171 +1,164 @@
package afp
import isabelle._
-object AFP_Check_Roots
-{
+object AFP_Check_Roots {
def print_good(string: String): Unit =
println(Console.BOLD + Console.GREEN + string + Console.RESET)
def print_bad(string: String): Unit =
println(Console.BOLD + Console.RED + string + Console.RESET)
class Check[T](
run: (Sessions.Structure, List[String]) => List[T],
failure_msg: String,
- failure_format: T => String)
- {
+ failure_format: T => String
+ ) {
def apply(tree: Sessions.Structure, selected: List[String]): Boolean =
run(tree, selected) match {
case Nil =>
true
case offenders =>
print_bad(failure_msg)
offenders.foreach(offender => println(" " + failure_format(offender)))
false
}
}
def afp_checks(afp_dir: Path, excludes: List[String]): List[Check[_]] =
{
val check_timeout = new Check[(String, List[String])](
run = { (tree, selected) =>
selected.flatMap { name =>
val info = tree(name)
val entry = info.dir.base.implode
val timeout = info.options.real("timeout")
if (timeout == 0 || timeout % 300 != 0)
Some((entry, name))
else
None
}.groupBy(_._1).view.mapValues(_.map(_._2)).toList
},
failure_msg = "The following entries contain sessions without timeouts or with timeouts not divisible by 300:",
failure_format = {
case (entry, sessions) => s"""$entry ${sessions.mkString("(", ", ", ")")}"""
}
)
val check_paths = new Check[(String, Path)](
run = { (tree, selected) =>
selected.flatMap { name =>
val info = tree(name)
val dir = info.dir
if (dir.dir.expand.file != afp_dir.file)
Some((name, dir))
else
None
}
},
failure_msg = "The following sessions are in the wrong directory:",
failure_format = {
case (session, dir) => s"""$session ($dir)"""
}
)
val check_chapter = new Check[String](
run = { (tree, selected) =>
selected.flatMap { name =>
val info = tree(name)
val entry = info.dir.base.implode
if (info.chapter != "AFP")
Some(entry)
else
None
}.distinct
},
failure_msg = "The following entries are not in the AFP chapter:",
failure_format = identity
)
val check_groups = new Check[(String, List[String])](
run = { (tree, selected) =>
selected.flatMap { name =>
val info = tree(name)
if (!info.groups.toSet.subsetOf(AFP.groups.keySet + "AFP") ||
!info.groups.contains("AFP"))
Some((name, info.groups))
else
None
}
},
failure_msg = "The following sessions have wrong groups:",
failure_format = {
case (session, groups) => s"""$session ${groups.mkString("{", ", ", "}")}"""
}
)
val check_presence = new Check[String](
run = { (tree, selected) =>
val fs_entries = File.read_dir(afp_dir).filterNot(excludes.contains)
fs_entries.flatMap { name =>
if (!selected.contains(name) || tree(name).dir.base.implode != name)
Some(name)
else
None
}
},
failure_msg = "The following entries (according to the file system) are not registered in ROOTS, or registered in the wrong ROOT:",
failure_format = identity
)
List(
check_timeout,
// check_paths,
check_chapter,
check_groups,
check_presence)
}
- def afp_check_roots(afp_dir: Path, excludes: List[String]): Unit =
- {
+ def afp_check_roots(afp_dir: Path, excludes: List[String]): Unit = {
val full_tree = Sessions.load_structure(Options.init(), Nil, List(afp_dir))
val selected = full_tree.build_selection(Sessions.Selection.empty)
val checks = afp_checks(afp_dir, excludes)
val bad = checks.exists(check => !check(full_tree, selected))
- if (bad)
- {
+ if (bad) {
print_bad("Errors found.")
System.exit(1)
}
- else
- {
+ else {
print_good(s"${selected.length} sessions have been checked")
print_good(s"${checks.length} checks have found no errors")
}
}
val isabelle_tool =
- Isabelle_Tool(
- "afp_check_roots",
- "check ROOT files of AFP sessions",
+ Isabelle_Tool("afp_check_roots", "check ROOT files of AFP sessions",
Scala_Project.here,
- args => {
+ { args =>
var excludes = List("ROOTS", "LICENSE", "LICENSE.LGPL", ".DS_Store", "etc")
- val getopts = Getopts(
- """
+ val getopts = Getopts("""
Usage: isabelle afp_check_roots [OPTIONS]
Options are:
-x NAME exclude directories with name
(default """ + excludes.map(quote).mkString(", ") + """)
Check ROOT files of AFP sessions.
""",
"x:" -> (arg => excludes ::= arg)
)
getopts(args)
val afp_dir = Path.explode("$AFP").expand
afp_check_roots(afp_dir, excludes)
}
)
}
diff --git a/tools/afp_dependencies.scala b/tools/afp_dependencies.scala
--- a/tools/afp_dependencies.scala
+++ b/tools/afp_dependencies.scala
@@ -1,95 +1,91 @@
/* Author: Fabian Huch, TU Muenchen
Tool to extract dependencies of AFP entries.
*/
package afp
import Metadata.Entry
import isabelle._
object AFP_Dependencies
{
case class Dependency(entry: Entry.Name, distrib_deps: List[Entry.Name], afp_deps: List[Entry.Name])
object JSON
{
private def from_dep(dependency: Dependency): (String, isabelle.JSON.T) =
dependency.entry ->
isabelle.JSON.Object(
"distrib_deps" -> dependency.distrib_deps,
"afp_deps" -> dependency.afp_deps
)
def from_dependency(dep: Dependency): isabelle.JSON.T =
isabelle.JSON.Object(from_dep(dep))
def from_dependencies(deps: List[Dependency]): isabelle.JSON.T =
deps.map(from_dep).toMap
}
def afp_dependencies(afp_dir: Path): List[Dependency] =
{
val tree = Sessions.load_structure(Options.init(), Nil, List(afp_dir))
val selected = tree.selection(Sessions.Selection(false, false, Nil, Nil, Nil, Nil))
.build_graph.keys
- def get_entry(name: String): Option[String] =
- {
- val info = tree(name)
- val dir = info.dir
+ def get_entry(name: String): Option[String] = {
+ val info = tree(name)
+ val dir = info.dir
if (selected.contains(dir.dir.expand))
None
else
Some(dir.base.implode)
}
selected.groupBy(get_entry).toList.map {
case (Some(e), sessions) =>
val dependencies = sessions.flatMap(tree.imports_graph.imm_preds)
.map(d => (d, get_entry(d)))
val distrib_deps = dependencies.collect { case (d, None) => d }.distinct
val afp_deps = dependencies.collect { case (_, Some(d)) if d != e => d }.distinct
Dependency(e, distrib_deps, afp_deps)
}
}
val isabelle_tool =
- Isabelle_Tool(
- "afp_dependencies",
- "extract dependencies between AFP entries",
+ Isabelle_Tool("afp_dependencies", "extract dependencies between AFP entries",
Scala_Project.here,
- args => {
+ { args =>
var output_file: Option[Path] = None
- val getopts = Getopts(
- """
+ val getopts = Getopts("""
Usage: isabelle afp_dependencies [OPTIONS]
Options are:
-o FILE output file name
Extract dependencies between AFP entries.
""",
"o:" -> (arg => output_file = Some(Path.explode(arg)))
)
getopts(args)
val afp_dir = Path.explode("$AFP").expand
val progress = new Console_Progress()
val res = afp_dependencies(afp_dir).map(JSON.from_dependency)
val json = isabelle.JSON.Format(res)
output_file match {
case Some(file) => File.write(file, json)
case None => progress.echo(json)
}
}
)
}