# HG changeset patch # User wenzelm # Date 1687944902 -7200 # Node ID af2963b7475262a10d513c2762e489120d6240dc # Parent a625bfb0e549bd461ec6ce3c4ad99897c00177af support for identified builds; more complete implementation of "isabelle build_worker"; diff -r a625bfb0e549 -r af2963b74752 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Jun 28 11:33:11 2023 +0200 +++ b/src/Pure/Tools/build.scala Wed Jun 28 11:35:02 2023 +0200 @@ -81,6 +81,14 @@ /* build */ + def build_results(options: Options, context: Build_Process.Context, progress: Progress): Results = + Isabelle_Thread.uninterruptible { + val engine = get_engine(options.string("build_engine")) + using(engine.init(context, progress)) { build_process => + Results(context, build_process.run()) + } + } + def build( options: Options, selection: Sessions.Selection = Sessions.Selection.empty, @@ -180,14 +188,7 @@ } } - val results = - Isabelle_Thread.uninterruptible { - val engine = get_engine(build_options.string("build_engine")) - using(engine.init(build_context, progress)) { build_process => - val res = build_process.run() - Results(build_context, res) - } - } + val results = build_results(build_options, build_context, progress) if (export_files) { for (name <- full_sessions_selection.iterator if results(name).ok) { @@ -378,25 +379,62 @@ /** "isabelle build_worker" **/ + /* identified builds */ + + def read_builds(options: Options): List[Build_Process.Build] = + using_option(Store(options).maybe_open_build_database(Build_Process.Data.database))( + Build_Process.read_builds).getOrElse(Nil) + + def print_builds(builds: List[Build_Process.Build]): String = + if (builds.isEmpty) "No build processes available" + else { + "Available build processes:" + + (for ((build, i) <- builds.iterator.zipWithIndex) + yield "\n " + (i + 1) + ": " + build.build_uuid).mkString + } + + def id_builds(id: String, builds: List[Build_Process.Build]): Build_Process.Build = + (id, builds.length) match { + case (Value.Int(i), n) if 1 <= i && i <= n => builds(i - 1) + case (UUID(_), _) if builds.exists(_.build_uuid == id) => builds.find(_.build_uuid == id).get + case ("", 0) => error(print_builds(builds)) + case ("", 1) => builds.head + case _ => cat_error("Cannot identify build process " + quote(id), print_builds(builds)) + } + + /* build_worker */ def build_worker( options: Options, - build_uuid: String, + build_master: Build_Process.Build, progress: Progress = new Progress, dirs: List[Path] = Nil, - infos: List[Sessions.Info] = Nil, numa_shuffling: Boolean = false, max_jobs: Int = 1, - session_setup: (String, Session) => Unit = (_, _) => (), cache: Term.Cache = Term.Cache.make() ): Results = { val store = build_init(options, cache = cache) val build_options = store.options - progress.echo("build worker for " + build_uuid) - progress.echo_warning("FIXME") - ??? + val sessions = + using_optional(Store(options).maybe_open_build_database(Build_Process.Data.database)) { + case None => error("Cannot access build database") + case Some(db) => Build_Process.read_sessions(db, build_master.build_uuid) + } + + val sessions_structure = + Sessions.load_structure(build_options, dirs = dirs). + selection(Sessions.Selection(sessions = sessions)) + + val build_deps = + Sessions.deps(sessions_structure, progress = progress, inlined_files = true).check_errors + + val build_context = + Build_Process.init_context(store, build_deps, progress = progress, + hostname = hostname(build_options), numa_shuffling = numa_shuffling, max_jobs = max_jobs) + + build_results(build_options, build_context, progress) } @@ -405,51 +443,63 @@ val isabelle_tool2 = Isabelle_Tool("build_worker", "external worker for session build process", Scala_Project.here, { args => + var build_id = "" + var list_builds = false var numa_shuffling = false var dirs: List[Path] = Nil var max_jobs = 1 - var options = Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS) + var options = + Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS ::: + List(Options.Spec.make("build_database_test"))) var verbose = false - var build_uuid = "" val getopts = Getopts(""" -Usage: isabelle build_worker [OPTIONS] ...] +Usage: isabelle build_worker [OPTIONS] Options are: -N cyclic shuffling of NUMA CPU nodes (performance tuning) - -U UUID Universally Unique Identifier of the build process -d DIR include session directory + -i ID identify build process, either via index (starting from 1) or + Universally Unique Identifier (UUID) -j INT maximum number of parallel jobs (default 1) + -l list build processes -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose Run as external worker for session build process, as identified via - option -U UUID. + option -i. The latter can be omitted, if there is exactly one build. """, "N" -> (_ => numa_shuffling = true), - "U:" -> (arg => build_uuid = arg), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), + "i:" -> (arg => build_id = arg), "j:" -> (arg => max_jobs = Value.Int.parse(arg)), + "l" -> (_ => list_builds = true), "o:" -> (arg => options = options + arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() - if (build_uuid.isEmpty) error("Missing UUID for build process (option -U)") - val progress = new Console_Progress(verbose = verbose) - val results = - progress.interrupt_handler { - build_worker(options, build_uuid, - progress = progress, - dirs = dirs, - numa_shuffling = Host.numa_check(progress, numa_shuffling), - max_jobs = max_jobs) - } + val builds = read_builds(options) + + if (list_builds) progress.echo(print_builds(builds)) + + if (!list_builds || build_id.nonEmpty) { + val build = id_builds(build_id, builds) - sys.exit(results.rc) + val results = + progress.interrupt_handler { + build_worker(options, build, + progress = progress, + dirs = dirs, + numa_shuffling = Host.numa_check(progress, numa_shuffling), + max_jobs = max_jobs) + } + + sys.exit(results.rc) + } }) diff -r a625bfb0e549 -r af2963b74752 src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Wed Jun 28 11:33:11 2023 +0200 +++ b/src/Pure/Tools/build_process.scala Wed Jun 28 11:35:02 2023 +0200 @@ -343,7 +343,7 @@ val start = res.date(Base.start) val stop = res.get_date(Base.stop) Build(build_uuid, ml_platform, options, start, stop) - }) + }).sortBy(_.start)(Date.Ordering) def start_build( db: SQL.Database,