# HG changeset patch # User wenzelm # Date 1699824848 -3600 # Node ID 7419b8d473acfc2369b30696228b345cc30d79de # Parent 74147aa81dbb0e560e51abb71934bacb65614914# Parent 890783dc4bc63c932d167b02dc3fe56c5d823822 merged diff -r 74147aa81dbb -r 7419b8d473ac src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Sat Nov 11 17:44:03 2023 +0000 +++ b/src/Pure/Admin/build_history.scala Sun Nov 12 22:34:08 2023 +0100 @@ -357,7 +357,7 @@ build_info.finished_sessions.flatMap { session_name => val heap = isabelle_output + Path.explode(session_name) if (heap.is_file) { - Some("Heap " + session_name + " (" + Value.Long(File.space(heap).bytes) + " bytes)") + Some("Heap " + session_name + " (" + Value.Long(File.size(heap)) + " bytes)") } else None } diff -r 74147aa81dbb -r 7419b8d473ac src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Sat Nov 11 17:44:03 2023 +0000 +++ b/src/Pure/General/bytes.scala Sun Nov 12 22:34:08 2023 +0100 @@ -73,7 +73,7 @@ def read_url(name: String): Bytes = using(Url(name).openStream)(read_stream(_)) def read_file(path: Path, offset: Long = 0L, limit: Long = Long.MaxValue): Bytes = { - val length = File.space(path).bytes + val length = File.size(path) val start = offset.max(0L) val len = (length - start).max(0L).min(limit) if (len > Int.MaxValue) error("Cannot read large file slice: " + Space.bytes(len).print) diff -r 74147aa81dbb -r 7419b8d473ac src/Pure/General/file.scala --- a/src/Pure/General/file.scala Sat Nov 11 17:44:03 2023 +0000 +++ b/src/Pure/General/file.scala Sun Nov 12 22:34:08 2023 +0100 @@ -408,8 +408,8 @@ } - /* space */ + /* strict file size */ - def space(path: Path): Space = - Space.bytes(path.check_file.file.length) + def size(path: Path): Long = path.check_file.file.length + def space(path: Path): Space = Space.bytes(size(path)) } diff -r 74147aa81dbb -r 7419b8d473ac src/Pure/General/long_name.scala --- a/src/Pure/General/long_name.scala Sat Nov 11 17:44:03 2023 +0000 +++ b/src/Pure/General/long_name.scala Sun Nov 12 22:34:08 2023 +0100 @@ -27,4 +27,12 @@ def base_name(name: String): String = if (name == "") "" else explode(name).last + + def try_unqualify(qual: String, name: String): Option[String] = { + val m = qual.length + val n = name.length + if (0 < m && m < n && name.startsWith(qual) && name(m) == separator_char) + Some(name.substring(m + 1)) + else None + } } diff -r 74147aa81dbb -r 7419b8d473ac src/Pure/General/mailman.scala --- a/src/Pure/General/mailman.scala Sat Nov 11 17:44:03 2023 +0000 +++ b/src/Pure/General/mailman.scala Sun Nov 12 22:34:08 2023 +0100 @@ -376,15 +376,14 @@ try { val length = connection.getContentLengthLong val timestamp = connection.getLastModified - val file = path.file - if (file.isFile && file.length == length && file.lastModified == timestamp) None + if (path.is_file && File.size(path) == length && path.file.lastModified == timestamp) None else { Isabelle_System.make_directory(path.dir) progress.echo("Getting " + url) val bytes = using(connection.getInputStream)(Bytes.read_stream(_, hint = length.toInt max 1024)) - Bytes.write(file, bytes) - file.setLastModified(timestamp) + Bytes.write(path, bytes) + path.file.setLastModified(timestamp) Some(path) } } diff -r 74147aa81dbb -r 7419b8d473ac src/Pure/General/path.scala --- a/src/Pure/General/path.scala Sat Nov 11 17:44:03 2023 +0000 +++ b/src/Pure/General/path.scala Sun Nov 12 22:34:08 2023 +0100 @@ -327,8 +327,8 @@ def is_file: Boolean = file.isFile def is_dir: Boolean = file.isDirectory - def check_file: Path = if (is_file) this else error("No such file: " + this) - def check_dir: Path = if (is_dir) this else error("No such directory: " + this) + def check_file: Path = if (is_file) this else error("No such file: " + this.expand) + def check_dir: Path = if (is_dir) this else error("No such directory: " + this.expand) def java_path: JPath = file.toPath diff -r 74147aa81dbb -r 7419b8d473ac src/Pure/ML/ml_heap.scala --- a/src/Pure/ML/ml_heap.scala Sat Nov 11 17:44:03 2023 +0000 +++ b/src/Pure/ML/ml_heap.scala Sun Nov 12 22:34:08 2023 +0100 @@ -21,7 +21,7 @@ if (heap.is_file) { val l = sha1_prefix.length val m = l + SHA1.digest_length - val n = heap.file.length + val n = File.size(heap) val bs = Bytes.read_file(heap, offset = n - m) if (bs.length == m) { val s = bs.text @@ -151,7 +151,7 @@ database match { case None => case Some(db) => - val size = File.space(heap).bytes - sha1_prefix.length - SHA1.digest_length + val size = File.size(heap) - sha1_prefix.length - SHA1.digest_length val slices = (size.toDouble / slice.toDouble).ceil.toInt val step = (size.toDouble / slices.toDouble).ceil.toLong diff -r 74147aa81dbb -r 7419b8d473ac src/Pure/PIDE/headless.scala --- a/src/Pure/PIDE/headless.scala Sat Nov 11 17:44:03 2023 +0000 +++ b/src/Pure/PIDE/headless.scala Sun Nov 12 22:34:08 2023 +0100 @@ -92,7 +92,7 @@ def finished: Load_State = Load_State(Nil, Nil, Space.zero) def count_file(name: Document.Node.Name): Long = - if (loaded_theory(name)) 0 else File.space(name.path).bytes + if (loaded_theory(name)) 0 else File.size(name.path) } private case class Load_State( diff -r 74147aa81dbb -r 7419b8d473ac src/Pure/System/registry.scala --- a/src/Pure/System/registry.scala Sat Nov 11 17:44:03 2023 +0000 +++ b/src/Pure/System/registry.scala Sun Nov 12 22:34:08 2023 +0100 @@ -20,49 +20,88 @@ /* interpreted entries */ - def err(msg: String, name: String): Nothing = - error(msg + " for registry entry " + quote(name)) + trait Category { + def prefix: String + override def toString: String = "Registry.Category(" + quote(prefix) + ")" + def qualify(name: String): String = Long_Name.qualify(prefix, name) + def try_unqualify(name: String): Option[String] = Long_Name.try_unqualify(prefix, name) + + type Value + def bad_value(name: String): Nothing = error("Bad registry entry " + quote(qualify(name))) + def default_value(registry: Registry, name: String): Value + def value(registry: Registry, t: TOML.T, name: String): Value - abstract class Category[A](val prefix: String) { - override def toString: String = "Registry.Category(" + quote(prefix) + ")" - def default_value: A - def value(name: String, t: TOML.T): A + def get(registry: Registry, name: String): Value = { + registry.root.any.get(prefix) match { + case None => default_value(registry, name) + case Some(t: TOML.Table) => + t.any.get(name) match { + case None => default_value(registry, name) + case Some(u) => value(registry, u, name) + } + case Some(_) => bad_value(name) + } + } } - abstract class Table[A](prefix: String) extends Category[A](prefix) { - def table_value(name: String, table: TOML.Table): A - override def default_value: A = table_value("", TOML.Table.empty) - override def value(name: String, t: TOML.T): A = + trait Strict extends Category { + override def default_value(registry: Registry, name: String): Value = bad_value(name) + } + + trait Table extends Category { + def table_value(registry: Registry, table: TOML.Table, name: String): Value + override def default_value(registry: Registry, name: String): Value = + table_value(registry, TOML.Table.empty, name) + override def value(registry: Registry, t: TOML.T, name: String): Value = t match { - case table: TOML.Table => table_value(name, table) - case _ => err("Table expected", Long_Name.qualify(prefix, name)) + case table: TOML.Table => table_value(registry, table, name) + case _ => bad_value(name) } } /* build cluster resources */ - object Host extends Table[List[Options.Spec]]("host") { + trait Host extends Table { + def prefix = "host" + type Value = List[Options.Spec] + def options_spec(a: TOML.Key, b: TOML.T): Option[Options.Spec] = TOML.Scalar.unapply(b).map(Options.Spec.eq(a, _)) - override def table_value(a: String, t: TOML.Table): List[Options.Spec] = + override def table_value(registry: Registry, t: TOML.Table, a: String): Value = for ((a, b) <- t.any.values; s <- options_spec(a, b)) yield s } + object Host extends Host + object Host_Strict extends Host with Strict + object Host_Cluster extends Host with Strict { override def prefix = Cluster.prefix } + + object Cluster extends Table with Strict { + def prefix = "cluster" + def prefix_hosts = "hosts" + type Value = List[(String, List[Options.Spec])] + + override def table_value(registry: Registry, t: TOML.Table, a: String): Value = { + val hosts = + t.array.get(prefix_hosts) match { + case Some(arr) => arr.string.values.map(_.rep) + case None => bad_value(Long_Name.qualify(a, prefix_hosts)) + } + val cluster_specs = Host_Cluster.get(registry, a) + hosts.map(h => (h, Host_Strict.get(registry, h) ::: cluster_specs)) + } + } } -class Registry private(val table: TOML.Table) { - override def toString: String = TOML.Format(table) - - def get[A](category: Registry.Category[A], name: String): A = { - table.any.get(category.prefix) match { - case None => category.default_value - case Some(t: TOML.Table) => - t.any.get(name) match { - case None => category.default_value - case Some(u) => category.value(name, u) +class Registry private(val root: TOML.Table) { + override def toString: String = + (for (a <- root.domain.toList.sorted.iterator) yield { + val size = + root.any.get(a) match { + case Some(t: TOML.Array) => "(" + t.length + ")" + case Some(t: TOML.Table) => "(" + t.domain.size + ")" + case _ => "" } - case Some(_) => Registry.err("Table expected", category.prefix) - } - } + a + size + }).mkString("Registry(", ", ", ")") } diff -r 74147aa81dbb -r 7419b8d473ac src/Pure/Tools/build_cluster.scala --- a/src/Pure/Tools/build_cluster.scala Sat Nov 11 17:44:03 2023 +0000 +++ b/src/Pure/Tools/build_cluster.scala Sun Nov 12 22:34:08 2023 +0100 @@ -73,16 +73,22 @@ } catch { case ERROR(msg) => err(msg) } - for (name <- space_explode(',', names)) yield { - val base_specs = registry.get(Registry.Host, name) + def get_registry(a: String): Registry.Cluster.Value = + Registry.Cluster.try_unqualify(a) match { + case Some(b) => Registry.Cluster.get(registry, b) + case None => List(a -> Registry.Host.get(registry, a)) + } + + for (name <- space_explode(',', names); (host, host_specs) <- get_registry(name)) + yield { val (params, options) = try { - val (specs1, specs2) = (base_specs ::: more_specs).partition(is_parameter) + val (specs1, specs2) = (host_specs ::: more_specs).partition(is_parameter) (parameters ++ specs1, { test_options ++ specs2; specs2 }) } catch { case ERROR(msg) => err(msg) } - apply(name = name, + apply(name = host, hostname = params.string(HOSTNAME), user = params.string(USER), port = params.int(PORT), diff -r 74147aa81dbb -r 7419b8d473ac src/Pure/Tools/profiling.scala --- a/src/Pure/Tools/profiling.scala Sat Nov 11 17:44:03 2023 +0000 +++ b/src/Pure/Tools/profiling.scala Sun Nov 12 22:34:08 2023 +0100 @@ -97,7 +97,7 @@ locales = session.locales, locale_thms = session.locale_thms, global_thms = session.global_thms, - heap_size = Space.bytes(store.the_heap(session_name).file.length), + heap_size = File.space(store.the_heap(session_name)), thys_id_size = session.sizeof_thys_id, thms_id_size = session.sizeof_thms_id, terms_size = session.sizeof_terms,