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,587 +1,586 @@
/* 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 cygwin_32 = "x86-cygwin"
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(cygwin_32)) cygwin_32
else if (check_dir(windows_32)) windows_32
else err(windows_32)
}
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
}
/** local build **/
private val default_multicore = (1, 1)
private val default_heap = 1500
private val default_isabelle_identifier = "build_history"
def local_build(
options: Options,
root: Path,
progress: Progress = new Progress,
afp: Boolean = false,
afp_partition: Int = 0,
isabelle_identifier: String = default_isabelle_identifier,
ml_statistics_step: Int = 1,
component_repository: String = Components.default_component_repository,
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 Admin/build_other within existing Isabelle settings environment")
}
/* Isabelle + AFP directory */
def directory(dir: Path): Mercurial.Hg_Sync.Directory = {
val directory = Mercurial.Hg_Sync.directory(dir)
if (verbose) progress.echo(directory.log)
directory
}
val isabelle_directory = directory(root)
val afp_directory = if (afp) Some(directory(root + Path.explode("AFP"))) else None
val (afp_build_args, afp_sessions) =
if (afp_directory.isEmpty) (Nil, Nil)
else {
val (opt, sessions) = {
if (afp_partition == 0) ("-d", Nil)
else {
try {
val afp_info = AFP.init(options, base_dir = afp_directory.get.root)
("-d", afp_info.partition(afp_partition))
} catch { case ERROR(_) => ("-D", Nil) }
}
}
(List(opt, "~~/AFP/thys"), sessions)
}
/* main */
val other_isabelle =
Other_Isabelle(root, isabelle_identifier = isabelle_identifier, 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.standard_components_base,
catalogs = Components.optional_catalogs)
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.expand_path(
Path.explode("$ISABELLE_HOME_USER/heaps/$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)
other_isabelle.scala_build(fresh = fresh, echo = verbose)
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.bash("bin/isabelle " + tool, echo = verbose)
Isabelle_System.rm_tree(isabelle_base_log)
}
Isabelle_System.rm_tree(isabelle_output)
Isabelle_System.make_directory(isabelle_output)
other_isabelle.expand_path(Path.explode("$ISABELLE_HOME_USER/mash_state")).file.delete
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.expand_path(Path.explode("$ISABELLE_HOME_USER/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_result =
Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
progress = build_out_progress)
.bash("bin/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_directory.id) :::
afp_directory.map(dir => Build_Log.Prop.afp_version.name -> dir.id).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), Compress.Options_XZ(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 = false
var multicore_base = false
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 ml_statistics_step = 1
var build_tags = List.empty[String]
var verbose = false
var exit_code = false
val getopts = Getopts("""
Usage: Admin/build_other [OPTIONS] ISABELLE_HOME [ARGS ...]
Options are:
-A include $ISABELLE_HOME/AFP directory
-B first multicore build serves as base for scheduling information
-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)
-n no build: sync only
-o FILE output file for log names (default: stdout)
-p TEXT additional text for generated etc/preferences
-s NUMBER step size for ML statistics (0=none, 1=all, n=step, default: 1)
-t TAG free-form build tag (multiple occurrences possible)
-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" -> (_ => afp = true),
"B" -> (_ => multicore_base = true),
"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)),
"s:" -> (arg => ml_statistics_step = Value.Int.parse(arg)),
"t:" -> (arg => build_tags = build_tags ::: List(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 =
local_build(Options.init(), root, progress = progress,
afp = afp, afp_partition = afp_partition,
isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step,
component_repository = component_repository,
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.isEmpty) {
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(Process_Result.RC.ok) { case (rc, (res, _)) => rc max res.rc }
if (rc != Process_Result.RC.ok && exit_code) sys.exit(rc)
}
}
/** remote build -- via rsync and ssh **/
def remote_build(
ssh: SSH.Session,
isabelle_self: Path,
isabelle_other: Path,
isabelle_identifier: String = "remote_build_history",
progress: Progress = new Progress,
protect_args: Boolean = false,
rev: String = "",
afp_repos: Option[Path] = None,
afp_rev: String = "",
options: String = "",
args: String = "",
no_build: Boolean = false
): List[(String, Bytes)] = {
/* synchronize Isabelle + AFP repositories */
def sync(target: Path, accurate: Boolean = false,
rev: String = "", afp_rev: String = "", afp: Boolean = false
): Unit = {
val context =
Rsync.Context(progress, ssh_port = ssh.port, ssh_control_path = ssh.control_path,
protect_args = protect_args)
Sync.sync(ssh.options, context, ssh.rsync_path(target),
thorough = accurate, preserve_jars = !accurate,
rev = rev, afp_rev = afp_rev, afp_root = if (afp) afp_repos else None)
}
def execute(command: String, args: String,
echo: Boolean = false,
strict: Boolean = true
): Unit =
ssh.execute(
Isabelle_System.export_isabelle_identifier(isabelle_identifier) +
ssh.bash_path(isabelle_self + Path.explode(command)) + " " + args,
progress_stdout = progress.echo_if(echo, _),
progress_stderr = progress.echo_if(echo, _),
strict = strict).check
sync(isabelle_self)
execute("bin/isabelle", "components -I")
execute("bin/isabelle", "components -a", echo = true)
execute("bin/isabelle", "jedit -bf")
sync(isabelle_other, accurate = true,
rev = proper_string(rev) getOrElse "tip",
afp_rev = proper_string(afp_rev) getOrElse "tip",
afp = true)
/* build */
if (no_build) Nil
else {
ssh.with_tmp_dir { tmp_dir =>
val output_file = tmp_dir + Path.explode("output")
val build_options = (if (afp_repos.isEmpty) "" else " -A") + " " + options
try {
execute("Admin/build_other",
"-o " + ssh.bash_path(output_file) + build_options + " " +
ssh.bash_path(isabelle_other) + " " + args,
echo = true, strict = false)
}
catch {
case ERROR(msg) =>
cat_error(msg, "The error(s) above occurred for Admin/build_other " + build_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,964 +1,954 @@
/* Title: Pure/Admin/build_release.scala
Author: Makarius
Build full Isabelle distribution from repository.
*/
package isabelle
object Build_Release {
/** release context **/
private def execute(dir: Path, script: String): Unit =
Isabelle_System.bash(script, cwd = dir.file).check
private def execute_tar(dir: Path, args: String, strip: Boolean = false): Process_Result =
Isabelle_System.gnutar(args, dir = dir, strip = strip).check
private def bash_java_opens(args: String*): String =
Bash.strings(args.toList.flatMap(arg => List("--add-opens", arg + "=ALL-UNNAMED")))
object Release_Context {
def apply(
target_dir: Path,
release_name: String = "",
- components_base: Path = Components.default_components_base,
progress: Progress = new Progress
): Release_Context = {
val date = Date.now()
val dist_name = proper_string(release_name) getOrElse ("Isabelle_" + Date.Format.date(date))
val dist_dir = (target_dir + Path.explode("dist-" + dist_name)).absolute
- new Release_Context(release_name, dist_name, dist_dir, components_base, progress)
+ new Release_Context(release_name, dist_name, dist_dir, progress)
}
}
class Release_Context private[Build_Release](
val release_name: String,
val dist_name: String,
val dist_dir: Path,
- val components_base: Path,
val progress: Progress
) {
override def toString: String = dist_name
val isabelle: Path = Path.explode(dist_name)
val isabelle_dir: Path = dist_dir + isabelle
val isabelle_archive: Path = dist_dir + isabelle.tar.gz
val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz")
def other_isabelle(dir: Path, suffix: String = "-build"): Other_Isabelle =
Other_Isabelle(dir + isabelle,
isabelle_identifier = dist_name + suffix,
progress = progress)
def make_announce(id: String): Unit = {
if (release_name.isEmpty) {
File.write(isabelle_dir + Path.explode("ANNOUNCE"),
"""
IMPORTANT NOTE
==============
This is a snapshot of Isabelle/""" + id + """ from the repository.
""")
}
}
def make_contrib(): Unit = {
Isabelle_System.make_directory(Components.contrib(isabelle_dir))
File.write(Components.contrib(isabelle_dir, name = "README"),
"""This directory contains add-on components that contribute to the main
Isabelle distribution. Separate licensing conditions apply, see each
directory individually.
""")
}
def bundle_info(platform: Platform.Family.Value): Bundle_Info =
platform match {
case Platform.Family.linux_arm =>
Bundle_Info(platform, "Linux (ARM)", dist_name + "_linux_arm.tar.gz")
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")
}
}
sealed case class Bundle_Info(
platform: Platform.Family.Value,
platform_description: String,
name: String
) {
def path: Path = Path.explode(name)
}
/** release archive **/
val ISABELLE: Path = Path.basic("Isabelle")
val ISABELLE_ID: Path = Path.explode("etc/ISABELLE_ID")
val ISABELLE_TAGS: Path = Path.explode("etc/ISABELLE_TAGS")
val ISABELLE_IDENTIFIER: Path = Path.explode("etc/ISABELLE_IDENTIFIER")
object Release_Archive {
def make(bytes: Bytes, rename: String = ""): Release_Archive = {
Isabelle_System.with_tmp_dir("build_release")(dir =>
Isabelle_System.with_tmp_file("archive", ext = "tar.gz") { archive_path =>
val isabelle_dir = Isabelle_System.make_directory(dir + ISABELLE)
Bytes.write(archive_path, bytes)
execute_tar(isabelle_dir, "-xzf " + File.bash_path(archive_path), strip = true)
val id = File.read(isabelle_dir + ISABELLE_ID)
val tags = File.read(isabelle_dir + ISABELLE_TAGS)
val identifier = File.read(isabelle_dir + ISABELLE_IDENTIFIER)
val (bytes1, identifier1) =
if (rename.isEmpty || rename == identifier) (bytes, identifier)
else {
File.write(isabelle_dir + ISABELLE_IDENTIFIER, rename)
Isabelle_System.move_file(isabelle_dir, dir + Path.basic(rename))
execute_tar(dir, "-czf " + File.bash_path(archive_path) + " " + Bash.string(rename))
(Bytes.read(archive_path), rename)
}
new Release_Archive(bytes1, id, tags, identifier1)
}
)
}
def read(path: Path, rename: String = ""): Release_Archive =
make(Bytes.read(path), rename = rename)
def get(
url: String,
rename: String = "",
progress: Progress = new Progress
): Release_Archive = {
val bytes =
if (Path.is_wellformed(url)) Bytes.read(Path.explode(url))
else Isabelle_System.download(url, progress = progress).bytes
make(bytes, rename = rename)
}
}
case class Release_Archive private[Build_Release](
bytes: Bytes, id: String, tags: String, identifier: String) {
override def toString: String = identifier
}
/** generated content **/
/* 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())) :::
Platform.Family.list.flatMap(platform =>
List(platform.toString, "bundled-" + platform.toString).
map((_, new Bundled(platform = Some(platform)))))
File.append(Components.Directory(dir).components,
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("#")
} 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.Directory(dir).read_components() } 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))
val component_dir = Components.Directory(dir)
component_dir.write_components(
component_dir.read_components().flatMap(line =>
line match {
case Bundled(name) =>
if (Components.Directory(Components.contrib(dir, name)).ok) Some(contrib_name(name))
else None
case _ => if (Bundled.detect(line)) None else Some(line)
}) ::: more_names.map(contrib_name))
}
/** build release **/
/* build heaps */
private def build_heaps(
options: Options,
platform: Platform.Family.Value,
build_sessions: List[String],
local_dir: Path,
progress: Progress = new Progress,
): Unit = {
val server_option = "build_host_" + platform.toString
val server = options.string(server_option)
progress.echo("Building heaps for " + commas_quote(build_sessions) +
" (" + server_option + " = " + quote(server) + ") ...")
val ssh =
if (server.nonEmpty) SSH.open_session(options, server)
else if (Platform.family == platform) SSH.Local
else error("Undefined option " + server_option + ": cannot build heaps")
try {
Isabelle_System.with_tmp_file("tmp", ext = "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 build_command =
"bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions)
def system_apple(b: Boolean): String =
"""{ echo "ML_system_apple = """ + b + """" > "$(bin/isabelle getenv -b ISABELLE_HOME_USER)/etc/preferences"; }"""
val build_script =
List(
"cd " + File.bash_path(remote_dir),
"tar -xf tmp.tar",
"""mkdir -p "$(bin/isabelle getenv -b ISABELLE_HOME_USER)/etc" """,
system_apple(false),
build_command,
system_apple(true),
build_command,
"tar -cf tmp.tar heaps")
ssh.execute(build_script.mkString(" && "), settings = false).check
ssh.read_file(remote_tmp_tar, local_tmp_tar)
}
execute_tar(local_dir, "-xvf " + File.bash_path(local_tmp_tar))
.out_lines.sorted.foreach(progress.echo)
}
}
finally { ssh.close() }
}
/* 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=($(grep -v '^#' "$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.jedit.JEdit_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.Family.standard(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
""")
}
/* NEWS */
private def make_news(other_isabelle: Other_Isabelle): Unit = {
val news_file = other_isabelle.isabelle_home + Path.explode("NEWS")
val doc_dir = other_isabelle.isabelle_home + Path.explode("doc")
val fonts_dir = Isabelle_System.make_directory(doc_dir + Path.explode("fonts"))
Isabelle_Fonts.make_entries(getenv = other_isabelle.getenv, hidden = true).
foreach(entry => Isabelle_System.copy_file(entry.path, fonts_dir))
HTML.write_document(doc_dir, "NEWS.html",
List(HTML.title("NEWS")),
List(
HTML.chapter("NEWS"),
HTML.source(Symbol.decode(File.read(news_file)))))
}
/* main */
def use_release_archive(
context: Release_Context,
archive: Release_Archive,
id: String = ""
): Unit = {
if (id.nonEmpty && id != archive.id) {
error("Mismatch of release identification " + id + " vs. archive " + archive.id)
}
if (!context.isabelle_archive.is_file || Bytes.read(context.isabelle_archive) != archive.bytes) {
Bytes.write(context.isabelle_archive, archive.bytes)
}
}
def build_release_archive(
context: Release_Context,
version: String,
parallel_jobs: Int = 1
): Unit = {
val progress = context.progress
val hg = Mercurial.self_repository()
val id =
try { hg.id(version) }
catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) }
if (context.isabelle_archive.is_file) {
progress.echo_warning("Found existing release archive: " + context.isabelle_archive)
use_release_archive(context, Release_Archive.read(context.isabelle_archive), id = id)
}
else {
progress.echo_warning("Preparing release " + context.dist_name + " ...")
Isabelle_System.new_directory(context.dist_dir)
hg.archive(File.standard_path(context.isabelle_dir), rev = id)
for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) {
(context.isabelle_dir + Path.explode(name)).file.delete
}
File.write(context.isabelle_dir + ISABELLE_ID, id)
File.write(context.isabelle_dir + ISABELLE_TAGS, hg.tags(rev = id))
File.write(context.isabelle_dir + ISABELLE_IDENTIFIER, context.dist_name)
context.make_announce(id)
context.make_contrib()
execute(context.isabelle_dir, """find . -print | xargs chmod -f u+rw""")
record_bundled_components(context.isabelle_dir)
/* build tools and documentation */
val other_isabelle = context.other_isabelle(context.dist_dir)
- other_isabelle.init_settings(
- other_isabelle.init_components(components_base = context.components_base))
+ other_isabelle.init_settings(other_isabelle.init_components())
other_isabelle.resolve_components(echo = true)
other_isabelle.scala_build(echo = true)
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)
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 release archive " + context.isabelle_archive + " ...")
execute(context.dist_dir, """chmod -R a+r . && chmod -R u+w . && chmod -R g=o .""")
execute(context.dist_dir,
"""find . -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w""")
execute_tar(context.dist_dir, "-czf " +
File.bash_path(context.isabelle_archive) + " " + Bash.string(context.dist_name))
}
}
def default_platform_families: List[Platform.Family.Value] = Platform.Family.list0
def build_release(
options: Options,
context: Release_Context,
afp_rev: String = "",
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
): Unit = {
val progress = context.progress
/* release directory */
val archive = Release_Archive.read(context.isabelle_archive)
for (path <- List(context.isabelle, ISABELLE)) {
Isabelle_System.rm_tree(context.dist_dir + path)
}
Isabelle_System.with_tmp_file("archive", ext = "tar.gz") { archive_path =>
Bytes.write(archive_path, archive.bytes)
val extract =
List("README", "NEWS", "ANNOUNCE", "COPYRIGHT", "CONTRIBUTORS", "doc").
map(name => context.dist_name + "/" + name)
execute_tar(context.dist_dir,
"-xzf " + File.bash_path(archive_path) + " " + Bash.strings(extract))
}
Isabelle_System.symlink(Path.explode(context.dist_name), context.dist_dir + ISABELLE)
/* make application bundles */
val bundle_infos = platform_families.map(context.bundle_info)
for (bundle_info <- bundle_infos) {
val isabelle_name = context.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(context.isabelle_archive))
val other_isabelle = context.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)
for (name <- bundled_components) {
- Components.resolve(context.components_base, name,
+ Components.resolve(Components.default_components_base, name,
target_dir = Some(contrib_dir),
copy_dir = Some(context.dist_dir + Path.explode("contrib")),
progress = progress)
}
val more_components_names =
more_components.map(Components.unpack(contrib_dir, _, progress = progress))
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
val classpath1 = Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH"))
val classpath2 = Path.split(other_isabelle.getenv("ISABELLE_SETUP_CLASSPATH"))
(classpath1 ::: classpath2).map { path =>
val abs_path = path.absolute
File.relative_path(base, abs_path) match {
case Some(rel_path) => rel_path
case None => error("Bad classpath element: " + abs_path)
}
}
}
val jedit_options = Path.explode("src/Tools/jEdit/etc/options")
val jedit_props =
Path.explode(other_isabelle.getenv("JEDIT_HOME") + "/properties/jEdit.props")
// build heaps
if (build_sessions.nonEmpty) {
build_heaps(options, platform, build_sessions, isabelle_target, progress = progress)
}
// application bundling
Components.purge(contrib_dir, platform)
platform match {
case Platform.Family.linux_arm | 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)
progress.echo("Packaging " + bundle_info.name + " ...")
execute_tar(tmp_dir,
"-czf " + File.bash_path(context.dist_dir + bundle_info.path) + " " +
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, archive.id)
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
progress.echo("Packaging " + bundle_info.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(context.dist_dir + bundle_info.path) + " " +
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 = bundle_info.path
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 + "\\"))
val java_opts =
bash_java_opens(
"java.base/java.io",
"java.base/java.lang",
"java.base/java.lang.reflect",
"java.base/java.text",
"java.base/java.util",
"java.desktop/java.awt.font")
val launch4j_jar =
Path.explode("windows_app/launch4j-" + Platform.family + "/launch4j.jar")
execute(tmp_dir,
cat_lines(List(
"export LAUNCH4J=" + File.bash_platform_path(launch4j_jar),
"isabelle java " + java_opts + " -jar \"$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(context.dist_dir + isabelle_exe,
Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
File.set_executable(context.dist_dir + isabelle_exe, true)
}
other_isabelle.cleanup()
}
progress.echo("DONE")
}
/* minimal website */
for (dir <- website) {
val website_platform_bundles =
for {
bundle_info <- bundle_infos
if (context.dist_dir + bundle_info.path).is_file
} yield (bundle_info.name, bundle_info)
val isabelle_link =
HTML.link(Isabelle_System.isabelle_repository.changeset(archive.id),
HTML.text("Isabelle/" + archive.id))
val afp_link =
HTML.link(Isabelle_System.afp_repository.changeset(afp_rev),
HTML.text("AFP/" + afp_rev))
HTML.write_document(dir, "index.html",
List(HTML.title(context.dist_name)),
List(
HTML.section(context.dist_name),
HTML.subsection("Downloads"),
HTML.itemize(
List(HTML.link(context.dist_name + ".tar.gz", HTML.text("Source archive"))) ::
website_platform_bundles.map({ case (bundle, bundle_info) =>
List(HTML.link(bundle, HTML.text(bundle_info.platform_description + " bundle"))) })),
HTML.subsection("Repositories"),
HTML.itemize(
List(List(isabelle_link)) ::: (if (afp_rev == "") Nil else List(List(afp_link))))))
Isabelle_System.copy_file(context.isabelle_archive, dir)
for ((bundle, _) <- website_platform_bundles) {
Isabelle_System.copy_file(context.dist_dir + Path.explode(bundle), dir)
}
}
/* HTML library */
if (build_library) {
if (context.isabelle_library_archive.is_file) {
progress.echo_warning("Library archive already exists: " + context.isabelle_library_archive)
}
else {
Isabelle_System.with_tmp_dir("build_release") { tmp_dir =>
val bundle =
context.dist_dir + Path.explode(context.dist_name + "_" + Platform.family + ".tar.gz")
execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
val other_isabelle = context.other_isabelle(tmp_dir, suffix = "")
Isabelle_System.make_directory(other_isabelle.etc)
File.write(other_isabelle.etc_settings, "ML_OPTIONS=\"--minheap 1000 --maxheap 4000\"\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(context.dist_name))
execute(tmp_dir, "chmod -R g=o " + Bash.string(context.dist_name))
execute_tar(tmp_dir, "-czf " + File.bash_path(context.isabelle_library_archive) +
" " + Bash.string(context.dist_name + "/browser_info"))
}
}
}
}
/** 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 release_name = ""
var source_archive = ""
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]
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 explicit release name
-S ARCHIVE use existing source archive (file or URL)
-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: """ + quote(default_platform_families.mkString(",")) + """)
-r REV Mercurial changeset id (default: ARCHIVE or 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 => release_name = arg),
"S:" -> (arg => source_archive = 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()
if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
error("Building for windows requires 7z")
val progress = new Console_Progress()
def make_context(name: String): Release_Context =
- Release_Context(target_dir,
- release_name = name,
- components_base = components_base,
- progress = progress)
+ Release_Context(target_dir, release_name = name, progress = progress)
val context =
if (source_archive.isEmpty) {
val context = make_context(release_name)
val version = proper_string(rev) orElse proper_string(release_name) getOrElse "tip"
build_release_archive(context, version, parallel_jobs = parallel_jobs)
context
}
else {
val archive =
Release_Archive.get(source_archive, rename = release_name, progress = progress)
val context = make_context(archive.identifier)
Isabelle_System.make_directory(context.dist_dir)
use_release_archive(context, archive, id = rev)
context
}
build_release(options, context, afp_rev = afp_rev, platform_families = platform_families,
more_components = more_components, build_sessions = build_sessions,
build_library = build_library, parallel_jobs = parallel_jobs, website = website)
}
}
}
diff --git a/src/Pure/Admin/other_isabelle.scala b/src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala
+++ b/src/Pure/Admin/other_isabelle.scala
@@ -1,136 +1,133 @@
/* Title: Pure/Admin/other_isabelle.scala
Author: Makarius
Manage other Isabelle distributions: support historic versions starting from
tag "build_history_base".
*/
package isabelle
object Other_Isabelle {
def apply(
isabelle_home: Path,
isabelle_identifier: String = "",
progress: Progress = new Progress
): Other_Isabelle = {
if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) {
error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT")
}
new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, progress)
}
}
final class Other_Isabelle private(
val isabelle_home: Path,
val isabelle_identifier: String,
progress: Progress
) {
override def toString: String = isabelle_home.toString
/* static system */
def bash(
script: String,
redirect: Boolean = false,
echo: Boolean = false,
strict: Boolean = true
): Process_Result = {
progress.bash(
Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict)
}
def getenv(name: String): String =
bash("bin/isabelle getenv -b " + Bash.string(name)).check.out
val settings: Isabelle_System.Settings = (name: String) => getenv(name)
def expand_path(path: Path): Path = path.expand_env(settings)
def bash_path(path: Path): String = Bash.string(expand_path(path).implode)
val isabelle_home_user: Path = expand_path(Path.explode("$ISABELLE_HOME_USER"))
def etc: Path = isabelle_home_user + Path.explode("etc")
def etc_settings: Path = etc + Path.explode("settings")
def etc_preferences: Path = etc + Path.explode("preferences")
def resolve_components(echo: Boolean = false): Unit = {
val missing = Path.split(getenv("ISABELLE_COMPONENTS_MISSING"))
for (path <- missing) {
Components.resolve(path.dir, path.file_name,
progress = if (echo) progress else new Progress)
}
}
def scala_build(fresh: Boolean = false, echo: Boolean = false): Unit = {
if (fresh) {
Isabelle_System.rm_tree(isabelle_home + Path.explode("lib/classes"))
}
val dummy_stty = Path.explode("~~/lib/dummy_stty/stty")
if (!expand_path(dummy_stty).is_file) {
Isabelle_System.copy_file(dummy_stty,
Isabelle_System.make_directory(expand_path(dummy_stty.dir)))
}
try {
bash(
"export PATH=\"" + bash_path(dummy_stty.dir) + ":$PATH\"\n" +
"export CLASSPATH=" + Bash.string(getenv("ISABELLE_CLASSPATH")) + "\n" +
"bin/isabelle jedit -b", echo = echo).check
}
catch { case ERROR(msg) => cat_error("Failed to build Isabelle/Scala/Java modules:", msg) }
}
/* components */
def init_components(
component_repository: String = Components.default_component_repository,
- components_base: Path = Components.default_components_base,
catalogs: List[String] = Components.default_catalogs,
components: List[String] = Nil
): List[String] = {
- val dir = Components.admin(isabelle_home)
+ val admin = Components.admin(Path.ISABELLE_HOME).implode
+ val components_base = quote("${ISABELLE_COMPONENTS_BASE:-$USER_HOME/.isabelle/contrib}")
("ISABELLE_COMPONENT_REPOSITORY=" + Bash.string(component_repository)) ::
- catalogs.map(name =>
- "init_components " + File.bash_path(components_base) + " " +
- File.bash_path(dir + Path.basic(name))) :::
- components.map(name =>
- "init_component " + File.bash_path(components_base + Path.basic(name)))
+ catalogs.map(name => "init_components " + components_base + " " + quote(admin + "/" + name)) :::
+ components.map(name => "init_component " + components_base + "/" + name)
}
/* settings */
def clean_settings(): Boolean =
if (!etc_settings.is_file) true
else if (File.read(etc_settings).startsWith("# generated by Isabelle")) {
etc_settings.file.delete
true
}
else false
def init_settings(settings: List[String]): Unit = {
if (clean_settings()) {
Isabelle_System.make_directory(etc_settings.dir)
File.write(etc_settings,
"# generated by Isabelle " + Date.now() + "\n" +
"#-*- shell-script -*- :mode=shellscript:\n" +
settings.mkString("\n", "\n", "\n"))
}
else error("Cannot proceed with existing user settings file: " + etc_settings)
}
/* cleanup */
def cleanup(): Unit = {
clean_settings()
etc.file.delete
isabelle_home_user.file.delete
}
}
diff --git a/src/Pure/System/components.scala b/src/Pure/System/components.scala
--- a/src/Pure/System/components.scala
+++ b/src/Pure/System/components.scala
@@ -1,387 +1,386 @@
/* Title: Pure/System/components.scala
Author: Makarius
Isabelle system components.
*/
package isabelle
import java.io.{File => JFile}
object Components {
/* archive name */
object Archive {
val suffix: String = ".tar.gz"
def apply(name: String): String =
if (name == "") error("Bad component name: " + quote(name))
else name + suffix
def unapply(archive: String): Option[String] = {
for {
name0 <- Library.try_unsuffix(suffix, archive)
name <- proper_string(name0)
} yield name
}
def get_name(archive: String): String =
unapply(archive) getOrElse
error("Bad component archive name (expecting .tar.gz): " + quote(archive))
}
/* component collections */
def default_component_repository: String =
Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY")
val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE")
- val standard_components_base: Path = Path.explode("$USER_HOME/.isabelle/contrib")
val default_catalogs: List[String] = List("main")
val optional_catalogs: List[String] = List("main", "optional")
def admin(dir: Path): Path = dir + Path.explode("Admin/components")
def contrib(dir: Path = Path.current, name: String = ""): Path =
dir + Path.explode("contrib") + Path.explode(name)
def unpack(
dir: Path,
archive: Path,
ssh: SSH.System = SSH.Local,
progress: Progress = new Progress
): String = {
val name = Archive.get_name(archive.file_name)
progress.echo("Unpacking " + name)
ssh.execute(
"tar -C " + ssh.bash_path(dir) + " -x -z -f " + ssh.bash_path(archive),
progress_stdout = progress.echo,
progress_stderr = progress.echo).check
name
}
def resolve(
base_dir: Path,
name: String,
target_dir: Option[Path] = None,
copy_dir: Option[Path] = None,
component_repository: String = Components.default_component_repository,
ssh: SSH.System = SSH.Local,
progress: Progress = new Progress
): Unit = {
ssh.make_directory(base_dir)
val archive_name = Archive(name)
val archive = base_dir + Path.basic(archive_name)
if (!ssh.is_file(archive)) {
val remote = Url.append_path(component_repository, archive_name)
ssh.download_file(remote, archive, progress = progress)
}
for (dir <- copy_dir) {
ssh.make_directory(dir)
ssh.copy_file(archive, dir)
}
unpack(target_dir getOrElse base_dir, archive, ssh = ssh, progress = progress)
}
private val platforms_family: Map[Platform.Family.Value, Set[String]] =
Map(
Platform.Family.linux_arm -> Set("arm64-linux", "arm64_32-linux"),
Platform.Family.linux -> Set("x86_64-linux", "x86_64_32-linux"),
Platform.Family.macos ->
Set("arm64-darwin", "arm64_32-darwin", "x86_64-darwin", "x86_64_32-darwin"),
Platform.Family.windows ->
Set("x86_64-cygwin", "x86_64-windows", "x86_64_32-windows", "x86-windows"))
private val platforms_all: Set[String] =
Set("x86-linux", "x86-cygwin") ++ platforms_family.iterator.flatMap(_._2)
def purge(dir: Path, platform: Platform.Family.Value): Unit = {
val purge_set = platforms_all -- platforms_family(platform)
File.find_files(dir.file,
(file: JFile) => file.isDirectory && purge_set(file.getName),
include_dirs = true).foreach(Isabelle_System.rm_tree)
}
/* component directories */
def directories(): List[Path] =
Path.split(Isabelle_System.getenv_strict("ISABELLE_COMPONENTS"))
/* component directory content */
object Directory {
def apply(path: Path): Directory = new Directory(path.absolute)
}
class Directory private(val path: Path) {
override def toString: String = path.toString
def etc: Path = path + Path.basic("etc")
def src: Path = path + Path.basic("src")
def lib: Path = path + Path.basic("lib")
def settings: Path = etc + Path.basic("settings")
def components: Path = etc + Path.basic("components")
def build_props: Path = etc + Path.basic("build.props")
def README: Path = path + Path.basic("README")
def LICENSE: Path = path + Path.basic("LICENSE")
def create(progress: Progress = new Progress): Directory = {
progress.echo("Creating component directory " + path)
Isabelle_System.new_directory(path)
Isabelle_System.make_directory(etc)
this
}
def ok: Boolean = settings.is_file || components.is_file || Sessions.is_session_dir(path)
def check: Directory =
if (!path.is_dir) error("Bad component directory: " + path)
else if (!ok) {
error("Malformed component directory: " + path +
"\n (missing \"etc/settings\" or \"etc/components\" or \"ROOT\" or \"ROOTS\")")
}
else this
def read_components(): List[String] =
split_lines(File.read(components)).filter(_.nonEmpty)
def write_components(lines: List[String]): Unit =
File.write(components, terminate_lines(lines))
def write_settings(text: String): Unit =
File.write(settings, "# -*- shell-script -*- :mode=shellscript:\n" + text)
}
/* component repository content */
val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1")
sealed case class SHA1_Digest(digest: SHA1.Digest, name: String) {
override def toString: String = digest.shasum(name)
}
def read_components_sha1(lines: List[String] = Nil): List[SHA1_Digest] =
(proper_list(lines) getOrElse split_lines(File.read(components_sha1))).flatMap(line =>
Word.explode(line) match {
case Nil => None
case List(sha1, name) => Some(SHA1_Digest(SHA1.fake_digest(sha1), name))
case _ => error("Bad components.sha1 entry: " + quote(line))
})
def write_components_sha1(entries: List[SHA1_Digest]): Unit =
File.write(components_sha1, entries.sortBy(_.name).mkString("", "\n", "\n"))
/** manage user components **/
val components_path: Path = Path.explode("$ISABELLE_HOME_USER/etc/components")
def read_components(): List[String] =
if (components_path.is_file) Library.trim_split_lines(File.read(components_path))
else Nil
def write_components(lines: List[String]): Unit = {
Isabelle_System.make_directory(components_path.dir)
File.write(components_path, Library.terminate_lines(lines))
}
def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = {
val path = path0.expand.absolute
if (add) Directory(path).check
val lines1 = read_components()
val lines2 =
lines1.filter(line =>
line.isEmpty || line.startsWith("#") || !File.eq(Path.explode(line), path))
val lines3 = if (add) lines2 ::: List(path.implode) else lines2
if (lines1 != lines3) write_components(lines3)
val prefix = if (lines1 == lines3) "Unchanged" else if (add) "Added" else "Removed"
progress.echo(prefix + " component " + path)
}
/* main entry point */
def main(args: Array[String]): Unit = {
Command_Line.tool {
for (arg <- args) {
val add =
if (arg.startsWith("+")) true
else if (arg.startsWith("-")) false
else error("Bad argument: " + quote(arg))
val path = Path.explode(arg.substring(1))
update_components(add, path, progress = new Console_Progress)
}
}
}
/** build and publish components **/
def build_components(
options: Options,
components: List[Path],
progress: Progress = new Progress,
publish: Boolean = false,
force: Boolean = false,
update_components_sha1: Boolean = false
): Unit = {
val archives: List[Path] =
for (path <- components) yield {
path.file_name match {
case Archive(_) => path
case name =>
Directory(path).check
val component_path = path.expand
val archive_dir = component_path.dir
val archive_name = Archive(name)
val archive = archive_dir + Path.explode(archive_name)
if (archive.is_file && !force) {
error("Component archive already exists: " + archive)
}
progress.echo("Packaging " + archive_name)
Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name),
dir = archive_dir).check
archive
}
}
if ((publish && archives.nonEmpty) || update_components_sha1) {
val server = options.string("isabelle_components_server")
if (server.isEmpty) error("Undefined option isabelle_components_server")
using(SSH.open_session(options, server)) { ssh =>
val components_dir = Path.explode(options.string("isabelle_components_dir"))
val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir"))
for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) {
error("Bad remote directory: " + dir)
}
if (publish) {
for (archive <- archives) {
val archive_name = archive.file_name
val name = Archive.get_name(archive_name)
val remote_component = components_dir + archive.base
val remote_contrib = contrib_dir + Path.explode(name)
// component archive
if (ssh.is_file(remote_component) && !force) {
error("Remote component archive already exists: " + remote_component)
}
progress.echo("Uploading " + archive_name)
ssh.write_file(remote_component, archive)
// contrib directory
val is_standard_component =
Isabelle_System.with_tmp_dir("component") { tmp_dir =>
Isabelle_System.extract(archive, tmp_dir)
Directory(tmp_dir + Path.explode(name)).ok
}
if (is_standard_component) {
if (ssh.is_dir(remote_contrib)) {
if (force) ssh.rm_tree(remote_contrib)
else error("Remote component directory already exists: " + remote_contrib)
}
progress.echo("Unpacking remote " + archive_name)
ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " +
ssh.bash_path(remote_component)).check
}
else {
progress.echo_warning("No unpacking of non-standard component: " + archive_name)
}
}
}
// remote SHA1 digests
if (update_components_sha1) {
val lines =
for {
entry <- ssh.read_dir(components_dir)
if ssh.is_file(components_dir + Path.basic(entry)) &&
entry.endsWith(Archive.suffix)
}
yield {
progress.echo("Digesting remote " + entry)
ssh.execute("cd " + ssh.bash_path(components_dir) +
"; sha1sum " + Bash.string(entry)).check.out
}
write_components_sha1(read_components_sha1(lines))
}
}
}
// local SHA1 digests
{
val new_entries =
for (archive <- archives)
yield {
val name = archive.file_name
progress.echo("Digesting local " + name)
SHA1_Digest(SHA1.digest(archive), name)
}
val new_names = new_entries.map(_.name).toSet
write_components_sha1(
new_entries :::
read_components_sha1().filterNot(entry => new_names.contains(entry.name)))
}
}
/* Isabelle tool wrapper */
private val relevant_options =
List("isabelle_components_server", "isabelle_components_dir", "isabelle_components_contrib_dir")
val isabelle_tool =
Isabelle_Tool("build_components", "build and publish Isabelle components",
Scala_Project.here,
{ args =>
var publish = false
var update_components_sha1 = false
var force = false
var options = Options.init()
def show_options: String =
cat_lines(relevant_options.flatMap(options.get).map(_.print))
val getopts = Getopts("""
Usage: isabelle build_components [OPTIONS] ARCHIVES... DIRS...
Options are:
-P publish on SSH server (see options below)
-f force: overwrite existing component archives and directories
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-u update all SHA1 keys in Isabelle repository Admin/components
Build and publish Isabelle components as .tar.gz archives on SSH server,
depending on system options:
""" + Library.indent_lines(2, show_options) + "\n",
"P" -> (_ => publish = true),
"f" -> (_ => force = true),
"o:" -> (arg => options = options + arg),
"u" -> (_ => update_components_sha1 = true))
val more_args = getopts(args)
if (more_args.isEmpty && !update_components_sha1) getopts.usage()
val progress = new Console_Progress
build_components(options, more_args.map(Path.explode), progress = progress,
publish = publish, force = force, update_components_sha1 = update_components_sha1)
})
}