--- a/src/HOL/Data_Structures/Selection.thy Wed Apr 17 22:07:07 2024 +0100
+++ b/src/HOL/Data_Structures/Selection.thy Wed Apr 17 22:07:21 2024 +0100
@@ -310,6 +310,12 @@
if y < x then (y # ls, es, gs) else if x = y then (ls, y # es, gs) else (ls, es, y # gs))"
by (auto simp: partition3_def)
+lemma length_partition3:
+ assumes "partition3 x xs = (ls, es, gs)"
+ shows "length xs = length ls + length es + length gs"
+ using assms by (induction xs arbitrary: ls es gs)
+ (auto simp: partition3_code split: if_splits prod.splits)
+
lemma sort_append:
assumes "\<forall>x\<in>set xs. \<forall>y\<in>set ys. x \<le> y"
shows "sort (xs @ ys) = sort xs @ sort ys"
@@ -643,19 +649,39 @@
definition T_slow_median :: "'a :: linorder list \<Rightarrow> nat" where
"T_slow_median xs = T_length xs + T_slow_select ((length xs - 1) div 2) xs"
-lemma T_slow_select_le: "T_slow_select k xs \<le> length xs ^ 2 + 3 * length xs + 2"
+lemma T_slow_select_le:
+ assumes "k < length xs"
+ shows "T_slow_select k xs \<le> length xs ^ 2 + 3 * length xs + 1"
proof -
- have "T_slow_select k xs \<le> (length xs + 1)\<^sup>2 + (length (insort xs) + 1)"
- unfolding T_slow_select_def
- by (intro add_mono T_insort_length) (auto simp: T_nth_eq)
- also have "\<dots> = length xs ^ 2 + 3 * length xs + 2"
- by (simp add: insort_correct algebra_simps power2_eq_square)
- finally show ?thesis .
+ have "T_slow_select k xs = T_insort xs + T_nth (Sorting.insort xs) k"
+ unfolding T_slow_select_def ..
+ also have "T_insort xs \<le> (length xs + 1) ^ 2"
+ by (rule T_insort_length)
+ also have "T_nth (Sorting.insort xs) k = k + 1"
+ using assms by (subst T_nth_eq) (auto simp: length_insort)
+ also have "k + 1 \<le> length xs"
+ using assms by linarith
+ also have "(length xs + 1) ^ 2 + length xs = length xs ^ 2 + 3 * length xs + 1"
+ by (simp add: algebra_simps power2_eq_square)
+ finally show ?thesis by - simp_all
qed
-lemma T_slow_median_le: "T_slow_median xs \<le> length xs ^ 2 + 4 * length xs + 3"
- unfolding T_slow_median_def using T_slow_select_le[of "(length xs - 1) div 2" xs]
- by (simp add: algebra_simps T_length_eq)
+lemma T_slow_median_le:
+ assumes "xs \<noteq> []"
+ shows "T_slow_median xs \<le> length xs ^ 2 + 4 * length xs + 2"
+proof -
+ have "T_slow_median xs = length xs + T_slow_select ((length xs - 1) div 2) xs + 1"
+ by (simp add: T_slow_median_def T_length_eq)
+ also from assms have "length xs > 0"
+ by simp
+ hence "(length xs - 1) div 2 < length xs"
+ by linarith
+ hence "T_slow_select ((length xs - 1) div 2) xs \<le> length xs ^ 2 + 3 * length xs + 1"
+ by (intro T_slow_select_le) auto
+ also have "length xs + \<dots> + 1 = length xs ^ 2 + 4 * length xs + 2"
+ by (simp add: algebra_simps)
+ finally show ?thesis by - simp_all
+qed
time_fun chop
@@ -717,16 +743,16 @@
function T'_mom_select :: "nat \<Rightarrow> nat" where
"T'_mom_select n =
(if n \<le> 20 then
- 483
+ 482
else
- T'_mom_select (nat \<lceil>0.2*n\<rceil>) + T'_mom_select (nat \<lceil>0.7*n+3\<rceil>) + 19 * n + 55)"
+ T'_mom_select (nat \<lceil>0.2*n\<rceil>) + T'_mom_select (nat \<lceil>0.7*n+3\<rceil>) + 19 * n + 54)"
by force+
termination by (relation "measure id"; simp; linarith)
lemmas [simp del] = T'_mom_select.simps
-lemma T'_mom_select_ge: "T'_mom_select n \<ge> 483"
+lemma T'_mom_select_ge: "T'_mom_select n \<ge> 482"
by (induction n rule: T'_mom_select.induct; subst T'_mom_select.simps) auto
lemma T'_mom_select_mono:
@@ -736,7 +762,7 @@
show ?case
proof (cases "m \<le> 20")
case True
- hence "T'_mom_select m = 483"
+ hence "T'_mom_select m = 482"
by (subst T'_mom_select.simps) auto
also have "\<dots> \<le> T'_mom_select n"
by (rule T'_mom_select_ge)
@@ -744,9 +770,9 @@
next
case False
hence "T'_mom_select m =
- T'_mom_select (nat \<lceil>0.2*m\<rceil>) + T'_mom_select (nat \<lceil>0.7*m + 3\<rceil>) + 19 * m + 55"
+ T'_mom_select (nat \<lceil>0.2*m\<rceil>) + T'_mom_select (nat \<lceil>0.7*m + 3\<rceil>) + 19 * m + 54"
by (subst T'_mom_select.simps) auto
- also have "\<dots> \<le> T'_mom_select (nat \<lceil>0.2*n\<rceil>) + T'_mom_select (nat \<lceil>0.7*n + 3\<rceil>) + 19 * n + 55"
+ also have "\<dots> \<le> T'_mom_select (nat \<lceil>0.2*n\<rceil>) + T'_mom_select (nat \<lceil>0.7*n + 3\<rceil>) + 19 * n + 54"
using \<open>m \<le> n\<close> and False by (intro add_mono less.IH; linarith)
also have "\<dots> = T'_mom_select n"
using \<open>m \<le> n\<close> and False by (subst T'_mom_select.simps) auto
@@ -754,7 +780,10 @@
qed
qed
-lemma T_mom_select_le_aux: "T_mom_select k xs \<le> T'_mom_select (length xs)"
+lemma T_mom_select_le_aux:
+ assumes "k < length xs"
+ shows "T_mom_select k xs \<le> T'_mom_select (length xs)"
+ using assms
proof (induction k xs rule: T_mom_select.induct)
case (1 k xs)
define n where [simp]: "n = length xs"
@@ -771,11 +800,12 @@
show ?case
proof (cases "length xs \<le> 20")
case True \<comment> \<open>base case\<close>
- hence "T_mom_select k xs \<le> (length xs)\<^sup>2 + 4 * length xs + 3"
- using T_slow_select_le[of k xs] by (subst T_mom_select.simps) (auto simp: T_length_eq)
- also have "\<dots> \<le> 20\<^sup>2 + 4 * 20 + 3"
+ hence "T_mom_select k xs \<le> (length xs)\<^sup>2 + 4 * length xs + 2"
+ using T_slow_select_le[of k xs] \<open>k < length xs\<close>
+ by (subst T_mom_select.simps) (auto simp: T_length_eq)
+ also have "\<dots> \<le> 20\<^sup>2 + 4 * 20 + 2"
using True by (intro add_mono power_mono) auto
- also have "\<dots> = 483"
+ also have "\<dots> = 482"
by simp
also have "\<dots> = T'_mom_select (length xs)"
using True by (simp add: T'_mom_select.simps)
@@ -794,34 +824,36 @@
text \<open>The cost of computing the medians of all the subgroups:\<close>
define T_ms where "T_ms = T_map T_slow_median (chop 5 xs)"
- have "T_ms \<le> 10 * n + 49"
+ have "T_ms \<le> 10 * n + 48"
proof -
have "T_ms = (\<Sum>ys\<leftarrow>chop 5 xs. T_slow_median ys) + length (chop 5 xs) + 1"
by (simp add: T_ms_def T_map_eq)
- also have "(\<Sum>ys\<leftarrow>chop 5 xs. T_slow_median ys) \<le> (\<Sum>ys\<leftarrow>chop 5 xs. 48)"
+ also have "(\<Sum>ys\<leftarrow>chop 5 xs. T_slow_median ys) \<le> (\<Sum>ys\<leftarrow>chop 5 xs. 47)"
proof (intro sum_list_mono)
fix ys assume "ys \<in> set (chop 5 xs)"
- hence "length ys \<le> 5"
- using length_chop_part_le by blast
- have "T_slow_median ys \<le> (length ys) ^ 2 + 4 * length ys + 3"
+ hence "length ys \<le> 5" "ys \<noteq> []"
+ using length_chop_part_le[of ys 5 xs] by auto
+ from \<open>ys \<noteq> []\<close> have "T_slow_median ys \<le> (length ys) ^ 2 + 4 * length ys + 2"
by (rule T_slow_median_le)
- also have "\<dots> \<le> 5 ^ 2 + 4 * 5 + 3"
+ also have "\<dots> \<le> 5 ^ 2 + 4 * 5 + 2"
using \<open>length ys \<le> 5\<close> by (intro add_mono power_mono) auto
- finally show "T_slow_median ys \<le> 48" by simp
+ finally show "T_slow_median ys \<le> 47" by simp
qed
- also have "(\<Sum>ys\<leftarrow>chop 5 xs. 48) + length (chop 5 xs) + 1 =
- 49 * nat \<lceil>real n / 5\<rceil> + 1"
+ also have "(\<Sum>ys\<leftarrow>chop 5 xs. 47) + length (chop 5 xs) + 1 =
+ 48 * nat \<lceil>real n / 5\<rceil> + 1"
by (simp add: map_replicate_const length_chop)
- also have "\<dots> \<le> 10 * n + 49"
+ also have "\<dots> \<le> 10 * n + 48"
by linarith
- finally show "T_ms \<le> 10 * n + 49" by simp
+ finally show "T_ms \<le> 10 * n + 48" by simp
qed
text \<open>The cost of the first recursive call (to compute the median of medians):\<close>
define T_rec1 where
"T_rec1 = T_mom_select (((length xs + 4) div 5 - 1) div 2) (map slow_median (chop 5 xs))"
- have "T_rec1 \<le> T'_mom_select (length (map slow_median (chop 5 xs)))"
- using False unfolding T_rec1_def by (intro IH(3)) auto
+ from False have "((length xs + 4) div 5 - Suc 0) div 2 < nat \<lceil>real (length xs) / 5\<rceil>"
+ by linarith
+ hence "T_rec1 \<le> T'_mom_select (length (map slow_median (chop 5 xs)))"
+ using False unfolding T_rec1_def by (intro IH(3)) (auto simp: length_chop)
hence "T_rec1 \<le> T'_mom_select (nat \<lceil>0.2 * n\<rceil>)"
by (simp add: length_chop)
@@ -855,7 +887,17 @@
hence "T_rec2 = T_mom_select (k - nl - ne) gs"
by (simp add: T_rec2_def)
also have "\<dots> \<le> T'_mom_select (length gs)"
- unfolding nl_def ne_def by (rule IH(2)) (use \<open>k \<ge> nl + ne\<close> False in \<open>auto simp: defs\<close>)
+ unfolding nl_def ne_def
+ proof (rule IH(2))
+ show "\<not> length xs \<le> 20"
+ using False by auto
+ show "\<not> k < length ls" "\<not>k < length ls + length es"
+ using \<open>k \<ge> nl + ne\<close> by (auto simp: nl_def ne_def)
+ have "length xs = nl + ne + length gs"
+ unfolding defs by (rule length_partition3) (simp_all add: partition3_def)
+ thus "k - length ls - length es < length gs"
+ using \<open>k \<ge> nl + ne\<close> \<open>k < length xs\<close> by (auto simp: nl_def ne_def)
+ qed
also have "length gs \<le> nat \<lceil>0.7 * n + 3\<rceil>"
unfolding gs_def using size_greater_than_median_of_medians[of xs]
by (auto simp: length_filter_conv_size_filter_mset slow_median_correct[abs_def] x_eq)
@@ -871,13 +913,13 @@
T_length_eq T_ms_def)
also have "nl \<le> n" by (simp add: nl_def ls_def)
also have "ne \<le> n" by (simp add: ne_def es_def)
- also note \<open>T_ms \<le> 10 * n + 49\<close>
+ also note \<open>T_ms \<le> 10 * n + 48\<close>
also have "T_chop 5 xs \<le> 5 * n + 1"
using T_chop_le[of 5 xs] by simp
also note \<open>T_rec1 \<le> T'_mom_select (nat \<lceil>0.2*n\<rceil>)\<close>
also note \<open>T_rec2 \<le> T'_mom_select (nat \<lceil>0.7*n + 3\<rceil>)\<close>
finally have "T_mom_select k xs \<le>
- T'_mom_select (nat \<lceil>0.7*n + 3\<rceil>) + T'_mom_select (nat \<lceil>0.2*n\<rceil>) + 19 * n + 55"
+ T'_mom_select (nat \<lceil>0.7*n + 3\<rceil>) + T'_mom_select (nat \<lceil>0.2*n\<rceil>) + 19 * n + 54"
by simp
also have "\<dots> = T'_mom_select n"
using False by (subst T'_mom_select.simps) auto
@@ -1034,7 +1076,7 @@
lemma T'_mom_select_le': "\<exists>C\<^sub>1 C\<^sub>2. \<forall>n. T'_mom_select n \<le> C\<^sub>1 * n + C\<^sub>2"
proof (rule akra_bazzi_light_nat)
show "\<forall>n>20. T'_mom_select n = T'_mom_select (nat \<lceil>0.2 * n + 0\<rceil>) +
- T'_mom_select (nat \<lceil>0.7 * n + 3\<rceil>) + 19 * n + 55"
+ T'_mom_select (nat \<lceil>0.7 * n + 3\<rceil>) + 19 * n + 54"
using T'_mom_select.simps by auto
qed auto
--- a/src/HOL/Data_Structures/Time_Funs.thy Wed Apr 17 22:07:07 2024 +0100
+++ b/src/HOL/Data_Structures/Time_Funs.thy Wed Apr 17 22:07:21 2024 +0100
@@ -43,12 +43,9 @@
lemmas [simp del] = T_filter.simps
+time_fun nth
-fun T_nth :: "'a list \<Rightarrow> nat \<Rightarrow> nat" where
- "T_nth [] n = 1"
-| "T_nth (x # xs) n = (case n of 0 \<Rightarrow> 1 | Suc n' \<Rightarrow> T_nth xs n' + 1)"
-
-lemma T_nth_eq: "T_nth xs n = min n (length xs) + 1"
+lemma T_nth_eq: "n < length xs \<Longrightarrow> T_nth xs n = n + 1"
by (induction xs n rule: T_nth.induct) (auto split: nat.splits)
lemmas [simp del] = T_nth.simps
--- a/src/HOL/Library/adhoc_overloading.ML Wed Apr 17 22:07:07 2024 +0100
+++ b/src/HOL/Library/adhoc_overloading.ML Wed Apr 17 22:07:21 2024 +0100
@@ -154,7 +154,9 @@
fun get_candidates ctxt (c, T) =
get_variants ctxt c
|> Option.map (map_filter (fn (t, T') =>
- if unifiable_with (Proof_Context.theory_of ctxt) T T' then SOME t
+ if unifiable_with (Proof_Context.theory_of ctxt) T T'
+ (*keep the type constraint for the type-inference check phase*)
+ then SOME (Type.constraint T t)
else NONE));
fun insert_variants ctxt t (oconst as Const (c, T)) =
--- a/src/Pure/Build/build.scala Wed Apr 17 22:07:07 2024 +0100
+++ b/src/Pure/Build/build.scala Wed Apr 17 22:07:21 2024 +0100
@@ -34,8 +34,9 @@
ml_platform: String = Isabelle_System.getenv("ML_PLATFORM"),
hostname: String = Isabelle_System.hostname(),
numa_shuffling: Boolean = false,
+ numa_nodes: List[Int] = Nil,
clean_sessions: List[String] = Nil,
- build_heap: Boolean = false,
+ store_heap: Boolean = false,
fresh_build: Boolean = false,
no_build: Boolean = false,
session_setup: (String, Session) => Unit = (_, _) => (),
@@ -78,10 +79,11 @@
def cache: Term.Cache = store.cache
def sessions_ok: List[String] =
- (for {
- name <- deps.sessions_structure.build_topological_order.iterator
- result <- results.get(name) if result.ok
- } yield name).toList
+ List.from(
+ for {
+ name <- deps.sessions_structure.build_topological_order.iterator
+ result <- results.get(name) if result.ok
+ } yield name)
def info(name: String): Sessions.Info = deps.sessions_structure(name)
def sessions: Set[String] = results.keySet
@@ -208,11 +210,9 @@
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
- }
+ val sources_shasum = deps0.sources_shasum(name)
+ val thorough = deps0.sessions_structure(name).build_thorough
+ if (Sessions.eq_sources(thorough, build.sources, sources_shasum)) None
else Some(name)
case _ => Some(name)
}
@@ -230,10 +230,11 @@
if (check_unknown_files) {
val source_files =
- (for {
- (_, base) <- build_deps.session_bases.iterator
- (path, _) <- base.session_sources.iterator
- } yield path).toList
+ List.from(
+ for {
+ (_, base) <- build_deps.session_bases.iterator
+ (path, _) <- base.session_sources.iterator
+ } yield path)
Mercurial.check_files(source_files)._2 match {
case Nil =>
case unknown_files =>
@@ -249,12 +250,13 @@
val clean_sessions =
if (clean_build) full_sessions.imports_descendants(full_sessions_selection) else Nil
+ val numa_nodes = Host.numa_nodes(enabled = numa_shuffling)
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,
+ clean_sessions = clean_sessions, store_heap = build_heap,
+ numa_shuffling = numa_shuffling, numa_nodes = numa_nodes,
+ 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)
--- a/src/Pure/Build/build_benchmark.scala Wed Apr 17 22:07:07 2024 +0100
+++ b/src/Pure/Build/build_benchmark.scala Wed Apr 17 22:07:21 2024 +0100
@@ -65,21 +65,11 @@
benchmark_requirements(local_options, progress)
for (db <- database_server) ML_Heap.restore(db, hierachy, cache = store.cache.compress)
- def get_shasum(session_name: String): SHA1.Shasum = {
- val ancestor_shasums = sessions(session_name).ancestors.map(get_shasum)
-
- val input_shasum =
- if (ancestor_shasums.isEmpty) ML_Process.bootstrap_shasum()
- else SHA1.flat_shasum(ancestor_shasums)
-
- store.check_output(
- database_server, session_name,
- session_options = build_context.sessions_structure(session_name).options,
- sources_shasum = sessions(session_name).sources_shasum,
- input_shasum = input_shasum,
- fresh_build = false,
- store_heap = false)._2
- }
+ def get_shasum(name: String): SHA1.Shasum =
+ store.check_output(database_server, name,
+ sources_shasum = sessions(name).sources_shasum,
+ input_shasum = ML_Process.make_shasum(sessions(name).ancestors.map(get_shasum)),
+ build_thorough = build_context.sessions_structure(name).build_thorough)._2
val deps = Sessions.deps(full_sessions.selection(selection)).check_errors
val background = deps.background(benchmark_session_name)
--- a/src/Pure/Build/build_job.scala Wed Apr 17 22:07:07 2024 +0100
+++ b/src/Pure/Build/build_job.scala Wed Apr 17 22:07:21 2024 +0100
@@ -514,14 +514,8 @@
case None => using(store.open_database(session_name, output = true))(write_info)
}
- using_optional(store.maybe_open_heaps_database(database_server, server = server)) {
- heaps_database =>
- for (db <- database_server orElse heaps_database) {
- val slice = Space.MiB(options.real("build_database_slice"))
- ML_Heap.store(db, store_session, slice,
- cache = store.cache.compress, progress = progress)
- }
- }
+ store.in_heaps_database(
+ List(store_session), database_server, server = server, progress = progress)
// messages
process_result.err_lines.foreach(progress.echo(_))
--- a/src/Pure/Build/build_process.scala Wed Apr 17 22:07:07 2024 +0100
+++ b/src/Pure/Build/build_process.scala Wed Apr 17 22:07:21 2024 +0100
@@ -94,6 +94,9 @@
def iterator: Iterator[Build_Job.Session_Context] =
for (name <- graph.topological_order.iterator) yield apply(name)
+ def store_heap(name: String): Boolean =
+ isabelle.Sessions.is_pure(name) || iterator.exists(_.ancestors.contains(name))
+
def data: Library.Update.Data[Build_Job.Session_Context] =
Map.from(for ((_, (session, _)) <- graph.iterator) yield session.name -> session)
@@ -221,7 +224,6 @@
sealed case class State(
serial: Long = 0,
- numa_nodes: List[Int] = Nil,
sessions: Sessions = Sessions.empty,
pending: State.Pending = Map.empty,
running: State.Running = Map.empty,
@@ -1148,9 +1150,10 @@
}
protected def next_node_info(state: Build_Process.State, session_name: String): Host.Node_Info = {
- def used_nodes: Set[Int] =
+ val available_nodes = build_context.numa_nodes
+ val used_nodes =
Set.from(for (job <- state.running.valuesIterator; i <- job.node_info.numa_node) yield i)
- val numa_node = Host.next_numa_node(_host_database, hostname, state.numa_nodes, used_nodes)
+ val numa_node = Host.next_numa_node(_host_database, hostname, available_nodes, used_nodes)
Host.Node_Info(hostname, numa_node, Nil)
}
@@ -1160,20 +1163,13 @@
ancestor_results: List[Build_Process.Result]
): Build_Process.State = {
val sources_shasum = state.sessions(session_name).sources_shasum
-
- val input_shasum =
- if (ancestor_results.isEmpty) ML_Process.bootstrap_shasum()
- else SHA1.flat_shasum(ancestor_results.map(_.output_shasum))
-
- val store_heap =
- build_context.build_heap || Sessions.is_pure(session_name) ||
- state.sessions.iterator.exists(_.ancestors.contains(session_name))
-
+ val input_shasum = ML_Process.make_shasum(ancestor_results.map(_.output_shasum))
+ val store_heap = build_context.store_heap || state.sessions.store_heap(session_name)
val (current, output_shasum) =
store.check_output(_database_server, session_name,
- session_options = build_context.sessions_structure(session_name).options,
sources_shasum = sources_shasum,
input_shasum = input_shasum,
+ build_thorough = build_context.sessions_structure(session_name).build_thorough,
fresh_build = build_context.fresh_build,
store_heap = store_heap)
@@ -1302,7 +1298,7 @@
finished || sleep
}
- protected def init_unsynchronized(): Unit = {
+ protected def init_unsynchronized(): Unit =
if (build_context.master) {
val sessions1 =
_state.sessions.init(build_context, _database_server, progress = build_progress)
@@ -1315,10 +1311,6 @@
_state = _state.copy(sessions = sessions1, pending = pending1)
}
- val numa_nodes = Host.numa_nodes(enabled = build_context.numa_shuffling)
- _state = _state.copy(numa_nodes = numa_nodes)
- }
-
protected def main_unsynchronized(): Unit = {
for (job <- _state.running.valuesIterator; build <- job.build if build.is_finished) {
val result = build.join
--- a/src/Pure/Build/build_schedule.scala Wed Apr 17 22:07:07 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala Wed Apr 17 22:07:21 2024 +0100
@@ -471,8 +471,9 @@
if (used.length >= host.max_jobs) false
else {
- if (host.numa_nodes.length <= 1)
+ if (host.numa_nodes.length <= 1) {
used.map(host_infos.num_threads).sum + threads <= host.max_threads
+ }
else {
def node_threads(n: Int): Int =
used.filter(_.numa_node.contains(n)).map(host_infos.num_threads).sum
@@ -1117,23 +1118,13 @@
def is_current(state: Build_Process.State, session_name: String): Boolean =
state.ancestor_results(session_name) match {
case Some(ancestor_results) if ancestor_results.forall(_.current) =>
- val sources_shasum = state.sessions(session_name).sources_shasum
-
- val input_shasum =
- if (ancestor_results.isEmpty) ML_Process.bootstrap_shasum()
- else SHA1.flat_shasum(ancestor_results.map(_.output_shasum))
-
- val store_heap =
- build_context.build_heap || Sessions.is_pure(session_name) ||
- state.sessions.iterator.exists(_.ancestors.contains(session_name))
-
store.check_output(
_database_server, session_name,
- session_options = build_context.sessions_structure(session_name).options,
- sources_shasum = sources_shasum,
- input_shasum = input_shasum,
+ sources_shasum = state.sessions(session_name).sources_shasum,
+ input_shasum = ML_Process.make_shasum(ancestor_results.map(_.output_shasum)),
+ build_thorough = build_context.sessions_structure(session_name).build_thorough,
fresh_build = build_context.fresh_build,
- store_heap = store_heap)._1
+ store_heap = build_context.store_heap || state.sessions.store_heap(session_name))._1
case _ => false
}
--- a/src/Pure/Build/sessions.scala Wed Apr 17 22:07:07 2024 +0100
+++ b/src/Pure/Build/sessions.scala Wed Apr 17 22:07:21 2024 +0100
@@ -577,8 +577,8 @@
}
}
- def eq_sources(options: Options, shasum1: SHA1.Shasum, shasum2: SHA1.Shasum): Boolean =
- if (options.bool("build_thorough")) shasum1 == shasum2
+ def eq_sources(thorough: Boolean, shasum1: SHA1.Shasum, shasum2: SHA1.Shasum): Boolean =
+ if (thorough) shasum1 == shasum2
else {
def trim(shasum: SHA1.Shasum): SHA1.Shasum =
shasum.filter(s => !is_build_prefs(s))
@@ -721,6 +721,8 @@
def main_group: Boolean = groups.contains("main")
def doc_group: Boolean = groups.contains("doc")
+ def build_thorough: Boolean = options.bool("build_thorough")
+
def timeout_ignored: Boolean =
!options.bool("timeout_build") || Time.seconds(options.real("timeout")) < Time.ms(1)
--- a/src/Pure/Build/store.scala Wed Apr 17 22:07:07 2024 +0100
+++ b/src/Pure/Build/store.scala Wed Apr 17 22:07:21 2024 +0100
@@ -83,7 +83,7 @@
new Sources(
session_base.session_sources.foldLeft(Map.empty) {
case (sources, (path, digest)) =>
- def err(): Nothing = error("Incoherent digest for source file: " + path)
+ def err(): Nothing = error("Incoherent digest for source file: " + path.expand)
val name = File.symbolic_path(path)
sources.get(name) match {
case Some(source_file) =>
@@ -383,7 +383,30 @@
server: SSH.Server = SSH.no_server
): Option[SQL.Database] = {
if (database_server.isDefined) None
- else store.maybe_open_database_server(server = server, guard = build_cluster)
+ else maybe_open_database_server(server = server, guard = build_cluster)
+ }
+
+ def maybe_using_heaps_database[A](
+ database_server: Option[SQL.Database],
+ server: SSH.Server = SSH.no_server
+ )(f: SQL.Database => A): Option[A] = {
+ using_optional(maybe_open_heaps_database(database_server, server = server)) {
+ heaps_database => (database_server orElse heaps_database).map(f)
+ }
+ }
+
+ def in_heaps_database(
+ sessions: List[Store.Session],
+ database_server: Option[SQL.Database],
+ server: SSH.Server = SSH.no_server,
+ progress: Progress = new Progress
+ ): Unit = {
+ if (sessions.nonEmpty) {
+ maybe_using_heaps_database(database_server, server = server) { db =>
+ val slice = Space.MiB(options.real("build_database_slice"))
+ sessions.foreach(ML_Heap.store(db, _, slice, cache = cache.compress, progress = progress))
+ }
+ }
}
def open_build_database(path: Path, server: SSH.Server = SSH.no_server): SQL.Database =
@@ -462,11 +485,11 @@
def check_output(
database_server: Option[SQL.Database],
name: String,
- session_options: Options,
sources_shasum: SHA1.Shasum,
input_shasum: SHA1.Shasum,
- fresh_build: Boolean,
- store_heap: Boolean
+ build_thorough: Boolean = false,
+ fresh_build: Boolean = false,
+ store_heap: Boolean = false
): (Boolean, SHA1.Shasum) = {
def no_check: (Boolean, SHA1.Shasum) = (false, SHA1.no_shasum)
@@ -477,7 +500,7 @@
val current =
!fresh_build &&
build.ok &&
- Sessions.eq_sources(session_options, build.sources, sources_shasum) &&
+ Sessions.eq_sources(build_thorough, build.sources, sources_shasum) &&
build.input_heaps == input_shasum &&
build.output_heap == output_shasum &&
!(store_heap && output_shasum.is_empty)
--- a/src/Pure/ML/ml_heap.scala Wed Apr 17 22:07:07 2024 +0100
+++ b/src/Pure/ML/ml_heap.scala Wed Apr 17 22:07:21 2024 +0100
@@ -11,16 +11,14 @@
/** heap file with SHA1 digest **/
private val sha1_prefix = "SHA1:"
+ private val sha1_length = sha1_prefix.length + SHA1.digest_length
def read_file_digest(heap: Path): Option[SHA1.Digest] = {
if (heap.is_file) {
- val l = sha1_prefix.length
- val m = l + SHA1.digest_length
- val n = File.size(heap)
- val bs = Bytes.read_file(heap, offset = n - m)
- if (bs.length == m) {
+ val bs = Bytes.read_file(heap, offset = File.size(heap) - sha1_length)
+ if (bs.length == sha1_length) {
val s = bs.text
- if (s.startsWith(sha1_prefix)) Some(SHA1.fake_digest(s.substring(l)))
+ if (s.startsWith(sha1_prefix)) Some(SHA1.fake_digest(s.substring(sha1_prefix.length)))
else None
}
else None
@@ -204,7 +202,7 @@
val heap_digest = session.heap.map(write_file_digest)
val heap_size =
session.heap match {
- case Some(heap) => File.size(heap) - sha1_prefix.length - SHA1.digest_length
+ case Some(heap) => File.size(heap) - sha1_length
case None => 0L
}
@@ -285,16 +283,13 @@
val base_dir = Isabelle_System.make_directory(heap.expand.dir)
Isabelle_System.with_tmp_file(session_name + "_", base_dir = base_dir.file) { tmp =>
- Bytes.write(tmp, Bytes.empty)
+ tmp.file.delete()
for (slice <- private_data.read_slices(db, session_name)) {
Bytes.append(tmp, slice.uncompress(cache = cache))
}
val digest = write_file_digest(tmp)
- if (db_digest.get == digest) {
- Isabelle_System.chmod("a+r", tmp)
- Isabelle_System.move_file(tmp, heap)
- }
- else error("Incoherent content for session heap " + heap)
+ if (db_digest.get == digest) Isabelle_System.move_file(tmp, heap)
+ else error("Incoherent content for session heap " + heap.expand)
}
}
}
@@ -303,14 +298,14 @@
/* log_db */
for (session <- sessions; path <- session.log_db) {
- val file_uuid = Store.read_build_uuid(path, session.name)
- private_data.read_log_db(db, session.name, old_uuid = file_uuid) match {
- case Some(log_db) if file_uuid.isEmpty =>
+ val old_uuid = Store.read_build_uuid(path, session.name)
+ for (log_db <- private_data.read_log_db(db, session.name, old_uuid = old_uuid)) {
+ if (old_uuid.isEmpty) {
progress.echo("Restoring " + session.log_db_name + " ...")
Isabelle_System.make_directory(path.expand.dir)
Bytes.write(path, log_db.content)
- case Some(_) => error("Incoherent content for session database " + path)
- case None =>
+ }
+ else error("Incoherent content for session database " + path.expand)
}
}
}
--- a/src/Pure/ML/ml_process.scala Wed Apr 17 22:07:07 2024 +0100
+++ b/src/Pure/ML/ml_process.scala Wed Apr 17 22:07:21 2024 +0100
@@ -12,8 +12,9 @@
object ML_Process {
- def bootstrap_shasum(): SHA1.Shasum =
- SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE")))
+ def make_shasum(ancestors: List[SHA1.Shasum]): SHA1.Shasum =
+ if (ancestors.isEmpty) SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE")))
+ else SHA1.flat_shasum(ancestors)
def session_heaps(
store: Store,
--- a/src/Pure/Tools/update.scala Wed Apr 17 22:07:07 2024 +0100
+++ b/src/Pure/Tools/update.scala Wed Apr 17 22:07:21 2024 +0100
@@ -217,13 +217,13 @@
sessions = sessions),
base_logics = base_logics,
progress = progress,
- build_heap,
- clean_build,
+ build_heap = build_heap,
+ clean_build = clean_build,
dirs = dirs,
select_dirs = select_dirs,
numa_shuffling = Host.numa_check(progress, numa_shuffling),
max_jobs = max_jobs,
- fresh_build,
+ fresh_build = fresh_build,
no_build = no_build)
}