# HG changeset patch
# User wenzelm
# Date 1689850547 -7200
# Node ID c157af5f346e6734acafa1d95185ec14dd3dca05
# Parent  dba39392d62eb1bd8c2e4804f57c512b36f93771
more pro-forma support for afp_root;

diff -r dba39392d62e -r c157af5f346e src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Thu Jul 20 12:44:46 2023 +0200
+++ b/src/Pure/Admin/afp.scala	Thu Jul 20 12:55:47 2023 +0200
@@ -27,6 +27,12 @@
 
   def main_dir(base_dir: Path = BASE): Path = base_dir + Path.explode("thys")
 
+  def make_dirs(afp_root: Option[Path]): List[Path] =
+    afp_root match {
+      case None => Nil
+      case Some(base_dir) => List(main_dir(base_dir = base_dir))
+    }
+
   def init(options: Options, base_dir: Path = BASE): AFP =
     new AFP(options, base_dir)
 
diff -r dba39392d62e -r c157af5f346e src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Jul 20 12:44:46 2023 +0200
+++ b/src/Pure/Tools/build.scala	Thu Jul 20 12:55:47 2023 +0200
@@ -138,12 +138,6 @@
     val store = build_engine.build_store(options, build_hosts = build_hosts, cache = cache)
     val build_options = store.options
 
-    val afp_dirs =
-      afp_root match {
-        case None => Nil
-        case Some(dir) => List(AFP.main_dir(base_dir = dir))
-      }
-
     using(store.open_server()) { server =>
       using_optional(store.maybe_open_database_server(server = server)) { database_server =>
 
@@ -151,7 +145,7 @@
         /* session selection and dependencies */
 
         val full_sessions =
-          Sessions.load_structure(build_options, dirs = afp_dirs ::: dirs,
+          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)
 
@@ -203,7 +197,7 @@
         /* build process and results */
 
         val build_context =
-          Build_Process.Context(store, build_deps, build_hosts = build_hosts,
+          Build_Process.Context(store, build_deps, afp_root = afp_root, build_hosts = build_hosts,
             hostname = hostname(build_options), build_heap = build_heap,
             numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build,
             no_build = no_build, session_setup = session_setup, master = true)
@@ -473,6 +467,7 @@
     build_id: String = "",
     progress: Progress = new Progress,
     list_builds: Boolean = false,
+    afp_root: Option[Path] = None,
     dirs: List[Path] = Nil,
     numa_shuffling: Boolean = false,
     max_jobs: Int = 1,
@@ -492,16 +487,16 @@
           val build_master = find_builds(build_database, build_id, builds)
 
           val sessions_structure =
-            Sessions.load_structure(build_options, dirs = dirs).
+            Sessions.load_structure(build_options, dirs = AFP.make_dirs(afp_root) ::: 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 =
-            Build_Process.Context(store, build_deps, hostname = hostname(build_options),
-              numa_shuffling = numa_shuffling, max_jobs = max_jobs,
-              build_uuid = build_master.build_uuid)
+            Build_Process.Context(store, build_deps, afp_root = afp_root,
+              hostname = hostname(build_options), numa_shuffling = numa_shuffling,
+              max_jobs = max_jobs, build_uuid = build_master.build_uuid)
 
           Some(build_engine.run_process(build_context, progress, server))
         }
@@ -516,6 +511,7 @@
   val isabelle_tool2 = Isabelle_Tool("build_worker", "external worker for session build process",
     Scala_Project.here,
     { args =>
+      var afp_root: Option[Path] = None
       var build_id = ""
       var list_builds = false
       var numa_shuffling = false
@@ -530,6 +526,7 @@
 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
@@ -538,6 +535,7 @@
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -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)),
@@ -557,6 +555,7 @@
             build_id = build_id,
             progress = progress,
             list_builds = list_builds,
+            afp_root = afp_root,
             dirs = dirs.toList,
             numa_shuffling = Host.numa_check(progress, numa_shuffling),
             max_jobs = max_jobs)
diff -r dba39392d62e -r c157af5f346e src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Thu Jul 20 12:44:46 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Thu Jul 20 12:55:47 2023 +0200
@@ -19,6 +19,7 @@
   sealed case class Context(
     store: Store,
     build_deps: isabelle.Sessions.Deps,
+    afp_root: Option[Path] = None,
     build_hosts: List[Build_Cluster.Host] = Nil,
     ml_platform: String = Isabelle_System.getenv("ML_PLATFORM"),
     hostname: String = Isabelle_System.hostname(),