# HG changeset patch # User wenzelm # Date 1708766501 -3600 # Node ID e59d93da9109a84797df84be5d446918859ba2cc # Parent d3a26436e679750301d0bcb8c1288ffcae1f7d22 removed unused database_server (amending 32ca3d1283de); diff -r d3a26436e679 -r e59d93da9109 src/Pure/Build/build.scala --- a/src/Pure/Build/build.scala Fri Feb 23 17:22:09 2024 +0100 +++ b/src/Pure/Build/build.scala Sat Feb 24 10:21:41 2024 +0100 @@ -186,108 +186,105 @@ val build_options = store.options using(store.open_server()) { server => - using_optional(store.maybe_open_database_server(server = server)) { database_server => - - /* session selection and dependencies */ + /* session selection and dependencies */ - val full_sessions = - Sessions.load_structure(build_options, dirs = AFP.make_dirs(afp_root) ::: dirs, - select_dirs = select_dirs, infos = infos, augment_options = augment_options) - val full_sessions_selection = full_sessions.imports_selection(selection) + val full_sessions = + Sessions.load_structure(build_options, dirs = AFP.make_dirs(afp_root) ::: dirs, + select_dirs = select_dirs, infos = infos, augment_options = augment_options) + val full_sessions_selection = full_sessions.imports_selection(selection) - val build_deps = { - val deps0 = - Sessions.deps(full_sessions.selection(selection), progress = progress, - inlined_files = true, list_files = list_files, check_keywords = check_keywords - ).check_errors + val build_deps = { + val deps0 = + Sessions.deps(full_sessions.selection(selection), progress = progress, + inlined_files = true, list_files = list_files, check_keywords = check_keywords + ).check_errors - if (soft_build && !fresh_build) { - val outdated = - deps0.sessions_structure.build_topological_order.flatMap(name => - store.try_open_database(name, server = server) match { - case Some(db) => - using(db)(store.read_build(_, name)) match { - case Some(build) if build.ok => - val session_options = deps0.sessions_structure(name).options - val session_sources = deps0.sources_shasum(name) - if (Sessions.eq_sources(session_options, build.sources, session_sources)) { - None - } - else Some(name) - case _ => Some(name) - } - case None => Some(name) - }) + if (soft_build && !fresh_build) { + val outdated = + deps0.sessions_structure.build_topological_order.flatMap(name => + store.try_open_database(name, server = server) match { + case Some(db) => + using(db)(store.read_build(_, name)) match { + case Some(build) if build.ok => + val session_options = deps0.sessions_structure(name).options + val session_sources = deps0.sources_shasum(name) + if (Sessions.eq_sources(session_options, build.sources, session_sources)) { + None + } + else Some(name) + case _ => Some(name) + } + case None => Some(name) + }) - Sessions.deps(full_sessions.selection(Sessions.Selection(sessions = outdated)), - progress = progress, inlined_files = true).check_errors - } - else deps0 + Sessions.deps(full_sessions.selection(Sessions.Selection(sessions = outdated)), + progress = progress, inlined_files = true).check_errors } + else deps0 + } - /* check unknown files */ + /* check unknown files */ - if (check_unknown_files) { - val source_files = - (for { - (_, base) <- build_deps.session_bases.iterator - (path, _) <- base.session_sources.iterator - } yield path).toList - Mercurial.check_files(source_files)._2 match { - case Nil => - case unknown_files => - progress.echo_warning( - "Unknown files (not part of the underlying Mercurial repository):" + - unknown_files.map(File.standard_path).sorted.mkString("\n ", "\n ", "")) - } + if (check_unknown_files) { + val source_files = + (for { + (_, base) <- build_deps.session_bases.iterator + (path, _) <- base.session_sources.iterator + } yield path).toList + Mercurial.check_files(source_files)._2 match { + case Nil => + case unknown_files => + progress.echo_warning( + "Unknown files (not part of the underlying Mercurial repository):" + + unknown_files.map(File.standard_path).sorted.mkString("\n ", "\n ", "")) } + } - /* build process and results */ + /* build process and results */ - val clean_sessions = - if (clean_build) full_sessions.imports_descendants(full_sessions_selection) else Nil + val clean_sessions = + if (clean_build) full_sessions.imports_descendants(full_sessions_selection) else Nil - val build_context = - Context(store, build_deps, engine = engine, afp_root = afp_root, - build_hosts = build_hosts, hostname = hostname(build_options), - clean_sessions = clean_sessions, build_heap = build_heap, - numa_shuffling = numa_shuffling, fresh_build = fresh_build, - no_build = no_build, session_setup = session_setup, - jobs = max_jobs.getOrElse(if (build_hosts.nonEmpty) 0 else 1), master = true) + val build_context = + Context(store, build_deps, engine = engine, afp_root = afp_root, + build_hosts = build_hosts, hostname = hostname(build_options), + clean_sessions = clean_sessions, build_heap = build_heap, + numa_shuffling = numa_shuffling, fresh_build = fresh_build, + no_build = no_build, session_setup = session_setup, + jobs = max_jobs.getOrElse(if (build_hosts.nonEmpty) 0 else 1), master = true) - val results = engine.run_build_process(build_context, progress, server) + val results = engine.run_build_process(build_context, progress, server) - if (export_files) { - for (name <- full_sessions_selection.iterator if results(name).ok) { - val info = results.info(name) - if (info.export_files.nonEmpty) { - progress.echo("Exporting " + info.name + " ...") - for ((dir, prune, pats) <- info.export_files) { - Export.export_files(store, name, info.dir + dir, - progress = if (progress.verbose) progress else new Progress, - export_prune = prune, - export_patterns = pats) - } + if (export_files) { + for (name <- full_sessions_selection.iterator if results(name).ok) { + val info = results.info(name) + if (info.export_files.nonEmpty) { + progress.echo("Exporting " + info.name + " ...") + for ((dir, prune, pats) <- info.export_files) { + Export.export_files(store, name, info.dir + dir, + progress = if (progress.verbose) progress else new Progress, + export_prune = prune, + export_patterns = pats) } } } + } - val presentation_sessions = - results.sessions_ok.filter(name => browser_info.enabled(results.info(name))) - if (presentation_sessions.nonEmpty && !progress.stopped) { - Browser_Info.build(browser_info, results.store, results.deps, presentation_sessions, - progress = progress, server = server) - } + val presentation_sessions = + results.sessions_ok.filter(name => browser_info.enabled(results.info(name))) + if (presentation_sessions.nonEmpty && !progress.stopped) { + Browser_Info.build(browser_info, results.store, results.deps, presentation_sessions, + progress = progress, server = server) + } - if (results.unfinished.nonEmpty && (progress.verbose || !no_build)) { - progress.echo("Unfinished session(s): " + commas(results.unfinished)) - } + if (results.unfinished.nonEmpty && (progress.verbose || !no_build)) { + progress.echo("Unfinished session(s): " + commas(results.unfinished)) + } - results - } + results } }