diff --git a/src/Pure/Admin/afp.scala b/src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala
+++ b/src/Pure/Admin/afp.scala
@@ -1,226 +1,224 @@
/* Title: Pure/Admin/afp.scala
Author: Makarius
Administrative support for the Archive of Formal Proofs.
*/
package isabelle
import java.time.LocalDate
import scala.collection.immutable.SortedMap
object AFP
{
- val repos_source = "https://isabelle.sketis.net/repos/afp-devel"
-
val groups: Map[String, String] =
Map("large" -> "full 64-bit memory model or word arithmetic required",
"slow" -> "CPU time much higher than 60min (on mid-range hardware)",
"very_slow" -> "elapsed time of many hours (on high-end hardware)")
val groups_bulky: List[String] = List("large", "slow")
val chapter: String = "AFP"
val force_partition1: List[String] = List("Category3", "HOL-ODE")
def init(options: Options, base_dir: Path = Path.explode("$AFP_BASE")): AFP =
new AFP(options, base_dir)
/* entries */
def parse_date(s: String): Date =
{
val t = Date.Formatter.pattern("uuuu-MM-dd").parse(s)
Date(LocalDate.from(t).atStartOfDay(Date.timezone_berlin))
}
def trim_mail(s: String): String = s.replaceAll("<[^>]*>", "").trim
sealed case class Entry(name: String, metadata: Properties.T, sessions: List[String])
{
def get(prop: String): Option[String] = Properties.get(metadata, prop)
def get_string(prop: String): String = get(prop).getOrElse("")
def get_strings(prop: String): List[String] =
space_explode(',', get_string(prop)).map(_.trim).filter(_.nonEmpty)
def title: String = get_string("title")
def authors: List[String] = get_strings("author")
def date: Date =
parse_date(get("date").getOrElse(error("Missing date for entry " + quote(name))))
def topics: List[String] = get_strings("topic")
def `abstract`: String = get_string("abstract").trim
def maintainers: List[String] = get_strings("notify")
def contributors: List[String] = get_strings("contributors")
def license: String = get("license").getOrElse("BSD")
def rdf_meta_data: Properties.T =
RDF.meta_data(
proper_string(title).map(Markup.META_TITLE -> _).toList :::
authors.map(Markup.META_CREATOR -> _) :::
contributors.map(Markup.META_CONTRIBUTOR -> _) :::
List(Markup.META_DATE -> RDF.date_format(date)) :::
List(Markup.META_LICENSE -> license) :::
proper_string(`abstract`).map(Markup.META_DESCRIPTION -> _).toList)
}
}
class AFP private(options: Options, val base_dir: Path)
{
override def toString: String = base_dir.expand.toString
val main_dir: Path = base_dir + Path.explode("thys")
/* metadata */
private val entry_metadata: Map[String, Properties.T] =
{
val metadata_file = base_dir + Path.explode("metadata/metadata")
var result = Map.empty[String, Properties.T]
var section = ""
var props = List.empty[Properties.Entry]
val Section = """^\[(\S+)\]\s*$""".r
val Property = """^(\S+)\s*=(.*)$""".r
val Extra_Line = """^\s+(.*)$""".r
val Blank_Line = """^\s*$""".r
def flush(): Unit =
{
if (section != "") result += (section -> props.reverse.filter(p => p._2.nonEmpty))
section = ""
props = Nil
}
for ((line, i) <- split_lines(File.read(metadata_file)).zipWithIndex)
{
def err(msg: String): Nothing =
error(msg + Position.here(Position.Line_File(i + 1, metadata_file.expand.implode)))
line match {
case Section(name) => flush(); section = name
case Property(a, b) =>
if (section == "") err("Property without a section")
props = (a -> b.trim) :: props
case Extra_Line(line) =>
props match {
case Nil => err("Extra line without a property")
case (a, b) :: rest => props = (a, b + "\n" + line.trim) :: rest
}
case Blank_Line() =>
case _ => err("Bad input")
}
}
flush()
result
}
/* entries */
val entries_map: SortedMap[String, AFP.Entry] =
{
val entries =
for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS)) yield {
val metadata =
entry_metadata.getOrElse(name, error("Entry without metadata: " + quote(name)))
val sessions =
Sessions.parse_root_entries(main_dir + Path.explode(name) + Sessions.ROOT).map(_.name)
AFP.Entry(name, metadata, sessions)
}
val entries_map =
entries.foldLeft(SortedMap.empty[String, AFP.Entry]) { case (m, e) => m + (e.name -> e) }
val extra_metadata =
(for ((name, _) <- entry_metadata.iterator if !entries_map.isDefinedAt(name)) yield name).
toList.sorted
if (extra_metadata.nonEmpty)
error("Meta data without entry: " + commas_quote(extra_metadata))
entries_map
}
val entries: List[AFP.Entry] = entries_map.toList.map(_._2)
/* sessions */
val sessions_map: SortedMap[String, AFP.Entry] =
entries.foldLeft(SortedMap.empty[String, AFP.Entry]) {
case (m1, e) => e.sessions.foldLeft(m1) { case (m2, s) => m2 + (s -> e) }
}
val sessions: List[String] = entries.flatMap(_.sessions)
val sessions_structure: Sessions.Structure =
Sessions.load_structure(options, dirs = List(main_dir)).
selection(Sessions.Selection(sessions = sessions.toList))
/* dependency graph */
private def sessions_deps(entry: AFP.Entry): List[String] =
entry.sessions.flatMap(sessions_structure.imports_graph.imm_preds).distinct.sorted
lazy val entries_graph: Graph[String, Unit] =
{
val session_entries =
entries.foldLeft(Map.empty[String, String]) {
case (m1, e) => e.sessions.foldLeft(m1) { case (m2, s) => m2 + (s -> e.name) }
}
entries.foldLeft(Graph.empty[String, Unit]) {
case (g, entry) =>
val e1 = entry.name
sessions_deps(entry).foldLeft(g.default_node(e1, ())) {
case (g1, s) =>
session_entries.get(s).filterNot(_ == e1).foldLeft(g1) {
case (g2, e2) =>
try { g2.default_node(e2, ()).add_edge_acyclic(e2, e1) }
catch {
case exn: Graph.Cycles[_] =>
error(cat_lines(exn.cycles.map(cycle =>
"Cyclic dependency of " + cycle.map(c => quote(c.toString)).mkString(" via ") +
" due to session " + quote(s))))
}
}
}
}
}
def entries_graph_display: Graph_Display.Graph =
Graph_Display.make_graph(entries_graph)
def entries_json_text: String =
(for (entry <- entries.iterator) yield {
val distrib_deps = sessions_deps(entry).filterNot(sessions.contains(_))
val afp_deps = entries_graph.imm_preds(entry.name).toList
"""
{""" + JSON.Format(entry.name) + """:
{"distrib_deps": """ + JSON.Format(distrib_deps) + """,
"afp_deps": """ + JSON.Format(afp_deps) + """
}
}"""
}).mkString("[", ", ", "\n]\n")
/* partition sessions */
def partition(n: Int): List[String] =
n match {
case 0 => Nil
case 1 | 2 =>
val graph = sessions_structure.build_graph.restrict(sessions.toSet)
val force_part1 =
graph.all_preds(graph.all_succs(AFP.force_partition1.filter(graph.defined))).toSet
val (part1, part2) = graph.keys.partition(a => force_part1(a) || graph.is_isolated(a))
if (n == 1) part1 else part2
case _ => error("Bad AFP partition: " + n + " (should be 0, 1, 2)")
}
}
diff --git a/src/Pure/Admin/build_history.scala b/src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala
+++ b/src/Pure/Admin/build_history.scala
@@ -1,618 +1,618 @@
/* Title: Pure/Admin/build_history.scala
Author: Makarius
Build other history versions.
*/
package isabelle
object Build_History
{
/* log files */
val engine = "build_history"
val log_prefix = engine + "_"
/* augment settings */
def augment_settings(
other_isabelle: Other_Isabelle,
threads: Int,
arch_64: Boolean,
heap: Int,
max_heap: Option[Int],
more_settings: List[String]): String =
{
val (ml_platform, ml_settings) =
{
val windows_32 = "x86-windows"
val windows_64 = "x86_64-windows"
val windows_64_32 = "x86_64_32-windows"
val platform_32 = other_isabelle.getenv("ISABELLE_PLATFORM32")
val platform_64 = other_isabelle.getenv("ISABELLE_PLATFORM64")
val platform_64_32 = platform_64.replace("x86_64-", "x86_64_32-")
val polyml_home =
try { Path.explode(other_isabelle.getenv("ML_HOME")).dir }
catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) }
def ml_home(platform: String): Path = polyml_home + Path.explode(platform)
def err(platform: String): Nothing =
error("Platform " + platform + " unavailable on this machine")
def check_dir(platform: String): Boolean =
platform != "" && ml_home(platform).is_dir
val ml_platform =
if (Platform.is_windows && arch_64) {
if (check_dir(windows_64)) windows_64 else err(windows_64)
}
else if (Platform.is_windows && !arch_64) {
if (check_dir(windows_64_32)) windows_64_32
else if (check_dir(windows_32)) windows_32
else platform_32 // x86-cygwin
}
else if (arch_64) {
if (check_dir(platform_64)) platform_64 else err(platform_64)
}
else if (check_dir(platform_64_32)) platform_64_32
else platform_32
val ml_options =
"--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") +
" --gcthreads " + threads +
(if (ml_platform.endsWith("-windows")) " --codepage utf8" else "")
(ml_platform,
List(
"ML_HOME=" + File.bash_path(ml_home(ml_platform)),
"ML_PLATFORM=" + quote(ml_platform),
"ML_OPTIONS=" + quote(ml_options)))
}
val thread_settings =
List(
"ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"",
"ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"")
val settings =
List(ml_settings, thread_settings) :::
(if (more_settings.isEmpty) Nil else List(more_settings))
File.append(other_isabelle.etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_))))
ml_platform
}
/** build_history **/
private val default_user_home = Path.USER_HOME
private val default_rev = "tip"
private val default_multicore = (1, 1)
private val default_heap = 1500
private val default_isabelle_identifier = "build_history"
def build_history(
options: Options,
root: Path,
user_home: Path = default_user_home,
progress: Progress = new Progress,
rev: String = default_rev,
afp_rev: Option[String] = None,
afp_partition: Int = 0,
isabelle_identifier: String = default_isabelle_identifier,
ml_statistics_step: Int = 1,
component_repository: String = Components.default_component_repository,
components_base: Path = Components.default_components_base,
fresh: Boolean = false,
hostname: String = "",
multicore_base: Boolean = false,
multicore_list: List[(Int, Int)] = List(default_multicore),
arch_64: Boolean = false,
heap: Int = default_heap,
max_heap: Option[Int] = None,
init_settings: List[String] = Nil,
more_settings: List[String] = Nil,
more_preferences: List[String] = Nil,
verbose: Boolean = false,
build_tags: List[String] = Nil,
build_args: List[String] = Nil): List[(Process_Result, Path)] =
{
/* sanity checks */
if (File.eq(Path.ISABELLE_HOME, root))
error("Repository coincides with ISABELLE_HOME=" + Path.ISABELLE_HOME.expand)
for ((threads, _) <- multicore_list if threads < 1)
error("Bad threads value < 1: " + threads)
for ((_, processes) <- multicore_list if processes < 1)
error("Bad processes value < 1: " + processes)
if (heap < 100) error("Bad heap value < 100: " + heap)
if (max_heap.isDefined && max_heap.get < heap)
error("Bad max_heap value < heap: " + max_heap.get)
System.getenv("ISABELLE_SETTINGS_PRESENT") match {
case null | "" =>
case _ => error("Cannot run build_history within existing Isabelle settings environment")
}
/* checkout Isabelle + AFP repository */
def checkout(dir: Path, version: String): String =
{
val hg = Mercurial.repository(dir)
hg.update(rev = version, clean = true)
progress.echo_if(verbose, hg.log(version, options = "-l1"))
hg.id(rev = version)
}
val isabelle_version = checkout(root, rev)
val afp_repos = root + Path.explode("AFP")
val afp_version = afp_rev.map(checkout(afp_repos, _))
val (afp_build_args, afp_sessions) =
if (afp_rev.isEmpty) (Nil, Nil)
else {
val (opt, sessions) =
try {
val afp = AFP.init(options, afp_repos)
("-d", afp.partition(afp_partition))
} catch { case ERROR(_) => ("-D", Nil) }
(List(opt, "~~/AFP/thys"), sessions)
}
/* main */
val other_isabelle =
Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
user_home = user_home, progress = progress)
val build_host = proper_string(hostname) getOrElse Isabelle_System.hostname()
val build_history_date = Date.now()
val build_group_id = build_host + ":" + build_history_date.time.ms
var first_build = true
for ((threads, processes) <- multicore_list) yield
{
/* init settings */
val component_settings =
other_isabelle.init_components(
component_repository = component_repository,
components_base = components_base,
catalogs = List("main", "optional"))
other_isabelle.init_settings(component_settings ::: init_settings)
other_isabelle.resolve_components(echo = verbose)
val ml_platform =
augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings)
File.write(other_isabelle.etc_preferences, cat_lines(more_preferences))
val isabelle_output =
other_isabelle.isabelle_home_user + Path.explode("heaps") +
Path.explode(other_isabelle.getenv("ML_IDENTIFIER"))
val isabelle_output_log = isabelle_output + Path.explode("log")
val isabelle_base_log = isabelle_output + Path.explode("../base_log")
if (first_build) {
other_isabelle.resolve_components(echo = verbose)
if (fresh)
Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode("lib/classes"))
other_isabelle.bash(
"env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " +
"bin/isabelle jedit -b", redirect = true, echo = verbose).check
for {
tool <- List("ghc_setup", "ocaml_setup")
if other_isabelle.getenv("ISABELLE_" + Word.uppercase(tool)) == "true" &&
(other_isabelle.isabelle_home + Path.explode("lib/Tools/" + tool)).is_file
} other_isabelle(tool, echo = verbose)
Isabelle_System.rm_tree(isabelle_base_log)
}
Isabelle_System.rm_tree(isabelle_output)
Isabelle_System.make_directory(isabelle_output)
val log_path =
other_isabelle.isabelle_home_user +
Build_Log.log_subdir(build_history_date) +
Build_Log.log_filename(Build_History.engine, build_history_date,
List(build_host, ml_platform, "M" + threads) ::: build_tags)
Isabelle_System.make_directory(log_path.dir)
val build_out = other_isabelle.isabelle_home_user + Path.explode("log/build.out")
val build_out_progress = new File_Progress(build_out)
build_out.file.delete
/* build */
if (multicore_base && !first_build && isabelle_base_log.is_dir)
Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log)
val build_start = Date.now()
val build_args1 = List("-v", "-j" + processes) ::: afp_build_args ::: build_args
val build_isabelle =
Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
user_home = user_home, progress = build_out_progress)
val build_result =
build_isabelle("build " + Bash.strings(build_args1 ::: afp_sessions),
redirect = true, echo = true, strict = false)
val build_end = Date.now()
val build_info: Build_Log.Build_Info =
Build_Log.Log_File(log_path.file_name, build_result.out_lines).
parse_build_info(ml_statistics = true)
/* output log */
val store = Sessions.store(options + "build_database_server=false")
val meta_info =
Properties.lines_nonempty(Build_Log.Prop.build_tags.name, build_tags) :::
Properties.lines_nonempty(Build_Log.Prop.build_args.name, build_args1) :::
List(
Build_Log.Prop.build_group_id.name -> build_group_id,
Build_Log.Prop.build_id.name -> (build_host + ":" + build_start.time.ms),
Build_Log.Prop.build_engine.name -> Build_History.engine,
Build_Log.Prop.build_host.name -> build_host,
Build_Log.Prop.build_start.name -> Build_Log.print_date(build_start),
Build_Log.Prop.build_end.name -> Build_Log.print_date(build_end),
Build_Log.Prop.isabelle_version.name -> isabelle_version) :::
afp_version.map(Build_Log.Prop.afp_version.name -> _).toList
build_out_progress.echo("Reading session build info ...")
val session_build_info =
build_info.finished_sessions.flatMap(session_name =>
{
val database = isabelle_output + store.database(session_name)
if (database.is_file) {
using(SQLite.open_database(database))(db =>
{
val theory_timings =
try {
store.read_theory_timings(db, session_name).map(ps =>
Protocol.Theory_Timing_Marker((Build_Log.SESSION_NAME, session_name) :: ps))
}
catch { case ERROR(_) => Nil }
val session_sources =
store.read_build(db, session_name).map(_.sources) match {
case Some(sources) if sources.length == SHA1.digest_length =>
List("Sources " + session_name + " " + sources)
case _ => Nil
}
theory_timings ::: session_sources
})
}
else Nil
})
build_out_progress.echo("Reading ML statistics ...")
val ml_statistics =
build_info.finished_sessions.flatMap(session_name =>
{
val database = isabelle_output + store.database(session_name)
val log_gz = isabelle_output + store.log_gz(session_name)
val properties =
if (database.is_file) {
using(SQLite.open_database(database))(db =>
store.read_ml_statistics(db, session_name))
}
else if (log_gz.is_file) {
Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics
}
else Nil
val trimmed_properties =
if (ml_statistics_step <= 0) Nil
else if (ml_statistics_step == 1) properties
else {
(for { (ps, i) <- properties.iterator.zipWithIndex if i % ml_statistics_step == 0 }
yield ps).toList
}
trimmed_properties.map(ps => (Build_Log.SESSION_NAME -> session_name) :: ps)
})
build_out_progress.echo("Reading error messages ...")
val session_errors =
build_info.failed_sessions.flatMap(session_name =>
{
val database = isabelle_output + store.database(session_name)
val errors =
if (database.is_file) {
try {
using(SQLite.open_database(database))(db => store.read_errors(db, session_name))
} // column "errors" could be missing
catch { case _: java.sql.SQLException => Nil }
}
else Nil
errors.map(msg => List(Build_Log.SESSION_NAME -> session_name, Markup.CONTENT -> msg))
})
build_out_progress.echo("Reading heap sizes ...")
val heap_sizes =
build_info.finished_sessions.flatMap(session_name =>
{
val heap = isabelle_output + Path.explode(session_name)
if (heap.is_file)
Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)")
else None
})
build_out_progress.echo("Writing log file " + log_path.xz + " ...")
File.write_xz(log_path.xz,
terminate_lines(
Protocol.Meta_Info_Marker(meta_info) :: build_result.out_lines :::
session_build_info :::
ml_statistics.map(Protocol.ML_Statistics_Marker.apply) :::
session_errors.map(Protocol.Error_Message_Marker.apply) :::
heap_sizes), XZ.options(6))
/* next build */
if (multicore_base && first_build && isabelle_output_log.is_dir)
Isabelle_System.copy_dir(isabelle_output_log, isabelle_base_log)
Isabelle_System.rm_tree(isabelle_output)
first_build = false
(build_result, log_path.xz)
}
}
/* command line entry point */
private object Multicore
{
private val Pat1 = """^(\d+)$""".r
private val Pat2 = """^(\d+)x(\d+)$""".r
def parse(s: String): (Int, Int) =
s match {
case Pat1(Value.Int(x)) => (x, 1)
case Pat2(Value.Int(x), Value.Int(y)) => (x, y)
case _ => error("Bad multicore configuration: " + quote(s))
}
}
def main(args: Array[String]): Unit =
{
Command_Line.tool {
var afp_rev: Option[String] = None
var multicore_base = false
var components_base: Path = Components.default_components_base
var heap: Option[Int] = None
var max_heap: Option[Int] = None
var multicore_list = List(default_multicore)
var isabelle_identifier = default_isabelle_identifier
var afp_partition = 0
var component_repository = Components.default_component_repository
var more_settings: List[String] = Nil
var more_preferences: List[String] = Nil
var fresh = false
var hostname = ""
var init_settings: List[String] = Nil
var arch_64 = false
var output_file = ""
var rev = default_rev
var ml_statistics_step = 1
var build_tags = List.empty[String]
var user_home = default_user_home
var verbose = false
var exit_code = false
val getopts = Getopts("""
Usage: Admin/build_history [OPTIONS] REPOSITORY [ARGS ...]
Options are:
-A REV include $ISABELLE_HOME/AFP repository at given revision
-B first multicore build serves as base for scheduling information
-C DIR base directory for Isabelle components (default: """ +
Components.default_components_base + """)
-H SIZE minimal ML heap in MB (default: """ + default_heap + """ for x86, """ +
default_heap * 2 + """ for x86_64)
-M MULTICORE multicore configurations (see below)
-N NAME alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
-P NUMBER AFP partition number (0, 1, 2, default: 0=unrestricted)
-R URL remote repository for Isabelle components (default: """ +
Components.default_component_repository + """)
-U SIZE maximal ML heap in MB (default: unbounded)
-e TEXT additional text for generated etc/settings
-f fresh build of Isabelle/Scala components (recommended)
-h NAME override local hostname
-i TEXT initial text for generated etc/settings
-m ARCH processor architecture (32=x86, 64=x86_64, default: x86)
-o FILE output file for log names (default: stdout)
-p TEXT additional text for generated etc/preferences
-r REV update to revision (default: """ + default_rev + """)
-s NUMBER step size for ML statistics (0=none, 1=all, n=step, default: 1)
-t TAG free-form build tag (multiple occurrences possible)
-u DIR alternative USER_HOME directory
-v verbose
-x return overall exit code from build processes
Build Isabelle sessions from the history of another REPOSITORY clone,
passing ARGS directly to its isabelle build tool.
Each MULTICORE configuration consists of one or two numbers (default 1):
THREADS or THREADSxPROCESSES, e.g. -M 1,2,4 or -M 1x4,2x2,4.
""",
"A:" -> (arg => afp_rev = Some(arg)),
"B" -> (_ => multicore_base = true),
"C:" -> (arg => components_base = Path.explode(arg)),
"H:" -> (arg => heap = Some(Value.Int.parse(arg))),
"M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse)),
"N:" -> (arg => isabelle_identifier = arg),
"P:" -> (arg => afp_partition = Value.Int.parse(arg)),
"R:" -> (arg => component_repository = arg),
"U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
"e:" -> (arg => more_settings = more_settings ::: List(arg)),
"f" -> (_ => fresh = true),
"h:" -> (arg => hostname = arg),
"i:" -> (arg => init_settings = init_settings ::: List(arg)),
"m:" ->
{
case "32" | "x86" => arch_64 = false
case "64" | "x86_64" => arch_64 = true
case bad => error("Bad processor architecture: " + quote(bad))
},
"o:" -> (arg => output_file = arg),
"p:" -> (arg => more_preferences = more_preferences ::: List(arg)),
"r:" -> (arg => rev = arg),
"s:" -> (arg => ml_statistics_step = Value.Int.parse(arg)),
"t:" -> (arg => build_tags = build_tags ::: List(arg)),
"u:" -> (arg => user_home = Path.explode(arg)),
"v" -> (_ => verbose = true),
"x" -> (_ => exit_code = true))
val more_args = getopts(args)
val (root, build_args) =
more_args match {
case root :: build_args => (Path.explode(root), build_args)
case _ => getopts.usage()
}
val progress = new Console_Progress(stderr = true)
val results =
build_history(Options.init(), root, user_home = user_home, progress = progress, rev = rev,
afp_rev = afp_rev, afp_partition = afp_partition,
isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step,
component_repository = component_repository, components_base = components_base,
fresh = fresh, hostname = hostname, multicore_base = multicore_base,
multicore_list = multicore_list, arch_64 = arch_64,
heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
max_heap = max_heap, init_settings = init_settings, more_settings = more_settings,
more_preferences = more_preferences, verbose = verbose, build_tags = build_tags,
build_args = build_args)
if (output_file == "") {
for ((_, log_path) <- results)
Output.writeln(log_path.implode, stdout = true)
}
else {
File.write(Path.explode(output_file),
cat_lines(for ((_, log_path) <- results) yield log_path.implode))
}
val rc = results.foldLeft(0) { case (rc, (res, _)) => rc max res.rc }
if (rc != 0 && exit_code) sys.exit(rc)
}
}
/** remote build_history -- via command-line **/
def remote_build_history(
ssh: SSH.Session,
isabelle_repos_self: Path,
isabelle_repos_other: Path,
- isabelle_repos_source: String = Isabelle_Cronjob.isabelle_repos_source,
- afp_repos_source: String = AFP.repos_source,
+ isabelle_repos_source: String = Isabelle_System.isabelle_repository,
+ afp_repos_source: String = Isabelle_System.afp_repository,
isabelle_identifier: String = "remote_build_history",
self_update: Boolean = false,
progress: Progress = new Progress,
rev: String = "",
afp_rev: Option[String] = None,
options: String = "",
args: String = ""): List[(String, Bytes)] =
{
/* Isabelle self repository */
val self_hg =
Mercurial.setup_repository(isabelle_repos_source, isabelle_repos_self, ssh = ssh)
def execute(cmd: String, args: String, echo: Boolean = false, strict: Boolean = true): Unit =
ssh.execute(
Isabelle_System.export_isabelle_identifier(isabelle_identifier) +
ssh.bash_path(isabelle_repos_self + Path.explode(cmd)) + " " + args,
progress_stdout = progress.echo_if(echo, _),
progress_stderr = progress.echo_if(echo, _),
strict = strict).check
if (self_update) {
val hg = Mercurial.repository(Path.ISABELLE_HOME)
hg.push(self_hg.root_url, force = true)
self_hg.update(rev = hg.parent(), clean = true)
execute("bin/isabelle", "components -I")
execute("bin/isabelle", "components -a", echo = true)
execute("Admin/build", "jars_fresh")
}
val rev_id = self_hg.id(rev)
/* Isabelle other + AFP repository */
if (Mercurial.is_repository(isabelle_repos_other, ssh = ssh)) {
ssh.rm_tree(isabelle_repos_other)
}
Mercurial.clone_repository(
ssh.bash_path(isabelle_repos_self), isabelle_repos_other, rev = rev_id, ssh = ssh)
val afp_options =
if (afp_rev.isEmpty) ""
else {
val afp_repos = isabelle_repos_other + Path.explode("AFP")
Mercurial.setup_repository(afp_repos_source, afp_repos, ssh = ssh)
" -A " + Bash.string(afp_rev.get)
}
/* Admin/build_history */
ssh.with_tmp_dir(tmp_dir =>
{
val output_file = tmp_dir + Path.explode("output")
val rev_options = if (rev == "") "" else " -r " + Bash.string(rev_id)
try {
execute("Admin/build_history",
"-o " + ssh.bash_path(output_file) + rev_options + afp_options + " " + options + " " +
ssh.bash_path(isabelle_repos_other) + " " + args,
echo = true, strict = false)
}
catch {
case ERROR(msg) =>
cat_error(msg,
"The error(s) above occurred for build_bistory " + rev_options + afp_options)
}
for (line <- split_lines(ssh.read(output_file)))
yield {
val log = Path.explode(line)
val bytes = ssh.read_bytes(log)
ssh.rm(log)
(log.file_name, bytes)
}
})
}
}
diff --git a/src/Pure/Admin/build_release.scala b/src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala
+++ b/src/Pure/Admin/build_release.scala
@@ -1,894 +1,894 @@
/* Title: Pure/Admin/build_release.scala
Author: Makarius
Build full Isabelle distribution from repository.
*/
package isabelle
object Build_Release
{
/** release info **/
sealed case class Bundle_Info(
platform: Platform.Family.Value,
platform_description: String,
name: String)
{
def path: Path = Path.explode(name)
}
class Release private[Build_Release](
progress: Progress,
val date: Date,
val dist_name: String,
val dist_dir: Path,
val dist_version: String,
val ident: String,
val tags: String)
{
val isabelle: Path = Path.explode(dist_name)
val isabelle_dir: Path = dist_dir + isabelle
val isabelle_id: Path = isabelle_dir + Path.explode("etc/ISABELLE_ID")
val isabelle_tags: Path = isabelle_dir + Path.explode("etc/ISABELLE_TAGS")
val isabelle_identifier: Path = isabelle_dir + Path.explode("etc/ISABELLE_IDENTIFIER")
val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz")
val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz")
def other_isabelle(dir: Path): Other_Isabelle =
Other_Isabelle(dir + isabelle,
isabelle_identifier = dist_name + "-build",
progress = progress)
def bundle_info(platform: Platform.Family.Value): Bundle_Info =
platform match {
case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz")
case Platform.Family.macos => Bundle_Info(platform, "macOS", dist_name + "_macos.tar.gz")
case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe")
}
}
/** generated content **/
/* ANNOUNCE */
def make_announce(release: Release): Unit =
{
File.write(release.isabelle_dir + Path.explode("ANNOUNCE"),
"""
IMPORTANT NOTE
==============
This is a snapshot of Isabelle/""" + release.ident + """ from the repository.
""")
}
/* NEWS */
def make_news(other_isabelle: Other_Isabelle, dist_version: String): Unit =
{
val target = other_isabelle.isabelle_home + Path.explode("doc")
val target_fonts = Isabelle_System.make_directory(target + Path.explode("fonts"))
other_isabelle.copy_fonts(target_fonts)
HTML.write_document(target, "NEWS.html",
List(HTML.title("NEWS (" + dist_version + ")")),
List(
HTML.chapter("NEWS"),
HTML.source(
Symbol.decode(File.read(other_isabelle.isabelle_home + Path.explode("NEWS"))))))
}
/* bundled components */
class Bundled(platform: Option[Platform.Family.Value] = None)
{
def detect(s: String): Boolean =
s.startsWith("#bundled") && !s.startsWith("#bundled ")
def apply(name: String): String =
"#bundled" + (platform match { case None => "" case Some(plat) => "-" + plat }) + ":" + name
private val Pattern1 = ("""^#bundled:(.*)$""").r
private val Pattern2 = ("""^#bundled-(.*):(.*)$""").r
def unapply(s: String): Option[String] =
s match {
case Pattern1(name) => Some(name)
case Pattern2(Platform.Family(plat), name) if platform == Some(plat) => Some(name)
case _ => None
}
}
def record_bundled_components(dir: Path): Unit =
{
val catalogs =
List("main", "bundled").map((_, new Bundled())) :::
default_platform_families.flatMap(platform =>
List(platform.toString, "bundled-" + platform.toString).
map((_, new Bundled(platform = Some(platform)))))
File.append(Components.components(dir),
terminate_lines("#bundled components" ::
(for {
(catalog, bundled) <- catalogs.iterator
path = Components.admin(dir) + Path.basic(catalog)
if path.is_file
line <- split_lines(File.read(path))
if line.nonEmpty && !line.startsWith("#") && !line.startsWith("jedit_build")
} yield bundled(line)).toList))
}
def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) =
{
val Bundled = new Bundled(platform = Some(platform))
val components =
for {
Bundled(name) <- Components.read_components(dir)
if !name.startsWith("jedit_build")
} yield name
val jdk_component =
components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component")
(components, jdk_component)
}
def activate_components(
dir: Path, platform: Platform.Family.Value, more_names: List[String]): Unit =
{
def contrib_name(name: String): String =
Components.contrib(name = name).implode
val Bundled = new Bundled(platform = Some(platform))
Components.write_components(dir,
Components.read_components(dir).flatMap(line =>
line match {
case Bundled(name) =>
if (Components.check_dir(Components.contrib(dir, name))) Some(contrib_name(name))
else None
case _ => if (Bundled.detect(line)) None else Some(line)
}) ::: more_names.map(contrib_name))
}
def make_contrib(dir: Path): Unit =
{
Isabelle_System.make_directory(Components.contrib(dir))
File.write(Components.contrib(dir, "README"),
"""This directory contains add-on components that contribute to the main
Isabelle distribution. Separate licensing conditions apply, see each
directory individually.
""")
}
/** build release **/
private def execute(dir: Path, script: String): Unit =
Isabelle_System.bash(script, cwd = dir.file).check
private def execute_tar(dir: Path, args: String): Unit =
Isabelle_System.gnutar(args, dir = dir).check
/* build heaps on remote server */
private def remote_build_heaps(
options: Options,
platform: Platform.Family.Value,
build_sessions: List[String],
local_dir: Path): Unit =
{
val server_option = "build_host_" + platform.toString
options.string(server_option) match {
case SSH.Target(user, host) =>
using(SSH.open_session(options, host = host, user = user))(ssh =>
{
Isabelle_System.with_tmp_file("tmp", "tar")(local_tmp_tar =>
{
execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .")
ssh.with_tmp_dir(remote_dir =>
{
val remote_tmp_tar = remote_dir + Path.basic("tmp.tar")
ssh.write_file(remote_tmp_tar, local_tmp_tar)
val remote_commands =
List(
"cd " + File.bash_path(remote_dir),
"tar -xf tmp.tar",
"./bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions),
"tar -cf tmp.tar heaps")
ssh.execute(remote_commands.mkString(" && ")).check
ssh.read_file(remote_tmp_tar, local_tmp_tar)
})
execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar))
})
})
case s => error("Bad " + server_option + ": " + quote(s))
}
}
/* Isabelle application */
def make_isabelle_options(path: Path, options: List[String], line_ending: String = "\n"): Unit =
{
val title = "# Java runtime options"
File.write(path, (title :: options).map(_ + line_ending).mkString)
}
def make_isabelle_app(
platform: Platform.Family.Value,
isabelle_target: Path,
isabelle_name: String,
jdk_component: String,
classpath: List[Path],
dock_icon: Boolean = false): Unit =
{
val script = """#!/usr/bin/env bash
#
# Author: Makarius
#
# Main Isabelle application script.
# minimal Isabelle environment
ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)/../.."; pwd)"
source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
#paranoia settings -- avoid intrusion of alien options
unset "_JAVA_OPTIONS"
unset "JAVA_TOOL_OPTIONS"
#paranoia settings -- avoid problems of Java/Swing versus XIM/IBus etc.
unset XMODIFIERS
COMPONENT="$ISABELLE_HOME/contrib/""" + jdk_component + """"
source "$COMPONENT/etc/settings"
# main
declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/Isabelle.options"))
"$ISABELLE_HOME/bin/isabelle" env "$ISABELLE_HOME/lib/scripts/java-gui-setup"
exec "$ISABELLE_JDK_HOME/bin/java" \
"-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \
-classpath """" + classpath.map(p => "$ISABELLE_HOME/" + p.implode).mkString(":") + """" \
"-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \
""" + (if (dock_icon) """"-Xdock:icon=$ISABELLE_HOME/lib/logo/isabelle_transparent-128.png" \
""" else "") + """isabelle.Main "$@"
"""
val script_path = isabelle_target + Path.explode("lib/scripts/Isabelle_app")
File.write(script_path, script)
File.set_executable(script_path, true)
val component_dir = isabelle_target + Path.explode("contrib/Isabelle_app")
Isabelle_System.move_file(
component_dir + Path.explode(Platform.standard_platform(platform)) + Path.explode("Isabelle"),
isabelle_target + Path.explode(isabelle_name))
Isabelle_System.rm_tree(component_dir)
}
def make_isabelle_plist(path: Path, isabelle_name: String, isabelle_rev: String): Unit =
{
File.write(path, """
CFBundleDevelopmentRegion
English
CFBundleIconFile
isabelle.icns
CFBundleIdentifier
de.tum.in.isabelle
CFBundleDisplayName
""" + isabelle_name + """
CFBundleInfoDictionaryVersion
6.0
CFBundleName
""" + isabelle_name + """
CFBundlePackageType
APPL
CFBundleShortVersionString
""" + isabelle_name + """
CFBundleSignature
????
CFBundleVersion
""" + isabelle_rev + """
NSHumanReadableCopyright
LSMinimumSystemVersion
10.11
LSApplicationCategoryType
public.app-category.developer-tools
NSHighResolutionCapable
true
NSSupportsAutomaticGraphicsSwitching
true
CFBundleDocumentTypes
CFBundleTypeExtensions
thy
CFBundleTypeIconFile
theory.icns
CFBundleTypeName
Isabelle theory file
CFBundleTypeRole
Editor
LSTypeIsPackage
""")
}
/* main */
private val default_platform_families: List[Platform.Family.Value] =
List(Platform.Family.linux, Platform.Family.windows, Platform.Family.macos)
def build_release(options: Options,
target_dir: Path = Path.current,
components_base: Path = Components.default_components_base,
progress: Progress = new Progress,
rev: String = "",
afp_rev: String = "",
proper_release_name: Option[String] = None,
platform_families: List[Platform.Family.Value] = default_platform_families,
more_components: List[Path] = Nil,
website: Option[Path] = None,
build_sessions: List[String] = Nil,
build_library: Boolean = false,
parallel_jobs: Int = 1): Release =
{
val hg = Mercurial.repository(Path.ISABELLE_HOME)
val release =
{
val date = Date.now()
val dist_name = proper_release_name getOrElse ("Isabelle_" + Date.Format.date(date))
val dist_dir = (target_dir + Path.explode("dist-" + dist_name)).absolute
val version = proper_string(rev) orElse proper_release_name getOrElse "tip"
val ident =
try { hg.id(version) }
catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) }
val tags = hg.tags(rev = ident)
val dist_version =
proper_release_name match {
case Some(name) => name + ": " + Date.Format("LLLL uuuu")(date)
case None => "Isabelle repository snapshot " + ident + " " + Date.Format.date(date)
}
new Release(progress, date, dist_name, dist_dir, dist_version, ident, tags)
}
/* make distribution */
if (release.isabelle_archive.is_file) {
progress.echo_warning("Release archive already exists: " + release.isabelle_archive)
val archive_ident =
Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
{
val isabelle_id = release.isabelle + Path.explode("etc/ISABELLE_ID")
execute_tar(tmp_dir, "-xzf " +
File.bash_path(release.isabelle_archive) + " " + File.bash_path(isabelle_id))
Isabelle_System.isabelle_id(root = tmp_dir + release.isabelle)
})
if (release.ident != archive_ident) {
error("Mismatch of release identification " + release.ident +
" vs. archive " + archive_ident)
}
}
else {
progress.echo_warning("Producing release archive " + release.isabelle_archive + " ...")
Isabelle_System.make_directory(release.dist_dir)
if (release.isabelle_dir.is_dir)
error("Directory " + release.isabelle_dir + " already exists")
progress.echo_warning("Retrieving Mercurial repository version " + release.ident)
hg.archive(release.isabelle_dir.expand.implode, rev = release.ident, options = "--type files")
for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) {
(release.isabelle_dir + Path.explode(name)).file.delete
}
progress.echo_warning("Preparing distribution " + quote(release.dist_name))
File.write(release.isabelle_id, release.ident)
File.write(release.isabelle_tags, release.tags)
File.write(release.isabelle_identifier, release.dist_name)
if (proper_release_name.isEmpty) make_announce(release)
make_contrib(release.isabelle_dir)
execute(release.isabelle_dir, """find . -print | xargs chmod -f u+rw""")
record_bundled_components(release.isabelle_dir)
/* build tools and documentation */
val other_isabelle = release.other_isabelle(release.dist_dir)
other_isabelle.init_settings(
other_isabelle.init_components(components_base = components_base, catalogs = List("main")))
other_isabelle.resolve_components(echo = true)
try {
val export_classpath =
"export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n"
other_isabelle.bash(export_classpath + "./Admin/build all", echo = true).check
other_isabelle.bash(export_classpath + "./bin/isabelle jedit -b", echo = true).check
}
catch { case ERROR(msg) => cat_error("Failed to build tools:", msg) }
try {
other_isabelle.bash(
"./bin/isabelle build_doc -a -o system_heaps -j " + parallel_jobs, echo = true).check
}
catch { case ERROR(msg) => cat_error("Failed to build documentation:", msg) }
make_news(other_isabelle, release.dist_version)
for (name <- List("Admin", "browser_info", "heaps")) {
Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name))
}
other_isabelle.cleanup()
progress.echo_warning("Creating distribution archive " + release.isabelle_archive)
def execute_dist_name(script: String): Unit =
Isabelle_System.bash(script, cwd = release.dist_dir.file,
env = Isabelle_System.settings() + ("DIST_NAME" -> release.dist_name)).check
execute_dist_name("""
set -e
chmod -R a+r "$DIST_NAME"
chmod -R u+w "$DIST_NAME"
chmod -R g=o "$DIST_NAME"
find "$DIST_NAME" -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w
""")
execute_tar(release.dist_dir, "-czf " +
File.bash_path(release.isabelle_archive) + " " + Bash.string(release.dist_name))
execute_dist_name("""
set -e
mv "$DIST_NAME" "${DIST_NAME}-old"
mkdir "$DIST_NAME"
mv "${DIST_NAME}-old/README" "${DIST_NAME}-old/NEWS" "${DIST_NAME}-old/ANNOUNCE" \
"${DIST_NAME}-old/COPYRIGHT" "${DIST_NAME}-old/CONTRIBUTORS" "$DIST_NAME"
mkdir "$DIST_NAME/doc"
mv "${DIST_NAME}-old/doc/"*.pdf \
"${DIST_NAME}-old/doc/"*.html \
"${DIST_NAME}-old/doc/"*.css \
"${DIST_NAME}-old/doc/fonts" \
"${DIST_NAME}-old/doc/Contents" "$DIST_NAME/doc"
rm -f Isabelle && ln -sf "$DIST_NAME" Isabelle
rm -rf "${DIST_NAME}-old"
""")
}
/* make application bundles */
val bundle_infos = platform_families.map(release.bundle_info)
for (bundle_info <- bundle_infos) {
val isabelle_name = release.dist_name
val platform = bundle_info.platform
progress.echo("\nApplication bundle for " + platform)
Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
{
// release archive
execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive))
val other_isabelle = release.other_isabelle(tmp_dir)
val isabelle_target = other_isabelle.isabelle_home
// bundled components
progress.echo("Bundled components:")
val contrib_dir = Components.contrib(isabelle_target)
val (bundled_components, jdk_component) =
get_bundled_components(isabelle_target, platform)
Components.resolve(components_base, bundled_components,
target_dir = Some(contrib_dir),
copy_dir = Some(release.dist_dir + Path.explode("contrib")),
progress = progress)
val more_components_names =
more_components.map(Components.unpack(contrib_dir, _, progress = progress))
Components.purge(contrib_dir, platform)
activate_components(isabelle_target, platform, more_components_names)
// Java parameters
val java_options: List[String] =
(for {
variable <-
List(
"ISABELLE_JAVA_SYSTEM_OPTIONS",
"JEDIT_JAVA_SYSTEM_OPTIONS",
"JEDIT_JAVA_OPTIONS")
opt <- Word.explode(other_isabelle.getenv(variable))
}
yield {
val s = "-Dapple.awt.application.name="
if (opt.startsWith(s)) s + isabelle_name else opt
}) ::: List("-Disabelle.jedit_server=" + isabelle_name)
val classpath: List[Path] =
{
val base = isabelle_target.absolute
Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).map(path =>
{
val abs_path = path.absolute
File.relative_path(base, abs_path) match {
case Some(rel_path) => rel_path
case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path)
}
}) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar"))
}
val jedit_options = Path.explode("src/Tools/jEdit/etc/options")
val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props")
// build heaps
if (build_sessions.nonEmpty) {
progress.echo("Building heaps ...")
remote_build_heaps(options, platform, build_sessions, isabelle_target)
}
// application bundling
platform match {
case Platform.Family.linux =>
File.change(isabelle_target + jedit_options,
_.replaceAll("jedit_reset_font_size : int =.*", "jedit_reset_font_size : int = 24"))
File.change(isabelle_target + jedit_props,
_.replaceAll("console.fontsize=.*", "console.fontsize=18")
.replaceAll("helpviewer.fontsize=.*", "helpviewer.fontsize=18")
.replaceAll("metal.primary.fontsize=.*", "metal.primary.fontsize=18")
.replaceAll("metal.secondary.fontsize=.*", "metal.secondary.fontsize=18")
.replaceAll("view.fontsize=.*", "view.fontsize=24")
.replaceAll("view.gutter.fontsize=.*", "view.gutter.fontsize=16"))
make_isabelle_options(
isabelle_target + Path.explode("Isabelle.options"), java_options)
make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component, classpath)
val archive_name = isabelle_name + "_linux.tar.gz"
progress.echo("Packaging " + archive_name + " ...")
execute_tar(tmp_dir,
"-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
Bash.string(isabelle_name))
case Platform.Family.macos =>
File.change(isabelle_target + jedit_props,
_.replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
.replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d"))
// macOS application bundle
val app_contents = isabelle_target + Path.explode("Contents")
for (icon <- List("lib/logo/isabelle.icns", "lib/logo/theory.icns")) {
Isabelle_System.copy_file(isabelle_target + Path.explode(icon),
Isabelle_System.make_directory(app_contents + Path.explode("Resources")))
}
make_isabelle_plist(
app_contents + Path.explode("Info.plist"), isabelle_name, release.ident)
make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component,
classpath, dock_icon = true)
val isabelle_options = Path.explode("Isabelle.options")
make_isabelle_options(
isabelle_target + isabelle_options,
java_options ::: List("-Disabelle.app=true"))
// application archive
val archive_name = isabelle_name + "_macos.tar.gz"
progress.echo("Packaging " + archive_name + " ...")
val isabelle_app = Path.explode(isabelle_name + ".app")
Isabelle_System.move_file(tmp_dir + Path.explode(isabelle_name),
tmp_dir + isabelle_app)
execute_tar(tmp_dir,
"-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
File.bash_path(isabelle_app))
case Platform.Family.windows =>
File.change(isabelle_target + jedit_props,
_.replaceAll("foldPainter=.*", "foldPainter=Square"))
// application launcher
Isabelle_System.move_file(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
val app_template = Path.explode("~~/Admin/Windows/launch4j")
make_isabelle_options(
isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
java_options, line_ending = "\r\n")
val isabelle_xml = Path.explode("isabelle.xml")
val isabelle_exe = Path.explode(isabelle_name + ".exe")
File.write(tmp_dir + isabelle_xml,
File.read(app_template + isabelle_xml)
.replace("{ISABELLE_NAME}", isabelle_name)
.replace("{OUTFILE}", File.platform_path(isabelle_target + isabelle_exe))
.replace("{ICON}",
File.platform_path(app_template + Path.explode("isabelle_transparent.ico")))
.replace("{SPLASH}",
File.platform_path(app_template + Path.explode("isabelle.bmp")))
.replace("{CLASSPATH}",
cat_lines(classpath.map(cp =>
" %EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "")))
.replace("\\jdk\\", "\\" + jdk_component + "\\"))
execute(tmp_dir,
"\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
Isabelle_System.copy_file(app_template + Path.explode("manifest.xml"),
isabelle_target + isabelle_exe.ext("manifest"))
// Cygwin setup
val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
Isabelle_System.copy_file(cygwin_template + Path.explode("Cygwin-Terminal.bat"),
isabelle_target)
val cygwin_mirror =
File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror"))
val cygwin_bat = Path.explode("Cygwin-Setup.bat")
File.write(isabelle_target + cygwin_bat,
File.read(cygwin_template + cygwin_bat).replace("{MIRROR}", cygwin_mirror))
File.set_executable(isabelle_target + cygwin_bat, true)
for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
val path = Path.explode(name)
Isabelle_System.copy_file(cygwin_template + path,
isabelle_target + Path.explode("contrib/cygwin") + path)
}
execute(isabelle_target,
"""find . -type f -not -name "*.exe" -not -name "*.dll" """ +
(if (Platform.is_macos) "-perm +100" else "-executable") +
" -print0 > contrib/cygwin/isabelle/executables")
execute(isabelle_target,
"""find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ +
"""> contrib/cygwin/isabelle/symlinks""")
execute(isabelle_target, """find . -type l -exec rm "{}" ";" """)
File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "")
// executable archive (self-extracting 7z)
val archive_name = isabelle_name + ".7z"
val exe_archive = tmp_dir + Path.explode(archive_name)
exe_archive.file.delete
progress.echo("Packaging " + archive_name + " ...")
execute(tmp_dir,
"7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name))
if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive)
val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx")
val sfx_txt =
File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt"))
.replace("{ISABELLE_NAME}", isabelle_name)
Bytes.write(release.dist_dir + isabelle_exe,
Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
File.set_executable(release.dist_dir + isabelle_exe, true)
}
})
progress.echo("DONE")
}
/* minimal website */
for (dir <- website) {
val website_platform_bundles =
for {
bundle_info <- bundle_infos
if (release.dist_dir + bundle_info.path).is_file
} yield (bundle_info.name, bundle_info)
val isabelle_link =
- HTML.link(Isabelle_Cronjob.isabelle_repos_source + "/rev/" + release.ident,
+ HTML.link(Isabelle_System.isabelle_repository + "/rev/" + release.ident,
HTML.text("Isabelle/" + release.ident))
val afp_link =
- HTML.link(AFP.repos_source + "/rev/" + afp_rev, HTML.text("AFP/" + afp_rev))
+ HTML.link(Isabelle_System.afp_repository + "/rev/" + afp_rev, HTML.text("AFP/" + afp_rev))
HTML.write_document(dir, "index.html",
List(HTML.title(release.dist_name)),
List(
HTML.section(release.dist_name),
HTML.subsection("Platforms"),
HTML.itemize(
website_platform_bundles.map({ case (bundle, bundle_info) =>
List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) })),
HTML.subsection("Repositories"),
HTML.itemize(
List(List(isabelle_link)) ::: (if (afp_rev == "") Nil else List(List(afp_link))))))
for ((bundle, _) <- website_platform_bundles)
Isabelle_System.copy_file(release.dist_dir + Path.explode(bundle), dir)
}
/* HTML library */
if (build_library) {
if (release.isabelle_library_archive.is_file) {
progress.echo_warning("Library archive already exists: " + release.isabelle_library_archive)
}
else {
Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
{
val bundle =
release.dist_dir + Path.explode(release.dist_name + "_" + Platform.family + ".tar.gz")
execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
val other_isabelle = release.other_isabelle(tmp_dir)
Isabelle_System.make_directory(other_isabelle.etc)
File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n")
other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs +
" -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
" -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check
other_isabelle.isabelle_home_user.file.delete
execute(tmp_dir, "chmod -R a+r " + Bash.string(release.dist_name))
execute(tmp_dir, "chmod -R g=o " + Bash.string(release.dist_name))
execute_tar(tmp_dir, "-czf " + File.bash_path(release.isabelle_library_archive) +
" " + Bash.string(release.dist_name + "/browser_info"))
})
}
}
release
}
/** command line entry point **/
def main(args: Array[String]): Unit =
{
Command_Line.tool {
var afp_rev = ""
var components_base: Path = Components.default_components_base
var target_dir = Path.current
var proper_release_name: Option[String] = None
var website: Option[Path] = None
var build_sessions: List[String] = Nil
var more_components: List[Path] = Nil
var parallel_jobs = 1
var build_library = false
var options = Options.init()
var platform_families = default_platform_families
var rev = ""
val getopts = Getopts("""
Usage: Admin/build_release [OPTIONS] BASE_DIR
Options are:
-A REV corresponding AFP changeset id
-C DIR base directory for Isabelle components (default: """ +
Components.default_components_base + """)
-D DIR target directory (default ".")
-R RELEASE proper release with name
-W WEBSITE produce minimal website in given directory
-b SESSIONS build platform-specific session images (separated by commas)
-c ARCHIVE clean bundling with additional component .tar.gz archive
-j INT maximum number of parallel jobs (default 1)
-l build library
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-p NAMES platform families (default: """ + default_platform_families.mkString(",") + """)
-r REV Mercurial changeset id (default: RELEASE or tip)
Build Isabelle release in base directory, using the local repository clone.
""",
"A:" -> (arg => afp_rev = arg),
"C:" -> (arg => components_base = Path.explode(arg)),
"D:" -> (arg => target_dir = Path.explode(arg)),
"R:" -> (arg => proper_release_name = Some(arg)),
"W:" -> (arg => website = Some(Path.explode(arg))),
"b:" -> (arg => build_sessions = space_explode(',', arg)),
"c:" -> (arg =>
{
val path = Path.explode(arg)
Components.Archive.get_name(path.file_name)
more_components = more_components ::: List(path)
}),
"j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
"l" -> (_ => build_library = true),
"o:" -> (arg => options = options + arg),
"p:" -> (arg => platform_families = space_explode(',', arg).map(Platform.Family.parse)),
"r:" -> (arg => rev = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
error("Building for windows requires 7z")
build_release(options, target_dir = target_dir, components_base = components_base,
progress = progress, rev = rev, afp_rev = afp_rev,
proper_release_name = proper_release_name, website = website,
platform_families =
if (platform_families.isEmpty) default_platform_families
else platform_families,
more_components = more_components, build_sessions = build_sessions,
build_library = build_library, parallel_jobs = parallel_jobs)
}
}
}
diff --git a/src/Pure/Admin/isabelle_cronjob.scala b/src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala
+++ b/src/Pure/Admin/isabelle_cronjob.scala
@@ -1,635 +1,634 @@
/* Title: Pure/Admin/isabelle_cronjob.scala
Author: Makarius
Main entry point for administrative cronjob at TUM.
*/
package isabelle
import java.nio.file.Files
import scala.annotation.tailrec
object Isabelle_Cronjob
{
/* global resources: owned by main cronjob */
val backup = "lxbroy10:cronjob"
val main_dir: Path = Path.explode("~/cronjob")
val main_state_file: Path = main_dir + Path.explode("run/main.state")
val current_log: Path = main_dir + Path.explode("run/main.log") // owned by log service
val cumulative_log: Path = main_dir + Path.explode("log/main.log") // owned by log service
- val isabelle_repos_source = "https://isabelle.sketis.net/repos/isabelle"
val isabelle_repos: Path = main_dir + Path.explode("isabelle")
val afp_repos: Path = main_dir + Path.explode("AFP")
val mailman_archives_dir = Path.explode("~/cronjob/Mailman")
val build_log_dirs =
List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log"))
/** logger tasks **/
sealed case class Logger_Task(name: String = "", body: Logger => Unit)
/* init and exit */
def get_rev(): String = Mercurial.repository(isabelle_repos).id()
def get_afp_rev(): String = Mercurial.repository(afp_repos).id()
val init: Logger_Task =
Logger_Task("init", logger =>
{
Isabelle_Devel.make_index()
- Mercurial.setup_repository(isabelle_repos_source, isabelle_repos)
- Mercurial.setup_repository(AFP.repos_source, afp_repos)
+ Mercurial.setup_repository(Isabelle_System.isabelle_repository, isabelle_repos)
+ Mercurial.setup_repository(Isabelle_System.afp_repository, afp_repos)
File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date),
Build_Log.Identify.content(logger.start_date, Some(get_rev()), Some(get_afp_rev())))
Isabelle_System.bash(
"""rsync -a --include="*/" --include="plain_identify*" --exclude="*" """ +
Bash.string(backup + "/log/.") + " " + File.bash_path(main_dir) + "/log/.").check
if (!Isabelle_Devel.cronjob_log.is_file)
Files.createSymbolicLink(Isabelle_Devel.cronjob_log.file.toPath, current_log.file.toPath)
})
val exit: Logger_Task =
Logger_Task("exit", logger =>
{
Isabelle_System.bash(
"rsync -a " + File.bash_path(main_dir) + "/log/." + " " + Bash.string(backup) + "/log/.")
.check
})
/* Mailman archives */
val mailman_archives: Logger_Task =
Logger_Task("mailman_archives", logger =>
{
Mailman.isabelle_users.download(mailman_archives_dir)
Mailman.isabelle_dev.download(mailman_archives_dir)
})
/* build release */
val build_release: Logger_Task =
Logger_Task("build_release", logger =>
{
Isabelle_Devel.release_snapshot(logger.options, rev = get_rev(), afp_rev = get_afp_rev())
})
/* remote build_history */
sealed case class Item(
known: Boolean,
isabelle_version: String,
afp_version: Option[String],
pull_date: Date)
{
def unknown: Boolean = !known
def versions: (String, Option[String]) = (isabelle_version, afp_version)
def known_versions(rev: String, afp_rev: Option[String]): Boolean =
known && rev != "" && isabelle_version == rev &&
(afp_rev.isEmpty || afp_rev.get != "" && afp_version == afp_rev)
}
def recent_items(db: SQL.Database,
days: Int, rev: String, afp_rev: Option[String], sql: SQL.Source): List[Item] =
{
val afp = afp_rev.isDefined
val select =
Build_Log.Data.select_recent_versions(
days = days, rev = rev, afp_rev = afp_rev, sql = "WHERE " + sql)
db.using_statement(select)(stmt =>
stmt.execute_query().iterator(res =>
{
val known = res.bool(Build_Log.Data.known)
val isabelle_version = res.string(Build_Log.Prop.isabelle_version)
val afp_version = if (afp) proper_string(res.string(Build_Log.Prop.afp_version)) else None
val pull_date = res.date(Build_Log.Data.pull_date(afp))
Item(known, isabelle_version, afp_version, pull_date)
}).toList)
}
def unknown_runs(items: List[Item]): List[List[Item]] =
{
val (run, rest) = Library.take_prefix[Item](_.unknown, items.dropWhile(_.known))
if (run.nonEmpty) run :: unknown_runs(rest) else Nil
}
sealed case class Remote_Build(
description: String,
host: String,
actual_host: String = "",
user: String = "",
port: Int = 0,
proxy_host: String = "",
proxy_user: String = "",
proxy_port: Int = 0,
self_update: Boolean = false,
historic: Boolean = false,
history: Int = 0,
history_base: String = "build_history_base",
java_heap: String = "",
options: String = "",
args: String = "",
afp: Boolean = false,
bulky: Boolean = false,
more_hosts: List[String] = Nil,
detect: SQL.Source = "",
active: Boolean = true)
{
def ssh_session(context: SSH.Context): SSH.Session =
context.open_session(host = host, user = user, port = port, actual_host = actual_host,
proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port,
permissive = proxy_host.nonEmpty)
def sql: SQL.Source =
Build_Log.Prop.build_engine.toString + " = " + SQL.string(Build_History.engine) + " AND " +
SQL.member(Build_Log.Prop.build_host.ident, host :: more_hosts) +
(if (detect == "") "" else " AND " + SQL.enclose(detect))
def profile: Build_Status.Profile =
Build_Status.Profile(description, history = history, afp = afp, bulky = bulky, sql = sql)
def pick(
options: Options,
rev: String = "",
filter: Item => Boolean = _ => true): Option[(String, Option[String])] =
{
val afp_rev = if (afp) Some(get_afp_rev()) else None
val store = Build_Log.store(options)
using(store.open_database())(db =>
{
def pick_days(days: Int, gap: Int): Option[(String, Option[String])] =
{
val items = recent_items(db, days, rev, afp_rev, sql).filter(filter)
def runs = unknown_runs(items).filter(run => run.length >= gap)
if (historic || items.exists(_.known_versions(rev, afp_rev))) {
val longest_run =
runs.foldLeft(List.empty[Item]) {
case (item1, item2) => if (item1.length >= item2.length) item1 else item2
}
if (longest_run.isEmpty) None
else Some(longest_run(longest_run.length / 2).versions)
}
else if (rev != "") Some((rev, afp_rev))
else runs.flatten.headOption.map(_.versions)
}
pick_days(options.int("build_log_history") max history, 2) orElse
pick_days(200, 5) orElse
pick_days(2000, 1)
})
}
def build_history_options: String =
" -h " + Bash.string(host) + " " +
(java_heap match {
case "" => ""
case h =>
"-e 'ISABELLE_TOOL_JAVA_OPTIONS=\"$ISABELLE_TOOL_JAVA_OPTIONS -Xmx" + h + "\"' "
}) + options
}
val remote_builds_old: List[Remote_Build] =
List(
Remote_Build("Linux A", "lxbroy9",
java_heap = "2g", options = "-m32 -B -M1x2,2", args = "-N -g timing"),
Remote_Build("Linux Benchmarks", "lxbroy5", historic = true, history = 90,
java_heap = "2g",
options = "-m32 -B -M1x2,2 -t Benchmarks" +
" -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" +
" -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind -e ISABELLE_SMLNJ=sml" +
" -e ISABELLE_SWIPL=swipl",
args = "-N -a -d '~~/src/Benchmarks'",
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("Benchmarks")),
Remote_Build("macOS 10.14 Mojave (Old)", "lapnipkow3",
options = "-m32 -M1,2 -e ISABELLE_GHC_SETUP=true -p pide_session=false",
self_update = true, args = "-a -d '~~/src/Benchmarks'"),
Remote_Build("AFP old bulky", "lrzcloud1", self_update = true,
proxy_host = "lxbroy10", proxy_user = "i21isatest",
options = "-m64 -M6 -U30000 -s10 -t AFP",
args = "-g large -g slow",
afp = true,
bulky = true,
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")),
Remote_Build("AFP old", "lxbroy7",
args = "-N -X large -X slow",
afp = true,
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")),
Remote_Build("Poly/ML 5.7 Linux", "lxbroy8",
history_base = "37074e22e8be",
options = "-m32 -B -M1x2,2 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'",
args = "-N -g timing",
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7") + " AND " +
Build_Log.Settings.ML_OPTIONS + " <> " + SQL.string("-H 500")),
Remote_Build("Poly/ML 5.7.1 Linux", "lxbroy8",
history_base = "a9d5b59c3e12",
options = "-m32 -B -M1x2,2 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'",
args = "-N -g timing",
detect =
Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " +
Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")),
Remote_Build("Poly/ML 5.7 macOS", "macbroy2",
history_base = "37074e22e8be",
options = "-m32 -B -M1x4,4 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'",
args = "-a",
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7")),
Remote_Build("Poly/ML 5.7.1 macOS", "macbroy2",
history_base = "a9d5b59c3e12",
options = "-m32 -B -M1x4,4 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'",
args = "-a",
detect =
Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " +
Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")),
Remote_Build("macOS", "macbroy2",
options = "-m32 -M8" +
" -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" +
" -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
" -e ISABELLE_OPAM_ROOT=\"$ISABELLE_HOME/opam\"" +
" -e ISABELLE_SMLNJ=/home/isabelle/smlnj/110.85/bin/sml" +
" -p pide_session=false",
args = "-a",
detect = Build_Log.Prop.build_tags.undefined,
history_base = "2c0f24e927dd"),
Remote_Build("macOS, quick_and_dirty", "macbroy2",
options = "-m32 -M8 -t quick_and_dirty -p pide_session=false", args = "-a -o quick_and_dirty",
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("quick_and_dirty"),
history_base = "2c0f24e927dd"),
Remote_Build("macOS, skip_proofs", "macbroy2",
options = "-m32 -M8 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs",
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("skip_proofs"),
history_base = "2c0f24e927dd"),
Remote_Build("Poly/ML test", "lxbroy8",
options = "-m32 -B -M1x2,2 -t polyml-test -i 'init_component /home/isabelle/contrib/polyml-5.7-20170217'",
args = "-N -g timing",
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-test")),
Remote_Build("macOS 10.12 Sierra", "macbroy30", options = "-m32 -M2 -p pide_session=false", args = "-a",
detect = Build_Log.Prop.build_start.toString + " > date '2017-03-03'"),
Remote_Build("macOS 10.10 Yosemite", "macbroy31", options = "-m32 -M2 -p pide_session=false", args = "-a"),
Remote_Build("macOS 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a",
detect = Build_Log.Prop.build_start.toString + " < date '2017-03-03'")) :::
{
for { (n, hosts) <- List(1 -> List("lxbroy6"), 2 -> List("lxbroy8", "lxbroy5")) }
yield {
Remote_Build("AFP old", host = hosts.head, more_hosts = hosts.tail,
options = "-m32 -M1x2 -t AFP -P" + n +
" -e ISABELLE_GHC=ghc" +
" -e ISABELLE_MLTON=mlton" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" +
" -e ISABELLE_SMLNJ=sml",
args = "-N -X large -X slow",
afp = true,
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP"))
}
}
val remote_builds1: List[List[Remote_Build]] =
{
List(
List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90,
options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),
List(Remote_Build("macOS 10.13 High Sierra", "lapbroy68",
options = "-m32 -B -M1,2,4 -e ISABELLE_GHC_SETUP=true -p pide_session=false",
self_update = true, args = "-a -d '~~/src/Benchmarks'")),
List(
Remote_Build("macOS 11.1 Big Sur", "mini1",
options = "-m32 -B -M1x2,2,4 -p pide_session=false" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
" -e ISABELLE_GHC_SETUP=true" +
" -e ISABELLE_MLTON=/usr/local/bin/mlton" +
" -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" +
" -e ISABELLE_SWIPL=/usr/local/bin/swipl",
self_update = true, args = "-a -d '~~/src/Benchmarks'")),
List(
Remote_Build("macOS 10.14 Mojave", "mini2",
options = "-m32 -B -M1x2,2,4 -p pide_session=false" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
" -e ISABELLE_GHC_SETUP=true" +
" -e ISABELLE_MLTON=/usr/local/bin/mlton" +
" -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" +
" -e ISABELLE_SWIPL=/usr/local/bin/swipl",
self_update = true, args = "-a -d '~~/src/Benchmarks'"),
Remote_Build("macOS, quick_and_dirty", "mini2",
options = "-m32 -M4 -t quick_and_dirty -p pide_session=false",
self_update = true, args = "-a -o quick_and_dirty",
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("quick_and_dirty")),
Remote_Build("macOS, skip_proofs", "mini2",
options = "-m32 -M4 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs",
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("skip_proofs"))),
List(Remote_Build("macOS 10.15 Catalina", "laramac01", user = "makarius",
proxy_host = "laraserver", proxy_user = "makarius",
self_update = true,
options = "-m32 -M4 -e ISABELLE_GHC_SETUP=true -p pide_session=false",
args = "-a -d '~~/src/Benchmarks'")),
List(
Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true,
options = "-m32 -M4" +
" -C /cygdrive/d/isatest/contrib" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
" -e ISABELLE_GHC_SETUP=true" +
" -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
args = "-a",
detect =
Build_Log.Settings.ML_PLATFORM.toString + " = " + SQL.string("x86-windows") + " OR " +
Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64_32-windows")),
Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true,
options = "-m64 -M4" +
" -C /cygdrive/d/isatest/contrib" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
" -e ISABELLE_GHC_SETUP=true" +
" -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
args = "-a",
detect = Build_Log.Settings.ML_PLATFORM.toString + " = " + SQL.string("x86_64-windows"))))
}
val remote_builds2: List[List[Remote_Build]] =
List(
List(
Remote_Build("AFP", "lrzcloud2", actual_host = "10.195.4.41", self_update = true,
proxy_host = "lxbroy10", proxy_user = "i21isatest",
java_heap = "8g",
options = "-m32 -M1x6 -t AFP" +
" -e ISABELLE_GHC=ghc" +
" -e ISABELLE_MLTON=mlton" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" +
" -e ISABELLE_SMLNJ=sml",
args = "-a -X large -X slow",
afp = true,
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")),
Remote_Build("AFP", "lrzcloud2", actual_host = "10.195.4.41", self_update = true,
proxy_host = "lxbroy10", proxy_user = "i21isatest",
java_heap = "8g",
options = "-m64 -M8 -U30000 -s10 -t AFP",
args = "-g large -g slow",
afp = true,
bulky = true,
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP"))))
def remote_build_history(rev: String, afp_rev: Option[String], i: Int, r: Remote_Build)
: Logger_Task =
{
val task_name = "build_history-" + r.host
Logger_Task(task_name, logger =>
{
using(r.ssh_session(logger.ssh_context))(ssh =>
{
val results =
Build_History.remote_build_history(ssh,
isabelle_repos,
isabelle_repos.ext(r.host),
isabelle_identifier = "cronjob_build_history",
self_update = r.self_update,
rev = rev,
afp_rev = afp_rev,
options =
" -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
" -R " + Bash.string(Components.default_component_repository) +
" -C '$USER_HOME/.isabelle/contrib' -f " +
r.build_history_options,
args = "-o timeout=10800 " + r.args)
for ((log_name, bytes) <- results) {
logger.log(Date.now(), log_name)
Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
}
})
})
}
val build_status_profiles: List[Build_Status.Profile] =
(remote_builds_old :: remote_builds1 ::: remote_builds2).flatten.map(_.profile)
/** task logging **/
object Log_Service
{
def apply(options: Options, progress: Progress = new Progress): Log_Service =
new Log_Service(SSH.init_context(options), progress)
}
class Log_Service private(val ssh_context: SSH.Context, progress: Progress)
{
current_log.file.delete
private val thread: Consumer_Thread[String] =
Consumer_Thread.fork("cronjob: logger", daemon = true)(
consume = (text: String) =>
{ // critical
File.append(current_log, text + "\n")
File.append(cumulative_log, text + "\n")
progress.echo(text)
true
})
def shutdown(): Unit = { thread.shutdown() }
val hostname: String = Isabelle_System.hostname()
def log(date: Date, task_name: String, msg: String): Unit =
if (task_name != "")
thread.send(
"[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg)
def start_logger(start_date: Date, task_name: String): Logger =
new Logger(this, start_date, task_name)
def run_task(start_date: Date, task: Logger_Task): Unit =
{
val logger = start_logger(start_date, task.name)
val res = Exn.capture { task.body(logger) }
val end_date = Date.now()
val err =
res match {
case Exn.Res(_) => None
case Exn.Exn(exn) =>
Output.writeln("Exception trace for " + quote(task.name) + ":")
exn.printStackTrace()
val first_line = split_lines(Exn.message(exn)).headOption getOrElse "exception"
Some(first_line)
}
logger.log_end(end_date, err)
}
def fork_task(start_date: Date, task: Logger_Task): Task =
new Task(task.name, run_task(start_date, task))
}
class Logger private[Isabelle_Cronjob](
val log_service: Log_Service, val start_date: Date, val task_name: String)
{
def ssh_context: SSH.Context = log_service.ssh_context
def options: Options = ssh_context.options
def log(date: Date, msg: String): Unit = log_service.log(date, task_name, msg)
def log_end(end_date: Date, err: Option[String]): Unit =
{
val elapsed_time = end_date.time - start_date.time
val msg =
(if (err.isEmpty) "finished" else "ERROR " + err.get) +
(if (elapsed_time.seconds < 3.0) "" else " (" + elapsed_time.message_hms + " elapsed time)")
log(end_date, msg)
}
val log_dir = Isabelle_System.make_directory(main_dir + Build_Log.log_subdir(start_date))
log(start_date, "started")
}
class Task private[Isabelle_Cronjob](name: String, body: => Unit)
{
private val future: Future[Unit] = Future.thread("cronjob: " + name) { body }
def is_finished: Boolean = future.is_finished
}
/** cronjob **/
def cronjob(progress: Progress, exclude_task: Set[String]): Unit =
{
/* soft lock */
val still_running =
try { Some(File.read(main_state_file)) }
catch { case ERROR(_) => None }
still_running match {
case None | Some("") =>
case Some(running) =>
error("Isabelle cronjob appears to be still running: " + running)
}
/* log service */
val log_service = Log_Service(Options.init(), progress = progress)
def run(start_date: Date, task: Logger_Task): Unit = log_service.run_task(start_date, task)
def run_now(task: Logger_Task): Unit = run(Date.now(), task)
/* structured tasks */
def SEQ(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ =>
for (task <- tasks.iterator if !exclude_task(task.name) || task.name == "")
run_now(task))
def PAR(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ =>
{
@tailrec def join(running: List[Task]): Unit =
{
running.partition(_.is_finished) match {
case (Nil, Nil) =>
case (Nil, _ :: _) => Time.seconds(0.5).sleep; join(running)
case (_ :: _, remaining) => join(remaining)
}
}
val start_date = Date.now()
val running =
for (task <- tasks if !exclude_task(task.name))
yield log_service.fork_task(start_date, task)
join(running)
})
/* repository structure */
val hg = Mercurial.repository(isabelle_repos)
val hg_graph = hg.graph()
def history_base_filter(r: Remote_Build): Item => Boolean =
{
val base_rev = hg.id(r.history_base)
val nodes = hg_graph.all_succs(List(base_rev)).toSet
(item: Item) => nodes(item.isabelle_version)
}
/* main */
val main_start_date = Date.now()
File.write(main_state_file, main_start_date.toString + " " + log_service.hostname)
run(main_start_date,
Logger_Task("isabelle_cronjob", logger =>
run_now(
SEQ(List(
init,
PAR(List(mailman_archives, build_release)),
PAR(
List(remote_builds1, remote_builds2).map(remote_builds =>
SEQ(List(
PAR(remote_builds.map(_.filter(_.active)).map(seq =>
SEQ(
for {
(r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
(rev, afp_rev) <- r.pick(logger.options, hg.id(), history_base_filter(r))
} yield remote_build_history(rev, afp_rev, i, r)))),
Logger_Task("jenkins_logs", _ =>
Jenkins.download_logs(logger.options, Jenkins.build_log_jobs, main_dir)),
Logger_Task("build_log_database",
logger => Isabelle_Devel.build_log_database(logger.options, build_log_dirs)),
Logger_Task("build_status",
logger => Isabelle_Devel.build_status(logger.options)))))),
exit)))))
log_service.shutdown()
main_state_file.file.delete
}
/** command line entry point **/
def main(args: Array[String]): Unit =
{
Command_Line.tool {
var force = false
var verbose = false
var exclude_task = Set.empty[String]
val getopts = Getopts("""
Usage: Admin/cronjob/main [OPTIONS]
Options are:
-f apply force to do anything
-v verbose
-x NAME exclude tasks with this name
""",
"f" -> (_ => force = true),
"v" -> (_ => verbose = true),
"x:" -> (arg => exclude_task += arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = if (verbose) new Console_Progress() else new Progress
if (force) cronjob(progress, exclude_task)
else error("Need to apply force to do anything")
}
}
}
diff --git a/src/Pure/System/isabelle_system.scala b/src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala
+++ b/src/Pure/System/isabelle_system.scala
@@ -1,620 +1,627 @@
/* Title: Pure/System/isabelle_system.scala
Author: Makarius
Fundamental Isabelle system environment: quasi-static module with
optional init operation.
*/
package isabelle
import java.io.{File => JFile, IOException}
import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult,
StandardCopyOption, FileSystemException}
import java.nio.file.attribute.BasicFileAttributes
import scala.jdk.CollectionConverters._
object Isabelle_System
{
/** bootstrap information **/
def jdk_home(): String =
{
val java_home = System.getProperty("java.home", "")
val home = new JFile(java_home)
val parent = home.getParent
if (home.getName == "jre" && parent != null &&
(new JFile(new JFile(parent, "bin"), "javac")).exists) parent
else java_home
}
def bootstrap_directory(
preference: String, envar: String, property: String, description: String): String =
{
val value =
proper_string(preference) orElse // explicit argument
proper_string(System.getenv(envar)) orElse // e.g. inherited from running isabelle tool
proper_string(System.getProperty(property)) getOrElse // e.g. via JVM application boot process
error("Unknown " + description + " directory")
if ((new JFile(value)).isDirectory) value
else error("Bad " + description + " directory " + quote(value))
}
/** implicit settings environment **/
abstract class Service
@volatile private var _settings: Option[Map[String, String]] = None
@volatile private var _services: Option[List[Class[Service]]] = None
def settings(): Map[String, String] =
{
if (_settings.isEmpty) init() // unsynchronized check
_settings.get
}
def services(): List[Class[Service]] =
{
if (_services.isEmpty) init() // unsynchronized check
_services.get
}
def make_services[C](c: Class[C]): List[C] =
for { c1 <- services() if Library.is_subclass(c1, c) }
yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C]
def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized
{
if (_settings.isEmpty || _services.isEmpty) {
val isabelle_root1 =
bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root")
val cygwin_root1 =
if (Platform.is_windows)
bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root")
else ""
if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1)
def set_cygwin_root(): Unit =
{
if (Platform.is_windows)
_settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1))
}
set_cygwin_root()
def default(env: Map[String, String], entry: (String, String)): Map[String, String] =
if (env.isDefinedAt(entry._1) || entry._2 == "") env
else env + entry
val env =
{
val temp_windows =
{
val temp = if (Platform.is_windows) System.getenv("TEMP") else null
if (temp != null && temp.contains('\\')) temp else ""
}
val user_home = System.getProperty("user.home", "")
val isabelle_app = System.getProperty("isabelle.app", "")
default(
default(
default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())),
"TEMP_WINDOWS" -> temp_windows),
"HOME" -> user_home),
"ISABELLE_APP" -> "true")
}
val settings =
{
val dump = JFile.createTempFile("settings", null)
dump.deleteOnExit
try {
val cmd1 =
if (Platform.is_windows)
List(cygwin_root1 + "\\bin\\bash", "-l",
File.standard_path(isabelle_root1 + "\\bin\\isabelle"))
else
List(isabelle_root1 + "/bin/isabelle")
val cmd = cmd1 ::: List("getenv", "-d", dump.toString)
val (output, rc) = process_output(process(cmd, env = env, redirect = true))
if (rc != 0) error(output)
val entries =
(for (entry <- space_explode('\u0000', File.read(dump)) if entry != "") yield {
val i = entry.indexOf('=')
if (i <= 0) entry -> ""
else entry.substring(0, i) -> entry.substring(i + 1)
}).toMap
entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
}
finally { dump.delete }
}
_settings = Some(settings)
set_cygwin_root()
val variable = "ISABELLE_SCALA_SERVICES"
val services =
for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable))))
yield {
def err(msg: String): Nothing =
error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
try { Class.forName(name).asInstanceOf[Class[Service]] }
catch {
case _: ClassNotFoundException => err("Class not found")
case exn: Throwable => err(Exn.message(exn))
}
}
_services = Some(services)
}
}
/* getenv -- dynamic process environment */
private def getenv_error(name: String): Nothing =
error("Undefined Isabelle environment variable: " + quote(name))
def getenv(name: String, env: Map[String, String] = settings()): String =
env.getOrElse(name, "")
def getenv_strict(name: String, env: Map[String, String] = settings()): String =
proper_string(getenv(name, env)) getOrElse
error("Undefined Isabelle environment variable: " + quote(name))
def cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
/* getetc -- static distribution parameters */
def getetc(name: String, root: Path = Path.ISABELLE_HOME): Option[String] =
{
val path = root + Path.basic("etc") + Path.basic(name)
if (path.is_file) {
Library.trim_split_lines(File.read(path)) match {
case Nil => None
case List(s) => Some(s)
case _ => error("Single line expected in " + path.absolute)
}
}
else None
}
/* Isabelle distribution identification */
def isabelle_id(root: Path = Path.ISABELLE_HOME): String =
getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) getOrElse {
if (Mercurial.is_repository(root)) Mercurial.repository(root).parent()
else error("Failed to identify Isabelle distribution " + root)
}
object Isabelle_Id extends Scala.Fun_String("isabelle_id")
{
val here = Scala_Project.here
def apply(arg: String): String = isabelle_id()
}
def isabelle_tags(root: Path = Path.ISABELLE_HOME): String =
getetc("ISABELLE_TAGS", root = root) orElse Mercurial.archive_tags(root) getOrElse {
if (Mercurial.is_repository(root)) {
val hg = Mercurial.repository(root)
hg.tags(rev = hg.parent())
}
else ""
}
def isabelle_identifier(): Option[String] = proper_string(getenv("ISABELLE_IDENTIFIER"))
def isabelle_heading(): String =
isabelle_identifier() match {
case None => ""
case Some(version) => " (" + version + ")"
}
def isabelle_name(): String = getenv_strict("ISABELLE_NAME")
def identification(): String = "Isabelle/" + isabelle_id() + isabelle_heading()
/** file-system operations **/
/* scala functions */
private def apply_paths(args: List[String], fun: List[Path] => Unit): List[String] =
{ fun(args.map(Path.explode)); Nil }
private def apply_paths1(args: List[String], fun: Path => Unit): List[String] =
apply_paths(args, { case List(path) => fun(path) })
private def apply_paths2(args: List[String], fun: (Path, Path) => Unit): List[String] =
apply_paths(args, { case List(path1, path2) => fun(path1, path2) })
private def apply_paths3(args: List[String], fun: (Path, Path, Path) => Unit): List[String] =
apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) })
/* permissions */
def chmod(arg: String, path: Path): Unit =
bash("chmod " + arg + " " + File.bash_path(path)).check
def chown(arg: String, path: Path): Unit =
bash("chown " + arg + " " + File.bash_path(path)).check
/* directories */
def make_directory(path: Path): Path =
{
if (!path.is_dir) {
try { Files.createDirectories(path.file.toPath) }
catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) }
}
path
}
def new_directory(path: Path): Path =
if (path.is_dir) error("Directory already exists: " + path.absolute)
else make_directory(path)
def copy_dir(dir1: Path, dir2: Path): Unit =
{
val res = bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2))
if (!res.ok) {
cat_error("Failed to copy directory " + dir1.absolute + " to " + dir2.absolute, res.err)
}
}
object Make_Directory extends Scala.Fun_Strings("make_directory")
{
val here = Scala_Project.here
def apply(args: List[String]): List[String] = apply_paths1(args, make_directory)
}
object Copy_Dir extends Scala.Fun_Strings("copy_dir")
{
val here = Scala_Project.here
def apply(args: List[String]): List[String] = apply_paths2(args, copy_dir)
}
/* copy files */
def copy_file(src: JFile, dst: JFile): Unit =
{
val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
if (!File.eq(src, target)) {
try {
Files.copy(src.toPath, target.toPath,
StandardCopyOption.COPY_ATTRIBUTES,
StandardCopyOption.REPLACE_EXISTING)
}
catch {
case ERROR(msg) =>
cat_error("Failed top copy file " +
File.path(src).absolute + " to " + File.path(dst).absolute, msg)
}
}
}
def copy_file(src: Path, dst: Path): Unit = copy_file(src.file, dst.file)
def copy_file_base(base_dir: Path, src: Path, target_dir: Path): Unit =
{
val src1 = src.expand
val src1_dir = src1.dir
if (!src1.starts_basic) error("Illegal path specification " + src1 + " beyond base directory")
copy_file(base_dir + src1, Isabelle_System.make_directory(target_dir + src1_dir))
}
object Copy_File extends Scala.Fun_Strings("copy_file")
{
val here = Scala_Project.here
def apply(args: List[String]): List[String] = apply_paths2(args, copy_file)
}
object Copy_File_Base extends Scala.Fun_Strings("copy_file_base")
{
val here = Scala_Project.here
def apply(args: List[String]): List[String] = apply_paths3(args, copy_file_base)
}
/* move files */
def move_file(src: JFile, dst: JFile): Unit =
{
val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
if (!File.eq(src, target))
Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING)
}
def move_file(src: Path, dst: Path): Unit = move_file(src.file, dst.file)
/* symbolic link */
def symlink(src: Path, dst: Path, force: Boolean = false): Unit =
{
val src_file = src.file
val dst_file = dst.file
val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file
if (force) target.delete
try { Files.createSymbolicLink(target.toPath, src_file.toPath) }
catch {
case _: UnsupportedOperationException if Platform.is_windows =>
Cygwin.link(File.standard_path(src), target)
case _: FileSystemException if Platform.is_windows =>
Cygwin.link(File.standard_path(src), target)
}
}
/* tmp files */
def isabelle_tmp_prefix(): JFile =
{
val path = Path.explode("$ISABELLE_TMP_PREFIX")
path.file.mkdirs // low-level mkdirs to avoid recursion via Isabelle environment
File.platform_file(path)
}
def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile =
{
val suffix = if (ext == "") "" else "." + ext
val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile
file.deleteOnExit
file
}
def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A =
{
val file = tmp_file(name, ext)
try { body(File.path(file)) } finally { file.delete }
}
/* tmp dirs */
def rm_tree(root: JFile): Unit =
{
root.delete
if (root.isDirectory) {
Files.walkFileTree(root.toPath,
new SimpleFileVisitor[JPath] {
override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult =
{
try { Files.deleteIfExists(file) }
catch { case _: IOException => }
FileVisitResult.CONTINUE
}
override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult =
{
if (e == null) {
try { Files.deleteIfExists(dir) }
catch { case _: IOException => }
FileVisitResult.CONTINUE
}
else throw e
}
}
)
}
}
def rm_tree(root: Path): Unit = rm_tree(root.file)
object Rm_Tree extends Scala.Fun_Strings("rm_tree")
{
val here = Scala_Project.here
def apply(args: List[String]): List[String] = apply_paths1(args, rm_tree)
}
def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile =
{
val dir = Files.createTempDirectory(base_dir.toPath, name).toFile
dir.deleteOnExit
dir
}
def with_tmp_dir[A](name: String)(body: Path => A): A =
{
val dir = tmp_dir(name)
try { body(File.path(dir)) } finally { rm_tree(dir) }
}
/* quasi-atomic update of directory */
def update_directory(dir: Path, f: Path => Unit): Unit =
{
val new_dir = dir.ext("new")
val old_dir = dir.ext("old")
rm_tree(new_dir)
rm_tree(old_dir)
f(new_dir)
if (dir.is_dir) move_file(dir, old_dir)
move_file(new_dir, dir)
rm_tree(old_dir)
}
/** external processes **/
/* raw process */
def process(command_line: List[String],
cwd: JFile = null,
env: Map[String, String] = settings(),
redirect: Boolean = false): Process =
{
val proc = new ProcessBuilder
// fragile on Windows:
// see https://docs.microsoft.com/en-us/cpp/cpp/main-function-command-line-args?view=msvc-160
proc.command(command_line.asJava)
if (cwd != null) proc.directory(cwd)
if (env != null) {
proc.environment.clear()
for ((x, y) <- env) proc.environment.put(x, y)
}
proc.redirectErrorStream(redirect)
proc.start
}
def process_output(proc: Process): (String, Int) =
{
proc.getOutputStream.close()
val output = File.read_stream(proc.getInputStream)
val rc =
try { proc.waitFor }
finally {
proc.getInputStream.close()
proc.getErrorStream.close()
proc.destroy()
Exn.Interrupt.dispose()
}
(output, rc)
}
def process_signal(group_pid: String, signal: String = "0"): Boolean =
{
val bash =
if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe")
else List("/usr/bin/env", "bash")
val (_, rc) = process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid)))
rc == 0
}
/* GNU bash */
def bash(script: String,
cwd: JFile = null,
env: Map[String, String] = settings(),
redirect: Boolean = false,
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
watchdog: Option[Bash.Watchdog] = None,
strict: Boolean = true,
cleanup: () => Unit = () => ()): Process_Result =
{
Bash.process(script, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup).
result(progress_stdout = progress_stdout, progress_stderr = progress_stderr,
watchdog = watchdog, strict = strict)
}
private lazy val gnutar_check: Boolean =
try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") }
catch { case ERROR(_) => false }
def gnutar(
args: String,
dir: Path = Path.current,
original_owner: Boolean = false,
redirect: Boolean = false): Process_Result =
{
val options =
(if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") +
(if (original_owner) "" else "--owner=root --group=staff ")
if (gnutar_check) bash("tar " + options + args, redirect = redirect)
else error("Expected to find GNU tar executable")
}
def require_command(cmds: String*): Unit =
{
for (cmd <- cmds) {
if (!bash(Bash.string(cmd) + " --version").ok) error("Missing system command: " + quote(cmd))
}
}
def hostname(): String = bash("hostname -s").check.out
def open(arg: String): Unit =
bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &")
def pdf_viewer(arg: Path): Unit =
bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &")
def open_external_file(name: String): Boolean =
{
val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString
val external =
ext.nonEmpty &&
Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext)
if (external) {
if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name))
else open(name)
}
external
}
def export_isabelle_identifier(isabelle_identifier: String): String =
if (isabelle_identifier == "") ""
else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n"
/** Isabelle resources **/
/* repository clone with Admin */
def admin(): Boolean = Path.explode("~~/Admin").is_dir
/* components */
def components(): List[Path] =
Path.split(getenv_strict("ISABELLE_COMPONENTS"))
/* default logic */
def default_logic(args: String*): String =
{
args.find(_ != "") match {
case Some(logic) => logic
case None => getenv_strict("ISABELLE_LOGIC")
}
}
/* download file */
def download(url_name: String, progress: Progress = new Progress): HTTP.Content =
{
val url = Url(url_name)
progress.echo("Getting " + quote(url_name))
try { HTTP.Client.get(url) }
catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) }
}
def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit =
Bytes.write(file, download(url_name, progress = progress).bytes)
object Download extends Scala.Fun("download", thread = true)
{
val here = Scala_Project.here
override def invoke(args: List[Bytes]): List[Bytes] =
args match { case List(url) => List(download(url.text).bytes) }
}
+
+
+ /* repositories */
+
+ val isabelle_repository: String = "https://isabelle.sketis.net/repos/isabelle"
+
+ val afp_repository: String = "https://isabelle.sketis.net/repos/afp-devel"
}