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.explode("$USER_HOME")
+ 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.explode("~~"), root))
- error("Repository coincides with ISABELLE_HOME=" + Path.explode("~~").expand)
+ if (File.eq(Path.ISABELLE_HOME, root))
+ error("Repository coincides with ISABELLE_HOME=" + Path.ISABELLE_HOME.expand)
for ((threads, _) <- multicore_list if threads < 1)
error("Bad threads value < 1: " + threads)
for ((_, processes) <- multicore_list if processes < 1)
error("Bad processes value < 1: " + processes)
if (heap < 100) error("Bad heap value < 100: " + heap)
if (max_heap.isDefined && max_heap.get < heap)
error("Bad max_heap value < heap: " + max_heap.get)
System.getenv("ISABELLE_SETTINGS_PRESENT") match {
case null | "" =>
case _ => error("Cannot run build_history within existing Isabelle settings environment")
}
/* checkout Isabelle + AFP repository */
def checkout(dir: Path, version: String): String =
{
val hg = Mercurial.repository(dir)
hg.update(rev = version, clean = true)
progress.echo_if(verbose, hg.log(version, options = "-l1"))
hg.id(rev = version)
}
val isabelle_version = checkout(root, rev)
val afp_repos = root + Path.explode("AFP")
val afp_version = afp_rev.map(checkout(afp_repos, _))
val (afp_build_args, afp_sessions) =
if (afp_rev.isEmpty) (Nil, Nil)
else {
val (opt, sessions) =
try {
val afp = AFP.init(options, afp_repos)
("-d", afp.partition(afp_partition))
} catch { case ERROR(_) => ("-D", Nil) }
(List(opt, "~~/AFP/thys"), sessions)
}
/* main */
val other_isabelle =
Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
user_home = user_home, progress = progress)
val build_host = proper_string(hostname) getOrElse Isabelle_System.hostname()
val build_history_date = Date.now()
val build_group_id = build_host + ":" + build_history_date.time.ms
var first_build = true
for ((threads, processes) <- multicore_list) yield
{
/* init settings */
val component_settings =
other_isabelle.init_components(
component_repository = component_repository,
components_base = components_base,
catalogs = List("main", "optional"))
other_isabelle.init_settings(component_settings ::: init_settings)
other_isabelle.resolve_components(echo = verbose)
val ml_platform =
augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings)
File.write(other_isabelle.etc_preferences, cat_lines(more_preferences))
val isabelle_output =
other_isabelle.isabelle_home_user + Path.explode("heaps") +
Path.explode(other_isabelle.getenv("ML_IDENTIFIER"))
val isabelle_output_log = isabelle_output + Path.explode("log")
val isabelle_base_log = isabelle_output + Path.explode("../base_log")
if (first_build) {
other_isabelle.resolve_components(echo = verbose)
if (fresh)
Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode("lib/classes"))
other_isabelle.bash(
"env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " +
"bin/isabelle jedit -b", redirect = true, echo = verbose).check
for {
tool <- List("ghc_setup", "ocaml_setup")
if other_isabelle.getenv("ISABELLE_" + Word.uppercase(tool)) == "true" &&
(other_isabelle.isabelle_home + Path.explode("lib/Tools/" + tool)).is_file
} other_isabelle(tool, echo = verbose)
Isabelle_System.rm_tree(isabelle_base_log)
}
Isabelle_System.rm_tree(isabelle_output)
Isabelle_System.make_directory(isabelle_output)
val log_path =
other_isabelle.isabelle_home_user +
Build_Log.log_subdir(build_history_date) +
Build_Log.log_filename(Build_History.engine, build_history_date,
List(build_host, ml_platform, "M" + threads) ::: build_tags)
Isabelle_System.make_directory(log_path.dir)
val build_out = other_isabelle.isabelle_home_user + Path.explode("log/build.out")
val build_out_progress = new File_Progress(build_out)
build_out.file.delete
/* build */
if (multicore_base && !first_build && isabelle_base_log.is_dir)
Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log)
val build_start = Date.now()
val build_args1 = List("-v", "-j" + processes) ::: afp_build_args ::: build_args
val build_isabelle =
Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
user_home = user_home, progress = build_out_progress)
val build_result =
build_isabelle("build " + Bash.strings(build_args1 ::: afp_sessions),
redirect = true, echo = true, strict = false)
val build_end = Date.now()
val build_info: Build_Log.Build_Info =
Build_Log.Log_File(log_path.file_name, build_result.out_lines).
parse_build_info(ml_statistics = true)
/* output log */
val store = Sessions.store(options + "build_database_server=false")
val meta_info =
Properties.lines_nonempty(Build_Log.Prop.build_tags.name, build_tags) :::
Properties.lines_nonempty(Build_Log.Prop.build_args.name, build_args1) :::
List(
Build_Log.Prop.build_group_id.name -> build_group_id,
Build_Log.Prop.build_id.name -> (build_host + ":" + build_start.time.ms),
Build_Log.Prop.build_engine.name -> Build_History.engine,
Build_Log.Prop.build_host.name -> build_host,
Build_Log.Prop.build_start.name -> Build_Log.print_date(build_start),
Build_Log.Prop.build_end.name -> Build_Log.print_date(build_end),
Build_Log.Prop.isabelle_version.name -> isabelle_version) :::
afp_version.map(Build_Log.Prop.afp_version.name -> _).toList
build_out_progress.echo("Reading session build info ...")
val session_build_info =
build_info.finished_sessions.flatMap(session_name =>
{
val database = isabelle_output + store.database(session_name)
if (database.is_file) {
using(SQLite.open_database(database))(db =>
{
val theory_timings =
try {
store.read_theory_timings(db, session_name).map(ps =>
Protocol.Theory_Timing_Marker((Build_Log.SESSION_NAME, session_name) :: ps))
}
catch { case ERROR(_) => Nil }
val session_sources =
store.read_build(db, session_name).map(_.sources) match {
case Some(sources) if sources.length == SHA1.digest_length =>
List("Sources " + session_name + " " + sources)
case _ => Nil
}
theory_timings ::: session_sources
})
}
else Nil
})
build_out_progress.echo("Reading ML statistics ...")
val ml_statistics =
build_info.finished_sessions.flatMap(session_name =>
{
val database = isabelle_output + store.database(session_name)
val log_gz = isabelle_output + store.log_gz(session_name)
val properties =
if (database.is_file) {
using(SQLite.open_database(database))(db =>
store.read_ml_statistics(db, session_name))
}
else if (log_gz.is_file) {
Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics
}
else Nil
val trimmed_properties =
if (ml_statistics_step <= 0) Nil
else if (ml_statistics_step == 1) properties
else {
(for { (ps, i) <- properties.iterator.zipWithIndex if i % ml_statistics_step == 0 }
yield ps).toList
}
trimmed_properties.map(ps => (Build_Log.SESSION_NAME -> session_name) :: ps)
})
build_out_progress.echo("Reading error messages ...")
val session_errors =
build_info.failed_sessions.flatMap(session_name =>
{
val database = isabelle_output + store.database(session_name)
val errors =
if (database.is_file) {
try {
using(SQLite.open_database(database))(db => store.read_errors(db, session_name))
} // column "errors" could be missing
catch { case _: java.sql.SQLException => Nil }
}
else Nil
errors.map(msg => List(Build_Log.SESSION_NAME -> session_name, Markup.CONTENT -> msg))
})
build_out_progress.echo("Reading heap sizes ...")
val heap_sizes =
build_info.finished_sessions.flatMap(session_name =>
{
val heap = isabelle_output + Path.explode(session_name)
if (heap.is_file)
Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)")
else None
})
build_out_progress.echo("Writing log file " + log_path.xz + " ...")
File.write_xz(log_path.xz,
terminate_lines(
Protocol.Meta_Info_Marker(meta_info) :: build_result.out_lines :::
session_build_info :::
ml_statistics.map(Protocol.ML_Statistics_Marker.apply) :::
session_errors.map(Protocol.Error_Message_Marker.apply) :::
heap_sizes), XZ.options(6))
/* next build */
if (multicore_base && first_build && isabelle_output_log.is_dir)
Isabelle_System.copy_dir(isabelle_output_log, isabelle_base_log)
Isabelle_System.rm_tree(isabelle_output)
first_build = false
(build_result, log_path.xz)
}
}
/* command line entry point */
private object Multicore
{
private val Pat1 = """^(\d+)$""".r
private val Pat2 = """^(\d+)x(\d+)$""".r
def parse(s: String): (Int, Int) =
s match {
case Pat1(Value.Int(x)) => (x, 1)
case Pat2(Value.Int(x), Value.Int(y)) => (x, y)
case _ => error("Bad multicore configuration: " + quote(s))
}
}
def main(args: Array[String]): Unit =
{
Command_Line.tool {
var afp_rev: Option[String] = None
var multicore_base = false
var components_base: Path = Components.default_components_base
var heap: Option[Int] = None
var max_heap: Option[Int] = None
var multicore_list = List(default_multicore)
var isabelle_identifier = default_isabelle_identifier
var afp_partition = 0
var component_repository = Components.default_component_repository
var more_settings: List[String] = Nil
var more_preferences: List[String] = Nil
var fresh = false
var hostname = ""
var init_settings: List[String] = Nil
var arch_64 = false
var output_file = ""
var rev = default_rev
var ml_statistics_step = 1
var build_tags = List.empty[String]
var user_home = default_user_home
var verbose = false
var exit_code = false
val getopts = Getopts("""
Usage: Admin/build_history [OPTIONS] REPOSITORY [ARGS ...]
Options are:
-A REV include $ISABELLE_HOME/AFP repository at given revision
-B first multicore build serves as base for scheduling information
-C DIR base directory for Isabelle components (default: """ +
Components.default_components_base + """)
-H SIZE minimal ML heap in MB (default: """ + default_heap + """ for x86, """ +
default_heap * 2 + """ for x86_64)
-M MULTICORE multicore configurations (see below)
-N NAME alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
-P NUMBER AFP partition number (0, 1, 2, default: 0=unrestricted)
-R URL remote repository for Isabelle components (default: """ +
Components.default_component_repository + """)
-U SIZE maximal ML heap in MB (default: unbounded)
-e TEXT additional text for generated etc/settings
-f fresh build of Isabelle/Scala components (recommended)
-h NAME override local hostname
-i TEXT initial text for generated etc/settings
-m ARCH processor architecture (32=x86, 64=x86_64, default: x86)
-o FILE output file for log names (default: stdout)
-p TEXT additional text for generated etc/preferences
-r REV update to revision (default: """ + default_rev + """)
-s NUMBER step size for ML statistics (0=none, 1=all, n=step, default: 1)
-t TAG free-form build tag (multiple occurrences possible)
-u DIR alternative USER_HOME directory
-v verbose
-x return overall exit code from build processes
Build Isabelle sessions from the history of another REPOSITORY clone,
passing ARGS directly to its isabelle build tool.
Each MULTICORE configuration consists of one or two numbers (default 1):
THREADS or THREADSxPROCESSES, e.g. -M 1,2,4 or -M 1x4,2x2,4.
""",
"A:" -> (arg => afp_rev = Some(arg)),
"B" -> (_ => multicore_base = true),
"C:" -> (arg => components_base = Path.explode(arg)),
"H:" -> (arg => heap = Some(Value.Int.parse(arg))),
"M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse)),
"N:" -> (arg => isabelle_identifier = arg),
"P:" -> (arg => afp_partition = Value.Int.parse(arg)),
"R:" -> (arg => component_repository = arg),
"U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
"e:" -> (arg => more_settings = more_settings ::: List(arg)),
"f" -> (_ => fresh = true),
"h:" -> (arg => hostname = arg),
"i:" -> (arg => init_settings = init_settings ::: List(arg)),
"m:" ->
{
case "32" | "x86" => arch_64 = false
case "64" | "x86_64" => arch_64 = true
case bad => error("Bad processor architecture: " + quote(bad))
},
"o:" -> (arg => output_file = arg),
"p:" -> (arg => more_preferences = more_preferences ::: List(arg)),
"r:" -> (arg => rev = arg),
"s:" -> (arg => ml_statistics_step = Value.Int.parse(arg)),
"t:" -> (arg => build_tags = build_tags ::: List(arg)),
"u:" -> (arg => user_home = Path.explode(arg)),
"v" -> (_ => verbose = true),
"x" -> (_ => exit_code = true))
val more_args = getopts(args)
val (root, build_args) =
more_args match {
case root :: build_args => (Path.explode(root), build_args)
case _ => getopts.usage()
}
val progress = new Console_Progress(stderr = true)
val results =
build_history(Options.init(), root, user_home = user_home, progress = progress, rev = rev,
afp_rev = afp_rev, afp_partition = afp_partition,
isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step,
component_repository = component_repository, components_base = components_base,
fresh = fresh, hostname = hostname, multicore_base = multicore_base,
multicore_list = multicore_list, arch_64 = arch_64,
heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
max_heap = max_heap, init_settings = init_settings, more_settings = more_settings,
more_preferences = more_preferences, verbose = verbose, build_tags = build_tags,
build_args = build_args)
if (output_file == "") {
for ((_, log_path) <- results)
Output.writeln(log_path.implode, stdout = true)
}
else {
File.write(Path.explode(output_file),
cat_lines(for ((_, log_path) <- results) yield log_path.implode))
}
val rc = results.foldLeft(0) { case (rc, (res, _)) => rc max res.rc }
if (rc != 0 && exit_code) sys.exit(rc)
}
}
/** remote build_history -- via command-line **/
def remote_build_history(
ssh: SSH.Session,
isabelle_repos_self: Path,
isabelle_repos_other: Path,
isabelle_repos_source: String = Isabelle_Cronjob.isabelle_repos_source,
afp_repos_source: String = AFP.repos_source,
isabelle_identifier: String = "remote_build_history",
self_update: Boolean = false,
progress: Progress = new Progress,
rev: String = "",
afp_rev: Option[String] = None,
options: String = "",
args: String = ""): List[(String, Bytes)] =
{
/* Isabelle self repository */
val self_hg =
Mercurial.setup_repository(isabelle_repos_source, isabelle_repos_self, ssh = ssh)
def execute(cmd: String, args: String, echo: Boolean = false, strict: Boolean = true): Unit =
ssh.execute(
Isabelle_System.export_isabelle_identifier(isabelle_identifier) +
ssh.bash_path(isabelle_repos_self + Path.explode(cmd)) + " " + args,
progress_stdout = progress.echo_if(echo, _),
progress_stderr = progress.echo_if(echo, _),
strict = strict).check
if (self_update) {
- val hg = Mercurial.repository(Path.explode("~~"))
+ val hg = Mercurial.repository(Path.ISABELLE_HOME)
hg.push(self_hg.root_url, force = true)
self_hg.update(rev = hg.parent(), clean = true)
execute("bin/isabelle", "components -I")
execute("bin/isabelle", "components -a", echo = true)
execute("Admin/build", "jars_fresh")
}
val rev_id = self_hg.id(rev)
/* Isabelle other + AFP repository */
if (Mercurial.is_repository(isabelle_repos_other, ssh = ssh)) {
ssh.rm_tree(isabelle_repos_other)
}
Mercurial.clone_repository(
ssh.bash_path(isabelle_repos_self), isabelle_repos_other, rev = rev_id, ssh = ssh)
val afp_options =
if (afp_rev.isEmpty) ""
else {
val afp_repos = isabelle_repos_other + Path.explode("AFP")
Mercurial.setup_repository(afp_repos_source, afp_repos, ssh = ssh)
" -A " + Bash.string(afp_rev.get)
}
/* Admin/build_history */
ssh.with_tmp_dir(tmp_dir =>
{
val output_file = tmp_dir + Path.explode("output")
val rev_options = if (rev == "") "" else " -r " + Bash.string(rev_id)
try {
execute("Admin/build_history",
"-o " + ssh.bash_path(output_file) + rev_options + afp_options + " " + options + " " +
ssh.bash_path(isabelle_repos_other) + " " + args,
echo = true, strict = false)
}
catch {
case ERROR(msg) =>
cat_error(msg,
"The error(s) above occurred for build_bistory " + rev_options + afp_options)
}
for (line <- split_lines(ssh.read(output_file)))
yield {
val log = Path.explode(line)
val bytes = ssh.read_bytes(log)
ssh.rm(log)
(log.file_name, bytes)
}
})
}
}
diff --git a/src/Pure/Admin/build_release.scala b/src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala
+++ b/src/Pure/Admin/build_release.scala
@@ -1,927 +1,927 @@
/* 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_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 **/
/* patch release */
private val getsettings_path = Path.explode("lib/scripts/getsettings")
def patch_release(release: Release): Unit =
{
val dir = release.isabelle_dir
for (name <- List("src/Pure/System/distribution.ML", "src/Pure/System/distribution.scala"))
{
File.change(dir + Path.explode(name),
_.replace("val is_identified = false", "val is_identified = true"))
}
File.change(dir + getsettings_path,
_.replace("ISABELLE_IDENTIFIER=\"\"", "ISABELLE_IDENTIFIER=" + quote(release.dist_name)))
File.change(dir + Path.explode("lib/html/library_index_header.template"),
_.replace("{ISABELLE}", release.dist_name))
for {
name <-
List(
"src/Pure/System/distribution.ML",
"src/Pure/System/distribution.scala",
"lib/Tools/version") }
{
File.change(dir + Path.explode(name), _.replace("repository version", release.dist_version))
}
File.change(dir + Path.explode("README"),
_.replace("some repository version of Isabelle", release.dist_version))
}
/* 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(base_dir: Path,
options: Options,
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.explode("$ISABELLE_HOME"))
+ 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 = (base_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 getsettings = release.isabelle + getsettings_path
execute_tar(tmp_dir, "-xzf " +
File.bash_path(release.isabelle_archive) + " " + File.bash_path(getsettings))
Isabelle_System.isabelle_id(root = tmp_dir + release.isabelle)
.getOrElse(error("Failed to determine ISABELLE_ID from " + release.isabelle_archive))
})
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)
patch_release(release)
if (proper_release_name.isEmpty) make_announce(release)
make_contrib(release.isabelle_dir)
execute(release.isabelle_dir, """find . -print | xargs chmod -f u+rw""")
record_bundled_components(release.isabelle_dir)
/* build tools and documentation */
val other_isabelle = release.other_isabelle(release.dist_dir)
other_isabelle.init_settings(
other_isabelle.init_components(components_base = components_base, catalogs = List("main")))
other_isabelle.resolve_components(echo = true)
try {
val export_classpath =
"export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n"
other_isabelle.bash(export_classpath + "./Admin/build all", echo = true).check
other_isabelle.bash(export_classpath + "./bin/isabelle jedit -b", echo = true).check
}
catch { case ERROR(msg) => cat_error("Failed to build tools:", msg) }
try {
other_isabelle.bash(
"./bin/isabelle build_doc -a -o system_heaps -j " + parallel_jobs, echo = true).check
}
catch { case ERROR(msg) => cat_error("Failed to build documentation:", msg) }
make_news(other_isabelle, release.dist_version)
for (name <- List("Admin", "browser_info", "heaps")) {
Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name))
}
other_isabelle.cleanup()
progress.echo_warning("Creating distribution archive " + release.isabelle_archive)
def execute_dist_name(script: String): Unit =
Isabelle_System.bash(script, cwd = release.dist_dir.file,
env = Isabelle_System.settings() + ("DIST_NAME" -> release.dist_name)).check
execute_dist_name("""
set -e
chmod -R a+r "$DIST_NAME"
chmod -R u+w "$DIST_NAME"
chmod -R g=o "$DIST_NAME"
find "$DIST_NAME" -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w
""")
execute_tar(release.dist_dir, "-czf " +
File.bash_path(release.isabelle_archive) + " " + Bash.string(release.dist_name))
execute_dist_name("""
set -e
mv "$DIST_NAME" "${DIST_NAME}-old"
mkdir "$DIST_NAME"
mv "${DIST_NAME}-old/README" "${DIST_NAME}-old/NEWS" "${DIST_NAME}-old/ANNOUNCE" \
"${DIST_NAME}-old/COPYRIGHT" "${DIST_NAME}-old/CONTRIBUTORS" "$DIST_NAME"
mkdir "$DIST_NAME/doc"
mv "${DIST_NAME}-old/doc/"*.pdf \
"${DIST_NAME}-old/doc/"*.html \
"${DIST_NAME}-old/doc/"*.css \
"${DIST_NAME}-old/doc/fonts" \
"${DIST_NAME}-old/doc/Contents" "$DIST_NAME/doc"
rm -f Isabelle && ln -sf "$DIST_NAME" Isabelle
rm -rf "${DIST_NAME}-old"
""")
}
/* make application bundles */
val bundle_infos = platform_families.map(release.bundle_info)
for (bundle_info <- bundle_infos) {
val isabelle_name = release.dist_name
val platform = bundle_info.platform
progress.echo("\nApplication bundle for " + platform)
Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
{
// release archive
execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive))
val other_isabelle = release.other_isabelle(tmp_dir)
val isabelle_target = other_isabelle.isabelle_home
// bundled components
progress.echo("Bundled components:")
val contrib_dir = Components.contrib(isabelle_target)
val (bundled_components, jdk_component) =
get_bundled_components(isabelle_target, platform)
Components.resolve(components_base, bundled_components,
target_dir = Some(contrib_dir),
copy_dir = Some(release.dist_dir + Path.explode("contrib")),
progress = progress)
val more_components_names =
more_components.map(Components.unpack(contrib_dir, _, progress = progress))
Components.purge(contrib_dir, platform)
activate_components(isabelle_target, platform, more_components_names)
// Java parameters
val java_options: List[String] =
(for {
variable <-
List(
"ISABELLE_JAVA_SYSTEM_OPTIONS",
"JEDIT_JAVA_SYSTEM_OPTIONS",
"JEDIT_JAVA_OPTIONS")
opt <- Word.explode(other_isabelle.getenv(variable))
}
yield {
val s = "-Dapple.awt.application.name="
if (opt.startsWith(s)) s + isabelle_name else opt
}) ::: List("-Disabelle.jedit_server=" + isabelle_name)
val classpath: List[Path] =
{
val base = isabelle_target.absolute
Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).map(path =>
{
val abs_path = path.absolute
File.relative_path(base, abs_path) match {
case Some(rel_path) => rel_path
case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path)
}
}) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar"))
}
val jedit_options = Path.explode("src/Tools/jEdit/etc/options")
val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props")
// build heaps
if (build_sessions.nonEmpty) {
progress.echo("Building heaps ...")
remote_build_heaps(options, platform, build_sessions, isabelle_target)
}
// application bundling
platform match {
case Platform.Family.linux =>
File.change(isabelle_target + jedit_options,
_.replaceAll("jedit_reset_font_size : int =.*", "jedit_reset_font_size : int = 24"))
File.change(isabelle_target + jedit_props,
_.replaceAll("console.fontsize=.*", "console.fontsize=18")
.replaceAll("helpviewer.fontsize=.*", "helpviewer.fontsize=18")
.replaceAll("metal.primary.fontsize=.*", "metal.primary.fontsize=18")
.replaceAll("metal.secondary.fontsize=.*", "metal.secondary.fontsize=18")
.replaceAll("view.fontsize=.*", "view.fontsize=24")
.replaceAll("view.gutter.fontsize=.*", "view.gutter.fontsize=16"))
make_isabelle_options(
isabelle_target + Path.explode("Isabelle.options"), java_options)
make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component, classpath)
val archive_name = isabelle_name + "_linux.tar.gz"
progress.echo("Packaging " + archive_name + " ...")
execute_tar(tmp_dir,
"-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
Bash.string(isabelle_name))
case Platform.Family.macos =>
File.change(isabelle_target + jedit_props,
_.replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
.replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d"))
// macOS application bundle
val app_contents = isabelle_target + Path.explode("Contents")
for (icon <- List("lib/logo/isabelle.icns", "lib/logo/theory.icns")) {
Isabelle_System.copy_file(isabelle_target + Path.explode(icon),
Isabelle_System.make_directory(app_contents + Path.explode("Resources")))
}
make_isabelle_plist(
app_contents + Path.explode("Info.plist"), isabelle_name, release.ident)
make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component,
classpath, dock_icon = true)
val isabelle_options = Path.explode("Isabelle.options")
make_isabelle_options(
isabelle_target + isabelle_options,
java_options ::: List("-Disabelle.app=true"))
// application archive
val archive_name = isabelle_name + "_macos.tar.gz"
progress.echo("Packaging " + archive_name + " ...")
val isabelle_app = Path.explode(isabelle_name + ".app")
Isabelle_System.move_file(tmp_dir + Path.explode(isabelle_name),
tmp_dir + isabelle_app)
execute_tar(tmp_dir,
"-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
File.bash_path(isabelle_app))
case Platform.Family.windows =>
File.change(isabelle_target + jedit_props,
_.replaceAll("foldPainter=.*", "foldPainter=Square"))
// application launcher
Isabelle_System.move_file(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
val app_template = Path.explode("~~/Admin/Windows/launch4j")
make_isabelle_options(
isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
java_options, line_ending = "\r\n")
val isabelle_xml = Path.explode("isabelle.xml")
val isabelle_exe = Path.explode(isabelle_name + ".exe")
File.write(tmp_dir + isabelle_xml,
File.read(app_template + isabelle_xml)
.replace("{ISABELLE_NAME}", isabelle_name)
.replace("{OUTFILE}", File.platform_path(isabelle_target + isabelle_exe))
.replace("{ICON}",
File.platform_path(app_template + Path.explode("isabelle_transparent.ico")))
.replace("{SPLASH}",
File.platform_path(app_template + Path.explode("isabelle.bmp")))
.replace("{CLASSPATH}",
cat_lines(classpath.map(cp =>
" %EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "")))
.replace("\\jdk\\", "\\" + jdk_component + "\\"))
execute(tmp_dir,
"\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
Isabelle_System.copy_file(app_template + Path.explode("manifest.xml"),
isabelle_target + isabelle_exe.ext("manifest"))
// Cygwin setup
val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
Isabelle_System.copy_file(cygwin_template + Path.explode("Cygwin-Terminal.bat"),
isabelle_target)
val cygwin_mirror =
File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror"))
val cygwin_bat = Path.explode("Cygwin-Setup.bat")
File.write(isabelle_target + cygwin_bat,
File.read(cygwin_template + cygwin_bat).replace("{MIRROR}", cygwin_mirror))
File.set_executable(isabelle_target + cygwin_bat, true)
for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
val path = Path.explode(name)
Isabelle_System.copy_file(cygwin_template + path,
isabelle_target + Path.explode("contrib/cygwin") + path)
}
execute(isabelle_target,
"""find . -type f -not -name "*.exe" -not -name "*.dll" """ +
(if (Platform.is_macos) "-perm +100" else "-executable") +
" -print0 > contrib/cygwin/isabelle/executables")
execute(isabelle_target,
"""find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ +
"""> contrib/cygwin/isabelle/symlinks""")
execute(isabelle_target, """find . -type l -exec rm "{}" ";" """)
File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "")
// executable archive (self-extracting 7z)
val archive_name = isabelle_name + ".7z"
val exe_archive = tmp_dir + Path.explode(archive_name)
exe_archive.file.delete
progress.echo("Packaging " + archive_name + " ...")
execute(tmp_dir,
"7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name))
if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive)
val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx")
val sfx_txt =
File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt"))
.replace("{ISABELLE_NAME}", isabelle_name)
Bytes.write(release.dist_dir + isabelle_exe,
Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
File.set_executable(release.dist_dir + isabelle_exe, true)
}
})
progress.echo("DONE")
}
/* minimal website */
for (dir <- website) {
val website_platform_bundles =
for {
bundle_info <- bundle_infos
if (release.dist_dir + bundle_info.path).is_file
} yield (bundle_info.name, bundle_info)
val isabelle_link =
HTML.link(Isabelle_Cronjob.isabelle_repos_source + "/rev/" + release.ident,
HTML.text("Isabelle/" + release.ident))
val afp_link =
HTML.link(AFP.repos_source + "/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 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 + """)
-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)),
"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)
val base_dir = more_args match { case List(base_dir) => base_dir case _ => 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(Path.explode(base_dir), options, components_base = components_base,
progress = progress, rev = rev, afp_rev = afp_rev,
proper_release_name = proper_release_name, website = website,
platform_families =
if (platform_families.isEmpty) default_platform_families
else platform_families,
more_components = more_components, build_sessions = build_sessions,
build_library = build_library, parallel_jobs = parallel_jobs)
}
}
}
diff --git a/src/Pure/Admin/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,120 +1,120 @@
/* Title: Pure/Admin/other_isabelle.scala
Author: Makarius
Manage other Isabelle distributions.
*/
package isabelle
object Other_Isabelle
{
def apply(isabelle_home: Path,
isabelle_identifier: String = "",
- user_home: Path = Path.explode("$USER_HOME"),
+ user_home: Path = Path.USER_HOME,
progress: Progress = new Progress): Other_Isabelle =
new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, user_home, progress)
}
class Other_Isabelle(
val isabelle_home: Path,
val isabelle_identifier: String,
user_home: Path,
progress: Progress)
{
other_isabelle =>
override def toString: String = isabelle_home.toString
if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined)
error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT")
/* static system */
def bash(
script: String,
redirect: Boolean = false,
echo: Boolean = false,
strict: Boolean = true): Process_Result =
progress.bash(
"export USER_HOME=" + File.bash_path(user_home) + "\n" +
Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict)
def apply(
cmdline: String,
redirect: Boolean = false,
echo: Boolean = false,
strict: Boolean = true): Process_Result =
bash("bin/isabelle " + cmdline, redirect = redirect, echo = echo, strict = strict)
def resolve_components(echo: Boolean): Unit =
other_isabelle(
"env ISABELLE_TOOLS=" + Bash.string(Isabelle_System.getenv("ISABELLE_TOOLS")) +
" isabelle components -a", redirect = true, echo = echo).check
def getenv(name: String): String =
other_isabelle("getenv -b " + Bash.string(name)).check.out
val isabelle_home_user: Path = Path.explode(getenv("ISABELLE_HOME_USER"))
val etc: Path = isabelle_home_user + Path.explode("etc")
val etc_settings: Path = etc + Path.explode("settings")
val etc_preferences: Path = etc + Path.explode("preferences")
def copy_fonts(target_dir: Path): Unit =
Isabelle_Fonts.make_entries(getenv = getenv, hidden = true).
foreach(entry => Isabelle_System.copy_file(entry.path, target_dir))
/* components */
def init_components(
component_repository: String = Components.default_component_repository,
components_base: Path = Components.default_components_base,
catalogs: List[String] = Nil,
components: List[String] = Nil): List[String] =
{
val dir = Components.admin(isabelle_home)
("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)))
}
/* 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())
error("Cannot proceed with existing user settings file: " + etc_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"))
}
/* cleanup */
def cleanup(): Unit =
{
clean_settings()
etc.file.delete
isabelle_home_user.file.delete
}
}
diff --git a/src/Pure/General/path.scala b/src/Pure/General/path.scala
--- a/src/Pure/General/path.scala
+++ b/src/Pure/General/path.scala
@@ -1,306 +1,309 @@
/* Title: Pure/General/path.scala
Author: Makarius
Algebra of file-system paths: basic POSIX notation, extended by named
roots (e.g. //foo) and variables (e.g. $BAR).
*/
package isabelle
import java.io.{File => JFile}
import scala.util.matching.Regex
object Path
{
/* path elements */
sealed abstract class Elem
private case class Root(name: String) extends Elem
private case class Basic(name: String) extends Elem
private case class Variable(name: String) extends Elem
private case object Parent extends Elem
private def err_elem(msg: String, s: String): Nothing =
error(msg + " path element " + quote(s))
private val illegal_elem = Set("", "~", "~~", ".", "..")
private val illegal_char = "/\\$:\"'<>|?*"
private def check_elem(s: String): String =
if (illegal_elem.contains(s)) err_elem("Illegal", s)
else {
for (c <- s) {
if (c.toInt < 32)
err_elem("Illegal control character " + c.toInt + " in", s)
if (illegal_char.contains(c))
err_elem("Illegal character " + quote(c.toString) + " in", s)
}
s
}
private def root_elem(s: String): Elem = Root(check_elem(s))
private def basic_elem(s: String): Elem = Basic(check_elem(s))
private def variable_elem(s: String): Elem = Variable(check_elem(s))
private def apply_elem(y: Elem, xs: List[Elem]): List[Elem] =
(y, xs) match {
case (Root(_), _) => List(y)
case (Parent, Root(_) :: _) => xs
case (Parent, Basic(_) :: rest) => rest
case _ => y :: xs
}
private def norm_elems(elems: List[Elem]): List[Elem] =
elems.foldRight(List.empty[Elem])(apply_elem)
private def implode_elem(elem: Elem, short: Boolean): String =
elem match {
case Root("") => ""
case Root(s) => "//" + s
case Basic(s) => s
case Variable("USER_HOME") if short => "~"
case Variable("ISABELLE_HOME") if short => "~~"
case Variable(s) => "$" + s
case Parent => ".."
}
private def squash_elem(elem: Elem): String =
elem match {
case Root("") => "ROOT"
case Root(s) => "SERVER_" + s
case Basic(s) => s
case Variable(s) => s
case Parent => "PARENT"
}
/* path constructors */
val current: Path = new Path(Nil)
val root: Path = new Path(List(Root("")))
def named_root(s: String): Path = new Path(List(root_elem(s)))
def make(elems: List[String]): Path = new Path(elems.reverse.map(basic_elem))
def basic(s: String): Path = new Path(List(basic_elem(s)))
def variable(s: String): Path = new Path(List(variable_elem(s)))
val parent: Path = new Path(List(Parent))
+ val USER_HOME: Path = variable("USER_HOME")
+ val ISABELLE_HOME: Path = variable("ISABELLE_HOME")
+
/* explode */
def explode(str: String): Path =
{
def explode_elem(s: String): Elem =
try {
if (s == "..") Parent
else if (s == "~") Variable("USER_HOME")
else if (s == "~~") Variable("ISABELLE_HOME")
else if (s.startsWith("$")) variable_elem(s.substring(1))
else basic_elem(s)
}
catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred in " + quote(str)) }
val ss = space_explode('/', str)
val r = ss.takeWhile(_.isEmpty).length
val es = ss.dropWhile(_.isEmpty)
val (roots, raw_elems) =
if (r == 0) (Nil, es)
else if (r == 1) (List(Root("")), es)
else if (es.isEmpty) (List(Root("")), Nil)
else (List(root_elem(es.head)), es.tail)
val elems = raw_elems.filterNot(s => s.isEmpty || s == ".").map(explode_elem)
new Path(norm_elems(elems reverse_::: roots))
}
def is_wellformed(str: String): Boolean =
try { explode(str); true } catch { case ERROR(_) => false }
def is_valid(str: String): Boolean =
try { explode(str).expand; true } catch { case ERROR(_) => false }
def split(str: String): List[Path] =
space_explode(':', str).filterNot(_.isEmpty).map(explode)
/* encode */
val encode: XML.Encode.T[Path] = (path => XML.Encode.string(path.implode))
/* reserved names */
private val reserved_windows: Set[String] =
Set("CON", "PRN", "AUX", "NUL",
"COM1", "COM2", "COM3", "COM4", "COM5", "COM6", "COM7", "COM8", "COM9",
"LPT1", "LPT2", "LPT3", "LPT4", "LPT5", "LPT6", "LPT7", "LPT8", "LPT9")
def is_reserved(name: String): Boolean =
Long_Name.explode(name).exists(a => reserved_windows.contains(Word.uppercase(a)))
/* case-insensitive names */
def check_case_insensitive(paths: List[Path]): Unit =
{
val table =
paths.foldLeft(Multi_Map.empty[String, String]) { case (tab, path) =>
val name = path.expand.implode
tab.insert(Word.lowercase(name), name)
}
val collisions =
(for { (_, coll) <- table.iterator_list if coll.length > 1 } yield coll).toList.flatten
if (collisions.nonEmpty) {
error(("Collision of file names due case-insensitivity:" :: collisions).mkString("\n "))
}
}
}
final class Path private(protected val elems: List[Path.Elem]) // reversed elements
{
override def hashCode: Int = elems.hashCode
override def equals(that: Any): Boolean =
that match {
case other: Path => elems == other.elems
case _ => false
}
def is_current: Boolean = elems.isEmpty
def is_absolute: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Root]
def is_root: Boolean = elems match { case List(Path.Root(_)) => true case _ => false }
def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false }
def starts_basic: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Basic]
def +(other: Path): Path = new Path(other.elems.foldRight(elems)(Path.apply_elem))
/* implode */
private def gen_implode(short: Boolean): String =
elems match {
case Nil => "."
case List(Path.Root("")) => "/"
case _ => elems.map(Path.implode_elem(_, short)).reverse.mkString("/")
}
def implode: String = gen_implode(false)
def implode_short: String = gen_implode(true)
override def toString: String = quote(implode)
/* base element */
private def split_path: (Path, String) =
elems match {
case Path.Basic(s) :: xs => (new Path(xs), s)
case _ => error("Cannot split path into dir/base: " + toString)
}
def dir: Path = split_path._1
def base: Path = new Path(List(Path.Basic(split_path._2)))
def ext(e: String): Path =
if (e == "") this
else {
val (prfx, s) = split_path
prfx + Path.basic(s + "." + e)
}
def xz: Path = ext("xz")
def html: Path = ext("html")
def tex: Path = ext("tex")
def pdf: Path = ext("pdf")
def thy: Path = ext("thy")
def backup: Path =
{
val (prfx, s) = split_path
prfx + Path.basic(s + "~")
}
def backup2: Path =
{
val (prfx, s) = split_path
prfx + Path.basic(s + "~~")
}
def platform_exe: Path =
if (Platform.is_windows) ext("exe") else this
private val Ext = new Regex("(.*)\\.([^.]*)")
def split_ext: (Path, String) =
{
val (prefix, base) = split_path
base match {
case Ext(b, e) => (prefix + Path.basic(b), e)
case _ => (prefix + Path.basic(base), "")
}
}
def drop_ext: Path = split_ext._1
def get_ext: String = split_ext._2
def squash: Path = new Path(elems.map(elem => Path.Basic(Path.squash_elem(elem))))
/* expand */
def expand_env(env: Map[String, String]): Path =
{
def eval(elem: Path.Elem): List[Path.Elem] =
elem match {
case Path.Variable(s) =>
val path = Path.explode(Isabelle_System.getenv_strict(s, env))
if (path.elems.exists(_.isInstanceOf[Path.Variable]))
error("Illegal path variable nesting: " + s + "=" + path.toString)
else path.elems
case x => List(x)
}
new Path(Path.norm_elems(elems.flatMap(eval)))
}
def expand: Path = expand_env(Isabelle_System.settings())
def file_name: String = expand.base.implode
/* implode wrt. given directories */
def implode_symbolic: String =
{
val directories =
Library.space_explode(':', Isabelle_System.getenv("ISABELLE_DIRECTORIES")).reverse
val full_name = expand.implode
directories.view.flatMap(a =>
try {
val b = Path.explode(a).expand.implode
if (full_name == b) Some(a)
else {
Library.try_unprefix(b + "/", full_name) match {
case Some(name) => Some(a + "/" + name)
case None => None
}
}
} catch { case ERROR(_) => None }).headOption.getOrElse(implode)
}
def position: Position.T = Position.File(implode_symbolic)
/* platform files */
def file: JFile = File.platform_file(this)
def is_file: Boolean = file.isFile
def is_dir: Boolean = file.isDirectory
def absolute_file: JFile = File.absolute(file)
def canonical_file: JFile = File.canonical(file)
def absolute: Path = File.path(absolute_file)
def canonical: Path = File.path(canonical_file)
}
diff --git a/src/Pure/ML/ml_statistics.scala b/src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala
+++ b/src/Pure/ML/ml_statistics.scala
@@ -1,324 +1,324 @@
/* Title: Pure/ML/ml_statistics.scala
Author: Makarius
ML runtime statistics.
*/
package isabelle
import scala.annotation.tailrec
import scala.collection.mutable
import scala.collection.immutable.{SortedSet, SortedMap}
import scala.swing.{Frame, Component}
import org.jfree.data.xy.{XYSeries, XYSeriesCollection}
import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory}
import org.jfree.chart.plot.PlotOrientation
object ML_Statistics
{
/* properties */
val Now = new Properties.Double("now")
def now(props: Properties.T): Double = Now.unapply(props).get
/* memory status */
val Heap_Size = new Properties.Long("size_heap")
val Heap_Free = new Properties.Long("size_heap_free_last_GC")
val GC_Percent = new Properties.Int("GC_percent")
sealed case class Memory_Status(heap_size: Long, heap_free: Long, gc_percent: Int)
{
def heap_used: Long = (heap_size - heap_free) max 0
def heap_used_fraction: Double =
if (heap_size == 0) 0.0 else heap_used.toDouble / heap_size
def gc_progress: Option[Double] =
if (1 <= gc_percent && gc_percent <= 100) Some((gc_percent - 1) * 0.01) else None
}
def memory_status(props: Properties.T): Memory_Status =
{
val heap_size = Heap_Size.get(props)
val heap_free = Heap_Free.get(props)
val gc_percent = GC_Percent.get(props)
Memory_Status(heap_size, heap_free, gc_percent)
}
/* monitor process */
def monitor(pid: Long,
stats_dir: String = "",
delay: Time = Time.seconds(0.5),
consume: Properties.T => Unit = Console.println): Unit =
{
def progress_stdout(line: String): Unit =
{
val props =
Library.space_explode(',', line).flatMap((entry: String) =>
Library.space_explode('=', entry) match {
case List(a, b) => Some((a, b))
case _ => None
})
if (props.nonEmpty) consume(props)
}
val env_prefix =
if (stats_dir.isEmpty) "" else "export POLYSTATSDIR=" + Bash.string(stats_dir) + "\n"
Bash.process(env_prefix + "exec \"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " +
Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " +
ML_Syntax.print_double(delay.seconds)),
- cwd = Path.explode("~~").file)
+ cwd = Path.ISABELLE_HOME.file)
.result(progress_stdout = progress_stdout, strict = false).check
}
/* protocol handler */
class Handler extends Session.Protocol_Handler
{
private var session: Session = null
private var monitoring: Future[Unit] = Future.value(())
override def init(session: Session): Unit = synchronized
{
this.session = session
}
override def exit(): Unit = synchronized
{
session = null
monitoring.cancel()
}
private def consume(props: Properties.T): Unit = synchronized
{
if (session != null) {
val props1 = (session.cache.props(props ::: Java_Statistics.jvm_statistics()))
session.runtime_statistics.post(Session.Runtime_Statistics(props1))
}
}
private def ml_statistics(msg: Prover.Protocol_Output): Boolean = synchronized
{
msg.properties match {
case Markup.ML_Statistics(pid, stats_dir) =>
monitoring =
Future.thread("ML_statistics") {
monitor(pid, stats_dir = stats_dir, consume = consume)
}
true
case _ => false
}
}
override val functions = List(Markup.ML_Statistics.name -> ml_statistics)
}
/* memory fields (mega bytes) */
def mem_print(x: Long): Option[String] =
if (x == 0L) None else Some(x.toString + " M")
def mem_scale(x: Long): Long = x / 1024 / 1024
def mem_field_scale(name: String, x: Double): Double =
if (heap_fields._2.contains(name) || program_fields._2.contains(name))
mem_scale(x.toLong).toDouble
else x
val CODE_SIZE = "size_code"
val STACK_SIZE = "size_stacks"
val HEAP_SIZE = "size_heap"
/* standard fields */
type Fields = (String, List[String])
val tasks_fields: Fields =
("Future tasks",
List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive",
"tasks_urgent", "tasks_total"))
val workers_fields: Fields =
("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
val GC_fields: Fields =
("GCs", List("partial_GCs", "full_GCs", "share_passes"))
val heap_fields: Fields =
("Heap", List(HEAP_SIZE, "size_allocation", "size_allocation_free",
"size_heap_free_last_full_GC", "size_heap_free_last_GC"))
val program_fields: Fields =
("Program", List("size_code", "size_stacks"))
val threads_fields: Fields =
("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar",
"threads_wait_IO", "threads_wait_mutex", "threads_wait_signal"))
val time_fields: Fields =
("Time", List("time_elapsed", "time_elapsed_GC", "time_CPU", "time_GC"))
val speed_fields: Fields =
("Speed", List("speed_CPU", "speed_GC"))
private val time_speed = Map("time_CPU" -> "speed_CPU", "time_GC" -> "speed_GC")
val java_heap_fields: Fields =
("Java heap", List("java_heap_size", "java_heap_used"))
val java_thread_fields: Fields =
("Java threads", List("java_threads_total", "java_workers_total", "java_workers_active"))
val main_fields: List[Fields] =
List(heap_fields, tasks_fields, workers_fields)
val other_fields: List[Fields] =
List(threads_fields, GC_fields, program_fields, time_fields, speed_fields,
java_heap_fields, java_thread_fields)
val all_fields: List[Fields] = main_fields ::: other_fields
/* content interpretation */
final case class Entry(time: Double, data: Map[String, Double])
{
def get(field: String): Double = data.getOrElse(field, 0.0)
}
val empty: ML_Statistics = apply(Nil)
def apply(ml_statistics0: List[Properties.T], heading: String = "",
domain: String => Boolean = (key: String) => true): ML_Statistics =
{
require(ml_statistics0.forall(props => Now.unapply(props).isDefined), "missing \"now\" field")
val ml_statistics = ml_statistics0.sortBy(now)
val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head)
val duration = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.last) - time_start
val fields =
SortedSet.empty[String] ++
(for {
props <- ml_statistics.iterator
(x, _) <- props.iterator
if x != Now.name && domain(x) } yield x)
val content =
{
var last_edge = Map.empty[String, (Double, Double, Double)]
val result = new mutable.ListBuffer[ML_Statistics.Entry]
for (props <- ml_statistics) {
val time = now(props) - time_start
// rising edges -- relative speed
val speeds =
(for {
(key, value) <- props.iterator
key1 <- time_speed.get(key)
if domain(key1)
} yield {
val (x0, y0, s0) = last_edge.getOrElse(key, (0.0, 0.0, 0.0))
val x1 = time
val y1 = java.lang.Double.parseDouble(value)
val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0)
if (y1 > y0) {
last_edge += (key -> (x1, y1, s1))
(key1, s1.toString)
}
else (key1, s0.toString)
}).toList
val data =
SortedMap.empty[String, Double] ++
(for {
(x, y) <- props.iterator ++ speeds.iterator
if x != Now.name && domain(x)
z = java.lang.Double.parseDouble(y) if z != 0.0
} yield { (x.intern, mem_field_scale(x, z)) })
result += ML_Statistics.Entry(time, data)
}
result.toList
}
new ML_Statistics(heading, fields, content, time_start, duration)
}
}
final class ML_Statistics private(
val heading: String,
val fields: Set[String],
val content: List[ML_Statistics.Entry],
val time_start: Double,
val duration: Double)
{
/* content */
def maximum(field: String): Double =
content.foldLeft(0.0) { case (m, e) => m max e.get(field) }
def average(field: String): Double =
{
@tailrec def sum(t0: Double, list: List[ML_Statistics.Entry], acc: Double): Double =
list match {
case Nil => acc
case e :: es =>
val t = e.time
sum(t, es, (t - t0) * e.get(field) + acc)
}
content match {
case Nil => 0.0
case List(e) => e.get(field)
case e :: es => sum(e.time, es, 0.0) / duration
}
}
/* charts */
def update_data(data: XYSeriesCollection, selected_fields: List[String]): Unit =
{
data.removeAllSeries
for (field <- selected_fields) {
val series = new XYSeries(field)
content.foreach(entry => series.add(entry.time, entry.get(field)))
data.addSeries(series)
}
}
def chart(title: String, selected_fields: List[String]): JFreeChart =
{
val data = new XYSeriesCollection
update_data(data, selected_fields)
ChartFactory.createXYLineChart(title, "time", "value", data,
PlotOrientation.VERTICAL, true, true, true)
}
def chart(fields: ML_Statistics.Fields): JFreeChart =
chart(fields._1, fields._2)
def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.main_fields): Unit =
fields.map(chart).foreach(c =>
GUI_Thread.later {
new Frame {
iconImage = GUI.isabelle_image()
title = heading
contents = Component.wrap(new ChartPanel(c))
visible = true
}
})
}
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,597 +1,597 @@
/* 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
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 <- Library.split_strings0(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.explode("~~")): Option[String] =
+ 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.explode("~~")): Option[String] =
+ def isabelle_id(root: Path = Path.ISABELLE_HOME): Option[String] =
getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) orElse {
if (Mercurial.is_repository(root)) Some(Mercurial.repository(root).parent())
else None
}
- def isabelle_tags(root: Path = Path.explode("~~")): String =
+ 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 ""
}
/** file-system operations **/
/* scala functions */
private def apply_paths(arg: String, fun: List[Path] => Unit): String =
{ fun(Library.split_strings0(arg).map(Path.explode)); "" }
private def apply_paths1(arg: String, fun: Path => Unit): String =
apply_paths(arg, { case List(path) => fun(path) })
private def apply_paths2(arg: String, fun: (Path, Path) => Unit): String =
apply_paths(arg, { case List(path1, path2) => fun(path1, path2) })
private def apply_paths3(arg: String, fun: (Path, Path, Path) => Unit): String =
apply_paths(arg, { 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("make_directory")
{
val here = Scala_Project.here
def apply(arg: String): String = apply_paths1(arg, make_directory)
}
object Copy_Dir extends Scala.Fun("copy_dir")
{
val here = Scala_Project.here
def apply(arg: String): String = apply_paths2(arg, 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("copy_file")
{
val here = Scala_Project.here
def apply(arg: String): String = apply_paths2(arg, copy_file)
}
object Copy_File_Base extends Scala.Fun("copy_file_base")
{
val here = Scala_Project.here
def apply(arg: String): String = apply_paths3(arg, 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("rm_tree")
{
val here = Scala_Project.here
def apply(arg: String): String = apply_paths1(arg, 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
proc.command(command_line:_*) // fragile on Windows
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 kill(signal: String, group_pid: String): (String, Int) =
{
val bash =
if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe")
else List("/usr/bin/env", "bash")
process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid)))
}
/* 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, file: Path, progress: Progress = new Progress): Unit =
{
val url = Url(url_name)
progress.echo("Getting " + quote(url_name))
val content =
try { HTTP.Client.get(url) }
catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) }
Bytes.write(file, content.bytes)
}
object Download extends Scala.Fun("download", thread = true)
{
val here = Scala_Project.here
def apply(arg: String): String =
Library.split_strings0(arg) match {
case List(url, file) => download(url, Path.explode(file)); ""
}
}
}
diff --git a/src/Pure/Tools/build.scala b/src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala
+++ b/src/Pure/Tools/build.scala
@@ -1,679 +1,679 @@
/* Title: Pure/Tools/build.scala
Author: Makarius
Options: :folding=explicit:
Build and manage Isabelle sessions.
*/
package isabelle
import scala.collection.immutable.SortedSet
import scala.annotation.tailrec
object Build
{
/** auxiliary **/
/* persistent build info */
sealed case class Session_Info(
sources: String,
input_heaps: List[String],
output_heap: Option[String],
return_code: Int)
{
def ok: Boolean = return_code == 0
}
/* queue with scheduling information */
private object Queue
{
type Timings = (List[Properties.T], Double)
def load_timings(progress: Progress, store: Sessions.Store, session_name: String): Timings =
{
val no_timings: Timings = (Nil, 0.0)
store.try_open_database(session_name) match {
case None => no_timings
case Some(db) =>
def ignore_error(msg: String) =
{
progress.echo_warning("Ignoring bad database " + db + (if (msg == "") "" else "\n" + msg))
no_timings
}
try {
val command_timings = store.read_command_timings(db, session_name)
val session_timing =
store.read_session_timing(db, session_name) match {
case Markup.Elapsed(t) => t
case _ => 0.0
}
(command_timings, session_timing)
}
catch {
case ERROR(msg) => ignore_error(msg)
case exn: java.lang.Error => ignore_error(Exn.message(exn))
case _: XML.Error => ignore_error("")
}
finally { db.close() }
}
}
def make_session_timing(sessions_structure: Sessions.Structure, timing: Map[String, Double])
: Map[String, Double] =
{
val maximals = sessions_structure.build_graph.maximals.toSet
def desc_timing(session_name: String): Double =
{
if (maximals.contains(session_name)) timing(session_name)
else {
val descendants = sessions_structure.build_descendants(List(session_name)).toSet
val g = sessions_structure.build_graph.restrict(descendants)
(0.0 :: g.maximals.flatMap(desc => {
val ps = g.all_preds(List(desc))
if (ps.exists(p => !timing.isDefinedAt(p))) None
else Some(ps.map(timing(_)).sum)
})).max
}
}
timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0)
}
def apply(progress: Progress, sessions_structure: Sessions.Structure, store: Sessions.Store)
: Queue =
{
val graph = sessions_structure.build_graph
val names = graph.keys
val timings = names.map(name => (name, load_timings(progress, store, name)))
val command_timings =
timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil)
val session_timing =
make_session_timing(sessions_structure,
timings.map({ case (name, (_, t)) => (name, t) }).toMap)
object Ordering extends scala.math.Ordering[String]
{
def compare(name1: String, name2: String): Int =
session_timing(name2) compare session_timing(name1) match {
case 0 =>
sessions_structure(name2).timeout compare sessions_structure(name1).timeout match {
case 0 => name1 compare name2
case ord => ord
}
case ord => ord
}
}
new Queue(graph, SortedSet(names: _*)(Ordering), command_timings)
}
}
private class Queue(
graph: Graph[String, Sessions.Info],
order: SortedSet[String],
val command_timings: String => List[Properties.T])
{
def is_inner(name: String): Boolean = !graph.is_maximal(name)
def is_empty: Boolean = graph.is_empty
def - (name: String): Queue =
new Queue(graph.del_node(name), order - name, command_timings)
def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] =
{
val it = order.iterator.dropWhile(name => skip(name) || !graph.is_minimal(name))
if (it.hasNext) { val name = it.next(); Some((name, graph.get_node(name))) }
else None
}
}
/** build with results **/
class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)])
{
def sessions: Set[String] = results.keySet
def infos: List[Sessions.Info] = results.values.map(_._2).toList
def cancelled(name: String): Boolean = results(name)._1.isEmpty
def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
def info(name: String): Sessions.Info = results(name)._2
val rc: Int =
results.iterator.map({ case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }).
foldLeft(0)(_ max _)
def ok: Boolean = rc == 0
override def toString: String = rc.toString
}
def session_finished(session_name: String, process_result: Process_Result): String =
"Finished " + session_name + " (" + process_result.timing.message_resources + ")"
def session_timing(session_name: String, build_log: Build_Log.Session_Info): String =
{
val props = build_log.session_timing
val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1
val timing = Markup.Timing_Properties.parse(props)
"Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")"
}
def build(
options: Options,
selection: Sessions.Selection = Sessions.Selection.empty,
presentation: Presentation.Context = Presentation.Context.none,
progress: Progress = new Progress,
check_unknown_files: Boolean = false,
build_heap: Boolean = false,
clean_build: Boolean = false,
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
infos: List[Sessions.Info] = Nil,
numa_shuffling: Boolean = false,
max_jobs: Int = 1,
list_files: Boolean = false,
check_keywords: Set[String] = Set.empty,
fresh_build: Boolean = false,
no_build: Boolean = false,
soft_build: Boolean = false,
verbose: Boolean = false,
export_files: Boolean = false): Results =
{
val build_options =
options +
"completion_limit=0" +
"editor_tracing_messages=0" +
"kodkod_scala=false" +
("pide_reports=" + options.bool("build_pide_reports"))
val store = Sessions.store(build_options)
Isabelle_Fonts.init()
/* session selection and dependencies */
val full_sessions =
Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
val full_sessions_selection = full_sessions.imports_selection(selection)
def sources_stamp(deps: Sessions.Deps, session_name: String): String =
{
val digests =
full_sessions(session_name).meta_digest ::
deps.sources(session_name) :::
deps.imported_sources(session_name)
SHA1.digest_set(digests).toString
}
val deps =
{
val deps0 =
Sessions.deps(full_sessions.selection(selection),
progress = progress, inlined_files = true, verbose = verbose,
list_files = list_files, check_keywords = check_keywords).check_errors
if (soft_build && !fresh_build) {
val outdated =
deps0.sessions_structure.build_topological_order.flatMap(name =>
store.try_open_database(name) match {
case Some(db) =>
using(db)(store.read_build(_, name)) match {
case Some(build)
if build.ok && build.sources == sources_stamp(deps0, name) => None
case _ => Some(name)
}
case None => Some(name)
})
Sessions.deps(full_sessions.selection(Sessions.Selection(sessions = outdated)),
progress = progress, inlined_files = true).check_errors
}
else deps0
}
/* check unknown files */
if (check_unknown_files) {
val source_files =
(for {
(_, base) <- deps.session_bases.iterator
(path, _) <- base.sources.iterator
} yield path).toList
val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file)
val unknown_files =
Mercurial.check_files(source_files)._2.
filterNot(path => exclude_files.contains(path.canonical_file))
if (unknown_files.nonEmpty) {
progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" +
unknown_files.map(path => path.expand.implode).sorted.mkString("\n ", "\n ", ""))
}
}
/* main build process */
val queue = Queue(progress, deps.sessions_structure, store)
store.prepare_output_dir()
if (clean_build) {
for (name <- full_sessions.imports_descendants(full_sessions_selection)) {
val (relevant, ok) = store.clean_output(name)
if (relevant) {
if (ok) progress.echo("Cleaned " + name)
else progress.echo(name + " FAILED to clean")
}
}
}
// scheduler loop
case class Result(
current: Boolean,
heap_digest: Option[String],
process: Option[Process_Result],
info: Sessions.Info)
{
def ok: Boolean =
process match {
case None => false
case Some(res) => res.rc == 0
}
}
def sleep(): Unit =
Isabelle_Thread.interrupt_handler(_ => progress.stop()) { Time.seconds(0.5).sleep }
val numa_nodes = new NUMA.Nodes(numa_shuffling)
@tailrec def loop(
pending: Queue,
running: Map[String, (List[String], Build_Job)],
results: Map[String, Result]): Map[String, Result] =
{
def used_node(i: Int): Boolean =
running.iterator.exists(
{ case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i })
if (pending.is_empty) results
else {
if (progress.stopped) {
for ((_, (_, job)) <- running) job.terminate()
}
running.find({ case (_, (_, job)) => job.is_finished }) match {
case Some((session_name, (input_heaps, job))) =>
//{{{ finish job
val (process_result, heap_digest) = job.join
val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test)
val process_result_tail =
{
val tail = job.info.options.int("process_output_tail")
process_result.copy(
out_lines =
"(see also " + store.output_log(session_name).file.toString + ")" ::
(if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
}
val build_log =
Build_Log.Log_File(session_name, process_result.out_lines).
parse_session_info(
command_timings = true,
theory_timings = true,
ml_statistics = true,
task_statistics = true)
// write log file
if (process_result.ok) {
File.write_gzip(store.output_log_gz(session_name), terminate_lines(log_lines))
}
else File.write(store.output_log(session_name), terminate_lines(log_lines))
// write database
using(store.open_database(session_name, output = true))(db =>
store.write_session_info(db, session_name,
build_log =
if (process_result.timeout) build_log.error("Timeout") else build_log,
build =
Session_Info(sources_stamp(deps, session_name), input_heaps, heap_digest,
process_result.rc)))
// messages
process_result.err_lines.foreach(progress.echo)
if (process_result.ok) {
if (verbose) progress.echo(session_timing(session_name, build_log))
progress.echo(session_finished(session_name, process_result))
}
else {
progress.echo(session_name + " FAILED")
if (!process_result.interrupted) progress.echo(process_result_tail.out)
}
loop(pending - session_name, running - session_name,
results +
(session_name -> Result(false, heap_digest, Some(process_result_tail), job.info)))
//}}}
case None if running.size < (max_jobs max 1) =>
//{{{ check/start next job
pending.dequeue(running.isDefinedAt) match {
case Some((session_name, info)) =>
val ancestor_results =
deps.sessions_structure.build_requirements(List(session_name)).
filterNot(_ == session_name).map(results(_))
val ancestor_heaps = ancestor_results.flatMap(_.heap_digest)
val do_store =
build_heap || Sessions.is_pure(session_name) || queue.is_inner(session_name)
val (current, heap_digest) =
{
store.try_open_database(session_name) match {
case Some(db) =>
using(db)(store.read_build(_, session_name)) match {
case Some(build) =>
val heap_digest = store.find_heap_digest(session_name)
val current =
!fresh_build &&
build.ok &&
build.sources == sources_stamp(deps, session_name) &&
build.input_heaps == ancestor_heaps &&
build.output_heap == heap_digest &&
!(do_store && heap_digest.isEmpty)
(current, heap_digest)
case None => (false, None)
}
case None => (false, None)
}
}
val all_current = current && ancestor_results.forall(_.current)
if (all_current)
loop(pending - session_name, running,
results +
(session_name -> Result(true, heap_digest, Some(Process_Result(0)), info)))
else if (no_build) {
progress.echo_if(verbose, "Skipping " + session_name + " ...")
loop(pending - session_name, running,
results +
(session_name -> Result(false, heap_digest, Some(Process_Result(1)), info)))
}
else if (ancestor_results.forall(_.ok) && !progress.stopped) {
progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...")
store.clean_output(session_name)
using(store.open_database(session_name, output = true))(
store.init_session_info(_, session_name))
val numa_node = numa_nodes.next(used_node)
val job =
new Build_Job(progress, session_name, info, deps, store, do_store,
verbose, numa_node, queue.command_timings(session_name))
loop(pending, running + (session_name -> (ancestor_heaps, job)), results)
}
else {
progress.echo(session_name + " CANCELLED")
loop(pending - session_name, running,
results + (session_name -> Result(false, heap_digest, None, info)))
}
case None => sleep(); loop(pending, running, results)
}
///}}}
case None => sleep(); loop(pending, running, results)
}
}
}
/* build results */
val results =
{
val results0 =
if (deps.is_empty) {
progress.echo_warning("Nothing to build")
Map.empty[String, Result]
}
else Isabelle_Thread.uninterruptible { loop(queue, Map.empty, Map.empty) }
new Results(
(for ((name, result) <- results0.iterator)
yield (name, (result.process, result.info))).toMap)
}
if (export_files) {
for (name <- full_sessions.imports_selection(selection).iterator if results(name).ok) {
val info = results.info(name)
if (info.export_files.nonEmpty) {
progress.echo("Exporting " + info.name + " ...")
for ((dir, prune, pats) <- info.export_files) {
Export.export_files(store, name, info.dir + dir,
progress = if (verbose) progress else new Progress,
export_prune = prune,
export_patterns = pats)
}
}
}
}
if (results.rc != 0 && (verbose || !no_build)) {
val unfinished =
(for {
name <- results.sessions.iterator
if !results(name).ok
} yield name).toList.sorted
progress.echo("Unfinished session(s): " + commas(unfinished))
}
/* PDF/HTML presentation */
if (!no_build && !progress.stopped && results.ok) {
val selected = full_sessions_selection.toSet
val presentation_chapters =
(for {
session_name <- deps.sessions_structure.build_topological_order.iterator
info = results.info(session_name)
if selected(session_name) && presentation.enabled(info) && results(session_name).ok }
yield (info.chapter, (session_name, info.description))).toList
if (presentation_chapters.nonEmpty) {
val presentation_dir = presentation.dir(store)
progress.echo("Presentation in " + presentation_dir.absolute)
val resources = Resources.empty
val html_context = Presentation.html_context()
using(store.open_database_context())(db_context =>
for ((_, (session_name, _)) <- presentation_chapters) {
progress.expose_interrupt()
progress.echo("Presenting " + session_name + " ...")
Presentation.session_html(
resources, session_name, deps, db_context, progress = progress,
verbose = verbose, html_context = html_context,
elements = Presentation.elements1, presentation = presentation)
})
val browser_chapters =
presentation_chapters.groupBy(_._1).
map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
for ((chapter, entries) <- browser_chapters)
Presentation.update_chapter_index(presentation_dir, chapter, entries)
if (browser_chapters.nonEmpty) Presentation.make_global_index(presentation_dir)
}
}
results
}
/* Isabelle tool wrapper */
val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions",
Scala_Project.here, args =>
{
val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
var base_sessions: List[String] = Nil
var select_dirs: List[Path] = Nil
var numa_shuffling = false
var presentation = Presentation.Context.none
var requirements = false
var soft_build = false
var exclude_session_groups: List[String] = Nil
var all_sessions = false
var build_heap = false
var clean_build = false
var dirs: List[Path] = Nil
var export_files = false
var fresh_build = false
var session_groups: List[String] = Nil
var max_jobs = 1
var check_keywords: Set[String] = Set.empty
var list_files = false
var no_build = false
var options = Options.init(opts = build_options)
var verbose = false
var exclude_sessions: List[String] = Nil
val getopts = Getopts("""
Usage: isabelle build [OPTIONS] [SESSIONS ...]
Options are:
-B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
-N cyclic shuffling of NUMA CPU nodes (performance tuning)
-P DIR enable HTML/PDF presentation in directory (":" for default)
-R refer to requirements of selected sessions
-S soft build: only observe changes of sources, not heap images
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
-b build heap images
-c clean build
-d DIR include session directory
-e export files from session specification into file-system
-f fresh build
-g NAME select session group NAME
-j INT maximum number of parallel jobs (default 1)
-k KEYWORD check theory sources for conflicts with proposed keywords
-l list session source files
-n no build -- test dependencies only
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-v verbose
-x NAME exclude session NAME and all descendants
Build and manage Isabelle sessions, depending on implicit settings:
""" + Library.prefix_lines(" ", Build_Log.Settings.show()) + "\n",
"B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
"D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
"N" -> (_ => numa_shuffling = true),
"P:" -> (arg => presentation = Presentation.Context.make(arg)),
"R" -> (_ => requirements = true),
"S" -> (_ => soft_build = true),
"X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
"a" -> (_ => all_sessions = true),
"b" -> (_ => build_heap = true),
"c" -> (_ => clean_build = true),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
"e" -> (_ => export_files = true),
"f" -> (_ => fresh_build = true),
"g:" -> (arg => session_groups = session_groups ::: List(arg)),
"j:" -> (arg => max_jobs = Value.Int.parse(arg)),
"k:" -> (arg => check_keywords = check_keywords + arg),
"l" -> (_ => list_files = true),
"n" -> (_ => no_build = true),
"o:" -> (arg => options = options + arg),
"v" -> (_ => verbose = true),
"x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
val sessions = getopts(args)
val progress = new Console_Progress(verbose = verbose)
val start_date = Date.now()
if (verbose) {
progress.echo(
"Started at " + Build_Log.print_date(start_date) +
" (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
progress.echo(Build_Log.Settings.show() + "\n")
}
val results =
progress.interrupt_handler {
build(options,
selection = Sessions.Selection(
requirements = requirements,
all_sessions = all_sessions,
base_sessions = base_sessions,
exclude_session_groups = exclude_session_groups,
exclude_sessions = exclude_sessions,
session_groups = session_groups,
sessions = sessions),
presentation = presentation,
progress = progress,
- check_unknown_files = Mercurial.is_repository(Path.explode("~~")),
+ check_unknown_files = Mercurial.is_repository(Path.ISABELLE_HOME),
build_heap = build_heap,
clean_build = clean_build,
dirs = dirs,
select_dirs = select_dirs,
numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
max_jobs = max_jobs,
list_files = list_files,
check_keywords = check_keywords,
fresh_build = fresh_build,
no_build = no_build,
soft_build = soft_build,
verbose = verbose,
export_files = export_files)
}
val end_date = Date.now()
val elapsed_time = end_date.time - start_date.time
if (verbose) {
progress.echo("\nFinished at " + Build_Log.print_date(end_date))
}
val total_timing =
results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _).
copy(elapsed = elapsed_time)
progress.echo(total_timing.message_resources)
sys.exit(results.rc)
})
/* build logic image */
def build_logic(options: Options, logic: String,
progress: Progress = new Progress,
build_heap: Boolean = false,
dirs: List[Path] = Nil,
fresh: Boolean = false,
strict: Boolean = false): Int =
{
val selection = Sessions.Selection.session(logic)
val rc =
if (!fresh && build(options, selection = selection,
build_heap = build_heap, no_build = true, dirs = dirs).ok) 0
else {
progress.echo("Build started for Isabelle/" + logic + " ...")
Build.build(options, selection = selection, progress = progress,
build_heap = build_heap, fresh_build = fresh, dirs = dirs).rc
}
if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc
}
}
diff --git a/src/Pure/Tools/scala_project.scala b/src/Pure/Tools/scala_project.scala
--- a/src/Pure/Tools/scala_project.scala
+++ b/src/Pure/Tools/scala_project.scala
@@ -1,193 +1,193 @@
/* Title: Pure/Tools/scala_project.scala
Author: Makarius
Setup Gradle project for Isabelle/Scala/jEdit.
*/
package isabelle
object Scala_Project
{
/* groovy syntax */
def groovy_string(s: String): String =
{
s.map(c =>
c match {
case '\t' | '\b' | '\n' | '\r' | '\f' | '\\' | '\'' | '"' => "\\" + c
case _ => c.toString
}).mkString("'", "", "'")
}
/* file and directories */
lazy val isabelle_files: List[String] =
{
val files1 =
{
- val isabelle_home = Path.explode("~~").canonical
+ val isabelle_home = Path.ISABELLE_HOME.canonical
Path.split(Isabelle_System.getenv("ISABELLE_CLASSPATH")).
map(path => File.relative_path(isabelle_home, path).getOrElse(path).implode)
}
val files2 =
(for {
path <-
List(
Path.explode("~~/lib/classes/Pure.shasum"),
Path.explode("~~/src/Tools/jEdit/dist/Isabelle-jEdit.shasum"))
if path.is_file
line <- Library.trim_split_lines(File.read(path))
name =
if (line.length > 42 && line(41) == '*') line.substring(42)
else error("Bad shasum entry: " + quote(line))
if name != "lib/classes/Pure.jar" &&
name != "src/Tools/jEdit/dist/jedit.jar" &&
name != "src/Tools/jEdit/dist/jars/Isabelle-jEdit-base.jar" &&
name != "src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar"
} yield name)
files1 ::: files2
}
lazy val isabelle_scala_files: Map[String, Path] =
isabelle_files.foldLeft(Map.empty[String, Path]) {
case (map, name) =>
if (!name.startsWith("src/Tools/jEdit/") && name.endsWith(".scala")) {
val path = Path.explode("~~/" + name)
val base = path.base.implode
map.get(base) match {
case None => map + (base -> path)
case Some(path1) => error("Conflicting base names: " + path + " vs. " + path1)
}
}
else map
}
val isabelle_dirs: List[(String, Path)] =
List(
"src/Pure/" -> Path.explode("isabelle"),
"src/Tools/Graphview/" -> Path.explode("isabelle.graphview"),
"src/Tools/VSCode/" -> Path.explode("isabelle.vscode"),
"src/Tools/jEdit/src-base/" -> Path.explode("isabelle.jedit_base"),
"src/Tools/jEdit/src/" -> Path.explode("isabelle.jedit"),
"src/HOL/SPARK/Tools" -> Path.explode("isabelle.spark"),
"src/HOL/Tools/ATP" -> Path.explode("isabelle.atp"),
"src/HOL/Tools/Nitpick" -> Path.explode("isabelle.nitpick"))
/* compile-time position */
def here: Here =
{
val exn = new Exception
exn.getStackTrace.toList match {
case _ :: caller :: _ =>
val name = proper_string(caller.getFileName).getOrElse("")
val line = caller.getLineNumber
new Here(name, line)
case _ => new Here("", 0)
}
}
class Here private[Scala_Project](name: String, line: Int)
{
override def toString: String = name + ":" + line
def position: Position.T =
isabelle_scala_files.get(name) match {
case Some(path) => Position.Line_File(line, path.implode)
case None => Position.none
}
}
/* scala project */
def scala_project(project_dir: Path, symlinks: Boolean = false): Unit =
{
if (symlinks && Platform.is_windows)
error("Cannot create symlinks on Windows")
if (project_dir.is_file || project_dir.is_dir)
error("Project directory already exists: " + project_dir)
val src_dir = project_dir + Path.explode("src/main/scala")
val java_src_dir = project_dir + Path.explode("src/main/java")
val scala_src_dir = Isabelle_System.make_directory(project_dir + Path.explode("src/main/scala"))
Isabelle_System.copy_dir(Path.explode("~~/src/Tools/jEdit/dist/jEdit"), java_src_dir)
val files = isabelle_files
isabelle_scala_files
for (file <- files if file.endsWith(".scala")) {
val (path, target) =
isabelle_dirs.collectFirst({
case (prfx, p) if file.startsWith(prfx) =>
- (Path.explode("~~") + Path.explode(file), scala_src_dir + p)
+ (Path.ISABELLE_HOME + Path.explode(file), scala_src_dir + p)
}).getOrElse(error("Unknown directory prefix for " + quote(file)))
Isabelle_System.make_directory(target)
if (symlinks) Isabelle_System.symlink(path, target)
else Isabelle_System.copy_file(path, target)
}
val jars =
for (file <- files if file.endsWith(".jar"))
yield {
if (file.startsWith("/")) file
else Isabelle_System.getenv("ISABELLE_HOME") + "/" + file
}
File.write(project_dir + Path.explode("settings.gradle"), "rootProject.name = 'Isabelle'\n")
File.write(project_dir + Path.explode("build.gradle"),
"""plugins {
id 'scala'
}
repositories {
mavenCentral()
}
dependencies {
implementation 'org.scala-lang:scala-library:""" + scala.util.Properties.versionNumberString + """'
compile files(
""" + jars.map(jar => groovy_string(File.platform_path(jar))).mkString("", ",\n ", ")") +
"""
}
""")
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("scala_project", "setup Gradle project for Isabelle/Scala/jEdit",
Scala_Project.here, args =>
{
var symlinks = false
val getopts = Getopts("""
Usage: isabelle scala_project [OPTIONS] PROJECT_DIR
Options are:
-L make symlinks to original scala files
Setup Gradle project for Isabelle/Scala/jEdit --- to support Scala IDEs
such as IntelliJ IDEA.
""",
"L" -> (_ => symlinks = true))
val more_args = getopts(args)
val project_dir =
more_args match {
case List(dir) => Path.explode(dir)
case _ => getopts.usage()
}
scala_project(project_dir, symlinks = symlinks)
})
}