# HG changeset patch # User wenzelm # Date 1716650525 -7200 # Node ID 9308bc5f65d645d3e1c0cb04df4c498e22a272e4 # Parent e2ccabd7a857e5545e5006c182f0e473ed91c53d more general dirs for Sync.sync; diff -r e2ccabd7a857 -r 9308bc5f65d6 src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Sat May 25 12:20:57 2024 +0200 +++ b/src/Pure/Admin/build_history.scala Sat May 25 17:22:05 2024 +0200 @@ -167,7 +167,7 @@ val isabelle_directory = directory(root) val (afp_directory, afp_build_args) = - if (afp) (Some(directory(root + Path.explode("AFP"))), List("-d", "~~/AFP/thys")) + if (afp) (Some(directory(root + Path.explode("AFP"))), List("-d", "~~/dirs/AFP/thys")) else (None, Nil) @@ -548,7 +548,7 @@ ): Unit = { Sync.sync(ssh.options, Rsync.Context(progress = progress, ssh = ssh), target, thorough = accurate, preserve_jars = !accurate, - rev = rev, afp_rev = afp_rev, afp_root = if (afp) afp_repos else None) + rev = rev, dirs = Sync.afp_dirs(if (afp) afp_repos else None, rev = afp_rev)) } if (!shared_isabelle_self) sync(isabelle_self) diff -r e2ccabd7a857 -r 9308bc5f65d6 src/Pure/Build/build.scala --- a/src/Pure/Build/build.scala Sat May 25 12:20:57 2024 +0200 +++ b/src/Pure/Build/build.scala Sat May 25 17:22:05 2024 +0200 @@ -599,7 +599,6 @@ build_options: List[Options.Spec] = Nil, build_id: String = "", isabelle_home: Path = Path.current, - afp_root: Option[Path] = None, dirs: List[Path] = Nil, quiet: Boolean = false, verbose: Boolean = false @@ -607,7 +606,6 @@ val options = build_options ::: Options.Spec.eq("build_hostname", host.name) :: host.options ssh.bash_path(Isabelle_Tool.exe(isabelle_home)) + " build_worker" + if_proper(build_id, " -B " + Bash.string(build_id)) + - if_proper(afp_root, " -A " + ssh.bash_path(afp_root.get)) + dirs.map(dir => " -d " + ssh.bash_path(dir)).mkString + if_proper(host.numa, " -N") + " -j" + host.jobs + Options.Spec.bash_strings(options, bg = true) + @@ -619,7 +617,6 @@ options: Options, build_id: String = "", progress: Progress = new Progress, - afp_root: Option[Path] = None, dirs: List[Path] = Nil, numa_shuffling: Boolean = false, max_jobs: Option[Int] = None @@ -634,18 +631,19 @@ val build_master = find_builds(build_database, build_id, builds.filter(_.active)) + val more_dirs = List(Path.ISABELLE_HOME + Sync.DIRS).filter(Sessions.is_session_dir(_)) + val sessions_structure = - Sessions.load_structure(build_options, dirs = AFP.main_dirs(afp_root) ::: dirs). + Sessions.load_structure(build_options, dirs = more_dirs ::: dirs). selection(Sessions.Selection(sessions = build_master.sessions)) val build_deps = Sessions.deps(sessions_structure, progress = progress, inlined_files = true).check_errors val build_context = - Context(store, build_deps, engine = engine, afp_root = afp_root, - hostname = hostname(build_options), numa_shuffling = numa_shuffling, - build_uuid = build_master.build_uuid, build_start = Some(build_master.start), - jobs = max_jobs.getOrElse(1)) + Context(store, build_deps, engine = engine, hostname = hostname(build_options), + numa_shuffling = numa_shuffling, build_uuid = build_master.build_uuid, + build_start = Some(build_master.start), jobs = max_jobs.getOrElse(1)) engine.run_build_process(build_context, progress, server) } @@ -655,7 +653,6 @@ val isabelle_tool3 = Isabelle_Tool("build_worker", "start worker for session build process", Scala_Project.here, { args => - var afp_root: Option[Path] = None var build_id = "" var numa_shuffling = false val dirs = new mutable.ListBuffer[Path] @@ -670,7 +667,6 @@ Usage: isabelle build_worker [OPTIONS] Options are: - -A ROOT include AFP with given root directory (":" for """ + AFP.BASE.implode + """) -B UUID existing UUID for build process (default: from database) -N cyclic shuffling of NUMA CPU nodes (performance tuning) -d DIR include session directory @@ -679,7 +675,6 @@ -q quiet mode: no progress -v verbose """, - "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))), "B:" -> (arg => build_id = arg), "N" -> (_ => numa_shuffling = true), "d:" -> (arg => dirs += Path.explode(arg)), @@ -701,7 +696,6 @@ build_worker(options, build_id = build_id, progress = progress, - afp_root = afp_root, dirs = dirs.toList, numa_shuffling = Host.numa_check(progress, numa_shuffling), max_jobs = max_jobs) diff -r e2ccabd7a857 -r 9308bc5f65d6 src/Pure/Build/build_cluster.scala --- a/src/Pure/Build/build_cluster.scala Sat May 25 12:20:57 2024 +0200 +++ b/src/Pure/Build/build_cluster.scala Sat May 25 17:22:05 2024 +0200 @@ -174,9 +174,6 @@ val build_cluster_identifier: String = options.string("build_cluster_identifier") val build_cluster_root: Path = Path.explode(options.string("build_cluster_root")) val built_cluster_isabelle_home: Path = build_cluster_root + Path.explode("isabelle") - val build_cluster_afp_root: Option[Path] = - if (build_context.afp_root.isEmpty) None - else Some(built_cluster_isabelle_home + Path.explode("AFP")) lazy val build_cluster_isabelle: Other_Isabelle = Other_Isabelle(built_cluster_isabelle_home, @@ -184,9 +181,9 @@ def sync(): Other_Isabelle = { Sync.sync(options, Rsync.Context(ssh = ssh), built_cluster_isabelle_home, - afp_root = build_context.afp_root, purge_heaps = true, - preserve_jars = true) + preserve_jars = true, + dirs = Sync.afp_dirs(build_context.afp_root)) build_cluster_isabelle } @@ -215,7 +212,6 @@ build_options = build_options.toList, build_id = build_context.build_uuid, isabelle_home = built_cluster_isabelle_home, - afp_root = build_cluster_afp_root, dirs = Path.split(host.dirs).map(build_cluster_isabelle.expand_path), quiet = true) build_cluster_isabelle.bash(script).check diff -r e2ccabd7a857 -r 9308bc5f65d6 src/Pure/Tools/sync.scala --- a/src/Pure/Tools/sync.scala Sat May 25 12:20:57 2024 +0200 +++ b/src/Pure/Tools/sync.scala Sat May 25 17:22:05 2024 +0200 @@ -34,6 +34,24 @@ /* sync */ + val DIRS: Path = Path.basic("dirs") + val DIRS_ROOTS: Path = DIRS + Sessions.ROOTS + + sealed case class Dir(name: String, root: Path, path: Path = Path.current, rev: String = "") { + lazy val hg: Mercurial.Repository = Mercurial.repository(root) + def check(): Unit = hg + + def source: Path = root + path + def target: Path = DIRS + Path.basic(name) + def roots_entry: String = ((if (name.isEmpty) Path.parent else Path.basic(name)) + path).implode + } + + def afp_dir(base_dir: Path = AFP.BASE, rev: String = ""): Dir = + Dir("AFP", base_dir, path = AFP.main_dir(base_dir = Path.current), rev = rev) + + def afp_dirs(root: Option[Path] = None, rev: String = ""): List[Dir] = + root.toList.map(base_dir => afp_dir(base_dir = base_dir, rev = rev)) + def sync(options: Options, context: Rsync.Context, target: Path, thorough: Boolean = false, purge_heaps: Boolean = false, @@ -41,13 +59,23 @@ preserve_jars: Boolean = false, dry_run: Boolean = false, rev: String = "", - afp_root: Option[Path] = None, - afp_rev: String = "" + dirs: List[Dir] = Nil ): Unit = { val progress = context.progress val self = Mercurial.self_repository() - val afp = afp_root.map(Mercurial.repository(_)) + dirs.foreach(_.check()) + + val sync_dirs: List[Dir] = { + val m = + Multi_Map.from( + for (dir <- dirs.iterator if dir.name.nonEmpty) yield dir.name -> dir.root.canonical) + for ((name, roots) <- m.iterator_list if roots.length > 1) { + error("Incoherent sync directory " + quote(name) + ":\n" + + cat_lines(roots.reverse.map(p => " " + p.toString))) + } + Library.distinct(dirs, (d1: Dir, d2: Dir) => d1.name == d2.name) + } val more_filter = if (preserve_jars) List("include *.jar", "protect *.jar") else Nil @@ -60,18 +88,20 @@ progress.echo("\n* Isabelle:", verbose = true) val filter_heaps = if (purge_heaps) Nil else List("protect /heaps", "protect /heaps/**") + val filter_dirs = sync_dirs.map(dir => "protect /" + dir.target.implode) synchronize(self, target, rev, contents = List(File.content(Path.explode("etc/ISABELLE_ID"), self.id(rev = rev))), - filter = filter_heaps ::: List("protect /AFP")) + filter = filter_heaps ::: filter_dirs) - for (src <- afp) { - progress.echo("\n* AFP:", verbose = true) - synchronize(src, target + Path.explode("AFP"), afp_rev) + context.ssh.make_directory(target + DIRS) + context.ssh.write(target + DIRS_ROOTS, Library.terminate_lines(dirs.map(_.roots_entry))) + + for (dir <- sync_dirs) { + progress.echo("\n* " + dir.name + ":", verbose = true) + synchronize(dir.hg, target + dir.target, dir.rev) } - val images = - find_images(options, session_images, - dirs = afp_root.map(_ + Path.explode("thys")).toList) + val images = find_images(options, session_images, dirs = dirs.map(_.source)) if (images.nonEmpty) { progress.echo("\n* Session images:", verbose = true) val heaps = context.target(target + Path.explode("heaps")) + "/" @@ -143,7 +173,7 @@ val context = Rsync.Context(progress = progress, ssh = ssh, stats = verbose) sync(options, context, target, thorough = thorough, purge_heaps = purge_heaps, session_images = session_images, preserve_jars = preserve_jars, dry_run = dry_run, - rev = rev, afp_root = afp_root, afp_rev = afp_rev) + rev = rev, dirs = afp_dirs(afp_root, afp_rev)) } } )