--- a/src/Pure/Build/build.scala Mon Feb 19 11:07:08 2024 +0100
+++ b/src/Pure/Build/build.scala Mon Feb 19 11:30:37 2024 +0100
@@ -122,7 +122,8 @@
build_cluster: Boolean = false,
cache: Term.Cache = Term.Cache.make()
): Store = {
- val store = Store(build_options(options, build_cluster = build_cluster), cache = cache)
+ val store_options = build_options(options, build_cluster = build_cluster)
+ val store = Store(store_options, build_cluster = build_cluster, cache = cache)
Isabelle_System.make_directory(store.output_dir + Path.basic("log"))
Isabelle_Fonts.init()
store
@@ -504,13 +505,14 @@
def build_process(
options: Options,
+ build_cluster: Boolean = false,
list_builds: Boolean = false,
remove_builds: Boolean = false,
force: Boolean = false,
progress: Progress = new Progress
): Unit = {
val build_engine = Engine(engine_name(options))
- val store = build_engine.build_store(options)
+ val store = build_engine.build_store(options, build_cluster = build_cluster)
using(store.open_server()) { server =>
using_optional(store.maybe_open_build_database(server = server)) { build_database =>
@@ -544,6 +546,7 @@
val isabelle_tool2 = Isabelle_Tool("build_process", "manage session build process",
Scala_Project.here,
{ args =>
+ var build_cluster = false
var force = false
var list_builds = false
var options =
@@ -557,6 +560,7 @@
Usage: isabelle build_process [OPTIONS]
Options are:
+ -C build cluster mode (database server)
-f extra force for option -r
-l list build processes
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
@@ -573,8 +577,8 @@
val progress = new Console_Progress()
- build_process(options, list_builds = list_builds, remove_builds = remove_builds,
- force = force, progress = progress)
+ build_process(options, build_cluster = build_cluster, list_builds = list_builds,
+ remove_builds = remove_builds, force = force, progress = progress)
})
@@ -613,7 +617,7 @@
max_jobs: Option[Int] = None
): Results = {
val build_engine = Engine(engine_name(options))
- val store = build_engine.build_store(options)
+ val store = build_engine.build_store(options, build_cluster = true)
val build_options = store.options
using(store.open_server()) { server =>
--- a/src/Pure/Build/store.scala Mon Feb 19 11:07:08 2024 +0100
+++ b/src/Pure/Build/store.scala Mon Feb 19 11:30:37 2024 +0100
@@ -11,8 +11,11 @@
object Store {
- def apply(options: Options, cache: Term.Cache = Term.Cache.make()): Store =
- new Store(options, cache)
+ def apply(
+ options: Options,
+ build_cluster: Boolean = false,
+ cache: Term.Cache = Term.Cache.make()
+ ): Store = new Store(options, build_cluster, cache)
/* session */
@@ -248,7 +251,11 @@
}
}
-class Store private(val options: Options, val cache: Term.Cache) {
+class Store private(
+ val options: Options,
+ val build_cluster: Boolean,
+ val cache: Term.Cache
+ ) {
store =>
override def toString: String = "Store(output_dir = " + output_dir.absolute + ")"
@@ -340,7 +347,7 @@
if (build_database_server) Some(open_database_server(server = server)) else None
def open_build_database(path: Path, server: SSH.Server = SSH.no_server): SQL.Database =
- if (build_database_server) open_database_server(server = server)
+ if (build_database_server || build_cluster) open_database_server(server = server)
else SQLite.open_database(path, restrict = true)
def maybe_open_build_database(