# HG changeset patch # User wenzelm # Date 1654535952 -7200 # Node ID cb4af8c6152f35e9a4c32924f39709633f17adb1 # Parent 292d7a9dc8a369799c92b28113400f38c6019041 clarified remote vs. local build_history: operate on hg_sync directory instead of repository; diff -r 292d7a9dc8a3 -r cb4af8c6152f Admin/build_history --- a/Admin/build_history Mon Jun 06 19:17:53 2022 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -#!/usr/bin/env bash -# -# DESCRIPTION: build history versions from another repository clone - -unset CDPATH -THIS="$(cd "$(dirname "$0")"; pwd)" - -"$THIS/../bin/isabelle" scala_build -q || exit $? -"$THIS/../bin/isabelle_java" isabelle.Build_History "$@" diff -r 292d7a9dc8a3 -r cb4af8c6152f Admin/build_other --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/build_other Mon Jun 06 19:19:12 2022 +0200 @@ -0,0 +1,9 @@ +#!/usr/bin/env bash +# +# DESCRIPTION: build other Isabelle from sync_repos directory + +unset CDPATH +THIS="$(cd "$(dirname "$0")"; pwd)" + +"$THIS/../bin/isabelle" scala_build -q || exit $? +"$THIS/../bin/isabelle_java" isabelle.Build_History "$@" diff -r 292d7a9dc8a3 -r cb4af8c6152f src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Mon Jun 06 19:17:53 2022 +0200 +++ b/src/Pure/Admin/build_history.scala Mon Jun 06 19:19:12 2022 +0200 @@ -89,21 +89,19 @@ - /** build_history **/ + /** local build --- from sync_repos directory **/ 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( + def local_build( options: Options, root: Path, user_home: Path = default_user_home, progress: Progress = new Progress, - rev: String = default_rev, - afp_rev: Option[String] = None, + afp: Boolean = false, afp_partition: Int = 0, isabelle_identifier: String = default_isabelle_identifier, ml_statistics_step: Int = 1, @@ -140,33 +138,30 @@ System.getenv("ISABELLE_SETTINGS_PRESENT") match { case null | "" => - case _ => error("Cannot run build_history within existing Isabelle settings environment") + case _ => error("Cannot run Admin/build_other within existing Isabelle settings environment") } - /* checkout Isabelle + AFP repository */ + /* Isabelle + AFP directory (produced via sync_repos) */ - 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) + def directory(dir: Path): Mercurial.Hg_Sync.Directory = { + val directory = Mercurial.Hg_Sync.directory(dir) + if (verbose) progress.echo(directory.log) + directory } - val isabelle_version = checkout(root, rev) - - val afp_repos = root + Path.explode("AFP") - val afp_version = afp_rev.map(checkout(afp_repos, _)) + 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_rev.isEmpty) (Nil, Nil) + if (afp_directory.isEmpty) (Nil, Nil) else { val (opt, sessions) = { if (afp_partition == 0) ("-d", Nil) else { try { - val afp = AFP.init(options, afp_repos) - ("-d", afp.partition(afp_partition)) + val afp_info = AFP.init(options, base_dir = afp_directory.get.root) + ("-d", afp_info.partition(afp_partition)) } catch { case ERROR(_) => ("-D", Nil) } } } @@ -276,8 +271,8 @@ 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_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 = @@ -397,7 +392,7 @@ def main(args: Array[String]): Unit = { Command_Line.tool { - var afp_rev: Option[String] = None + var afp = false var multicore_base = false var components_base: Path = Components.default_components_base var heap: Option[Int] = None @@ -413,7 +408,6 @@ 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 @@ -421,10 +415,10 @@ var exit_code = false val getopts = Getopts(""" -Usage: Admin/build_history [OPTIONS] REPOSITORY [ARGS ...] +Usage: Admin/build_other [OPTIONS] ISABELLE_HOME [ARGS ...] Options are: - -A REV include $ISABELLE_HOME/AFP repository at given revision + -A include $ISABELLE_HOME/AFP directory -B first multicore build serves as base for scheduling information -C DIR base directory for Isabelle components (default: """ + Components.default_components_base + """) @@ -441,9 +435,9 @@ -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 - -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 @@ -456,7 +450,7 @@ 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)), + "A" -> (_ => afp = true), "B" -> (_ => multicore_base = true), "C:" -> (arg => components_base = Path.explode(arg)), "H:" -> (arg => heap = Some(Value.Int.parse(arg))), @@ -477,7 +471,6 @@ }, "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)), @@ -494,8 +487,8 @@ 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, + local_build(Options.init(), root, user_home = user_home, 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, fresh = fresh, hostname = hostname, multicore_base = multicore_base, @@ -521,91 +514,81 @@ - /** remote build_history -- via command-line **/ + /** remote build -- via rsync and ssh **/ - def remote_build_history( + def remote_build( ssh: SSH.Session, - isabelle_repos_self: Path, - isabelle_repos_other: Path, - isabelle_repository: Mercurial.Server = Isabelle_System.isabelle_repository, - afp_repository: Mercurial.Server = Isabelle_System.afp_repository, + isabelle_self: Path, + isabelle_other: Path, isabelle_identifier: String = "remote_build_history", self_update: Boolean = false, progress: Progress = new Progress, rev: String = "", - afp_rev: Option[String] = None, + afp_repos: Option[Path] = None, + afp_rev: String = "", options: String = "", - args: String = "" + args: String = "", + no_build: Boolean = false ): List[(String, Bytes)] = { - /* Isabelle self repository */ + /* synchronize Isabelle + AFP repositories */ - val self_hg = - Mercurial.setup_repository(isabelle_repository.root, isabelle_repos_self, ssh = ssh) + def sync_repos(target: Path, accurate: Boolean = false, + rev: String = "", afp_rev: String = "", afp: Boolean = false + ): Unit = { + Sync_Repos.sync_repos(ssh.rsync_path(target), port = ssh.port, progress = progress, + thorough = accurate, preserve_jars = !accurate, + rev = rev, afp_rev = afp_rev, afp_root = if (afp) afp_repos else None) + } - def execute(cmd: String, args: String, echo: Boolean = false, strict: Boolean = true): Unit = + def execute(command: String, args: String, + echo: Boolean = false, + strict: Boolean = true + ): Unit = ssh.execute( Isabelle_System.export_isabelle_identifier(isabelle_identifier) + - ssh.bash_path(isabelle_repos_self + Path.explode(cmd)) + " " + args, + ssh.bash_path(isabelle_self + Path.explode(command)) + " " + args, progress_stdout = progress.echo_if(echo, _), progress_stderr = progress.echo_if(echo, _), strict = strict).check if (self_update) { - val hg = Mercurial.self_repository() - hg.push(self_hg.root_url, force = true) - self_hg.update(rev = hg.parent(), clean = true) - + sync_repos(isabelle_self) execute("bin/isabelle", "components -I") execute("bin/isabelle", "components -a", echo = true) execute("bin/isabelle", "jedit -bf") } - 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_repository.root, afp_repos, ssh = ssh) - " -A " + Bash.string(afp_rev.get) - } + sync_repos(isabelle_other, accurate = true, + rev = proper_string(rev) getOrElse "tip", + afp_rev = proper_string(afp_rev) getOrElse "tip", + afp = true) - /* 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) + /* build */ - 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) - } + if (no_build) Nil + else { + ssh.with_tmp_dir { tmp_dir => + val output_file = tmp_dir + Path.explode("output") + val build_options = (if (afp_repos.isEmpty) "" else " -A") + " " + options + try { + execute("Admin/build_other", + "-o " + ssh.bash_path(output_file) + build_options + " " + + ssh.bash_path(isabelle_other) + " " + args, + echo = true, strict = false) + } + catch { + case ERROR(msg) => + cat_error(msg, "The error(s) above occurred for Admin/build_other " + build_options) + } - for (line <- split_lines(ssh.read(output_file))) - yield { - val log = Path.explode(line) - val bytes = ssh.read_bytes(log) - ssh.rm(log) - (log.file_name, bytes) + 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 -r 292d7a9dc8a3 -r cb4af8c6152f src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Mon Jun 06 19:17:53 2022 +0200 +++ b/src/Pure/Admin/build_log.scala Mon Jun 06 19:19:12 2022 +0200 @@ -257,7 +257,7 @@ - /** digested meta info: produced by Admin/build_history in log.xz file **/ + /** digested meta info: produced by Admin/build_other in log.xz file **/ object Meta_Info { val empty: Meta_Info = Meta_Info(Nil, Nil) @@ -404,7 +404,7 @@ - /** build info: toplevel output of isabelle build or Admin/build_history **/ + /** build info: toplevel output of isabelle build or Admin/build_other **/ val SESSION_NAME = "session_name" diff -r 292d7a9dc8a3 -r cb4af8c6152f src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Mon Jun 06 19:17:53 2022 +0200 +++ b/src/Pure/Admin/isabelle_cronjob.scala Mon Jun 06 19:19:12 2022 +0200 @@ -406,13 +406,14 @@ { logger => using(r.ssh_session(logger.ssh_context)) { ssh => val results = - Build_History.remote_build_history(ssh, + Build_History.remote_build(ssh, isabelle_repos, isabelle_repos.ext(r.host), isabelle_identifier = "cronjob_build_history", self_update = r.self_update, rev = rev, - afp_rev = afp_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) +