--- a/NEWS Wed Jan 22 22:22:27 2025 +0000
+++ b/NEWS Wed Jan 22 22:22:37 2025 +0000
@@ -361,7 +361,7 @@
isabelle find_facts_index HOL
isabelle find_facts_server
- open http://localhost:8080/app#search?q=Hilbert
+ open http://localhost:8080/find_facts#search?q=Hilbert
Persistent data is stored in $ISABELLE_HOME_USER/find_facts/.
--- a/src/HOL/Bit_Operations.thy Wed Jan 22 22:22:27 2025 +0000
+++ b/src/HOL/Bit_Operations.thy Wed Jan 22 22:22:37 2025 +0000
@@ -132,6 +132,17 @@
using div_mult_mod_eq [of \<open>1 + a\<close> \<open>2 ^ n\<close>] div_mult_mod_eq [of a \<open>2 ^ n\<close>] that
by simp (metis (full_types) add.left_commute add_left_imp_eq)
+lemma half_numeral_Bit1_eq [simp]:
+ \<open>numeral (num.Bit1 m) div 2 = numeral (num.Bit0 m) div 2\<close>
+ using even_half_succ_eq [of \<open>2 * numeral m\<close>]
+ by simp
+
+lemma double_half_numeral_Bit_0_eq [simp]:
+ \<open>2 * (numeral (num.Bit0 m) div 2) = numeral (num.Bit0 m)\<close>
+ \<open>(numeral (num.Bit0 m) div 2) * 2 = numeral (num.Bit0 m)\<close>
+ using mod_mult_div_eq [of \<open>numeral (Num.Bit0 m)\<close> 2]
+ by (simp_all add: mod2_eq_if ac_simps)
+
named_theorems bit_simps \<open>Simplification rules for \<^const>\<open>bit\<close>\<close>
definition possible_bit :: \<open>'a itself \<Rightarrow> nat \<Rightarrow> bool\<close>
@@ -1195,7 +1206,7 @@
by (cases n) (auto simp: bit_0 bit_double_iff even_bit_succ_iff)
qed
-lemma set_bit_0 [simp]:
+lemma set_bit_0:
\<open>set_bit 0 a = 1 + 2 * (a div 2)\<close>
by (auto simp: bit_eq_iff bit_simps even_bit_succ_iff simp flip: bit_Suc)
@@ -1204,7 +1215,7 @@
by (auto simp: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc
elim: possible_bit_less_imp)
-lemma unset_bit_0 [simp]:
+lemma unset_bit_0:
\<open>unset_bit 0 a = 2 * (a div 2)\<close>
by (auto simp: bit_eq_iff bit_simps simp flip: bit_Suc)
@@ -1212,7 +1223,7 @@
\<open>unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\<close>
by (auto simp: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc)
-lemma flip_bit_0 [simp]:
+lemma flip_bit_0:
\<open>flip_bit 0 a = of_bool (even a) + 2 * (a div 2)\<close>
by (auto simp: bit_eq_iff bit_simps even_bit_succ_iff bit_0 simp flip: bit_Suc)
@@ -1557,7 +1568,7 @@
lemma drop_bit_Suc_bit1 [simp]:
\<open>drop_bit (Suc n) (numeral (Num.Bit1 k)) = drop_bit n (numeral k)\<close>
- by (simp add: drop_bit_Suc numeral_Bit1_div_2)
+ by (simp add: drop_bit_Suc numeral_Bit0_div_2)
lemma drop_bit_numeral_bit0 [simp]:
\<open>drop_bit (numeral l) (numeral (Num.Bit0 k)) = drop_bit (pred_numeral l) (numeral k)\<close>
@@ -1565,7 +1576,7 @@
lemma drop_bit_numeral_bit1 [simp]:
\<open>drop_bit (numeral l) (numeral (Num.Bit1 k)) = drop_bit (pred_numeral l) (numeral k)\<close>
- by (simp add: drop_bit_rec numeral_Bit1_div_2)
+ by (simp add: drop_bit_rec numeral_Bit0_div_2)
lemma take_bit_Suc_1 [simp]:
\<open>take_bit (Suc n) 1 = 1\<close>
@@ -1577,7 +1588,7 @@
lemma take_bit_Suc_bit1:
\<open>take_bit (Suc n) (numeral (Num.Bit1 k)) = take_bit n (numeral k) * 2 + 1\<close>
- by (simp add: take_bit_Suc numeral_Bit1_div_2 mod_2_eq_odd)
+ by (simp add: take_bit_Suc numeral_Bit0_div_2 mod_2_eq_odd)
lemma take_bit_numeral_1 [simp]:
\<open>take_bit (numeral l) 1 = 1\<close>
@@ -1589,7 +1600,7 @@
lemma take_bit_numeral_bit1:
\<open>take_bit (numeral l) (numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (numeral k) * 2 + 1\<close>
- by (simp add: take_bit_rec numeral_Bit1_div_2 mod_2_eq_odd)
+ by (simp add: take_bit_rec numeral_Bit0_div_2 mod_2_eq_odd)
lemma bit_of_nat_iff_bit [bit_simps]:
\<open>bit (of_nat m) n \<longleftrightarrow> bit m n\<close>
@@ -2600,7 +2611,7 @@
lemma [code]:
\<open>unset_bit 0 m = 2 * (m div 2)\<close>
\<open>unset_bit (Suc n) m = m mod 2 + 2 * unset_bit n (m div 2)\<close> for m n :: nat
- by (simp_all add: unset_bit_Suc)
+ by (simp_all add: unset_bit_0 unset_bit_Suc)
lemma push_bit_of_Suc_0 [simp]:
\<open>push_bit n (Suc 0) = 2 ^ n\<close>
@@ -2778,7 +2789,7 @@
lemma bit_numeral_Bit1_Suc_iff [simp]:
\<open>bit (numeral (Num.Bit1 m)) (Suc n) \<longleftrightarrow> bit (numeral m) n\<close>
- by (simp add: bit_Suc numeral_Bit1_div_2)
+ by (simp add: bit_Suc numeral_Bit0_div_2)
lemma bit_numeral_rec:
\<open>bit (numeral (Num.Bit0 w)) n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc m \<Rightarrow> bit (numeral w) m)\<close>
@@ -3278,6 +3289,86 @@
end
+context semiring_bit_operations
+begin
+
+lemma push_bit_eq_pow:
+ \<open>push_bit (numeral n) 1 = numeral (Num.pow (Num.Bit0 Num.One) n)\<close>
+ by simp
+
+lemma set_bit_of_0 [simp]:
+ \<open>set_bit n 0 = 2 ^ n\<close>
+ by (simp add: set_bit_eq_or)
+
+lemma unset_bit_of_0 [simp]:
+ \<open>unset_bit n 0 = 0\<close>
+ by (simp add: unset_bit_eq_or_xor)
+
+lemma flip_bit_of_0 [simp]:
+ \<open>flip_bit n 0 = 2 ^ n\<close>
+ by (simp add: flip_bit_eq_xor)
+
+lemma set_bit_0_numeral_eq [simp]:
+ \<open>set_bit 0 (numeral Num.One) = 1\<close>
+ \<open>set_bit 0 (numeral (Num.Bit0 m)) = numeral (Num.Bit1 m)\<close>
+ \<open>set_bit 0 (numeral (Num.Bit1 m)) = numeral (Num.Bit1 m)\<close>
+ by (simp_all add: set_bit_0)
+
+lemma set_bit_numeral_eq_or [simp]:
+ \<open>set_bit (numeral n) (numeral m) = numeral m OR push_bit (numeral n) 1\<close>
+ by (fact set_bit_eq_or)
+
+lemma unset_bit_0_numeral_eq_and_not' [simp]:
+ \<open>unset_bit 0 (numeral Num.One) = 0\<close>
+ \<open>unset_bit 0 (numeral (Num.Bit0 m)) = numeral (Num.Bit0 m)\<close>
+ \<open>unset_bit 0 (numeral (Num.Bit1 m)) = numeral (Num.Bit0 m)\<close>
+ by (simp_all add: unset_bit_0)
+
+lemma unset_bit_numeral_eq_or [simp]:
+ \<open>unset_bit (numeral n) (numeral m) =
+ (case and_not_num m (Num.pow (Num.Bit0 Num.One) n)
+ of None \<Rightarrow> 0
+ | Some q \<Rightarrow> numeral q)\<close> (is \<open>?lhs = _\<close>)
+proof -
+ have \<open>?lhs = of_nat (unset_bit (numeral n) (numeral m))\<close>
+ by (simp add: of_nat_unset_bit_eq)
+ also have \<open>unset_bit (numeral n) (numeral m) = nat (unset_bit (numeral n) (numeral m))\<close>
+ by (simp flip: int_int_eq add: Bit_Operations.of_nat_unset_bit_eq)
+ finally have *: \<open>?lhs = of_nat (nat (unset_bit (numeral n) (numeral m)))\<close> .
+ show ?thesis
+ by (simp only: * unset_bit_eq_and_not Bit_Operations.push_bit_eq_pow int_numeral_and_not_num)
+ (auto split: option.splits)
+qed
+
+lemma flip_bit_0_numeral_eq_or [simp]:
+ \<open>flip_bit 0 (numeral Num.One) = 0\<close>
+ \<open>flip_bit 0 (numeral (Num.Bit0 m)) = numeral (Num.Bit1 m)\<close>
+ \<open>flip_bit 0 (numeral (Num.Bit1 m)) = numeral (Num.Bit0 m)\<close>
+ by (simp_all add: flip_bit_0)
+
+lemma flip_bit_numeral_eq_xor [simp]:
+ \<open>flip_bit (numeral n) (numeral m) = numeral m XOR push_bit (numeral n) 1\<close>
+ by (fact flip_bit_eq_xor)
+
+end
+
+context ring_bit_operations
+begin
+
+lemma set_bit_minus_numeral_eq_or [simp]:
+ \<open>set_bit (numeral n) (- numeral m) = - numeral m OR push_bit (numeral n) 1\<close>
+ by (fact set_bit_eq_or)
+
+lemma unset_bit_minus_numeral_eq_and_not [simp]:
+ \<open>unset_bit (numeral n) (- numeral m) = - numeral m AND NOT (push_bit (numeral n) 1)\<close>
+ by (fact unset_bit_eq_and_not)
+
+lemma flip_bit_minus_numeral_eq_xor [simp]:
+ \<open>flip_bit (numeral n) (- numeral m) = - numeral m XOR push_bit (numeral n) 1\<close>
+ by (fact flip_bit_eq_xor)
+
+end
+
lemma xor_int_code [code]:
fixes i j :: int shows
\<open>0 XOR j = j\<close>
--- a/src/HOL/List.thy Wed Jan 22 22:22:27 2025 +0000
+++ b/src/HOL/List.thy Wed Jan 22 22:22:37 2025 +0000
@@ -263,6 +263,15 @@
replicate_0: "replicate 0 x = []" |
replicate_Suc: "replicate (Suc n) x = x # replicate n x"
+overloading pow_list == "compow :: nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
+begin
+
+primrec pow_list :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"pow_list 0 xs = []" |
+"pow_list (Suc n) xs = xs @ pow_list n xs"
+
+end
+
text \<open>
Function \<open>size\<close> is overloaded for all datatypes. Users may
refer to the list version as \<open>length\<close>.\<close>
@@ -1168,7 +1177,7 @@
by(blast dest:map_injective)
lemma inj_mapI: "inj f \<Longrightarrow> inj (map f)"
-by (iprover dest: map_injective injD intro: inj_onI)
+by (rule list.inj_map)
lemma inj_mapD: "inj (map f) \<Longrightarrow> inj f"
by (metis (no_types, opaque_lifting) injI list.inject list.simps(9) the_inv_f_f)
@@ -1180,7 +1189,7 @@
by (blast intro:inj_onI dest:inj_onD map_inj_on)
lemma map_idI: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = x) \<Longrightarrow> map f xs = xs"
-by (induct xs, auto)
+by (rule list.map_ident_strong)
lemma map_fun_upd [simp]: "y \<notin> set xs \<Longrightarrow> map (f(y:=v)) xs = map f xs"
by (induct xs) auto
@@ -1218,6 +1227,9 @@
lemma rev_rev_ident [simp]: "rev (rev xs) = xs"
by (induct xs) auto
+lemma rev_involution[simp]: "rev \<circ> rev = id"
+by auto
+
lemma rev_swap: "(rev xs = ys) = (xs = rev ys)"
by auto
@@ -1284,6 +1296,21 @@
qed
qed simp
+lemma rev_induct2:
+ "\<lbrakk> P [] [];
+ \<And>x xs. P (xs @ [x]) [];
+ \<And>y ys. P [] (ys @ [y]);
+ \<And>x xs y ys. P xs ys \<Longrightarrow> P (xs @ [x]) (ys @ [y]) \<rbrakk>
+ \<Longrightarrow> P xs ys"
+proof (induct xs arbitrary: ys rule: rev_induct)
+ case Nil
+ then show ?case using rev_induct[of "P []"] by presburger
+next
+ case (snoc x xs)
+ hence "P xs ys'" for ys' by simp
+ then show ?case by (simp add: rev_induct snoc.prems(2,4))
+qed
+
lemma length_Suc_conv_rev: "(length xs = Suc n) = (\<exists>y ys. xs = ys @ [y] \<and> length ys = n)"
by (induct xs rule: rev_induct) auto
@@ -4404,6 +4431,10 @@
"\<lbrakk> inj_on f (set xs); x \<in> set xs \<rbrakk> \<Longrightarrow> count_list (map f xs) (f x) = count_list xs x"
by (induction xs) (simp, fastforce)
+lemma count_list_map_conv:
+assumes "inj f" shows "count_list (map f xs) (f x) = count_list xs x"
+by (induction xs) (simp_all add: inj_eq[OF assms])
+
lemma count_list_rev[simp]: "count_list (rev xs) x = count_list xs x"
by (induction xs) auto
@@ -4714,6 +4745,9 @@
"concat (replicate i []) = []"
by (induct i) (auto simp add: map_replicate_const)
+lemma concat_replicate_single[simp]: "concat (replicate m [a]) = replicate m a"
+by(induction m) auto
+
lemma replicate_empty[simp]: "(replicate n x = []) \<longleftrightarrow> n=0"
by (induct n) auto
@@ -4812,6 +4846,134 @@
by (subst foldr_fold [symmetric]) simp_all
+subsubsection \<open>\<^term>\<open>xs ^^ n\<close>\<close>
+
+context
+begin
+
+interpretation monoid_mult "[]" "append"
+ rewrites "power u n = u ^^ n"
+proof-
+ show "class.monoid_mult [] (@)"
+ by (unfold_locales, simp_all)
+ show "power.power [] (@) u n = u ^^ n"
+ by(induction n) (auto simp add: power.power.simps)
+qed
+
+\<comment> \<open>inherited power properties\<close>
+
+lemmas pow_list_zero = power.power_0 and
+ pow_list_one = power_Suc0_right and
+ pow_list_1 = power_one_right and
+ pow_list_Nil = power_one and
+ pow_list_2 = power2_eq_square and
+ pow_list_Suc = power_Suc and
+ pow_list_Suc2 = power_Suc2 and
+ pow_list_comm = power_commutes and
+ pow_list_add = power_add and
+ pow_list_eq_if = power_eq_if and
+ pow_list_mult = power_mult and
+ pow_list_commuting_commutes = power_commuting_commutes
+
+end
+
+lemma pow_list_alt: "xs^^n = concat (replicate n xs)"
+by (induct n) auto
+
+lemma pow_list_single: "[a] ^^ m = replicate m a"
+by(simp add: pow_list_alt)
+
+lemma length_pow_list_single [simp]: "length([a] ^^ n) = n"
+by (simp add: pow_list_single)
+
+lemma nth_pow_list_single: "i < m \<Longrightarrow> ([a] ^^ m) ! i = a"
+by (simp add: pow_list_single)
+
+lemma pow_list_not_NilD: "xs ^^ m \<noteq> [] \<Longrightarrow> 0 < m"
+by (cases m) auto
+
+lemma length_pow_list: "length(xs ^^ k) = k * length xs"
+by (induction k) simp+
+
+lemma pow_list_set: "set (w ^^ Suc k) = set w"
+by (induction k)(simp_all)
+
+lemma pow_list_slide: "xs @ (ys @ xs) ^^ n @ ys = (xs @ ys)^^(Suc n)"
+by (induction n) simp+
+
+lemma hd_pow_list: "0 < n \<Longrightarrow> hd(xs ^^ n) = hd xs"
+by(auto simp: pow_list_alt hd_append gr0_conv_Suc)
+
+lemma rev_pow_list: "rev (xs ^^ m) = (rev xs) ^^ m"
+by (induction m)(auto simp: pow_list_comm)
+
+lemma eq_pow_list_iff_eq_exp[simp]: assumes "xs \<noteq> []" shows "xs ^^ k = xs ^^ m \<longleftrightarrow> k = m"
+proof
+ assume "k = m" thus "xs ^^ k = xs ^^ m" by simp
+next
+ assume "xs ^^ k = xs ^^ m"
+ thus "k = m" using \<open>xs \<noteq> []\<close>[folded length_0_conv]
+ by (metis length_pow_list mult_cancel2)
+qed
+
+lemma pow_list_Nil_iff_0: "xs \<noteq> [] \<Longrightarrow> xs ^^ m = [] \<longleftrightarrow> m = 0"
+by (simp add: pow_list_eq_if)
+
+lemma pow_list_Nil_iff_Nil: "0 < m \<Longrightarrow> xs ^^ m = [] \<longleftrightarrow> xs = []"
+by (cases xs) (auto simp add: pow_list_Nil pow_list_Nil_iff_0)
+
+lemma pow_eq_eq:
+ assumes "xs ^^ k = ys ^^ k" and "0 < k"
+ shows "(xs::'a list) = ys"
+proof-
+ have "length xs = length ys"
+ using assms(1) length_pow_list by (metis nat_mult_eq_cancel1[OF \<open>0 < k\<close>])
+ thus ?thesis by (metis Suc_pred append_eq_append_conv assms(1,2) pow_list.simps(2))
+qed
+
+lemma map_pow_list[simp]: "map f (xs ^^ k) = (map f xs) ^^ k"
+by (induction k) simp_all
+
+lemma concat_pow_list: "concat (xs ^^ k) = (concat xs) ^^ k"
+by (induction k) simp_all
+
+lemma concat_pow_list_single[simp]: "concat ([a] ^^ k) = a ^^ k"
+by (simp add: pow_list_alt)
+
+lemma pow_list_single_Nil_iff: "[a] ^^ n = [] \<longleftrightarrow> n = 0"
+by (simp add: pow_list_single)
+
+lemma hd_pow_list_single: "k \<noteq> 0 \<Longrightarrow> hd ([a] ^^ k) = a"
+by (cases k) simp+
+
+lemma index_pow_mod: "i < length(xs ^^ k) \<Longrightarrow> (xs ^^ k)!i = xs!(i mod length xs)"
+proof(induction k)
+ have aux: "length(xs ^^ Suc l) = length(xs ^^ l) + length xs" for l
+ by simp
+ have aux1: "length (xs ^^ l) \<le> i \<Longrightarrow> i < length(xs ^^ l) + length xs \<Longrightarrow> i mod length xs = i - length(xs^^l)" for l
+ unfolding length_pow_list[of l xs]
+ using less_diff_conv2[of "l * length xs" i "length xs", unfolded add.commute[of "length xs" "l * length xs"]]
+ le_add_diff_inverse[of "l*length xs" i]
+ by (simp add: mod_nat_eqI)
+ case (Suc k)
+ show ?case
+ unfolding aux sym[OF pow_list_Suc2[symmetric]] nth_append le_mod_geq
+ using aux1[ OF _ Suc.prems[unfolded aux]]
+ Suc.IH pow_list_Suc2[symmetric] Suc.prems[unfolded aux] leI[of i "length(xs ^^ k)"] by presburger
+qed auto
+
+lemma unique_letter_word: assumes "\<And>c. c \<in> set w \<Longrightarrow> c = a" shows "w = [a] ^^ length w"
+ using assms proof (induction w)
+ case (Cons b w)
+ have "[a] ^^ length w = w" using Cons.IH[OF Cons.prems[OF list.set_intros(2)]]..
+ then show "b # w = [a] ^^ length(b # w)"
+ unfolding Cons.prems[OF list.set_intros(1)] by auto
+qed simp
+
+lemma count_list_pow_list: "count_list (w ^^ k) a = k * (count_list w a)"
+by (induction k) simp+
+
+
subsubsection \<open>\<^const>\<open>enumerate\<close>\<close>
lemma enumerate_simps [simp, code]:
@@ -6612,8 +6774,7 @@
lemma Cons_in_lists_iff[simp]: "x#xs \<in> lists A \<longleftrightarrow> x \<in> A \<and> xs \<in> lists A"
by auto
-lemma append_in_listsp_conv [iff]:
- "(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
+lemma append_in_listsp_conv [iff]: "(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
by (induct xs) auto
lemmas append_in_lists_conv [iff] = append_in_listsp_conv [to_set]
@@ -6634,6 +6795,9 @@
lemmas in_listsI [intro!] = in_listspI [to_set]
+lemma mono_lists: "mono lists"
+unfolding mono_def by auto
+
lemma lists_eq_set: "lists A = {xs. set xs \<le> A}"
by auto
@@ -6650,6 +6814,41 @@
then show ?thesis by auto
qed
+lemma inj_on_map_lists: assumes "inj_on f A"
+ shows "inj_on (map f) (lists A)"
+proof
+ fix xs ys
+ assume "xs \<in> lists A" and "ys \<in> lists A" and "map f xs = map f ys"
+ have "x = y" if "x \<in> set xs" and "y \<in> set ys" and "f x = f y" for x y
+ using in_listsD[OF \<open>xs \<in> lists A\<close>, rule_format, OF \<open>x \<in> set xs\<close>]
+ in_listsD[OF \<open>ys \<in> lists A\<close>, rule_format, OF \<open>y \<in> set ys\<close>]
+ \<open>inj_on f A\<close>[unfolded inj_on_def, rule_format, OF _ _ \<open>f x = f y\<close>] by blast
+ from list.inj_map_strong[OF this \<open>map f xs = map f ys\<close>]
+ show "xs = ys".
+qed
+
+lemma bij_lists: "bij_betw f X Y \<Longrightarrow> bij_betw (map f) (lists X) (lists Y)"
+unfolding bij_betw_def using inj_on_map_lists lists_image by metis
+
+lemma replicate_in_lists: "a \<in> A \<Longrightarrow> replicate k a \<in> lists A"
+by (induction k) auto
+
+lemma sing_pow_lists: "a \<in> A \<Longrightarrow> [a] ^^ n \<in> lists A"
+by (induction n) auto
+
+lemma one_generated_list_power: "u \<in> lists {x} \<Longrightarrow> \<exists>k. concat u = x ^^ k"
+proof(induction u rule: lists.induct)
+ case Nil
+ then show ?case by (metis concat.simps(1) pow_list.simps(1))
+next
+ case Cons
+ then show ?case by (metis concat.simps(2) pow_list_Suc singletonD)
+qed
+
+lemma pow_list_in_lists: "0 < k \<Longrightarrow> u ^^ k \<in> lists B \<Longrightarrow> u \<in> lists B"
+by (metis Suc_pred in_lists_conv_set pow_list_set)
+
+
subsubsection \<open>Inductive definition for membership\<close>
inductive ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
--- a/src/HOL/ROOT Wed Jan 22 22:22:27 2025 +0000
+++ b/src/HOL/ROOT Wed Jan 22 22:22:37 2025 +0000
@@ -694,6 +694,7 @@
BigO
BinEx
Birthday_Paradox
+ Bit_Operation_Calculations
Bubblesort
CTL
Cartouche_Examples
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Bit_Operation_Calculations.thy Wed Jan 22 22:22:37 2025 +0000
@@ -0,0 +1,145 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+section \<open>Tests for simplifying bit operations on ground terms\<close>
+
+theory Bit_Operation_Calculations
+ imports
+ "HOL.Bit_Operations"
+ "HOL-Library.Word"
+begin
+
+unbundle bit_operations_syntax
+
+subsection \<open>Generic unsigned computations\<close>
+
+locale unsigned_computations =
+ fixes type :: \<open>'a::semiring_bit_operations itself\<close>
+begin
+
+definition computations where
+ \<open>computations = (
+ [bit (473514 :: 'a) 5],
+ [473514 AND 767063 :: 'a],
+ [473514 OR 767063 :: 'a],
+ [473514 XOR 767063 :: 'a],
+ mask 11 :: 'a,
+ [set_bit 15 473514 :: 'a],
+ [unset_bit 13 473514 :: 'a],
+ [flip_bit 15 473514 :: 'a],
+ [push_bit 12 473514 :: 'a],
+ [drop_bit 12 65344 :: 'a],
+ [take_bit 12 473514 :: 'a]
+ )\<close>
+
+definition results where
+ \<open>results = (
+ [True],
+ [208898 :: 'a::semiring_bit_operations],
+ [1031679 :: 'a],
+ [822781 :: 'a],
+ 2047 :: 'a,
+ [506282 :: 'a],
+ [465322 :: 'a],
+ [506282 :: 'a],
+ [1939513344 :: 'a],
+ [15 :: 'a],
+ [2474 :: 'a]
+ )\<close>
+
+lemmas evaluation_simps = computations_def results_def mask_numeral
+ \<comment> \<open>Expressions like \<term>\<open>mask 42\<close> are deliberately not simplified by default\<close>
+
+end
+
+global_interpretation unsigned_computations_nat: unsigned_computations \<open>TYPE(nat)\<close>
+ defines unsigned_computations_nat = unsigned_computations_nat.computations
+ and unsigned_results_nat = unsigned_computations_nat.results .
+
+lemma \<open>unsigned_computations_nat.computations = unsigned_computations_nat.results\<close>
+ by (simp add: unsigned_computations_nat.evaluation_simps)
+
+global_interpretation unsigned_computations_int: unsigned_computations \<open>TYPE(int)\<close>
+ defines unsigned_computations_int = unsigned_computations_int.computations
+ and unsigned_results_int = unsigned_computations_int.results .
+
+lemma \<open>unsigned_computations_int.computations = unsigned_computations_int.results\<close>
+ by (simp add: unsigned_computations_int.evaluation_simps)
+
+global_interpretation unsigned_computations_word16: unsigned_computations \<open>TYPE(16 word)\<close>
+ defines unsigned_computations_word16 = unsigned_computations_word16.computations
+ and unsigned_results_word16 = unsigned_computations_word16.results .
+
+lemma \<open>unsigned_computations_word16 = unsigned_results_word16\<close>
+ by (simp add: unsigned_computations_word16.evaluation_simps)
+
+
+subsection \<open>Generic unsigned computations\<close>
+
+locale signed_computations =
+ fixes type :: \<open>'a::ring_bit_operations itself\<close>
+begin
+
+definition computations where
+ \<open>computations = (
+ [bit (- 805167 :: 'a) 7],
+ [- 805167 AND 767063, 473514 AND - 314527, - 805167 AND - 314527 :: 'a],
+ [- 805167 OR 767063, 473514 OR - 314527, - 805167 OR - 314527 :: 'a],
+ [- 805167 XOR 767063, 473514 XOR - 314527, - 805167 XOR - 314527 :: 'a],
+ [NOT 473513, NOT (- 805167) :: 'a],
+ [set_bit 11 (- 805167) :: 'a],
+ [unset_bit 12 (- 805167) :: 'a],
+ [flip_bit 12 (- 805167) :: 'a],
+ [push_bit 12 (- 805167) :: 'a],
+ [take_bit 12 (- 805167) :: 'a],
+ [signed_take_bit 12 473514, signed_take_bit 12 (- 805167) :: 'a]
+ )\<close>
+
+definition results where
+ \<open>results = (
+ [True],
+ [242769, 209184, - 839103 :: 'a],
+ [- 280873, - 50197, - 280591 :: 'a],
+ [- 523642, - 259381, 558512 :: 'a],
+ [- 473514, 805166 :: 'a],
+ [- 803119 :: 'a],
+ [- 809263 :: 'a],
+ [- 809263 :: 'a],
+ [- 3297964032 :: 'a],
+ [1745 :: 'a],
+ [- 1622, - 2351 :: 'a]
+ )\<close>
+
+lemmas evaluation_simps = computations_def results_def
+
+end
+
+global_interpretation signed_computations_int: signed_computations \<open>TYPE(int)\<close>
+ defines signed_computations_int = signed_computations_int.computations
+ and signed_results_int = signed_computations_int.results .
+
+lemma \<open>signed_computations_int.computations = signed_computations_int.results\<close>
+ by (simp add: signed_computations_int.evaluation_simps)
+
+global_interpretation signed_computations_word16: signed_computations \<open>TYPE(16 word)\<close>
+ defines signed_computations_word16 = signed_computations_word16.computations
+ and signed_results_word16 = signed_computations_word16.results .
+
+lemma \<open>signed_computations_word16 = signed_results_word16\<close>
+ by (simp add: signed_computations_word16.evaluation_simps)
+
+
+subsection \<open>Special cases on particular type instances\<close>
+
+lemma
+ \<open>drop_bit 12 (- 17405 :: int) = - 5\<close>
+ by simp
+
+lemma
+ \<open>signed_drop_bit 12 (- 17405 :: 16 word) = - 5\<close>
+ by simp
+
+lemma
+ \<open>drop_bit 12 (- 17405 :: 16 word) = 11\<close>
+ by simp
+
+end
--- a/src/Pure/Build/build_ci.scala Wed Jan 22 22:22:27 2025 +0000
+++ b/src/Pure/Build/build_ci.scala Wed Jan 22 22:22:37 2025 +0000
@@ -70,16 +70,14 @@
case object On_Commit extends Trigger
object Timed {
- def nightly(start_time: Time = Time.zero): Timed =
- Timed { (before, now) =>
- val start0 = before.midnight + start_time
- val start1 = now.midnight + start_time
- (before.time < start0.time && start0.time <= now.time) ||
- (before.time < start1.time && start1.time <= now.time)
- }
+ def nightly(start: Time = Time.hms(0, 17, 0)): Timed = Timed(Date.Daily(start))
+ def weekly(day: Date.Day = Date.Day.sun, start: Time = Time.hms(0, 17, 0)): Timed =
+ Timed(Date.Weekly(day, Date.Daily(start)))
}
- case class Timed(in_interval: (Date, Date) => Boolean) extends Trigger
+ case class Timed(cycle: Date.Cycle) extends Trigger {
+ def next(previous: Date, now: Date): Boolean = cycle.next(previous).time < cycle.next(now).time
+ }
/* build hooks */
--- a/src/Pure/Build/build_manager.scala Wed Jan 22 22:22:27 2025 +0000
+++ b/src/Pure/Build/build_manager.scala Wed Jan 22 22:22:37 2025 +0000
@@ -1135,7 +1135,7 @@
private def add_tasks(previous: Date, next: Date): Unit = synchronized_database("add_tasks") {
for (ci_job <- ci_jobs)
ci_job.trigger match {
- case Build_CI.Timed(in_interval) if in_interval(previous, next) =>
+ case timer: Build_CI.Timed if timer.next(previous, next) =>
val task = CI_Build.task(ci_job)
echo("Triggered task " + task.kind)
_state = _state.add_pending(task)
@@ -1411,7 +1411,7 @@
def render_diff(data: Report.Data, components: List[Component]): XML.Body =
par(List(page_link(Page.BUILD, "back to build", Markup.Name(build.name)))) ::
(for (component <- components if !component.is_local) yield {
- val infos =
+ val infos =
data.component_logs.toMap.get(component.name).toList.flatMap(colored) :::
data.component_diffs.toMap.get(component.name).toList.flatMap(colored)
@@ -1508,7 +1508,7 @@
Web_App.More_HTML.icon("data:image/x-icon;base64," + logo.encode_base64.text),
HTML.style_file("https://hawkz.github.io/gdcss/gd.css"),
HTML.style("""
-:root {
+:root {
--color-secondary: var(--color-tertiary);
--color-secondary-hover: var(--color-tertiary-hover);
}
@@ -1894,7 +1894,7 @@
progress.interrupt_handler {
using(store.open_ssh()) { ssh =>
val user = ssh.execute("whoami").check.out
-
+
val build_config = User_Build(user, afp_rev, prefs, requirements, all_sessions,
base_sessions, exclude_session_groups, exclude_sessions, session_groups, sessions,
build_heap, clean_build, export_files, fresh_build, presentation, verbose)
--- a/src/Pure/General/date.scala Wed Jan 22 22:22:27 2025 +0000
+++ b/src/Pure/General/date.scala Wed Jan 22 22:22:37 2025 +0000
@@ -10,7 +10,7 @@
import java.util.Locale
import java.time.{Instant, ZonedDateTime, LocalTime, ZoneId}
import java.time.format.{DateTimeFormatter, DateTimeParseException}
-import java.time.temporal.TemporalAccessor
+import java.time.temporal.{ChronoUnit, TemporalAccessor}
import scala.annotation.tailrec
@@ -99,9 +99,67 @@
def apply(t: Time, timezone: ZoneId = Date.timezone()): Date =
instant(t.instant, timezone)
+
+
+ /* varying-length calendar cycles */
+
+ enum Day { case mon, tue, wed, thu, fri, sat, sun }
+ enum Month { case jan, feb, mar, apr, may, jun, jul, aug, sep, okt, nov, dec }
+
+ sealed trait Cycle {
+ def zero(date: Date): Date
+ def next(date: Date): Date
+ }
+
+ case class Daily(at: Time = Time.zero) extends Cycle {
+ require(at >= Time.zero && at < Time.hms(24, 0, 0))
+
+ def zero(date: Date): Date = date.midnight
+ def next(date: Date): Date = {
+ val start = zero(date) + at
+ if (date.time < start.time) start else start.shift(1)
+ }
+
+ override def toString: String = "Daily(" + Format.time(Date(at, timezone_utc)) + ")"
+ }
+
+ case class Weekly(on: Day = Day.mon, step: Daily = Daily()) extends Cycle {
+ def zero(date: Date): Date = date.shift(1 - date.rep.getDayOfWeek.getValue).midnight
+ def next(date: Date): Date = {
+ val next = step.next(zero(date).shift(on.ordinal) - Time.ms(1))
+ if (date.time < next.time) next else Date(next.rep.plus(1, ChronoUnit.WEEKS))
+ }
+ }
+
+ case class Monthly(nth: Int = 1, step: Daily = Daily()) extends Cycle {
+ require(nth > 0 && nth <= 31)
+
+ def zero(date: Date): Date = date.shift(1 - date.rep.getDayOfMonth).midnight
+ def next(date: Date): Date = {
+ @tailrec def find_next(zero: Date): Date = {
+ val next = step.next(zero.shift(nth - 1) - Time.ms(1))
+ if (next.rep.getDayOfMonth == nth && date.time < next.time) next
+ else find_next(Date(zero.rep.plus(1, ChronoUnit.MONTHS)))
+ }
+ find_next(zero(date))
+ }
+ }
+
+ case class Yearly(in: Month = Month.jan, step: Monthly = Monthly()) extends Cycle {
+ def zero(date: Date): Date = date.shift(1 - date.rep.getDayOfYear).midnight
+ def next(date: Date): Date = {
+ @tailrec def find_next(zero: Date): Date = {
+ val next = step.next(Date(zero.rep.plus(in.ordinal, ChronoUnit.MONTHS)) - Time.ms(1))
+ if (next.rep.getMonthValue - 1 == in.ordinal && date.time < next.time) next
+ else find_next(Date(zero.rep.plus(1, ChronoUnit.YEARS)))
+ }
+ find_next(zero(date))
+ }
+ }
}
sealed case class Date(rep: ZonedDateTime) {
+ def shift(days: Int): Date = Date(rep.plus(days, ChronoUnit.DAYS))
def midnight: Date =
new Date(ZonedDateTime.of(rep.toLocalDate, LocalTime.MIDNIGHT, rep.getZone))
--- a/src/Tools/Code/code_target.ML Wed Jan 22 22:22:27 2025 +0000
+++ b/src/Tools/Code/code_target.ML Wed Jan 22 22:22:37 2025 +0000
@@ -384,16 +384,27 @@
val serializer = (#serializer o #language) target;
in { serializer = serializer, data = data, modify = modify } end;
-fun project_program_for_syms ctxt syms_hidden syms1 program1 =
+fun report_unimplemented ctxt program requested unimplemented =
let
- val syms2 = subtract (op =) syms_hidden syms1;
+ val deps = flat (map_product (fn req => fn unimpl =>
+ Code_Symbol.Graph.irreducible_paths program (req, Constant unimpl)) requested unimplemented)
+ val pretty_dep = space_implode " -> " o map (Code_Symbol.quote ctxt)
+ in
+ error ("No code equations for "
+ ^ commas (map (Proof_Context.markup_const ctxt) unimplemented)
+ ^ ",\nrequested by dependencies\n"
+ ^ space_implode "\n" (map pretty_dep deps))
+ end;
+
+fun project_program_for_syms ctxt syms_hidden requested1 program1 =
+ let
+ val requested2 = subtract (op =) syms_hidden requested1;
val program2 = Code_Symbol.Graph.restrict (not o member (op =) syms_hidden) program1;
val unimplemented = Code_Thingol.unimplemented program2;
val _ =
if null unimplemented then ()
- else error ("No code equations for " ^
- commas (map (Proof_Context.markup_const ctxt) unimplemented));
- val syms3 = Code_Symbol.Graph.all_succs program2 syms2;
+ else report_unimplemented ctxt program2 requested2 unimplemented;
+ val syms3 = Code_Symbol.Graph.all_succs program2 requested2;
val program3 = Code_Symbol.Graph.restrict (member (op =) syms3) program2;
in program3 end;
--- a/src/Tools/Find_Facts/etc/settings Wed Jan 22 22:22:27 2025 +0000
+++ b/src/Tools/Find_Facts/etc/settings Wed Jan 22 22:22:37 2025 +0000
@@ -1,9 +1,7 @@
# -*- shell-script -*- :mode=shellscript:
FIND_FACTS_HOME="$COMPONENT"
-FIND_FACTS_WEB="$ISABELLE_HOME_USER/find_facts/web"
-
-SOLR_DATA="$ISABELLE_HOME_USER/find_facts/solr"
-SOLR_COMPONENTS=""
+FIND_FACTS_HOME_USER="$ISABELLE_HOME_USER/find_facts"
+FIND_FACTS_INDEXES=""
ISABELLE_TOOLS="$ISABELLE_TOOLS:$FIND_FACTS_HOME/Tools"
--- a/src/Tools/Find_Facts/src/find_facts.scala Wed Jan 22 22:22:27 2025 +0000
+++ b/src/Tools/Find_Facts/src/find_facts.scala Wed Jan 22 22:22:37 2025 +0000
@@ -112,6 +112,8 @@
/** Solr data model **/
+ val solr_data_dir: Path = Path.explode("$FIND_FACTS_HOME_USER/solr")
+
object private_data extends Solr.Data("find_facts") {
/* types */
@@ -577,29 +579,52 @@
} yield block)
}
+ def find_facts_index_command(
+ sessions: List[String],
+ ssh: SSH.System = SSH.Local,
+ isabelle_home: Path = Path.current,
+ options: List[Options.Spec] = Nil,
+ dirs: List[Path] = Nil,
+ clean: Boolean = false,
+ no_build: Boolean = false,
+ verbose: Boolean = false,
+ ): String = {
+ ssh.bash_path(Isabelle_Tool.exe(isabelle_home)) + " find_facts_index" +
+ dirs.map(dir => " -d " + ssh.bash_path(dir)).mkString +
+ if_proper(clean, " -c") +
+ if_proper(no_build, " -n") +
+ if_proper(verbose, " -v") +
+ Options.Spec.bash_strings(options, bg = true) +
+ sessions.map(session => " " + session).mkString
+ }
+
def find_facts_index(
options: Options,
sessions: List[String],
+ afp_root: Option[Path] = None,
dirs: List[Path] = Nil,
clean: Boolean = false,
progress: Progress = new Progress
): Unit = {
val store = Store(options)
+ val solr = Solr.init(solr_data_dir)
val database = options.string("find_facts_database_name")
val session = Session(options, Resources.bootstrap)
val selection = Sessions.Selection(sessions = sessions)
- val session_structure = Sessions.load_structure(options, dirs = dirs).selection(selection)
+ val session_structure =
+ Sessions.load_structure(options, dirs = AFP.main_dirs(afp_root) ::: dirs).selection(selection)
val deps = Sessions.Deps.load(session_structure)
val browser_info_context = Browser_Info.context(session_structure)
if (sessions.isEmpty) progress.echo("Nothing to index")
else {
+ val start_date = Date.now()
val stats =
- using(Solr.init_database(database, Find_Facts.private_data, clean = clean)) { db =>
+ using(solr.init_database(database, Find_Facts.private_data, clean = clean)) { db =>
using(Export.open_database_context(store)) { database_context =>
val document_info = Document_Info.read(database_context, deps, sessions)
-
+
def index_session(session_name: String): Unit = {
using(database_context.open_session0(session_name)) { session_context =>
val info = session_structure(session_name)
@@ -611,7 +636,7 @@
Build.read_theory(theory_context) match {
case None => progress.echo_warning("No snapshot for theory " + name.theory)
case Some(snapshot) =>
- progress.echo("Theory " + name.theory + " ...")
+ progress.echo("Indexing theory " + quote(name.theory), verbose = true)
val blocks =
make_thy_blocks(options, session, browser_info_context, document_info,
theory_context, snapshot, info.chapter)
@@ -628,8 +653,9 @@
Find_Facts.query_stats(db, query)
}
- progress.echo("Indexed " + stats.results + " blocks with " +
- stats.consts + " consts, " + stats.typs + " typs, " + stats.thms + " thms")
+ val timing = Date.now() - start_date
+ progress.echo("Indexed " + stats.results + " blocks with " + stats.consts + " consts, " +
+ stats.typs + " typs, " + stats.thms + " thms in " + timing.message)
}
}
@@ -638,6 +664,7 @@
def main_tool1(args: Array[String]): Unit = {
Command_Line.tool {
+ var afp_root: Option[Path] = None
var clean = false
val dirs_buffer = new mutable.ListBuffer[Path]
var no_build = false
@@ -648,6 +675,7 @@
Usage: isabelle find_facts_index [OPTIONS] [SESSIONS ...]
Options are:
+ -A ROOT include AFP with given root directory (":" for """ + AFP.BASE.implode + """)
-c clean previous index
-d DIR include session directory
-n no build -- take existing session build databases
@@ -656,6 +684,7 @@
Build and index sessions for Find_Facts.
""",
+ "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
"c" -> (_ => clean = true),
"d:" -> (arg => dirs_buffer += Path.explode(arg)),
"n" -> (_ => no_build = true),
@@ -673,7 +702,7 @@
if (!no_build) {
def build(test: Boolean = false): Build.Results =
Build.build(options, selection = Sessions.Selection(sessions = sessions), dirs = dirs,
- no_build = test, progress = if (test) new Progress else progress)
+ afp_root = afp_root, no_build = test, progress = if (test) new Progress else progress)
progress.interrupt_handler {
if (!build(test = true).ok) {
@@ -690,56 +719,66 @@
/* index */
- find_facts_index(options, sessions, dirs = dirs, clean = clean, progress = progress)
+ find_facts_index(options, sessions, dirs = dirs, afp_root = afp_root, clean = clean,
+ progress = progress)
}
}
-
/** index components **/
- def find_facts_index_component(
- options: Options,
+ def resolve_indexes(solr: Solr.System): Unit =
+ for {
+ path <- Path.split(Isabelle_System.getenv("FIND_FACTS_INDEXES"))
+ database = Library.perhaps_unprefix("find_facts-", path.file_name)
+ database_dir = solr.database_dir(database)
+ if !database_dir.is_dir
+ } Isabelle_System.copy_dir(path, database_dir, direct = true)
+
+ def find_facts_index_build(
+ database: String,
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
- val database = options.string("find_facts_database_name")
+ val solr = Solr.init(solr_data_dir)
- val component = "find_facts_index-" + database
+ val component = "find_facts-" + database
val component_dir =
Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
- Isabelle_System.copy_dir(Solr.database_dir(database), component_dir.path)
- component_dir.write_settings("SOLR_COMPONENTS=\"$SOLR_COMPONENTS:$COMPONENT/" + database + "\"")
+ Isabelle_System.copy_dir(solr.database_dir(database), component_dir.path)
+ component_dir.write_settings(
+ "FIND_FACTS_INDEXES=\"$FIND_FACTS_INDEXES:$COMPONENT/" + database + "\"")
}
/* Isabelle tool wrapper */
- val isabelle_tool2 = Isabelle_Tool("find_facts_index_component",
+ val isabelle_tool2 = Isabelle_Tool("find_facts_index_build",
"build Isabelle component from Find_Facts index", Scala_Project.here,
{ args =>
- var options = Options.init()
var target_dir = Path.current
val getopts = Getopts("""
- Usage: isabelle find_facts_index_component
+ Usage: isabelle find_facts_index_build DATABASE
Options are:
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-D DIR target directory (default ".")
- Build Isabelle component from finalized Find_Facts index with given name.
+ Build Isabelle component from finalized Find_Facts index with given database name.
""",
- "o:" -> (arg => options = options + arg),
"D:" -> (arg => target_dir = Path.explode(arg)))
val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val database =
+ more_args match {
+ case database :: Nil => database
+ case _ => getopts.usage()
+ }
val progress = new Console_Progress()
- find_facts_index_component(options, target_dir = target_dir, progress = progress)
+ find_facts_index_build(database, target_dir = target_dir, progress = progress)
})
@@ -846,19 +885,18 @@
/* find facts */
- val template_web_dir: Path = Path.explode("$FIND_FACTS_HOME/web")
- val default_web_dir: Path = Path.explode("$FIND_FACTS_WEB")
+ val web_sources: Path = Path.explode("$FIND_FACTS_HOME/web")
+ val web_dir: Path = Path.explode("$FIND_FACTS_HOME_USER/web")
val default_port = 8080
- def find_facts(
+ def find_facts_server(
options: Options,
port: Int = default_port,
devel: Boolean = false,
- web_dir: Path = default_web_dir,
progress: Progress = new Progress
): Unit = {
- Isabelle_System.copy_dir(template_web_dir, web_dir, direct = true)
+ Isabelle_System.copy_dir(web_sources, web_dir, direct = true)
val database = options.string("find_facts_database_name")
val encode = new Encode(options)
@@ -878,7 +916,10 @@
val frontend = project.build_html(progress = progress)
- using(Solr.open_database(database)) { db =>
+ val solr = Solr.init(solr_data_dir)
+ resolve_indexes(solr)
+
+ using(solr.open_database(database)) { db =>
val stats = Find_Facts.query_stats(db, Query(Nil))
progress.echo("Started Find_Facts with " + stats.results + " blocks, " +
stats.consts + " consts, " + stats.typs + " typs, " + stats.thms + " thms")
@@ -890,7 +931,7 @@
def apply(request: HTTP.Request): Option[HTTP.Response] =
Some(HTTP.Response(Bytes(isabelle_style), "text/css"))
},
- new HTTP.Service("app") {
+ new HTTP.Service("find_facts") {
def apply(request: HTTP.Request): Option[HTTP.Response] =
Some(HTTP.Response.html(
if (devel) project.build_html(progress = progress) else frontend))
@@ -917,7 +958,7 @@
}))
server.start()
- progress.echo("Server started " + server.toString + "/app")
+ progress.echo("Server started " + server.toString + "/find_facts")
@tailrec
def loop(): Unit = {
@@ -938,7 +979,6 @@
var options = Options.init()
var port = default_port
var verbose = false
- var web_dir = default_web_dir
val getopts = Getopts("""
Usage: isabelle find_facts_server [OPTIONS]
@@ -948,22 +988,20 @@
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-p PORT explicit web server port (default: """ + default_port + """)
-v verbose server
- -w DIR web directory (default: """ + default_web_dir + """)
Run server for Find_Facts.
""",
"d" -> (_ => devel = true),
"o:" -> (arg => options = options + arg),
"p:" -> (arg => port = Value.Int.parse(arg)),
- "v" -> (_ => verbose = true),
- "w:" -> (arg => web_dir = Path.explode(arg)))
+ "v" -> (_ => verbose = true))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress(verbose = verbose)
- find_facts(options, port = port, devel = devel, web_dir = web_dir, progress = progress)
+ find_facts_server(options, port = port, devel = devel, progress = progress)
}
}
}
--- a/src/Tools/Find_Facts/src/solr.scala Wed Jan 22 22:22:27 2025 +0000
+++ b/src/Tools/Find_Facts/src/solr.scala Wed Jan 22 22:22:37 2025 +0000
@@ -23,20 +23,12 @@
object Solr {
- def init(solr_data: Path): Path = {
+ def init(solr_data: Path): System = {
File.write(Isabelle_System.make_directory(solr_data) + Path.basic("solr.xml"), "<solr/>")
-
- // non-portable: only for Linux or macOS
- for (path <- Path.split(Isabelle_System.getenv("SOLR_COMPONENTS"))) {
- Isabelle_System.symlink(path.absolute, solr_data, force = true)
- }
-
java.util.logging.LogManager.getLogManager.reset()
- solr_data
+ new System(solr_data)
}
- lazy val solr_data: Path = init(Path.explode("$SOLR_DATA"))
-
/** query language */
@@ -347,32 +339,36 @@
/* database */
- def database_dir(database: String): Path = solr_data + Path.basic(database)
+ class System private[Solr](val solr_data: Path) {
+ def database_dir(database: String): Path = solr_data + Path.basic(database)
- def init_database(database: String, data: Data, clean: Boolean = false): Database = {
- val db_dir = database_dir(database)
+ def init_database(database: String, data: Data, clean: Boolean = false): Database = {
+ val db_dir = database_dir(database)
- if (clean) Isabelle_System.rm_tree(db_dir)
+ if (clean) Isabelle_System.rm_tree(db_dir)
- val conf_dir = db_dir + Path.basic("conf")
- if (!conf_dir.is_dir) {
- Isabelle_System.make_directory(conf_dir)
- File.write(conf_dir + Path.basic("schema.xml"), XML.string_of_body(data.schema))
- File.write(conf_dir + Path.basic("solrconfig.xml"), XML.string_of_body(data.solr_config))
- data.more_config.foreach((path, content) => File.write(conf_dir + path, content))
+ val conf_dir = db_dir + Path.basic("conf")
+ if (!conf_dir.is_dir) {
+ Isabelle_System.make_directory(conf_dir)
+ File.write(conf_dir + Path.basic("schema.xml"), XML.string_of_body(data.schema))
+ File.write(conf_dir + Path.basic("solrconfig.xml"), XML.string_of_body(data.solr_config))
+ data.more_config.foreach((path, content) => File.write(conf_dir + path, content))
+ }
+
+ open_database(database)
}
- open_database(database)
- }
-
- def open_database(database: String): Database = {
- val server = new EmbeddedSolrServer(solr_data.java_path, database)
-
- val cores = server.getCoreContainer.getAllCoreNames.asScala
- if (cores.contains(database)) server.getCoreContainer.reload(database)
- else server.getCoreContainer.create(database, Map.empty.asJava)
-
- new Database(server)
+ def open_database(database: String): Database =
+ if (!database_dir(database).is_dir) error("Missing Solr database: " + quote(database))
+ else {
+ val server = new EmbeddedSolrServer(solr_data.java_path, database)
+
+ val cores = server.getCoreContainer.getAllCoreNames.asScala
+ if (cores.contains(database)) server.getCoreContainer.reload(database)
+ else server.getCoreContainer.create(database, Map.empty.asJava)
+
+ new Database(server)
+ }
}
class Database private[Solr](solr: EmbeddedSolrServer) extends AutoCloseable {