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,607 +1,607 @@ /* Title: Pure/Admin/build_history.scala Author: Makarius Build other history versions. */ package isabelle object Build_History { /* log files */ val engine = "build_history" val log_prefix = engine + "_" /* augment settings */ def augment_settings( other_isabelle: Other_Isabelle, threads: Int, arch_64: Boolean, heap: Int, max_heap: Option[Int], more_settings: List[String] ): String = { val (ml_platform, ml_settings) = { val cygwin_32 = "x86-cygwin" val windows_32 = "x86-windows" val windows_64 = "x86_64-windows" val windows_64_32 = "x86_64_32-windows" val platform_32 = other_isabelle.getenv("ISABELLE_PLATFORM32") val platform_64 = other_isabelle.getenv("ISABELLE_PLATFORM64") val platform_64_32 = platform_64.replace("x86_64-", "x86_64_32-") val polyml_home = try { Path.explode(other_isabelle.getenv("ML_HOME")).dir } catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) } def ml_home(platform: String): Path = polyml_home + Path.explode(platform) def err(platform: String): Nothing = error("Platform " + platform + " unavailable on this machine") def check_dir(platform: String): Boolean = platform != "" && ml_home(platform).is_dir val ml_platform = if (Platform.is_windows && arch_64) { if (check_dir(windows_64)) windows_64 else err(windows_64) } else if (Platform.is_windows && !arch_64) { if (check_dir(windows_64_32)) windows_64_32 else if (check_dir(cygwin_32)) cygwin_32 else if (check_dir(windows_32)) windows_32 else err(windows_32) } else if (arch_64) { if (check_dir(platform_64)) platform_64 else err(platform_64) } else if (check_dir(platform_64_32)) platform_64_32 else platform_32 val ml_options = "--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") + " --gcthreads " + threads + (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "") (ml_platform, List( "ML_HOME=" + File.bash_path(ml_home(ml_platform)), "ML_PLATFORM=" + quote(ml_platform), "ML_OPTIONS=" + quote(ml_options))) } val thread_settings = List( "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"", "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"") val settings = List(ml_settings, thread_settings) ::: (if (more_settings.isEmpty) Nil else List(more_settings)) File.append(other_isabelle.etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_)))) ml_platform } /** local build **/ private val default_multicore = (1, 1) private val default_heap = 1500 private val default_isabelle_identifier = "build_history" def local_build( options: Options, root: Path, progress: Progress = new Progress, afp: Boolean = false, afp_partition: Int = 0, isabelle_identifier: String = default_isabelle_identifier, ml_statistics_step: Int = 1, - component_repository: String = Components.default_component_repository, - components_base: String = Components.standard_components_base, + component_repository: String = Components.static_component_repository, + components_base: String = Components.dynamic_components_base, clean_platforms: Option[List[Platform.Family.Value]] = None, clean_archives: Boolean = false, fresh: Boolean = false, hostname: String = "", multicore_base: Boolean = false, multicore_list: List[(Int, Int)] = List(default_multicore), arch_64: Boolean = false, heap: Int = default_heap, max_heap: Option[Int] = None, init_settings: List[String] = Nil, more_settings: List[String] = Nil, more_preferences: List[String] = Nil, verbose: Boolean = false, build_tags: List[String] = Nil, build_args: List[String] = Nil ): List[(Process_Result, Path)] = { /* sanity checks */ if (File.eq(Path.ISABELLE_HOME, root)) { error("Repository coincides with ISABELLE_HOME=" + Path.ISABELLE_HOME.expand) } for ((threads, _) <- multicore_list if threads < 1) { error("Bad threads value < 1: " + threads) } for ((_, processes) <- multicore_list if processes < 1) { error("Bad processes value < 1: " + processes) } if (heap < 100) error("Bad heap value < 100: " + heap) if (max_heap.isDefined && max_heap.get < heap) { error("Bad max_heap value < heap: " + max_heap.get) } System.getenv("ISABELLE_SETTINGS_PRESENT") match { case null | "" => case _ => error("Cannot run Admin/build_other within existing Isabelle settings environment") } /* Isabelle + AFP directory */ def directory(dir: Path): Mercurial.Hg_Sync.Directory = { val directory = Mercurial.Hg_Sync.directory(dir) if (verbose) progress.echo(directory.log) directory } val isabelle_directory = directory(root) val afp_directory = if (afp) Some(directory(root + Path.explode("AFP"))) else None val (afp_build_args, afp_sessions) = if (afp_directory.isEmpty) (Nil, Nil) else { val (opt, sessions) = { if (afp_partition == 0) ("-d", Nil) else { try { val afp_info = AFP.init(options, base_dir = afp_directory.get.root) ("-d", afp_info.partition(afp_partition)) } catch { case ERROR(_) => ("-D", Nil) } } } (List(opt, "~~/AFP/thys"), sessions) } /* main */ val other_isabelle = Other_Isabelle(root, isabelle_identifier = isabelle_identifier, progress = progress) def resolve_components(): Unit = other_isabelle.resolve_components( echo = verbose, component_repository = component_repository, clean_platforms = clean_platforms, clean_archives = clean_archives) 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( components_base = components_base, catalogs = Components.optional_catalogs) other_isabelle.init_settings(component_settings ::: init_settings) resolve_components() val ml_platform = augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings) File.write(other_isabelle.etc_preferences, cat_lines(more_preferences)) val isabelle_output = other_isabelle.expand_path( Path.explode("$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER")) val isabelle_output_log = isabelle_output + Path.explode("log") val isabelle_base_log = isabelle_output + Path.explode("../base_log") if (first_build) { resolve_components() other_isabelle.scala_build(fresh = fresh, echo = verbose) for { tool <- List("ghc_setup", "ocaml_setup") if other_isabelle.getenv("ISABELLE_" + Word.uppercase(tool)) == "true" && (other_isabelle.isabelle_home + Path.explode("lib/Tools/" + tool)).is_file } other_isabelle.bash("bin/isabelle " + tool, echo = verbose) Isabelle_System.rm_tree(isabelle_base_log) } Isabelle_System.rm_tree(isabelle_output) Isabelle_System.make_directory(isabelle_output) other_isabelle.expand_path(Path.explode("$ISABELLE_HOME_USER/mash_state")).file.delete val log_path = other_isabelle.isabelle_home_user + Build_Log.log_subdir(build_history_date) + Build_Log.log_filename(Build_History.engine, build_history_date, List(build_host, ml_platform, "M" + threads) ::: build_tags) Isabelle_System.make_directory(log_path.dir) val build_out = other_isabelle.expand_path(Path.explode("$ISABELLE_HOME_USER/log/build.out")) val build_out_progress = new File_Progress(build_out) build_out.file.delete /* build */ if (multicore_base && !first_build && isabelle_base_log.is_dir) { Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log) } val build_start = Date.now() val build_args1 = List("-v", "-j" + processes) ::: afp_build_args ::: build_args val build_result = Other_Isabelle(root, isabelle_identifier = isabelle_identifier, progress = build_out_progress) .bash("bin/isabelle build " + Bash.strings(build_args1 ::: afp_sessions), redirect = true, echo = true, strict = false) val build_end = Date.now() val build_info: Build_Log.Build_Info = Build_Log.Log_File(log_path.file_name, build_result.out_lines). parse_build_info(ml_statistics = true) /* output log */ val store = Sessions.store(options + "build_database_server=false") val meta_info = Properties.lines_nonempty(Build_Log.Prop.build_tags.name, build_tags) ::: Properties.lines_nonempty(Build_Log.Prop.build_args.name, build_args1) ::: List( Build_Log.Prop.build_group_id.name -> build_group_id, Build_Log.Prop.build_id.name -> (build_host + ":" + build_start.time.ms), Build_Log.Prop.build_engine.name -> Build_History.engine, Build_Log.Prop.build_host.name -> build_host, Build_Log.Prop.build_start.name -> Build_Log.print_date(build_start), Build_Log.Prop.build_end.name -> Build_Log.print_date(build_end), Build_Log.Prop.isabelle_version.name -> isabelle_directory.id) ::: afp_directory.map(dir => Build_Log.Prop.afp_version.name -> dir.id).toList build_out_progress.echo("Reading session build info ...") val session_build_info = build_info.finished_sessions.flatMap { session_name => val database = isabelle_output + store.database(session_name) if (database.is_file) { using(SQLite.open_database(database)) { db => val theory_timings = try { store.read_theory_timings(db, session_name).map(ps => Protocol.Theory_Timing_Marker((Build_Log.SESSION_NAME, session_name) :: ps)) } catch { case ERROR(_) => Nil } val session_sources = store.read_build(db, session_name).map(_.sources) match { case Some(sources) if sources.length == SHA1.digest_length => List("Sources " + session_name + " " + sources) case _ => Nil } theory_timings ::: session_sources } } else Nil } build_out_progress.echo("Reading ML statistics ...") val ml_statistics = build_info.finished_sessions.flatMap { session_name => val database = isabelle_output + store.database(session_name) val log_gz = isabelle_output + store.log_gz(session_name) val properties = if (database.is_file) { using(SQLite.open_database(database))(db => store.read_ml_statistics(db, session_name)) } else if (log_gz.is_file) { Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics } else Nil val trimmed_properties = if (ml_statistics_step <= 0) Nil else if (ml_statistics_step == 1) properties else { (for { (ps, i) <- properties.iterator.zipWithIndex if i % ml_statistics_step == 0 } yield ps).toList } trimmed_properties.map(ps => (Build_Log.SESSION_NAME -> session_name) :: ps) } build_out_progress.echo("Reading error messages ...") val session_errors = build_info.failed_sessions.flatMap { session_name => val database = isabelle_output + store.database(session_name) val errors = if (database.is_file) { try { using(SQLite.open_database(database))(db => store.read_errors(db, session_name)) } // column "errors" could be missing catch { case _: java.sql.SQLException => Nil } } else Nil errors.map(msg => List(Build_Log.SESSION_NAME -> session_name, Markup.CONTENT -> msg)) } build_out_progress.echo("Reading heap sizes ...") val heap_sizes = build_info.finished_sessions.flatMap { session_name => val heap = isabelle_output + Path.explode(session_name) if (heap.is_file) { Some("Heap " + session_name + " (" + Value.Long(File.space(heap).bytes) + " bytes)") } else None } build_out_progress.echo("Writing log file " + log_path.xz + " ...") File.write_xz(log_path.xz, terminate_lines( Protocol.Meta_Info_Marker(meta_info) :: build_result.out_lines ::: session_build_info ::: ml_statistics.map(Protocol.ML_Statistics_Marker.apply) ::: session_errors.map(Protocol.Error_Message_Marker.apply) ::: heap_sizes), Compress.Options_XZ(6)) /* next build */ if (multicore_base && first_build && isabelle_output_log.is_dir) { Isabelle_System.copy_dir(isabelle_output_log, isabelle_base_log) } Isabelle_System.rm_tree(isabelle_output) first_build = false (build_result, log_path.xz) } } /* command line entry point */ private object Multicore { private val Pat1 = """^(\d+)$""".r private val Pat2 = """^(\d+)x(\d+)$""".r def parse(s: String): (Int, Int) = s match { case Pat1(Value.Int(x)) => (x, 1) case Pat2(Value.Int(x), Value.Int(y)) => (x, y) case _ => error("Bad multicore configuration: " + quote(s)) } } def main(args: Array[String]): Unit = { Command_Line.tool { var afp = false var multicore_base = false - var components_base = Components.standard_components_base + var components_base = Components.dynamic_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 clean_platforms: Option[List[Platform.Family.Value]] = None var afp_partition = 0 var clean_archives = false - var component_repository = Components.default_component_repository + var component_repository = Components.static_component_repository var more_settings: List[String] = Nil var more_preferences: List[String] = Nil var fresh = false var hostname = "" var init_settings: List[String] = Nil var arch_64 = false var output_file = "" var ml_statistics_step = 1 var build_tags = List.empty[String] var verbose = false var exit_code = false val getopts = Getopts(""" Usage: Admin/build_other [OPTIONS] ISABELLE_HOME [ARGS ...] Options are: -A include $ISABELLE_HOME/AFP directory -B first multicore build serves as base for scheduling information -C DIR base directory for Isabelle components (default: """ + - quote(Components.standard_components_base) + """) + quote(Components.dynamic_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 + """) -O PLATFORMS clean resolved components, retaining only the given list platform families (separated by commas; default: do nothing) -P NUMBER AFP partition number (0, 1, 2, default: 0=unrestricted) -Q clean archives of downloaded components -R URL remote repository for Isabelle components (default: """ + - Components.default_component_repository + """) + Components.static_component_repository + """) -U SIZE maximal ML heap in MB (default: unbounded) -e TEXT additional text for generated etc/settings -f fresh build of Isabelle/Scala components (recommended) -h NAME override local hostname -i TEXT initial text for generated etc/settings -m ARCH processor architecture (32=x86, 64=x86_64, default: x86) -n no build: sync only -o FILE output file for log names (default: stdout) -p TEXT additional text for generated etc/preferences -s NUMBER step size for ML statistics (0=none, 1=all, n=step, default: 1) -t TAG free-form build tag (multiple occurrences possible) -v verbose -x return overall exit code from build processes Build Isabelle sessions from the history of another REPOSITORY clone, passing ARGS directly to its isabelle build tool. Each MULTICORE configuration consists of one or two numbers (default 1): THREADS or THREADSxPROCESSES, e.g. -M 1,2,4 or -M 1x4,2x2,4. """, "A" -> (_ => afp = true), "B" -> (_ => multicore_base = true), "C:" -> (arg => components_base = arg), "H:" -> (arg => heap = Some(Value.Int.parse(arg))), "M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse)), "N:" -> (arg => isabelle_identifier = arg), "O:" -> (arg => clean_platforms = Some(space_explode(',',arg).map(Platform.Family.parse))), "P:" -> (arg => afp_partition = Value.Int.parse(arg)), "Q" -> (_ => clean_archives = true), "R:" -> (arg => component_repository = arg), "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))), "e:" -> (arg => more_settings = more_settings ::: List(arg)), "f" -> (_ => fresh = true), "h:" -> (arg => hostname = arg), "i:" -> (arg => init_settings = init_settings ::: List(arg)), "m:" -> { case "32" | "x86" => arch_64 = false case "64" | "x86_64" => arch_64 = true case bad => error("Bad processor architecture: " + quote(bad)) }, "o:" -> (arg => output_file = arg), "p:" -> (arg => more_preferences = more_preferences ::: List(arg)), "s:" -> (arg => ml_statistics_step = Value.Int.parse(arg)), "t:" -> (arg => build_tags = build_tags ::: List(arg)), "v" -> (_ => verbose = true), "x" -> (_ => exit_code = true)) val more_args = getopts(args) val (root, build_args) = more_args match { case root :: build_args => (Path.explode(root), build_args) case _ => getopts.usage() } val progress = new Console_Progress(stderr = true) val results = local_build(Options.init(), root, progress = progress, afp = afp, afp_partition = afp_partition, isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step, component_repository = component_repository, components_base = components_base, clean_platforms = clean_platforms, clean_archives = clean_archives, fresh = fresh, hostname = hostname, multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64, heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap), max_heap = max_heap, init_settings = init_settings, more_settings = more_settings, more_preferences = more_preferences, verbose = verbose, build_tags = build_tags, build_args = build_args) if (output_file.isEmpty) { for ((_, log_path) <- results) Output.writeln(log_path.implode, stdout = true) } else { File.write(Path.explode(output_file), cat_lines(for ((_, log_path) <- results) yield log_path.implode)) } val rc = results.foldLeft(Process_Result.RC.ok) { case (rc, (res, _)) => rc max res.rc } if (rc != Process_Result.RC.ok && exit_code) sys.exit(rc) } } /** remote build -- via rsync and ssh **/ def remote_build( ssh: SSH.Session, isabelle_self: Path, isabelle_other: Path, isabelle_identifier: String = "remote_build_history", clean_platforms: Boolean = false, clean_archives: Boolean = false, progress: Progress = new Progress, protect_args: Boolean = false, rev: String = "", afp_repos: Option[Path] = None, afp_rev: String = "", options: String = "", args: String = "", no_build: Boolean = false, ): List[(String, Bytes)] = { /* synchronize Isabelle + AFP repositories */ def sync(target: Path, accurate: Boolean = false, rev: String = "", afp_rev: String = "", afp: Boolean = false ): Unit = { val context = Rsync.Context(progress, ssh_port = ssh.port, ssh_control_path = ssh.control_path, protect_args = protect_args) Sync.sync(ssh.options, context, ssh.rsync_path(target), thorough = accurate, preserve_jars = !accurate, rev = rev, afp_rev = afp_rev, afp_root = if (afp) afp_repos else None) } sync(isabelle_self) val self_isabelle = Other_Isabelle(isabelle_self, isabelle_identifier = isabelle_identifier, ssh = ssh, progress = progress) self_isabelle.init(fresh = true, echo = true) sync(isabelle_other, accurate = true, rev = proper_string(rev) getOrElse "tip", afp_rev = proper_string(afp_rev) getOrElse "tip", afp = true) /* build */ if (no_build) Nil else { ssh.with_tmp_dir { tmp_dir => val output_file = tmp_dir + Path.explode("output") val build_options = (if (afp_repos.isEmpty) "" else " -A") + " " + options try { val script = ssh.bash_path(Path.explode("Admin/build_other")) + (if (clean_platforms) " -O " + Bash.string(ssh.isabelle_platform.ISABELLE_PLATFORM_FAMILY) else "") + (if (clean_archives) " -Q" else "") + " -o " + ssh.bash_path(output_file) + build_options + " " + ssh.bash_path(isabelle_other) + " " + args self_isabelle.bash(script, echo = true, strict = false).check } catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred for Admin/build_other " + build_options) } for (line <- split_lines(ssh.read(output_file))) yield { val log = Path.explode(line) val bytes = ssh.read_bytes(log) ssh.delete(log) (log.file_name, bytes) } } } } } diff --git a/src/Pure/Admin/isabelle_cronjob.scala b/src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala +++ b/src/Pure/Admin/isabelle_cronjob.scala @@ -1,639 +1,639 @@ /* Title: Pure/Admin/isabelle_cronjob.scala Author: Makarius Main entry point for administrative cronjob at TUM. */ package isabelle import java.nio.file.Files import scala.annotation.tailrec object Isabelle_Cronjob { /* global resources: owned by main cronjob */ val backup = "lxbroy10:cronjob" val main_dir: Path = Path.explode("~/cronjob") val main_state_file: Path = main_dir + Path.explode("run/main.state") val build_release_log: Path = main_dir + Path.explode("run/build_release.log") val current_log: Path = main_dir + Path.explode("run/main.log") // owned by log service val cumulative_log: Path = main_dir + Path.explode("log/main.log") // owned by log service val isabelle_repos: Path = main_dir + Path.explode("isabelle") val afp_repos: Path = main_dir + Path.explode("AFP") val mailman_archives_dir = Path.explode("~/cronjob/Mailman") val build_log_dirs = List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log")) /** logger tasks **/ sealed case class Logger_Task(name: String = "", body: Logger => Unit) /* init and exit */ def get_rev(): String = Mercurial.repository(isabelle_repos).id() def get_afp_rev(): String = Mercurial.repository(afp_repos).id() val init: Logger_Task = Logger_Task("init", { logger => Isabelle_Devel.make_index() Mercurial.setup_repository(Isabelle_System.afp_repository.root, afp_repos) File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date), Build_Log.Identify.content(logger.start_date, Some(get_rev()), Some(get_afp_rev()))) Isabelle_System.bash( """rsync -a --include="*/" --include="plain_identify*" --exclude="*" """ + Bash.string(backup + "/log/.") + " " + File.bash_path(main_dir) + "/log/.").check if (!Isabelle_Devel.cronjob_log.is_file) Files.createSymbolicLink(Isabelle_Devel.cronjob_log.java_path, current_log.java_path) }) val exit: Logger_Task = Logger_Task("exit", { logger => Isabelle_System.bash( "rsync -a " + File.bash_path(main_dir) + "/log/." + " " + Bash.string(backup) + "/log/.") .check }) /* Mailman archives */ val mailman_archives: Logger_Task = Logger_Task("mailman_archives", { logger => Mailman.Isabelle_Users.download(mailman_archives_dir) Mailman.Isabelle_Dev.download(mailman_archives_dir) }) /* build release */ val build_release: Logger_Task = Logger_Task("build_release", { logger => build_release_log.file.delete Isabelle_Devel.release_snapshot(logger.options, get_rev(), get_afp_rev(), progress = new File_Progress(build_release_log)) }) /* remote build_history */ sealed case class Item( known: Boolean, isabelle_version: String, afp_version: Option[String], pull_date: Date ) { def unknown: Boolean = !known def versions: (String, Option[String]) = (isabelle_version, afp_version) def known_versions(rev: String, afp_rev: Option[String]): Boolean = known && rev != "" && isabelle_version == rev && (afp_rev.isEmpty || afp_rev.get != "" && afp_version == afp_rev) } def recent_items( db: SQL.Database, days: Int, rev: String, afp_rev: Option[String], sql: PostgreSQL.Source ): List[Item] = { val afp = afp_rev.isDefined val select = Build_Log.Data.select_recent_versions( days = days, rev = rev, afp_rev = afp_rev, sql = "WHERE " + sql) db.using_statement(select)(stmt => stmt.execute_query().iterator({ res => val known = res.bool(Build_Log.Data.known) val isabelle_version = res.string(Build_Log.Prop.isabelle_version) val afp_version = if (afp) proper_string(res.string(Build_Log.Prop.afp_version)) else None val pull_date = res.date(Build_Log.Data.pull_date(afp)) Item(known, isabelle_version, afp_version, pull_date) }).toList) } def unknown_runs(items: List[Item]): List[List[Item]] = { val (run, rest) = Library.take_prefix[Item](_.unknown, items.dropWhile(_.known)) if (run.nonEmpty) run :: unknown_runs(rest) else Nil } sealed case class Remote_Build( description: String, host: String, user: String = "", port: Int = 0, historic: Boolean = false, history: Int = 0, history_base: String = "build_history_base", clean_components: Boolean = false, java_heap: String = "", options: String = "", args: String = "", afp: Boolean = false, bulky: Boolean = false, more_hosts: List[String] = Nil, detect: PostgreSQL.Source = "", active: Boolean = true ) { def open_session(options: Options): SSH.Session = SSH.open_session(options, host = host, user = user, port = port) def sql: PostgreSQL.Source = Build_Log.Prop.build_engine.toString + " = " + SQL.string(Build_History.engine) + " AND " + SQL.member(Build_Log.Prop.build_host.ident, host :: more_hosts) + (if (detect == "") "" else " AND " + SQL.enclose(detect)) def profile: Build_Status.Profile = Build_Status.Profile(description, history = history, afp = afp, bulky = bulky, sql = sql) def pick( options: Options, rev: String = "", filter: Item => Boolean = _ => true ): Option[(String, Option[String])] = { val afp_rev = if (afp) Some(get_afp_rev()) else None val store = Build_Log.store(options) using(store.open_database()) { db => def pick_days(days: Int, gap: Int): Option[(String, Option[String])] = { val items = recent_items(db, days, rev, afp_rev, sql).filter(filter) def runs = unknown_runs(items).filter(run => run.length >= gap) if (historic || items.exists(_.known_versions(rev, afp_rev))) { val longest_run = runs.foldLeft(List.empty[Item]) { case (item1, item2) => if (item1.length >= item2.length) item1 else item2 } if (longest_run.isEmpty) None else Some(longest_run(longest_run.length / 2).versions) } else if (rev != "") Some((rev, afp_rev)) else runs.flatten.headOption.map(_.versions) } pick_days(options.int("build_log_history") max history, 2) orElse pick_days(200, 5) orElse pick_days(2000, 1) } } def build_history_options: String = " -h " + Bash.string(host) + " " + (java_heap match { case "" => "" case h => "-e 'ISABELLE_TOOL_JAVA_OPTIONS=\"$ISABELLE_TOOL_JAVA_OPTIONS -Xmx" + h + "\"' " }) + options } val remote_builds_old: List[Remote_Build] = List( Remote_Build("macOS 10.15 Catalina", "laramac01", user = "makarius", options = "-m32 -M4 -e ISABELLE_GHC_SETUP=true -p pide_session=false", args = "-a -d '~~/src/Benchmarks'"), Remote_Build("Linux A", "i21of4", user = "i21isatest", options = "-m32 -M1x4,2,4" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + " -e ISABELLE_GHC_SETUP=true" + " -e ISABELLE_MLTON=mlton" + " -e ISABELLE_SMLNJ=sml" + " -e ISABELLE_SWIPL=swipl", args = "-a -d '~~/src/Benchmarks'"), Remote_Build("Linux A", "lxbroy9", java_heap = "2g", options = "-m32 -B -M1x2,2", args = "-N -g timing"), Remote_Build("Linux Benchmarks", "lxbroy5", historic = true, history = 90, java_heap = "2g", options = "-m32 -B -M1x2,2 -t Benchmarks" + " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" + " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind -e ISABELLE_SMLNJ=sml" + " -e ISABELLE_SWIPL=swipl", args = "-N -a -d '~~/src/Benchmarks'", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("Benchmarks")), Remote_Build("macOS 10.14 Mojave (Old)", "lapnipkow3", options = "-m32 -M1,2 -e ISABELLE_GHC_SETUP=true -p pide_session=false", args = "-a -d '~~/src/Benchmarks'"), Remote_Build("AFP old bulky", "lrzcloud1", options = "-m64 -M6 -U30000 -s10 -t AFP", args = "-g large -g slow", afp = true, bulky = true, detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")), Remote_Build("AFP old", "lxbroy7", args = "-N -X large -X slow", afp = true, detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")), Remote_Build("Poly/ML 5.7 Linux", "lxbroy8", history_base = "37074e22e8be", options = "-m32 -B -M1x2,2 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'", args = "-N -g timing", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7") + " AND " + Build_Log.Settings.ML_OPTIONS + " <> " + SQL.string("-H 500")), Remote_Build("Poly/ML 5.7.1 Linux", "lxbroy8", history_base = "a9d5b59c3e12", options = "-m32 -B -M1x2,2 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'", args = "-N -g timing", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " + Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")), Remote_Build("Poly/ML 5.7 macOS", "macbroy2", history_base = "37074e22e8be", options = "-m32 -B -M1x4,4 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'", args = "-a", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7")), Remote_Build("Poly/ML 5.7.1 macOS", "macbroy2", history_base = "a9d5b59c3e12", options = "-m32 -B -M1x4,4 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'", args = "-a", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " + Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")), Remote_Build("macOS", "macbroy2", options = "-m32 -M8" + " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" + " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + " -e ISABELLE_OPAM_ROOT=\"$ISABELLE_HOME/opam\"" + " -e ISABELLE_SMLNJ=/home/isabelle/smlnj/110.85/bin/sml" + " -p pide_session=false", args = "-a", detect = Build_Log.Prop.build_tags.undefined, history_base = "2c0f24e927dd"), Remote_Build("macOS, quick_and_dirty", "macbroy2", options = "-m32 -M8 -t quick_and_dirty -p pide_session=false", args = "-a -o quick_and_dirty", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("quick_and_dirty"), history_base = "2c0f24e927dd"), Remote_Build("macOS, skip_proofs", "macbroy2", options = "-m32 -M8 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("skip_proofs"), history_base = "2c0f24e927dd"), Remote_Build("Poly/ML test", "lxbroy8", options = "-m32 -B -M1x2,2 -t polyml-test -i 'init_component /home/isabelle/contrib/polyml-5.7-20170217'", args = "-N -g timing", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-test")), Remote_Build("macOS 10.12 Sierra", "macbroy30", options = "-m32 -M2 -p pide_session=false", args = "-a", detect = Build_Log.Prop.build_start.toString + " > date '2017-03-03'"), Remote_Build("macOS 10.10 Yosemite", "macbroy31", options = "-m32 -M2 -p pide_session=false", args = "-a"), Remote_Build("macOS 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a", detect = Build_Log.Prop.build_start.toString + " < date '2017-03-03'")) ::: { for { (n, hosts) <- List(1 -> List("lxbroy6"), 2 -> List("lxbroy8", "lxbroy5")) } yield { Remote_Build("AFP old", host = hosts.head, more_hosts = hosts.tail, options = "-m32 -M1x2 -t AFP -P" + n + " -e ISABELLE_GHC=ghc" + " -e ISABELLE_MLTON=mlton" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" + " -e ISABELLE_SMLNJ=sml", args = "-N -X large -X slow", afp = true, detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")) } } val remote_builds1: List[List[Remote_Build]] = { List( List(Remote_Build("Linux A", "augsburg1", options = "-m32 -B -M4" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" + " -e ISABELLE_GHC_SETUP=true" + " -e ISABELLE_MLTON=mlton -e ISABELLE_MLTON_OPTIONS=" + " -e ISABELLE_SMLNJ=sml" + " -e ISABELLE_SWIPL=swipl", args = "-a -d '~~/src/Benchmarks'")), List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90, options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")), List(Remote_Build("macOS 10.13 High Sierra", "lapbroy68", options = "-m32 -B -M1,2,4 -e ISABELLE_GHC_SETUP=true -p pide_session=false", args = "-a -d '~~/src/Benchmarks'")), List( Remote_Build("macOS 11 Big Sur", "mini1", options = "-m32 -B -M1x2,2,4 -p pide_session=false" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + " -e ISABELLE_GHC_SETUP=true" + " -e ISABELLE_MLTON=/usr/local/bin/mlton -e ISABELLE_MLTON_OPTIONS=" + " -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" + " -e ISABELLE_SWIPL=/usr/local/bin/swipl", args = "-a -d '~~/src/Benchmarks'")), List( Remote_Build("macOS 10.14 Mojave", "mini2", options = "-m32 -B -M1x2,2,4 -p pide_session=false" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + " -e ISABELLE_GHC_SETUP=true" + " -e ISABELLE_MLTON=/usr/local/bin/mlton -e ISABELLE_MLTON_OPTIONS=" + " -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" + " -e ISABELLE_SWIPL=/usr/local/bin/swipl", args = "-a -d '~~/src/Benchmarks'"), Remote_Build("macOS, quick_and_dirty", "mini2", options = "-m32 -M4 -t quick_and_dirty -p pide_session=false", args = "-a -o quick_and_dirty", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("quick_and_dirty")), Remote_Build("macOS, skip_proofs", "mini2", options = "-m32 -M4 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs", detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("skip_proofs"))), List( Remote_Build("macOS 12 Monterey", "monterey", user = "makarius", options = "-m32 -M4 -e ISABELLE_GHC_SETUP=true -p pide_session=false", args = "-a -d '~~/src/Benchmarks'")), List( Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, options = "-m32 -M4" + " -C /cygdrive/d/isatest/contrib" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + " -e ISABELLE_GHC_SETUP=true" + " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml", args = "-a", detect = Build_Log.Settings.ML_PLATFORM.toString + " = " + SQL.string("x86-windows") + " OR " + Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64_32-windows")), Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, options = "-m64 -M4" + " -C /cygdrive/d/isatest/contrib" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + " -e ISABELLE_GHC_SETUP=true" + " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml", args = "-a", detect = Build_Log.Settings.ML_PLATFORM.toString + " = " + SQL.string("x86_64-windows")))) } val remote_builds2: List[List[Remote_Build]] = List( List( Remote_Build("AFP", "lrzcloud2", java_heap = "8g", options = "-m32 -M1x6 -t AFP" + " -e ISABELLE_GHC=ghc" + " -e ISABELLE_MLTON=mlton -e ISABELLE_MLTON_OPTIONS=" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" + " -e ISABELLE_SMLNJ=sml", args = "-a -X large -X slow", afp = true, detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")), Remote_Build("AFP", "lrzcloud2", java_heap = "8g", options = "-m64 -M8 -U30000 -s10 -t AFP", args = "-g large -g slow", afp = true, bulky = true, detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")))) def remote_build_history( rev: String, afp_rev: Option[String], i: Int, r: Remote_Build ) : Logger_Task = { val task_name = "build_history-" + r.host Logger_Task(task_name, { logger => using(r.open_session(logger.options)) { ssh => val results = Build_History.remote_build(ssh, isabelle_repos, isabelle_repos.ext(r.host), isabelle_identifier = "cronjob_build_history", clean_platforms = r.clean_components, clean_archives = r.clean_components, rev = rev, afp_repos = if (afp_rev.isDefined) Some(afp_repos) else None, afp_rev = afp_rev.getOrElse(""), options = " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) + - " -R " + Bash.string(Components.default_component_repository) + + " -R " + Bash.string(Components.static_component_repository) + " -f " + r.build_history_options, args = "-o timeout=10800 " + r.args) for ((log_name, bytes) <- results) { logger.log(Date.now(), log_name) Bytes.write(logger.log_dir + Path.explode(log_name), bytes) } } }) } val build_status_profiles: List[Build_Status.Profile] = (remote_builds_old :: remote_builds1 ::: remote_builds2).flatten.map(_.profile) /** task logging **/ object Log_Service { def apply(options: Options, progress: Progress = new Progress): Log_Service = new Log_Service(options, progress) } class Log_Service private(val options: Options, progress: Progress) { current_log.file.delete private val thread: Consumer_Thread[String] = Consumer_Thread.fork("cronjob: logger", daemon = true)( consume = { (text: String) => // critical File.append(current_log, text + "\n") File.append(cumulative_log, text + "\n") progress.echo(text) true }) def shutdown(): Unit = { thread.shutdown() } val hostname: String = Isabelle_System.hostname() def log(date: Date, task_name: String, msg: String): Unit = if (task_name != "") { thread.send( "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg) } def start_logger(start_date: Date, task_name: String): Logger = new Logger(this, start_date, task_name) def run_task(start_date: Date, task: Logger_Task): Unit = { val logger = start_logger(start_date, task.name) val res = Exn.capture { task.body(logger) } val end_date = Date.now() val err = res match { case Exn.Res(_) => None case Exn.Exn(exn) => Output.writeln("Exception trace for " + quote(task.name) + ":") exn.printStackTrace() val first_line = split_lines(Exn.message(exn)).headOption getOrElse "exception" Some(first_line) } logger.log_end(end_date, err) } def fork_task(start_date: Date, task: Logger_Task): Task = new Task(task.name, run_task(start_date, task)) } class Logger private[Isabelle_Cronjob]( log_service: Log_Service, val start_date: Date, val task_name: String ) { def options: Options = log_service.options def log(date: Date, msg: String): Unit = log_service.log(date, task_name, msg) def log_end(end_date: Date, err: Option[String]): Unit = { val elapsed_time = end_date.time - start_date.time val msg = (if (err.isEmpty) "finished" else "ERROR " + err.get) + (if (elapsed_time.seconds < 3.0) "" else " (" + elapsed_time.message_hms + " elapsed time)") log(end_date, msg) } val log_dir = Isabelle_System.make_directory(main_dir + Build_Log.log_subdir(start_date)) log(start_date, "started") } class Task private[Isabelle_Cronjob](name: String, body: => Unit) { private val future: Future[Unit] = Future.thread("cronjob: " + name) { body } def is_finished: Boolean = future.is_finished } /** cronjob **/ def cronjob(progress: Progress, exclude_task: Set[String]): Unit = { /* soft lock */ val still_running = try { Some(File.read(main_state_file)) } catch { case ERROR(_) => None } still_running match { case None | Some("") => case Some(running) => error("Isabelle cronjob appears to be still running: " + running) } /* log service */ val log_service = Log_Service(Options.init(), progress = progress) def run(start_date: Date, task: Logger_Task): Unit = log_service.run_task(start_date, task) def run_now(task: Logger_Task): Unit = run(Date.now(), task) /* structured tasks */ def SEQ(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ => for (task <- tasks.iterator if !exclude_task(task.name) || task.name == "") run_now(task)) def PAR(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = { _ => @tailrec def join(running: List[Task]): Unit = { running.partition(_.is_finished) match { case (Nil, Nil) => case (Nil, _ :: _) => Time.seconds(0.5).sleep(); join(running) case (_ :: _, remaining) => join(remaining) } } val start_date = Date.now() val running = for (task <- tasks if !exclude_task(task.name)) yield log_service.fork_task(start_date, task) join(running) }) /* repository structure */ val hg = Mercurial.repository(isabelle_repos) val hg_graph = hg.graph() def history_base_filter(r: Remote_Build): Item => Boolean = { val base_rev = hg.id(r.history_base) val nodes = hg_graph.all_succs(List(base_rev)).toSet (item: Item) => nodes(item.isabelle_version) } /* main */ val main_start_date = Date.now() File.write(main_state_file, main_start_date.toString + " " + log_service.hostname) run(main_start_date, Logger_Task("isabelle_cronjob", logger => run_now( SEQ(List( init, PAR(List(mailman_archives, build_release)), PAR( List(remote_builds1, remote_builds2).map(remote_builds => SEQ(List( PAR(remote_builds.map(_.filter(_.active)).map(seq => SEQ( for { (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex) (rev, afp_rev) <- r.pick(logger.options, hg.id(), history_base_filter(r)) } yield remote_build_history(rev, afp_rev, i, r)))), Logger_Task("jenkins_logs", _ => Jenkins.download_logs(logger.options, Jenkins.build_log_jobs, main_dir)), Logger_Task("build_log_database", logger => Isabelle_Devel.build_log_database(logger.options, build_log_dirs)), Logger_Task("build_status", logger => Isabelle_Devel.build_status(logger.options)))))), exit))))) log_service.shutdown() main_state_file.file.delete } /** command line entry point **/ def main(args: Array[String]): Unit = { Command_Line.tool { var force = false var verbose = false var exclude_task = Set.empty[String] val getopts = Getopts(""" Usage: Admin/cronjob/main [OPTIONS] Options are: -f apply force to do anything -v verbose -x NAME exclude tasks with this name """, "f" -> (_ => force = true), "v" -> (_ => verbose = true), "x:" -> (arg => exclude_task += arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = if (verbose) new Console_Progress() else new Progress if (force) cronjob(progress, exclude_task) else error("Need to apply force to do anything") } } } diff --git a/src/Pure/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,176 +1,176 @@ /* Title: Pure/Admin/other_isabelle.scala Author: Makarius Manage other Isabelle distributions: support historic versions starting from tag "build_history_base". */ package isabelle object Other_Isabelle { def apply( root: Path, isabelle_identifier: String = "", ssh: SSH.System = SSH.Local, progress: Progress = new Progress ): Other_Isabelle = { val (isabelle_home, url_prefix) = ssh match { case session: SSH.Session => (ssh.absolute_path(root), session.rsync_prefix) case _ => if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) { error("Cannot manage other Isabelle distribution: global ISABELLE_SETTINGS_PRESENT") } (root.canonical, "") } val isabelle_home_url = url_prefix + isabelle_home.implode new Other_Isabelle(isabelle_home, isabelle_identifier, isabelle_home_url, ssh, progress) } } final class Other_Isabelle private( val isabelle_home: Path, val isabelle_identifier: String, isabelle_home_url: String, ssh: SSH.System, progress: Progress ) { override def toString: String = isabelle_home_url /* static system */ def bash( script: String, redirect: Boolean = false, echo: Boolean = false, strict: Boolean = true ): Process_Result = { ssh.execute( Isabelle_System.export_isabelle_identifier(isabelle_identifier) + "cd " + ssh.bash_path(isabelle_home) + "\n" + script, progress_stdout = progress.echo_if(echo, _), progress_stderr = progress.echo_if(echo, _), redirect = redirect, settings = false, strict = strict) } def getenv(name: String): String = bash("bin/isabelle getenv -b " + Bash.string(name)).check.out val settings: Isabelle_System.Settings = (name: String) => getenv(name) def expand_path(path: Path): Path = path.expand_env(settings) def bash_path(path: Path): String = Bash.string(expand_path(path).implode) val isabelle_home_user: Path = expand_path(Path.explode("$ISABELLE_HOME_USER")) def etc: Path = isabelle_home_user + Path.explode("etc") def etc_settings: Path = etc + Path.explode("settings") def etc_preferences: Path = etc + Path.explode("preferences") /* components */ def init_components( - components_base: String = Components.standard_components_base, + components_base: String = Components.dynamic_components_base, catalogs: List[String] = Components.default_catalogs, components: List[String] = Nil ): List[String] = { val admin = Components.admin(Path.ISABELLE_HOME).implode catalogs.map(name => "init_components " + quote(components_base) + " " + quote(admin + "/" + name)) ::: components.map(name => "init_component " + quote(components_base) + "/" + name) } def resolve_components( echo: Boolean = false, clean_platforms: Option[List[Platform.Family.Value]] = None, clean_archives: Boolean = false, - component_repository: String = Components.default_component_repository + component_repository: String = Components.static_component_repository ): Unit = { val missing = Path.split(getenv("ISABELLE_COMPONENTS_MISSING")) for (path <- missing) { Components.resolve(path.dir, path.file_name, clean_platforms = clean_platforms, clean_archives = clean_archives, component_repository = component_repository, ssh = ssh, progress = if (echo) progress else new Progress) } } def scala_build(fresh: Boolean = false, echo: Boolean = false): Unit = { if (fresh) ssh.rm_tree(isabelle_home + Path.explode("lib/classes")) val dummy_stty = Path.explode("~~/lib/dummy_stty/stty") val dummy_stty_remote = expand_path(dummy_stty) if (!ssh.is_file(dummy_stty_remote)) { ssh.make_directory(dummy_stty_remote.dir) ssh.write_file(dummy_stty_remote, dummy_stty) ssh.set_executable(dummy_stty_remote, true) } try { bash( "export PATH=\"" + bash_path(dummy_stty_remote.dir) + ":$PATH\"\n" + "export CLASSPATH=" + Bash.string(getenv("ISABELLE_CLASSPATH")) + "\n" + "bin/isabelle jedit -b", echo = echo).check } catch { case ERROR(msg) => cat_error("Failed to build Isabelle/Scala/Java modules:", msg) } } /* settings */ def clean_settings(): Boolean = if (!ssh.is_file(etc_settings)) true else if (ssh.read(etc_settings).startsWith("# generated by Isabelle")) { ssh.delete(etc_settings) true } else false def init_settings(settings: List[String]): Unit = { if (clean_settings()) { ssh.make_directory(etc_settings.dir) ssh.write(etc_settings, "# generated by Isabelle " + Date.now() + "\n" + "#-*- shell-script -*- :mode=shellscript:\n" + settings.mkString("\n", "\n", "\n")) } else error("Cannot proceed with existing user settings file: " + etc_settings) } /* init */ def init( other_settings: List[String] = init_components(), fresh: Boolean = false, echo: Boolean = false, clean_platforms: Option[List[Platform.Family.Value]] = None, clean_archives: Boolean = false, - component_repository: String = Components.default_component_repository + component_repository: String = Components.static_component_repository ): Unit = { init_settings(other_settings) resolve_components( echo = echo, clean_platforms = clean_platforms, clean_archives = clean_archives, component_repository = component_repository) scala_build(fresh = fresh, echo = echo) } /* cleanup */ def cleanup(): Unit = { clean_settings() ssh.delete(etc) ssh.delete(isabelle_home_user) } } diff --git a/src/Pure/System/components.scala b/src/Pure/System/components.scala --- a/src/Pure/System/components.scala +++ b/src/Pure/System/components.scala @@ -1,441 +1,441 @@ /* Title: Pure/System/components.scala Author: Makarius Isabelle system components. */ package isabelle import java.io.{File => JFile} object Components { /* archive name */ object Archive { val suffix: String = ".tar.gz" def apply(name: String): String = if (name == "") error("Bad component name: " + quote(name)) else name + suffix def unapply(archive: String): Option[String] = { for { name0 <- Library.try_unsuffix(suffix, archive) name <- proper_string(name0) } yield name } def get_name(archive: String): String = unapply(archive) getOrElse error("Bad component archive name (expecting .tar.gz): " + quote(archive)) } /* platforms */ private val family_platforms: Map[Platform.Family.Value, List[String]] = Map( Platform.Family.linux_arm -> List("arm64-linux", "arm64_32-linux"), Platform.Family.linux -> List("x86_64-linux", "x86_64_32-linux"), Platform.Family.macos -> List("arm64-darwin", "arm64_32-darwin", "x86_64-darwin", "x86_64_32-darwin"), Platform.Family.windows -> List("x86_64-cygwin", "x86_64-windows", "x86_64_32-windows", "x86-windows")) private val platform_names: Set[String] = Set("x86-linux", "x86-cygwin") ++ family_platforms.iterator.flatMap(_._2) def platform_purge(platforms: List[Platform.Family.Value]): String => Boolean = { val preserve = (for { family <- platforms.iterator platform <- family_platforms(family) } yield platform).toSet (name: String) => platform_names(name) && !preserve(name) } /* component collections */ - def default_component_repository: String = + def static_component_repository: String = Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE") - val standard_components_base: String = "${ISABELLE_COMPONENTS_BASE:-$USER_HOME/.isabelle/contrib}" + val dynamic_components_base: String = "${ISABELLE_COMPONENTS_BASE:-$USER_HOME/.isabelle/contrib}" val default_catalogs: List[String] = List("main") val optional_catalogs: List[String] = List("main", "optional") def admin(dir: Path): Path = dir + Path.explode("Admin/components") def contrib(dir: Path = Path.current, name: String = ""): Path = dir + Path.explode("contrib") + Path.explode(name) def unpack( dir: Path, archive: Path, ssh: SSH.System = SSH.Local, progress: Progress = new Progress ): String = { val name = Archive.get_name(archive.file_name) progress.echo("Unpacking " + archive.base) ssh.execute( "tar -C " + ssh.bash_path(dir) + " -x -z -f " + ssh.bash_path(archive), progress_stdout = progress.echo, progress_stderr = progress.echo).check name } def clean( component_dir: Path, platforms: List[Platform.Family.Value] = Platform.Family.list, ssh: SSH.System = SSH.Local, progress: Progress = new Progress ): Unit = { val purge = platform_purge(platforms) for { name <- ssh.read_dir(component_dir) path = Path.basic(name) if purge(name) && ssh.is_dir(component_dir + path) } { progress.echo("Removing " + (component_dir.base + path)) ssh.rm_tree(component_dir + path) } } def clean_base( base_dir: Path, platforms: List[Platform.Family.Value] = Platform.Family.list, ssh: SSH.System = SSH.Local, progress: Progress = new Progress ): Unit = { for { name <- ssh.read_dir(base_dir) dir = base_dir + Path.basic(name) if is_component_dir(dir) } clean(dir, platforms = platforms, ssh = ssh, progress = progress) } def resolve( base_dir: Path, name: String, target_dir: Option[Path] = None, copy_dir: Option[Path] = None, clean_platforms: Option[List[Platform.Family.Value]] = None, clean_archives: Boolean = false, - component_repository: String = Components.default_component_repository, + component_repository: String = Components.static_component_repository, ssh: SSH.System = SSH.Local, progress: Progress = new Progress ): Unit = { ssh.make_directory(base_dir) val archive_name = Archive(name) val archive = base_dir + Path.basic(archive_name) if (!ssh.is_file(archive)) { val remote = Url.append_path(component_repository, archive_name) ssh.download_file(remote, archive, progress = progress) } for (dir <- copy_dir) { ssh.make_directory(dir) ssh.copy_file(archive, dir) } val unpack_dir = target_dir getOrElse base_dir unpack(unpack_dir, archive, ssh = ssh, progress = progress) if (clean_platforms.isDefined) { clean(unpack_dir + Path.basic(name), platforms = clean_platforms.get, ssh = ssh, progress = progress) } if (clean_archives) { progress.echo("Removing " + quote(archive_name)) ssh.delete(archive) } } /* component directories */ def directories(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_COMPONENTS")) def is_component_dir(dir: Path, ssh: SSH.System = SSH.Local): Boolean = ssh.is_file(dir + Path.explode("etc/settings")) || ssh.is_file(dir + Path.explode("etc/components")) /* component directory content */ object Directory { def apply(path: Path): Directory = new Directory(path.absolute) } class Directory private(val path: Path) { override def toString: String = path.toString def etc: Path = path + Path.basic("etc") def src: Path = path + Path.basic("src") def lib: Path = path + Path.basic("lib") def settings: Path = etc + Path.basic("settings") def components: Path = etc + Path.basic("components") def build_props: Path = etc + Path.basic("build.props") def README: Path = path + Path.basic("README") def LICENSE: Path = path + Path.basic("LICENSE") def create(progress: Progress = new Progress): Directory = { progress.echo("Creating component directory " + path) Isabelle_System.new_directory(path) Isabelle_System.make_directory(etc) this } def ok: Boolean = settings.is_file || components.is_file || Sessions.is_session_dir(path) def check: Directory = if (!path.is_dir) error("Bad component directory: " + path) else if (!ok) { error("Malformed component directory: " + path + "\n (missing \"etc/settings\" or \"etc/components\" or \"ROOT\" or \"ROOTS\")") } else this def read_components(): List[String] = split_lines(File.read(components)).filter(_.nonEmpty) def write_components(lines: List[String]): Unit = File.write(components, terminate_lines(lines)) def write_settings(text: String): Unit = File.write(settings, "# -*- shell-script -*- :mode=shellscript:\n" + text) } /* component repository content */ val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1") sealed case class SHA1_Digest(digest: SHA1.Digest, name: String) { override def toString: String = digest.shasum(name) } def read_components_sha1(lines: List[String] = Nil): List[SHA1_Digest] = (proper_list(lines) getOrElse split_lines(File.read(components_sha1))).flatMap(line => Word.explode(line) match { case Nil => None case List(sha1, name) => Some(SHA1_Digest(SHA1.fake_digest(sha1), name)) case _ => error("Bad components.sha1 entry: " + quote(line)) }) def write_components_sha1(entries: List[SHA1_Digest]): Unit = File.write(components_sha1, entries.sortBy(_.name).mkString("", "\n", "\n")) /** manage user components **/ val components_path: Path = Path.explode("$ISABELLE_HOME_USER/etc/components") def read_components(): List[String] = if (components_path.is_file) Library.trim_split_lines(File.read(components_path)) else Nil def write_components(lines: List[String]): Unit = { Isabelle_System.make_directory(components_path.dir) File.write(components_path, Library.terminate_lines(lines)) } def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = { val path = path0.expand.absolute if (add) Directory(path).check val lines1 = read_components() val lines2 = lines1.filter(line => line.isEmpty || line.startsWith("#") || !File.eq(Path.explode(line), path)) val lines3 = if (add) lines2 ::: List(path.implode) else lines2 if (lines1 != lines3) write_components(lines3) val prefix = if (lines1 == lines3) "Unchanged" else if (add) "Added" else "Removed" progress.echo(prefix + " component " + path) } /* main entry point */ def main(args: Array[String]): Unit = { Command_Line.tool { for (arg <- args) { val add = if (arg.startsWith("+")) true else if (arg.startsWith("-")) false else error("Bad argument: " + quote(arg)) val path = Path.explode(arg.substring(1)) update_components(add, path, progress = new Console_Progress) } } } /** build and publish components **/ def build_components( options: Options, components: List[Path], progress: Progress = new Progress, publish: Boolean = false, force: Boolean = false, update_components_sha1: Boolean = false ): Unit = { val archives: List[Path] = for (path <- components) yield { path.file_name match { case Archive(_) => path case name => Directory(path).check val component_path = path.expand val archive_dir = component_path.dir val archive_name = Archive(name) val archive = archive_dir + Path.explode(archive_name) if (archive.is_file && !force) { error("Component archive already exists: " + archive) } progress.echo("Packaging " + archive_name) Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name), dir = archive_dir).check archive } } if ((publish && archives.nonEmpty) || update_components_sha1) { val server = options.string("isabelle_components_server") if (server.isEmpty) error("Undefined option isabelle_components_server") using(SSH.open_session(options, server)) { ssh => val components_dir = Path.explode(options.string("isabelle_components_dir")) val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir")) for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) { error("Bad remote directory: " + dir) } if (publish) { for (archive <- archives) { val archive_name = archive.file_name val name = Archive.get_name(archive_name) val remote_component = components_dir + archive.base val remote_contrib = contrib_dir + Path.explode(name) // component archive if (ssh.is_file(remote_component) && !force) { error("Remote component archive already exists: " + remote_component) } progress.echo("Uploading " + archive_name) ssh.write_file(remote_component, archive) // contrib directory val is_standard_component = Isabelle_System.with_tmp_dir("component") { tmp_dir => Isabelle_System.extract(archive, tmp_dir) Directory(tmp_dir + Path.explode(name)).ok } if (is_standard_component) { if (ssh.is_dir(remote_contrib)) { if (force) ssh.rm_tree(remote_contrib) else error("Remote component directory already exists: " + remote_contrib) } progress.echo("Unpacking remote " + archive_name) ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " + ssh.bash_path(remote_component)).check } else { progress.echo_warning("No unpacking of non-standard component: " + archive_name) } } } // remote SHA1 digests if (update_components_sha1) { val lines = for { entry <- ssh.read_dir(components_dir) if ssh.is_file(components_dir + Path.basic(entry)) && entry.endsWith(Archive.suffix) } yield { progress.echo("Digesting remote " + entry) ssh.execute("cd " + ssh.bash_path(components_dir) + "; sha1sum " + Bash.string(entry)).check.out } write_components_sha1(read_components_sha1(lines)) } } } // local SHA1 digests { val new_entries = for (archive <- archives) yield { val name = archive.file_name progress.echo("Digesting local " + name) SHA1_Digest(SHA1.digest(archive), name) } val new_names = new_entries.map(_.name).toSet write_components_sha1( new_entries ::: read_components_sha1().filterNot(entry => new_names.contains(entry.name))) } } /* Isabelle tool wrapper */ private val relevant_options = List("isabelle_components_server", "isabelle_components_dir", "isabelle_components_contrib_dir") val isabelle_tool = Isabelle_Tool("build_components", "build and publish Isabelle components", Scala_Project.here, { args => var publish = false var update_components_sha1 = false var force = false var options = Options.init() def show_options: String = cat_lines(relevant_options.flatMap(options.get).map(_.print)) val getopts = Getopts(""" Usage: isabelle build_components [OPTIONS] ARCHIVES... DIRS... Options are: -P publish on SSH server (see options below) -f force: overwrite existing component archives and directories -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -u update all SHA1 keys in Isabelle repository Admin/components Build and publish Isabelle components as .tar.gz archives on SSH server, depending on system options: """ + Library.indent_lines(2, show_options) + "\n", "P" -> (_ => publish = true), "f" -> (_ => force = true), "o:" -> (arg => options = options + arg), "u" -> (_ => update_components_sha1 = true)) val more_args = getopts(args) if (more_args.isEmpty && !update_components_sha1) getopts.usage() val progress = new Console_Progress build_components(options, more_args.map(Path.explode), progress = progress, publish = publish, force = force, update_components_sha1 = update_components_sha1) }) }