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,325 +1,325 @@ /* Title: Pure/Admin/build_history.scala Author: Makarius Build other history versions. */ package isabelle import java.io.{File => JFile} import java.time.format.DateTimeFormatter import java.util.Locale object Build_History { /* log files */ val BUILD_HISTORY = "build_history" val META_INFO_MARKER = "\fmeta_info = " /* augment settings */ def augment_settings( other_isabelle: Other_Isabelle, threads: Int, arch_64: Boolean = false, heap: Int = default_heap, max_heap: Option[Int] = None, more_settings: List[String]): String = { val (ml_platform, ml_settings) = { val windows_32 = "x86-windows" val windows_64 = "x86_64-windows" val platform_32 = other_isabelle("getenv -b ISABELLE_PLATFORM32").check.out val platform_64 = other_isabelle("getenv -b ISABELLE_PLATFORM64").check.out val platform_family = other_isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out val polyml_home = try { Path.explode(other_isabelle("getenv -b ML_HOME").check.out).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_32)) windows_32 else platform_32 // x86-cygwin } else { val (platform, platform_name) = if (arch_64) (platform_64, "x86_64-" + platform_family) else (platform_32, "x86-" + platform_family) if (check_dir(platform)) platform else err(platform_name) } 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_rev = "tip" private val default_threads = 1 private val default_heap = 1000 private val default_isabelle_identifier = "build_history" def build_history( progress: Progress, hg: Mercurial.Repository, rev: String = default_rev, isabelle_identifier: String = default_isabelle_identifier, components_base: String = "", fresh: Boolean = false, nonfree: Boolean = false, multicore_base: Boolean = false, threads_list: List[Int] = List(default_threads), arch_64: Boolean = false, heap: Int = default_heap, max_heap: Option[Int] = None, more_settings: List[String] = Nil, verbose: Boolean = false, build_args: List[String] = Nil): List[Process_Result] = { /* sanity checks */ if (File.eq(Path.explode("~~").file, hg.root.file)) error("Repository coincides with ISABELLE_HOME=" + Path.explode("~~").expand) for (threads <- threads_list if threads < 1) error("Bad threads value < 1: " + threads) 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") } /* init repository */ hg.update(rev = rev, clean = true) progress.echo_if(verbose, hg.log(rev, options = "-l1")) val isabelle_version = hg.identify(rev, options = "-i") val other_isabelle = new Other_Isabelle(progress, hg.root, isabelle_identifier) /* main */ val build_history_date = Date.now() val build_host = Isabelle_System.hostname() var first_build = true for (threads <- threads_list) yield { /* init settings */ other_isabelle.init_settings(components_base, nonfree) other_isabelle.resolve_components(verbose) val ml_platform = augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings) val isabelle_output = Path.explode(other_isabelle("getenv -b ISABELLE_OUTPUT").check.out) 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(verbose) other_isabelle.bash( "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " + "bin/isabelle jedit -b" + (if (fresh) " -f" else ""), redirect = true, echo = verbose).check Isabelle_System.rm_tree(isabelle_base_log.file) } Isabelle_System.rm_tree(isabelle_output.file) Isabelle_System.mkdirs(isabelle_output) /* build */ if (multicore_base && !first_build && isabelle_base_log.is_dir) - other_isabelle.copy_dir(isabelle_base_log, isabelle_output_log) + Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log) val build_start = Date.now() val res = other_isabelle("build -v " + File.bash_args(build_args), redirect = true, echo = verbose) val build_end = Date.now() /* output log */ val log_path = other_isabelle.isabelle_home_user + Path.explode("log") + Build_Log.log_path(BUILD_HISTORY, build_history_date, ml_platform, "M" + threads).ext("gz") val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info() val meta_info = List(Build_Log.Field.build_engine -> BUILD_HISTORY, Build_Log.Field.build_host -> build_host, Build_Log.Field.build_start -> Build_Log.print_date(build_start), Build_Log.Field.build_end -> Build_Log.print_date(build_end), Build_Log.Field.isabelle_version -> isabelle_version) val ml_statistics = build_info.finished_sessions.flatMap(session_name => { val session_log = isabelle_output_log + Path.explode(session_name).ext("gz") if (session_log.is_file) { Build_Log.Log_File(session_log).parse_session_info(ml_statistics = true). ml_statistics.map(props => (Build_Log.SESSION_NAME -> session_name) :: props) } else Nil }) 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 }) Isabelle_System.mkdirs(log_path.dir) File.write_gzip(log_path, terminate_lines( Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: res.out_lines ::: ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) ::: heap_sizes)) Output.writeln(log_path.implode, stdout = true) /* next build */ if (multicore_base && first_build && isabelle_output_log.is_dir) - other_isabelle.copy_dir(isabelle_output_log, isabelle_base_log) + Isabelle_System.copy_dir(isabelle_output_log, isabelle_base_log) first_build = false res } } /* command line entry point */ def main(args: Array[String]) { Command_Line.tool0 { var multicore_base = false var components_base = "" var heap: Option[Int] = None var max_heap: Option[Int] = None var threads_list = List(default_threads) var isabelle_identifier = default_isabelle_identifier var more_settings: List[String] = Nil var fresh = false var arch_64 = false var nonfree = false var rev = default_rev var verbose = false val getopts = Getopts(""" Usage: isabelle build_history [OPTIONS] REPOSITORY [ARGS ...] Options are: -B first multicore build serves as base for scheduling information -C DIR base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib) -H SIZE minimal ML heap in MB (default: """ + default_heap + """ for x86, """ + default_heap * 2 + """ for x86_64) -M THREADS multicore configurations (comma-separated list, default: """ + default_threads + """) -N NAME alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """) -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) -m ARCH processor architecture (32=x86, 64=x86_64, default: x86) -n include nonfree components -r REV update to revision (default: """ + default_rev + """) -v verbose Build Isabelle sessions from the history of another REPOSITORY clone, passing ARGS directly to its isabelle build tool. """, "B" -> (_ => multicore_base = true), "C:" -> (arg => components_base = arg), "H:" -> (arg => heap = Some(Value.Int.parse(arg))), "M:" -> (arg => threads_list = space_explode(',', arg).map(Value.Int.parse(_))), "N:" -> (arg => isabelle_identifier = arg), "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))), "e:" -> (arg => more_settings = more_settings ::: List(arg)), "f" -> (_ => fresh = true), "m:" -> { case "32" | "x86" => arch_64 = false case "64" | "x86_64" => arch_64 = true case bad => error("Bad processor architecture: " + quote(bad)) }, "n" -> (_ => nonfree = true), "r:" -> (arg => rev = arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) val (root, build_args) = more_args match { case root :: build_args => (root, build_args) case _ => getopts.usage() } val hg = Mercurial.repository(Path.explode(root)) val progress = new Console_Progress(stderr = true) val results = build_history(progress, hg, rev = rev, isabelle_identifier = isabelle_identifier, components_base = components_base, fresh = fresh, nonfree = nonfree, multicore_base = multicore_base, threads_list = threads_list, arch_64 = arch_64, heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap), max_heap = max_heap, more_settings = more_settings, verbose = verbose, build_args = build_args) val rc = (0 /: results) { case (rc, res) => rc max res.rc } if (rc != 0) sys.exit(rc) } } } 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,66 +1,63 @@ /* Title: Pure/Admin/other_isabelle.scala Author: Makarius Manage other Isabelle distributions. */ package isabelle private class Other_Isabelle(progress: Progress, isabelle_home: Path, isabelle_identifier: String) { other_isabelle => /* static system */ def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = Isabelle_System.bash( "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script, env = null, cwd = isabelle_home.file, redirect = redirect, progress_stdout = progress.echo_if(echo, _), progress_stderr = progress.echo_if(echo, _)) - def copy_dir(dir1: Path, dir2: Path): Unit = - bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check - def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = bash("bin/isabelle " + cmdline, redirect, echo) def resolve_components(echo: Boolean): Unit = other_isabelle("components -a", redirect = true, echo = echo).check val isabelle_home_user: Path = Path.explode(other_isabelle("getenv -b ISABELLE_HOME_USER").check.out) val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings") /* init settings */ def init_settings(components_base: String, nonfree: Boolean) { if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle")) error("Cannot proceed with existing user settings file: " + etc_settings) Isabelle_System.mkdirs(etc_settings.dir) File.write(etc_settings, "# generated by Isabelle " + Date.now() + "\n" + "#-*- shell-script -*- :mode=shellscript:\n") val component_settings = { val components_base_path = if (components_base == "") isabelle_home_user.dir + Path.explode("contrib") else Path.explode(components_base).expand val catalogs = if (nonfree) List("main", "optional", "nonfree") else List("main", "optional") catalogs.map(catalog => "init_components " + File.bash_path(components_base_path) + " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"") } File.append(etc_settings, "\n" + terminate_lines(component_settings)) } } 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,344 +1,347 @@ /* 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, BufferedReader, InputStreamReader} import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult} import java.nio.file.attribute.BasicFileAttributes import scala.collection.mutable 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 = { def check(s: String): Option[String] = if (s != null && s != "") Some(s) else None val value = check(preference) orElse // explicit argument check(System.getenv(envar)) orElse // e.g. inherited from running isabelle tool check(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 **/ @volatile private var _settings: Option[Map[String, String]] = None def settings(): Map[String, String] = { if (_settings.isEmpty) init() // unsynchronized check _settings.get } def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized { if (_settings.isEmpty) { import scala.collection.JavaConversions._ 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() { 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") else Nil val cmd2 = List(isabelle_root1 + JFile.separator + "bin" + JFile.separator + "isabelle", "getenv", "-d", dump.toString) val (output, rc) = process_output(process(cmd1 ::: cmd2, env = env, redirect = true)) if (rc != 0) error(output) val entries = (for (entry <- File.read(dump).split("\u0000") 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() } } /* getenv */ def getenv(name: String): String = settings().getOrElse(name, "") def getenv_strict(name: String): String = { val value = getenv(name) if (value != "") value else error("Undefined Isabelle environment variable: " + quote(name)) } def cygwin_root(): String = getenv_strict("CYGWIN_ROOT") def library_path(env: Map[String, String], elem: String): Map[String, String] = if (Platform.is_windows) env else { val x = if (Platform.is_macos) "DYLD_LIBRARY_PATH" else "LD_LIBRARY_PATH" env.getOrElse(x, "") match { case "" => env + (x -> elem) case y => env + (x -> (y + ":" + elem)) } } /** file-system operations **/ /* source files of Isabelle/ML bootstrap */ def source_file(path: Path): Option[Path] = { def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None if (path.is_absolute || path.is_current) check(path) else { check(Path.explode("~~/src/Pure") + path) orElse (if (getenv("ML_SOURCES") == "") None else check(Path.explode("$ML_SOURCES") + path)) } } - /* mkdirs */ + /* directories */ def mkdirs(path: Path): Unit = if (!path.is_dir) { bash("perl -e \"use File::Path make_path; make_path('" + File.standard_path(path) + "');\"") if (!path.is_dir) error("Failed to create directory: " + quote(File.platform_path(path))) } + def copy_dir(dir1: Path, dir2: Path): Unit = + bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check + /* tmp files */ private def isabelle_tmp_prefix(): JFile = { val path = Path.explode("$ISABELLE_TMP_PREFIX") path.file.mkdirs // low-level mkdirs File.platform_file(path) } def tmp_file(name: String, ext: String = ""): JFile = { val suffix = if (ext == "") "" else "." + ext val file = Files.createTempFile(isabelle_tmp_prefix().toPath, name, suffix).toFile file.deleteOnExit file } def with_tmp_file[A](name: String, ext: String = "")(body: JFile => A): A = { val file = tmp_file(name, ext) try { body(file) } finally { file.delete } } /* tmp dirs */ def rm_tree(root: JFile) { root.delete if (root.isDirectory) { Files.walkFileTree(root.toPath, new SimpleFileVisitor[JPath] { override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult = { Files.delete(file) FileVisitResult.CONTINUE } override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult = { if (e == null) { Files.delete(dir) FileVisitResult.CONTINUE } else throw e } } ) } } def tmp_dir(name: String): JFile = { val dir = Files.createTempDirectory(isabelle_tmp_prefix().toPath, name).toFile dir.deleteOnExit dir } def with_tmp_dir[A](name: String)(body: JFile => A): A = { val dir = tmp_dir(name) try { body(dir) } finally { rm_tree(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 Thread.interrupted } (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) => (), progress_limit: Option[Long] = None, strict: Boolean = true, cleanup: () => Unit = () => ()): Process_Result = { Bash.process(script, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup). result(progress_stdout, progress_stderr, progress_limit, strict) } def hostname(): String = bash("hostname -s").check.out def open(arg: String): Unit = bash("exec \"$ISABELLE_OPEN\" " + File.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 &") /** 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 => Isabelle_System.getenv_strict("ISABELLE_LOGIC") } } }