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_System.isabelle_repository,
- afp_repos_source: String = Isabelle_System.afp_repository,
+ isabelle_repository: Mercurial.Address = Isabelle_System.isabelle_repository,
+ afp_repository: Mercurial.Address = 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)
+ Mercurial.setup_repository(isabelle_repository, 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)
+ Mercurial.setup_repository(afp_repository, 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_System.isabelle_repository + "/rev/" + release.ident,
+ HTML.link(Isabelle_System.isabelle_repository.rev(release.ident),
HTML.text("Isabelle/" + release.ident))
val afp_link =
- HTML.link(Isabelle_System.afp_repository + "/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/General/mercurial.scala b/src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala
+++ b/src/Pure/General/mercurial.scala
@@ -1,367 +1,381 @@
/* Title: Pure/General/mercurial.scala
Author: Makarius
Support for Mercurial repositories, with local or remote repository clone
and working directory (via ssh connection).
*/
package isabelle
-import java.io.{File => JFile}
-
import scala.annotation.tailrec
import scala.collection.mutable
object Mercurial
{
type Graph = isabelle.Graph[String, Unit]
+ /* HTTP server addresses */
+
+ object Address
+ {
+ def apply(root: String): Address = new Address(root)
+ }
+
+ final class Address private(val root: String)
+ {
+ override def toString: String = root
+
+ def rev(r: String): String = root + "/rev/" + r
+ }
+
+
/* command-line syntax */
def optional(s: String, prefix: String = ""): String =
if (s == "") "" else " " + prefix + " " + Bash.string(s)
def opt_flag(flag: String, b: Boolean): String = if (b) " " + flag else ""
def opt_rev(s: String): String = optional(s, "--rev")
def opt_template(s: String): String = optional(s, "--template")
/* repository archives */
private val Archive_Node = """^node: (\S{12}).*$""".r
private val Archive_Tag = """^tag: (\S+).*$""".r
sealed case class Archive_Info(lines: List[String])
{
def id: Option[String] = lines.collectFirst({ case Archive_Node(a) => a })
def tags: List[String] = for (Archive_Tag(tag) <- lines if tag != "tip") yield tag
}
def archive_info(root: Path): Option[Archive_Info] =
{
val path = root + Path.explode(".hg_archival.txt")
if (path.is_file) Some(Archive_Info(Library.trim_split_lines(File.read(path)))) else None
}
def archive_id(root: Path): Option[String] =
archive_info(root).flatMap(_.id)
def archive_tags(root: Path): Option[String] =
archive_info(root).map(info => info.tags.mkString(" "))
/* repository access */
def is_repository(root: Path, ssh: SSH.System = SSH.Local): Boolean =
ssh.is_dir(root + Path.explode(".hg")) &&
new Repository(root, ssh).command("root").ok
def repository(root: Path, ssh: SSH.System = SSH.Local): Repository =
{
val hg = new Repository(root, ssh)
hg.command("root").check
hg
}
def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] =
{
@tailrec def find(root: Path): Option[Repository] =
if (is_repository(root, ssh)) Some(repository(root, ssh = ssh))
else if (root.is_root) None
else find(root + Path.parent)
find(ssh.expand_path(start))
}
private def make_repository(root: Path, cmd: String, args: String, ssh: SSH.System = SSH.Local)
: Repository =
{
val hg = new Repository(root, ssh)
ssh.make_directory(hg.root.dir)
hg.command(cmd, args, repository = false).check
hg
}
def init_repository(root: Path, ssh: SSH.System = SSH.Local): Repository =
make_repository(root, "init", ssh.bash_path(root), ssh = ssh)
def clone_repository(source: String, root: Path,
rev: String = "", options: String = "", ssh: SSH.System = SSH.Local): Repository =
make_repository(root, "clone",
options + " " + Bash.string(source) + " " + ssh.bash_path(root) + opt_rev(rev), ssh = ssh)
- def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository =
+ def setup_repository(address: Address, root: Path, ssh: SSH.System = SSH.Local): Repository =
{
+ val source = address.root
if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
else clone_repository(source, root, options = "--noupdate", ssh = ssh)
}
class Repository private[Mercurial](root_path: Path, ssh: SSH.System = SSH.Local)
{
hg =>
val root: Path = ssh.expand_path(root_path)
def root_url: String = ssh.hg_url + root.implode
override def toString: String = ssh.hg_url + root.implode
def command(name: String, args: String = "", options: String = "",
repository: Boolean = true): Process_Result =
{
val cmdline =
"export LANG=C HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
(if (repository) " --repository " + ssh.bash_path(root) else "") +
" --noninteractive " + name + " " + options + " " + args
ssh.execute(cmdline)
}
def add(files: List[Path]): Unit =
hg.command("add", files.map(ssh.bash_path).mkString(" "))
def archive(target: String, rev: String = "", options: String = ""): Unit =
hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check
def heads(template: String = "{node|short}\n", options: String = ""): List[String] =
hg.command("heads", opt_template(template), options).check.out_lines
def identify(rev: String = "tip", options: String = ""): String =
hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse ""
def id(rev: String = "tip"): String = identify(rev, options = "-i")
def tags(rev: String = "tip"): String =
{
val result = identify(rev, options = "-t")
Library.space_explode(' ', result).filterNot(_ == "tip").mkString(" ")
}
def paths(args: String = "", options: String = ""): List[String] =
hg.command("paths", args = args, options = options).check.out_lines
def manifest(rev: String = "", options: String = ""): List[String] =
hg.command("manifest", opt_rev(rev), options).check.out_lines
def log(rev: String = "", template: String = "", options: String = ""): String =
hg.command("log", opt_rev(rev) + opt_template(template), options).check.out
def parent(): String = log(rev = "p1()", template = "{node|short}")
def push(
remote: String = "", rev: String = "", force: Boolean = false, options: String = ""): Unit =
{
hg.command("push", opt_rev(rev) + opt_flag("--force", force) + optional(remote), options).
check_rc(rc => rc == 0 | rc == 1)
}
def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
hg.command("pull", opt_rev(rev) + optional(remote), options).check
def update(
rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = ""): Unit =
{
hg.command("update",
opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check
}
def known_files(): List[String] =
hg.command("status", options = "--modified --added --clean --no-status").check.out_lines
def graph(): Graph =
{
val Node = """^node: (\w{12}) (\w{12}) (\w{12})""".r
val log_result =
log(template = """node: {node|short} {p1node|short} {p2node|short}\n""")
split_lines(log_result).foldLeft(Graph.string[Unit]) {
case (graph, Node(x, y, z)) =>
val deps = List(y, z).filterNot(s => s.forall(_ == '0'))
val graph1 = (x :: deps).foldLeft(graph)(_.default_node(_, ()))
deps.foldLeft(graph1)({ case (g, dep) => g.add_edge(dep, x) })
case (graph, _) => graph
}
}
}
/* check files */
def check_files(files: List[Path], ssh: SSH.System = SSH.Local): (List[Path], List[Path]) =
{
val outside = new mutable.ListBuffer[Path]
val unknown = new mutable.ListBuffer[Path]
@tailrec def check(paths: List[Path]): Unit =
{
paths match {
case path :: rest =>
find_repository(path, ssh) match {
case None => outside += path; check(rest)
case Some(hg) =>
val known =
hg.known_files().iterator.map(name =>
(hg.root + Path.explode(name)).canonical_file).toSet
if (!known(path.canonical_file)) unknown += path
check(rest.filterNot(p => known(p.canonical_file)))
}
case Nil =>
}
}
check(files)
(outside.toList, unknown.toList)
}
/* setup remote vs. local repository */
private def edit_hgrc(local_hg: Repository, path_name: String, source: String): Unit =
{
val hgrc = local_hg.root + Path.explode(".hg/hgrc")
def header(line: String): Boolean = line.startsWith("[paths]")
val Entry = """^(\S+)\s*=\s*(.*)$""".r
val new_entry = path_name + " = " + source
def commit(lines: List[String]): Boolean =
{
File.write(hgrc, cat_lines(lines))
true
}
val edited =
hgrc.is_file && {
val lines = split_lines(File.read(hgrc))
lines.count(header) == 1 && {
if (local_hg.paths(options = "-q").contains(path_name)) {
val old_source = local_hg.paths(args = path_name).head
val old_entry = path_name + ".old = " + old_source
val lines1 =
lines.map {
case Entry(a, b) if a == path_name && b == old_source =>
new_entry + "\n" + old_entry
case line => line
}
lines != lines1 && commit(lines1)
}
else {
val prefix = lines.takeWhile(line => !header(line))
val n = prefix.length
commit(prefix ::: List(lines(n), new_entry) ::: lines.drop(n + 1))
}
}
}
if (!edited) File.append(hgrc, "\n[paths]\n" + new_entry + "\n")
}
val default_path_name = "default"
def hg_setup(
remote: String,
local_path: Path,
remote_name: String = "",
path_name: String = default_path_name,
remote_exists: Boolean = false,
progress: Progress = new Progress): Unit =
{
/* local repository */
Isabelle_System.make_directory(local_path)
val repos_name =
proper_string(remote_name) getOrElse local_path.absolute.base.implode
val local_hg =
if (is_repository(local_path)) repository(local_path)
else init_repository(local_path)
progress.echo("Local repository " + local_hg.root.absolute)
/* remote repository */
val remote_url =
remote match {
case _ if remote.startsWith("ssh://") =>
val ssh_url = remote + "/" + repos_name
if (!remote_exists) {
try { local_hg.command("init", ssh_url, repository = false).check }
catch { case ERROR(msg) => progress.echo_warning(msg) }
}
ssh_url
case SSH.Target(user, host) =>
val phabricator = Phabricator.API(user, host)
var repos =
phabricator.get_repositories().find(r => r.short_name == repos_name) getOrElse {
if (remote_exists) {
error("Remote repository " +
quote(phabricator.hg_url + "/source/" + repos_name) + " expected to exist")
}
else phabricator.create_repository(repos_name, short_name = repos_name)
}
while (repos.importing) {
progress.echo("Awaiting remote repository ...")
Time.seconds(0.5).sleep
repos = phabricator.the_repository(repos.phid)
}
repos.ssh_url
case _ => error("Malformed remote specification " + quote(remote))
}
progress.echo("Remote repository " + quote(remote_url))
/* synchronize local and remote state */
progress.echo("Synchronizing ...")
edit_hgrc(local_hg, path_name, remote_url)
local_hg.pull(options = "-u")
local_hg.push(remote = remote_url)
}
val isabelle_tool =
Isabelle_Tool("hg_setup", "setup remote vs. local Mercurial repository",
Scala_Project.here, args =>
{
var remote_name = ""
var path_name = default_path_name
var remote_exists = false
val getopts = Getopts("""
Usage: isabelle hg_setup [OPTIONS] REMOTE LOCAL_DIR
Options are:
-n NAME remote repository name (default: base name of LOCAL_DIR)
-p PATH Mercurial path name (default: """ + quote(default_path_name) + """)
-r assume that remote repository already exists
Setup a remote vs. local Mercurial repository: REMOTE either refers to a
Phabricator server "user@host" or SSH file server "ssh://user@host/path".
""",
"n:" -> (arg => remote_name = arg),
"p:" -> (arg => path_name = arg),
"r" -> (_ => remote_exists = true))
val more_args = getopts(args)
val (remote, local_path) =
more_args match {
case List(arg1, arg2) => (arg1, Path.explode(arg2))
case _ => getopts.usage()
}
val progress = new Console_Progress
hg_setup(remote, local_path, remote_name = remote_name, path_name = path_name,
remote_exists = remote_exists, progress = progress)
})
}
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,627 +1,629 @@
/* 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 isabelle_repository: Mercurial.Address =
+ Mercurial.Address("https://isabelle.sketis.net/repos/isabelle")
- val afp_repository: String = "https://isabelle.sketis.net/repos/afp-devel"
+ val afp_repository: Mercurial.Address =
+ Mercurial.Address("https://isabelle.sketis.net/repos/afp-devel")
}