--- a/etc/build.props Tue Feb 21 11:25:23 2023 +0000
+++ b/etc/build.props Tue Feb 21 13:02:33 2023 +0100
@@ -306,6 +306,7 @@
services = \
isabelle.Bash$Handler \
isabelle.Bibtex$File_Format \
+ isabelle.Build$Default_Engine \
isabelle.Document_Build$Build_Engine \
isabelle.Document_Build$LIPIcs_LuaLaTeX_Engine \
isabelle.Document_Build$LIPIcs_PDFLaTeX_Engine \
--- a/etc/options Tue Feb 21 11:25:23 2023 +0000
+++ b/etc/options Tue Feb 21 13:02:33 2023 +0100
@@ -172,7 +172,7 @@
-- "ML process command prefix (process policy)"
-section "PIDE Build"
+section "Build Process"
option pide_reports : bool = true
-- "report PIDE markup (in ML)"
@@ -180,6 +180,9 @@
option build_pide_reports : bool = true
-- "report PIDE markup (in batch build)"
+option build_engine : string = ""
+ -- "alternative session build engine"
+
section "Editor Session"
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala Tue Feb 21 11:25:23 2023 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Tue Feb 21 13:02:33 2023 +0100
@@ -215,7 +215,7 @@
progress = progress,
dirs = dirs,
select_dirs = select_dirs,
- numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
+ numa_shuffling = NUMA.check(progress, numa_shuffling),
max_jobs = max_jobs,
verbose = verbose)
}
--- a/src/Pure/System/isabelle_platform.scala Tue Feb 21 11:25:23 2023 +0000
+++ b/src/Pure/System/isabelle_platform.scala Tue Feb 21 13:02:33 2023 +0100
@@ -48,7 +48,9 @@
ISABELLE_PLATFORM64.startsWith("arm64-") ||
ISABELLE_APPLE_PLATFORM64.startsWith("arm64-")
- def is_linux: Boolean = ISABELLE_PLATFORM_FAMILY == "linux"
+ def is_linux: Boolean =
+ ISABELLE_PLATFORM_FAMILY == "linux" ||
+ ISABELLE_PLATFORM_FAMILY == "linux_arm"
def is_macos: Boolean = ISABELLE_PLATFORM_FAMILY == "macos"
def is_windows: Boolean = ISABELLE_PLATFORM_FAMILY == "windows"
--- a/src/Pure/System/numa.scala Tue Feb 21 11:25:23 2023 +0000
+++ b/src/Pure/System/numa.scala Tue Feb 21 13:02:33 2023 +0100
@@ -8,25 +8,28 @@
object NUMA {
- /* available nodes */
+ /* information about nodes */
- def nodes(): List[Int] = {
- val numa_nodes_linux = Path.explode("/sys/devices/system/node/online")
+ private val numa_info_linux: Path = Path.explode("/sys/devices/system/node/online")
- val Single = """^(\d+)$""".r
- val Multiple = """^(\d+)-(\d+)$""".r
+ private val Info_Single = """^(\d+)$""".r
+ private val Info_Multiple = """^(\d+)-(\d+)$""".r
- def read(s: String): List[Int] =
- s match {
- case Single(Value.Int(i)) => List(i)
- case Multiple(Value.Int(i), Value.Int(j)) => (i to j).toList
- case _ => error("Cannot parse CPU node specification: " + quote(s))
- }
+ private def parse_nodes(s: String): List[Int] =
+ s match {
+ case Info_Single(Value.Int(i)) => List(i)
+ case Info_Multiple(Value.Int(i), Value.Int(j)) => (i to j).toList
+ case _ => error("Cannot parse CPU node specification: " + quote(s))
+ }
- if (numa_nodes_linux.is_file) {
- space_explode(',', File.read(numa_nodes_linux).trim).flatMap(read)
- }
- else Nil
+ def nodes(enabled: Boolean = true, ssh: SSH.System = SSH.Local): List[Int] = {
+ val numa_info = if (ssh.isabelle_platform.is_linux) Some(numa_info_linux) else None
+ for {
+ path <- numa_info.toList
+ if enabled && ssh.is_file(path)
+ s <- space_explode(',', ssh.read(path).trim)
+ n <- parse_nodes(s)
+ } yield n
}
@@ -58,7 +61,7 @@
/* shuffling of CPU nodes */
- def enabled_warning(progress: Progress, enabled: Boolean): Boolean = {
+ def check(progress: Progress, enabled: Boolean): Boolean = {
def warning =
nodes() match {
case ns if ns.length < 2 => Some("no NUMA nodes available")
--- a/src/Pure/Tools/build.scala Tue Feb 21 11:25:23 2023 +0000
+++ b/src/Pure/Tools/build.scala Tue Feb 21 13:02:33 2023 +0100
@@ -9,7 +9,7 @@
object Build {
- /** build with results **/
+ /* results */
object Results {
def apply(context: Build_Process.Context, results: Map[String, Process_Result]): Results =
@@ -41,6 +41,29 @@
override def toString: String = rc.toString
}
+
+ /* engine */
+
+ abstract class Engine(val name: String) extends Isabelle_System.Service {
+ override def toString: String = name
+ def init(build_context: Build_Process.Context): Build_Process
+ }
+
+ class Default_Engine extends Engine("") {
+ override def toString: String = "<default>"
+ override def init(build_context: Build_Process.Context): Build_Process =
+ new Build_Process(build_context)
+ }
+
+ lazy val engines: List[Engine] =
+ Isabelle_System.make_services(classOf[Engine])
+
+ def get_engine(name: String): Engine =
+ engines.find(_.name == name).getOrElse(error("Bad build engine " + quote(name)))
+
+
+ /* build */
+
def build(
options: Options,
selection: Sessions.Selection = Sessions.Selection.empty,
@@ -147,7 +170,8 @@
val results =
Isabelle_Thread.uninterruptible {
- val build_process = new Build_Process(build_context)
+ val engine = get_engine(build_options.string("build_engine"))
+ val build_process = engine.init(build_context)
val res = build_process.run()
Results(build_context, res)
}
@@ -293,7 +317,7 @@
clean_build = clean_build,
dirs = dirs,
select_dirs = select_dirs,
- numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
+ numa_shuffling = NUMA.check(progress, numa_shuffling),
max_jobs = max_jobs,
list_files = list_files,
check_keywords = check_keywords,
--- a/src/Pure/Tools/build_process.scala Tue Feb 21 11:25:23 2023 +0000
+++ b/src/Pure/Tools/build_process.scala Tue Feb 21 13:02:33 2023 +0100
@@ -13,7 +13,7 @@
object Build_Process {
- /* static information */
+ /* static context */
object Session_Context {
def empty(session: String, timeout: Time): Session_Context =
@@ -119,7 +119,7 @@
}
}
- val numa_nodes = if (numa_shuffling) NUMA.nodes() else Nil
+ val numa_nodes = NUMA.nodes(enabled = numa_shuffling)
new Context(store, deps, sessions, ordering, progress, numa_nodes,
build_heap = build_heap, max_jobs = max_jobs, fresh_build = fresh_build,
no_build = no_build, verbose = verbose, session_setup)
@@ -150,7 +150,7 @@
}
- /* main */
+ /* dynamic state */
case class Entry(name: String, deps: List[String]) {
def is_ready: Boolean = deps.isEmpty
@@ -166,6 +166,58 @@
def ok: Boolean = process_result.ok
}
+ sealed case class State(
+ numa_index: Int = 0,
+ pending: List[Entry] = Nil,
+ running: Map[String, Build_Job] = Map.empty,
+ results: Map[String, Build_Process.Result] = Map.empty
+ ) {
+ def get_numa: (Int, Set[Int]) = (numa_index, numa_running)
+ def put_numa(i: Int): State = copy(numa_index = i)
+
+ def finished: Boolean = pending.isEmpty
+
+ def remove_pending(name: String): State =
+ copy(pending = pending.flatMap(
+ entry => if (entry.name == name) None else Some(entry.resolve(name))))
+
+ def is_running(name: String): Boolean = running.isDefinedAt(name)
+
+ def numa_running: Set[Int] =
+ Set.from(for (job <- running.valuesIterator; i <- job.numa_node) yield i)
+
+ def stop_running(): Unit = running.valuesIterator.foreach(_.terminate())
+
+ def finished_running(): List[Build_Job.Build_Session] =
+ List.from(
+ running.valuesIterator.flatMap {
+ case job: Build_Job.Build_Session if job.is_finished => Some(job)
+ case _ => None
+ })
+
+ def add_running(name: String, job: Build_Job): State =
+ copy(running = running + (name -> job))
+
+ def remove_running(name: String): State =
+ copy(running = running - name)
+
+ def make_result(
+ name: String,
+ current: Boolean,
+ output_heap: SHA1.Shasum,
+ process_result: Process_Result
+ ): State = {
+ val result = Build_Process.Result(current, output_heap, process_result)
+ copy(results = results + (name -> result))
+ }
+
+ def get_results(names: List[String]): List[Build_Process.Result] =
+ names.map(results.apply)
+ }
+
+
+ /* main process */
+
def session_finished(session_name: String, process_result: Process_Result): String =
"Finished " + session_name + " (" + process_result.timing.message_resources + ")"
@@ -177,14 +229,14 @@
}
}
-class Build_Process(build_context: Build_Process.Context) {
- private val store = build_context.store
- private val build_options = store.options
- private val build_deps = build_context.deps
- private val progress = build_context.progress
- private val verbose = build_context.verbose
+class Build_Process(protected val build_context: Build_Process.Context) {
+ protected val store: Sessions.Store = build_context.store
+ protected val build_options: Options = store.options
+ protected val build_deps: Sessions.Deps = build_context.deps
+ protected val progress: Progress = build_context.progress
+ protected val verbose: Boolean = build_context.verbose
- private val log =
+ protected val log: Logger =
build_options.string("system_log") match {
case "" => No_Logger
case "-" => Logger.make(progress)
@@ -192,76 +244,50 @@
}
// global state
- private var _numa_index = 0
- private var _pending: List[Build_Process.Entry] =
- (for ((name, (_, (preds, _))) <- build_context.sessions_structure.build_graph.iterator)
- yield Build_Process.Entry(name, preds.toList)).toList
- private var _running = Map.empty[String, Build_Job]
- private var _results = Map.empty[String, Build_Process.Result]
+ protected var _state: Build_Process.State = init_state()
- private def test_pending(): Boolean = synchronized { _pending.nonEmpty }
+ protected def init_state(): Build_Process.State =
+ Build_Process.State(pending =
+ (for ((name, (_, (preds, _))) <- build_context.sessions_structure.build_graph.iterator)
+ yield Build_Process.Entry(name, preds.toList)).toList)
- private def remove_pending(name: String): Unit = synchronized {
- _pending = _pending.flatMap(entry => if (entry.name == name) None else Some(entry.resolve(name)))
- }
+ protected def finished(): Boolean = synchronized { _state.finished }
- private def next_pending(): Option[String] = synchronized {
- if (_running.size < (build_context.max_jobs max 1)) {
- _pending.filter(entry => entry.is_ready && !_running.isDefinedAt(entry.name))
+ protected def next_pending(): Option[String] = synchronized {
+ if (_state.running.size < (build_context.max_jobs max 1)) {
+ _state.pending.filter(entry => entry.is_ready && !_state.is_running(entry.name))
.sortBy(_.name)(build_context.ordering)
.headOption.map(_.name)
}
else None
}
- private def next_numa_node(): Option[Int] = synchronized {
+ protected def next_numa_node(): Option[Int] = synchronized {
val available = build_context.numa_nodes.zipWithIndex
if (available.isEmpty) None
else {
- val used = Set.from(for (job <- _running.valuesIterator; i <- job.numa_node) yield i)
- val index = _numa_index
+ val (index, used) = _state.get_numa
val candidates = available.drop(index) ::: available.take(index)
val (n, i) =
candidates.find({ case (n, i) => i == index && !used(n) }) orElse
candidates.find({ case (n, _) => !used(n) }) getOrElse candidates.head
- _numa_index = (i + 1) % available.length
+ _state = _state.put_numa((i + 1) % available.length)
Some(n)
}
}
- private def stop_running(): Unit = synchronized { _running.valuesIterator.foreach(_.terminate()) }
+ protected def stop_running(): Unit = synchronized { _state.stop_running() }
- private def finished_running(): List[Build_Job.Build_Session] = synchronized {
- List.from(
- _running.valuesIterator.flatMap {
- case job: Build_Job.Build_Session if job.is_finished => Some(job)
- case _ => None
- })
+ protected def finished_running(): List[Build_Job.Build_Session] = synchronized {
+ _state.finished_running()
}
- private def job_running(name: String, job: Build_Job): Build_Job = synchronized {
- _running += (name -> job)
+ protected def job_running(name: String, job: Build_Job): Build_Job = synchronized {
+ _state = _state.add_running(name, job)
job
}
- private def remove_running(name: String): Unit = synchronized {
- _running -= name
- }
-
- private def add_result(
- name: String,
- current: Boolean,
- output_heap: SHA1.Shasum,
- process_result: Process_Result
- ): Unit = synchronized {
- _results += (name -> Build_Process.Result(current, output_heap, process_result))
- }
-
- private def get_results(names: List[String]): List[Build_Process.Result] = synchronized {
- names.map(_results.apply)
- }
-
- private def finish_job(job: Build_Job.Build_Session): Unit = {
+ protected def finish_job(job: Build_Job.Build_Session): Unit = {
val session_name = job.session_name
val process_result = job.join
val output_heap = job.finish
@@ -311,17 +337,19 @@
}
synchronized {
- remove_pending(session_name)
- remove_running(session_name)
- add_result(session_name, false, output_heap, process_result_tail)
+ _state = _state.
+ remove_pending(session_name).
+ remove_running(session_name).
+ make_result(session_name, false, output_heap, process_result_tail)
}
}
- private def start_job(session_name: String): Unit = {
- val ancestor_results =
- get_results(
+ protected def start_job(session_name: String): Unit = {
+ val ancestor_results = synchronized {
+ _state.get_results(
build_deps.sessions_structure.build_requirements(List(session_name)).
filterNot(_ == session_name))
+ }
val input_heaps =
if (ancestor_results.isEmpty) {
SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE")))
@@ -352,15 +380,17 @@
if (all_current) {
synchronized {
- remove_pending(session_name)
- add_result(session_name, true, output_heap, Process_Result.ok)
+ _state = _state.
+ remove_pending(session_name).
+ make_result(session_name, true, output_heap, Process_Result.ok)
}
}
else if (build_context.no_build) {
progress.echo_if(verbose, "Skipping " + session_name + " ...")
synchronized {
- remove_pending(session_name)
- add_result(session_name, false, output_heap, Process_Result.error)
+ _state = _state.
+ remove_pending(session_name).
+ make_result(session_name, false, output_heap, Process_Result.error)
}
}
else if (ancestor_results.forall(_.ok) && !progress.stopped) {
@@ -387,36 +417,37 @@
else {
progress.echo(session_name + " CANCELLED")
synchronized {
- remove_pending(session_name)
- add_result(session_name, false, output_heap, Process_Result.undefined)
+ _state = _state.
+ remove_pending(session_name).
+ make_result(session_name, false, output_heap, Process_Result.undefined)
}
}
}
- private def sleep(): Unit =
+ protected def sleep(): Unit =
Isabelle_Thread.interrupt_handler(_ => progress.stop()) {
build_options.seconds("editor_input_delay").sleep()
}
def run(): Map[String, Process_Result] = {
- if (test_pending()) {
- while (test_pending()) {
+ if (finished()) {
+ progress.echo_warning("Nothing to build")
+ Map.empty[String, Process_Result]
+ }
+ else {
+ while (!finished()) {
if (progress.stopped) stop_running()
for (job <- finished_running()) finish_job(job)
next_pending() match {
- case Some(session_name) => start_job(session_name)
+ case Some(name) => start_job(name)
case None => sleep()
}
}
synchronized {
- for ((name, result) <- _results) yield name -> result.process_result
+ for ((name, result) <- _state.results) yield name -> result.process_result
}
}
- else {
- progress.echo_warning("Nothing to build")
- Map.empty[String, Process_Result]
- }
}
}
--- a/src/Pure/Tools/update.scala Tue Feb 21 11:25:23 2023 +0000
+++ b/src/Pure/Tools/update.scala Tue Feb 21 13:02:33 2023 +0100
@@ -220,7 +220,7 @@
clean_build,
dirs = dirs,
select_dirs = select_dirs,
- numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
+ numa_shuffling = NUMA.check(progress, numa_shuffling),
max_jobs = max_jobs,
fresh_build,
no_build = no_build,
--- a/src/Tools/VSCode/src/build_vscodium.scala Tue Feb 21 11:25:23 2023 +0000
+++ b/src/Tools/VSCode/src/build_vscodium.scala Tue Feb 21 13:02:33 2023 +0100
@@ -63,7 +63,7 @@
build_name: String,
env: List[String]
) {
- def is_linux: Boolean = platform == Platform.Family.linux
+ def primary: Boolean = platform == Platform.Family.linux
def download_name: String = "VSCodium-" + download_template.replace("{VERSION}", version)
def download_ext: String = if (download_template.endsWith(".zip")) "zip" else "tar.gz"
@@ -342,13 +342,13 @@
platform_info.get_vscodium_repository(build_dir, progress = progress)
val sources_patch = platform_info.patch_sources(build_dir)
- if (platform_info.is_linux) write_patch("02-isabelle_sources", sources_patch)
+ if (platform_info.primary) write_patch("02-isabelle_sources", sources_patch)
progress.echo("Build ...")
progress.bash(platform_info.environment + "\n" + "./build.sh",
cwd = build_dir.file, echo = verbose).check
- if (platform_info.is_linux) {
+ if (platform_info.primary) {
Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path)
}
@@ -358,7 +358,7 @@
platform_info.setup_electron(platform_dir)
val resources_patch = platform_info.patch_resources(platform_dir)
- if (platform_info.is_linux) write_patch("03-isabelle_resources", resources_patch)
+ if (platform_info.primary) write_patch("03-isabelle_resources", resources_patch)
Isabelle_System.copy_file(
build_dir + Path.explode("vscode/node_modules/electron/dist/resources/default_app.asar"),