--- a/Admin/components/components.sha1 Tue Nov 09 16:17:13 2021 +0100
+++ b/Admin/components/components.sha1 Tue Nov 09 19:47:24 2021 +0100
@@ -145,6 +145,7 @@
127a75ae33e97480d352087fcb9b47a632d77169 isabelle_setup-20210724.tar.gz
309909ec6d43ae460338e9af54c1b2a48adcb1ec isabelle_setup-20210726.tar.gz
a14ce46c62c64c3413f3cc9239242e33570d0f3d isabelle_setup-20210922.tar.gz
+b22066a9dcde6f813352dcf6404ac184440a22df isabelle_setup-20211109.tar.gz
0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz
e12574d838ed55ef2845acf1152329572ab0cc56 jdk-11.0.10+9.tar.gz
3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz
@@ -266,6 +267,7 @@
ad5d0e640ce3609a885cecab645389a2204e03bb macos_app-20150916.tar.gz
400af57ec5cd51f96928d9de00d077524a6fe316 macos_app-20181205.tar.gz
3bc42b8e22f0be5ec5614f1914066164c83498f8 macos_app-20181208.tar.gz
+5fb1a2d21b220d0e588790c0203ac87c10ed0870 minisat-2.2.1-1.tar.gz
ae76bfaade3bf72ff6b2d3aafcd52fa45609fcd1 minisat-2.2.1.tar.gz
eda10c62da927a842c0a8881f726eac85e1cb4f7 naproche-20210122.tar.gz
edcb517b7578db4eec1b6573b624f291776e11f6 naproche-20210124.tar.gz
--- a/Admin/components/main Tue Nov 09 16:17:13 2021 +0100
+++ b/Admin/components/main Tue Nov 09 19:47:24 2021 +0100
@@ -8,13 +8,13 @@
flatlaf-1.6
idea-icons-20210508
isabelle_fonts-20211004
-isabelle_setup-20210922
+isabelle_setup-20211109
jdk-17.0.1+12
jedit-20211103
jfreechart-1.5.3
jortho-1.0-2
kodkodi-1.5.7
-minisat-2.2.1
+minisat-2.2.1-1
nunchaku-0.5
opam-2.0.7
polyml-5.9-5d4caa8f7148
--- a/NEWS Tue Nov 09 16:17:13 2021 +0100
+++ b/NEWS Tue Nov 09 19:47:24 2021 +0100
@@ -95,11 +95,6 @@
specifies the name of the logo variant, while "_" (underscore) refers to
the unnamed variant. The output file name is always "isabelle_logo.pdf".
-* Option "document_preprocessor" specifies the name of an executable
-that is run within the document output directory, after preparing the
-document sources and before the actual build process. This allows to
-apply adhoc patches, without requiring a separate "build" script.
-
* Option "document_build" determines the document build engine, as
defined in Isabelle/Scala (as system service). The subsequent engines
are provided by the Isabelle distribution:
@@ -116,6 +111,9 @@
explicitly requires document_build=build. Minor INCOMPATIBILITY, need to
adjust session ROOT options.
+* Option "document_echo" informs about document file names during
+session presentation.
+
* The command-line tool "isabelle latex" has been discontinued,
INCOMPATIBILITY for old document build scripts.
--- a/etc/options Tue Nov 09 16:17:13 2021 +0100
+++ b/etc/options Tue Nov 09 19:47:24 2021 +0100
@@ -9,14 +9,14 @@
-- "build PDF document (enabled for \"pdf\" or \"true\", disabled for \"\" or \"false\")"
option document_output : string = ""
-- "document output directory"
+option document_echo : bool = false
+ -- "inform about document file names during session presentation"
option document_variants : string = "document"
-- "alternative document variants (separated by colons)"
option document_tags : string = ""
-- "default command tags (separated by commas)"
option document_bibliography : bool = false
-- "explicitly enable use of bibtex (default: according to presence of root.bib)"
-option document_preprocessor : string = ""
- -- "document preprocessor: executable relative to document output directory"
option document_build : string = "lualatex"
-- "document build engine (e.g. lualatex, pdflatex, build)"
option document_logo : string = ""
--- a/src/Doc/System/Sessions.thy Tue Nov 09 16:17:13 2021 +0100
+++ b/src/Doc/System/Sessions.thy Tue Nov 09 19:47:24 2021 +0100
@@ -243,12 +243,6 @@
of \<^verbatim>\<open>bibtex\<close>; the default is to check the presence of \<^verbatim>\<open>root.bib\<close>, but it
could have a different name.
- \<^item> @{system_option_def "document_preprocessor"} specifies the name of an
- executable that is run within the document output directory, after
- preparing the document sources and before the actual build process. This
- allows to apply adhoc patches, without requiring a separate \<^verbatim>\<open>build\<close>
- script.
-
\<^item> @{system_option_def "threads"} determines the number of worker threads
for parallel checking of theories and proofs. The default \<open>0\<close> means that a
sensible maximum value is determined by the underlying hardware. For
--- a/src/HOL/Analysis/Convex.thy Tue Nov 09 16:17:13 2021 +0100
+++ b/src/HOL/Analysis/Convex.thy Tue Nov 09 19:47:24 2021 +0100
@@ -344,6 +344,14 @@
where "convex_on S f \<longleftrightarrow>
(\<forall>x\<in>S. \<forall>y\<in>S. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y)"
+definition\<^marker>\<open>tag important\<close> concave_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
+ where "concave_on S f \<equiv> convex_on S (\<lambda>x. - f x)"
+
+lemma concave_on_iff:
+ "concave_on S f \<longleftrightarrow>
+ (\<forall>x\<in>S. \<forall>y\<in>S. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> f (u *\<^sub>R x + v *\<^sub>R y) \<ge> u * f x + v * f y)"
+ by (auto simp: concave_on_def convex_on_def algebra_simps)
+
lemma convex_onI [intro?]:
assumes "\<And>t x y. t > 0 \<Longrightarrow> t < 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow>
f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
@@ -865,35 +873,44 @@
assumes conv: "convex C"
and f': "\<And>x. x \<in> C \<Longrightarrow> DERIV f x :> (f' x)"
and f'': "\<And>x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)"
- and pos: "\<And>x. x \<in> C \<Longrightarrow> f'' x \<ge> 0"
+ and 0: "\<And>x. x \<in> C \<Longrightarrow> f'' x \<ge> 0"
shows "convex_on C f"
- using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function
+ using f''_imp_f'[OF conv f' f'' 0] assms pos_convex_function
by fastforce
+lemma f''_le0_imp_concave:
+ fixes f :: "real \<Rightarrow> real"
+ assumes "convex C"
+ and "\<And>x. x \<in> C \<Longrightarrow> DERIV f x :> (f' x)"
+ and "\<And>x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)"
+ and "\<And>x. x \<in> C \<Longrightarrow> f'' x \<le> 0"
+ shows "concave_on C f"
+ unfolding concave_on_def
+ by (rule assms f''_ge0_imp_convex derivative_eq_intros | simp)+
+
+lemma log_concave:
+ fixes b :: real
+ assumes "b > 1"
+ shows "concave_on {0<..} (\<lambda> x. log b x)"
+ using assms
+ by (intro f''_le0_imp_concave derivative_eq_intros | simp)+
+
+lemma ln_concave: "concave_on {0<..} ln"
+ unfolding log_ln by (simp add: log_concave)
+
lemma minus_log_convex:
fixes b :: real
assumes "b > 1"
shows "convex_on {0 <..} (\<lambda> x. - log b x)"
-proof -
- have "\<And>z. z > 0 \<Longrightarrow> DERIV (log b) z :> 1 / (ln b * z)"
- using DERIV_log by auto
- then have f': "\<And>z. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - log b z) z :> - 1 / (ln b * z)"
- by (auto simp: DERIV_minus)
- have "\<And>z::real. z > 0 \<Longrightarrow> DERIV inverse z :> - (inverse z ^ Suc (Suc 0))"
- using less_imp_neq[THEN not_sym, THEN DERIV_inverse] by auto
- from this[THEN DERIV_cmult, of _ "- 1 / ln b"]
- have "\<And>z::real. z > 0 \<Longrightarrow>
- DERIV (\<lambda> z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))"
- by auto
- then have f''0: "\<And>z::real. z > 0 \<Longrightarrow>
- DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
- unfolding inverse_eq_divide by (auto simp: mult.assoc)
- have f''_ge0: "\<And>z::real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
- using \<open>b > 1\<close> by (auto intro!: less_imp_le)
- from f''_ge0_imp_convex[OF convex_real_interval(3), unfolded greaterThan_iff, OF f' f''0 f''_ge0]
- show ?thesis
- by auto
-qed
+ using assms concave_on_def log_concave by blast
+
+lemma powr_convex:
+ assumes "p \<ge> 1" shows "convex_on {0<..} (\<lambda>x. x powr p)"
+ using assms
+ by (intro f''_ge0_imp_convex derivative_eq_intros | simp)+
+
+lemma exp_convex: "convex_on UNIV exp"
+ by (intro f''_ge0_imp_convex derivative_eq_intros | simp)+
subsection\<^marker>\<open>tag unimportant\<close> \<open>Convexity of real functions\<close>
@@ -1003,6 +1020,63 @@
finally show ?thesis .
qed (insert assms(2), simp_all)
+subsection \<open>Some inequalities\<close>
+
+lemma Youngs_inequality_0:
+ fixes a::real
+ assumes "0 \<le> \<alpha>" "0 \<le> \<beta>" "\<alpha>+\<beta> = 1" "a>0" "b>0"
+ shows "a powr \<alpha> * b powr \<beta> \<le> \<alpha>*a + \<beta>*b"
+proof -
+ have "\<alpha> * ln a + \<beta> * ln b \<le> ln (\<alpha> * a + \<beta> * b)"
+ using assms ln_concave by (simp add: concave_on_iff)
+ moreover have "0 < \<alpha> * a + \<beta> * b"
+ using assms by (smt (verit) mult_pos_pos split_mult_pos_le)
+ ultimately show ?thesis
+ using assms by (simp add: powr_def mult_exp_exp flip: ln_ge_iff)
+qed
+
+lemma Youngs_inequality:
+ fixes p::real
+ assumes "p>1" "q>1" "1/p + 1/q = 1" "a\<ge>0" "b\<ge>0"
+ shows "a * b \<le> a powr p / p + b powr q / q"
+proof (cases "a=0 \<or> b=0")
+ case False
+ then show ?thesis
+ using Youngs_inequality_0 [of "1/p" "1/q" "a powr p" "b powr q"] assms
+ by (simp add: powr_powr)
+qed (use assms in auto)
+
+lemma Cauchy_Schwarz_ineq_sum:
+ fixes a :: "'a \<Rightarrow> 'b::linordered_field"
+ shows "(\<Sum>i\<in>I. a i * b i)\<^sup>2 \<le> (\<Sum>i\<in>I. (a i)\<^sup>2) * (\<Sum>i\<in>I. (b i)\<^sup>2)"
+proof (cases "(\<Sum>i\<in>I. (b i)\<^sup>2) > 0")
+ case False
+ then consider "\<And>i. i\<in>I \<Longrightarrow> b i = 0" | "infinite I"
+ by (metis (mono_tags, lifting) sum_pos2 zero_le_power2 zero_less_power2)
+ thus ?thesis
+ by fastforce
+next
+ case True
+ define r where "r \<equiv> (\<Sum>i\<in>I. a i * b i) / (\<Sum>i\<in>I. (b i)\<^sup>2)"
+ with True have *: "(\<Sum>i\<in>I. a i * b i) = r * (\<Sum>i\<in>I. (b i)\<^sup>2)"
+ by simp
+ have "0 \<le> (\<Sum>i\<in>I. (a i - r * b i)\<^sup>2)"
+ by (meson sum_nonneg zero_le_power2)
+ also have "... = (\<Sum>i\<in>I. (a i)\<^sup>2) - 2 * r * (\<Sum>i\<in>I. a i * b i) + r\<^sup>2 * (\<Sum>i\<in>I. (b i)\<^sup>2)"
+ by (simp add: algebra_simps power2_eq_square sum_distrib_left flip: sum.distrib)
+ also have "\<dots> = (\<Sum>i\<in>I. (a i)\<^sup>2) - (\<Sum>i\<in>I. a i * b i) * r"
+ by (simp add: * power2_eq_square)
+ also have "\<dots> = (\<Sum>i\<in>I. (a i)\<^sup>2) - ((\<Sum>i\<in>I. a i * b i))\<^sup>2 / (\<Sum>i\<in>I. (b i)\<^sup>2)"
+ by (simp add: r_def power2_eq_square)
+ finally have "0 \<le> (\<Sum>i\<in>I. (a i)\<^sup>2) - ((\<Sum>i\<in>I. a i * b i))\<^sup>2 / (\<Sum>i\<in>I. (b i)\<^sup>2)" .
+ hence "((\<Sum>i\<in>I. a i * b i))\<^sup>2 / (\<Sum>i\<in>I. (b i)\<^sup>2) \<le> (\<Sum>i\<in>I. (a i)\<^sup>2)"
+ by (simp add: le_diff_eq)
+ thus "((\<Sum>i\<in>I. a i * b i))\<^sup>2 \<le> (\<Sum>i\<in>I. (a i)\<^sup>2) * (\<Sum>i\<in>I. (b i)\<^sup>2)"
+ by (simp add: pos_divide_le_eq True)
+qed
+
+subsection \<open>Misc related lemmas\<close>
+
lemma convex_translation_eq [simp]:
"convex ((+) a ` s) \<longleftrightarrow> convex s"
by (metis convex_translation translation_galois)
@@ -1016,9 +1090,6 @@
shows "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> convex (f ` s) \<longleftrightarrow> convex s"
by (metis (no_types) convex_linear_image convex_linear_vimage inj_vimage_image_eq)
-lemma fst_snd_linear: "linear (\<lambda>(x,y). x + y)"
- unfolding linear_iff by (simp add: algebra_simps)
-
lemma vector_choose_size:
assumes "0 \<le> c"
obtains x :: "'a::{real_normed_vector, perfect_space}" where "norm x = c"
@@ -1045,18 +1116,6 @@
unfolding * using sum.delta[OF assms, of y "\<lambda>x. f x *\<^sub>R x"] by auto
qed
-lemma dist_triangle_eq:
- fixes x y z :: "'a::real_inner"
- shows "dist x z = dist x y + dist y z \<longleftrightarrow>
- norm (x - y) *\<^sub>R (y - z) = norm (y - z) *\<^sub>R (x - y)"
-proof -
- have *: "x - y + (y - z) = x - z" by auto
- show ?thesis unfolding dist_norm norm_triangle_eq[of "x - y" "y - z", unfolded *]
- by (auto simp:norm_minus_commute)
-qed
-
-
-
subsection \<open>Cones\<close>
--- a/src/HOL/Analysis/Linear_Algebra.thy Tue Nov 09 16:17:13 2021 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy Tue Nov 09 19:47:24 2021 +0100
@@ -1143,6 +1143,15 @@
finally show ?thesis .
qed
+lemma dist_triangle_eq:
+ fixes x y z :: "'a::real_inner"
+ shows "dist x z = dist x y + dist y z \<longleftrightarrow>
+ norm (x - y) *\<^sub>R (y - z) = norm (y - z) *\<^sub>R (x - y)"
+proof -
+ have *: "x - y + (y - z) = x - z" by auto
+ show ?thesis unfolding dist_norm norm_triangle_eq[of "x - y" "y - z", unfolded *]
+ by (auto simp:norm_minus_commute)
+qed
subsection \<open>Collinearity\<close>
--- a/src/HOL/Analysis/Starlike.thy Tue Nov 09 16:17:13 2021 +0100
+++ b/src/HOL/Analysis/Starlike.thy Tue Nov 09 19:47:24 2021 +0100
@@ -2398,6 +2398,9 @@
by (intro closure_bounded_linear_image_subset bounded_linear_add
bounded_linear_fst bounded_linear_snd)
+lemma fst_snd_linear: "linear (\<lambda>(x,y). x + y)"
+ unfolding linear_iff by (simp add: algebra_simps)
+
lemma rel_interior_sum:
fixes S T :: "'n::euclidean_space set"
assumes "convex S"
--- a/src/HOL/Analysis/ex/Metric_Arith_Examples.thy Tue Nov 09 16:17:13 2021 +0100
+++ b/src/HOL/Analysis/ex/Metric_Arith_Examples.thy Tue Nov 09 19:47:24 2021 +0100
@@ -54,7 +54,7 @@
by metric
lemma "dist a e \<le> dist a b + dist b c + dist c d + dist d e"
- using [[argo_timeout = 25]] by metric
+ by metric
lemma "max (dist x y) \<bar>dist x z - dist z y\<bar> = dist x y"
by metric
--- a/src/HOL/Analysis/metric_arith.ML Tue Nov 09 16:17:13 2021 +0100
+++ b/src/HOL/Analysis/metric_arith.ML Tue Nov 09 19:47:24 2021 +0100
@@ -7,6 +7,7 @@
signature METRIC_ARITH =
sig
val trace: bool Config.T
+ val argo_timeout: real Config.T
val metric_arith_tac : Proof.context -> int -> tactic
end
@@ -21,10 +22,15 @@
fun trace_tac ctxt msg =
if Config.get ctxt trace then print_tac ctxt msg else all_tac
-fun argo_trace_ctxt ctxt =
- if Config.get ctxt trace
- then Config.map (Argo_Tactic.trace) (K "basic") ctxt
- else ctxt
+val argo_timeout = Attrib.setup_config_real \<^binding>\<open>metric_argo_timeout\<close> (K 20.0)
+
+fun argo_ctxt ctxt =
+ let
+ val ctxt1 =
+ if Config.get ctxt trace
+ then Config.map (Argo_Tactic.trace) (K "basic") ctxt
+ else ctxt
+ in Config.put Argo_Tactic.timeout (Config.get ctxt1 argo_timeout) ctxt1 end
fun free_in v t =
Term.exists_subterm (fn u => u aconv Thm.term_of v) (Thm.term_of t);
@@ -218,10 +224,8 @@
(* decision procedure for linear real arithmetic *)
fun lin_real_arith_tac ctxt metric_ty = CSUBGOAL (fn (goal, i) =>
- let
- val dist_thms = augment_dist_pos metric_ty goal
- val ctxt' = argo_trace_ctxt ctxt
- in Argo_Tactic.argo_tac ctxt' dist_thms i end)
+ let val dist_thms = augment_dist_pos metric_ty goal
+ in Argo_Tactic.argo_tac (argo_ctxt ctxt) dist_thms i end)
fun basic_metric_arith_tac ctxt metric_ty =
SELECT_GOAL (
--- a/src/HOL/Eisbach/Example_Metric.thy Tue Nov 09 16:17:13 2021 +0100
+++ b/src/HOL/Eisbach/Example_Metric.thy Tue Nov 09 19:47:24 2021 +0100
@@ -8,6 +8,8 @@
text \<open>An Eisbach implementation of the method @{method metric}.
Slower than the Isabelle/ML implementation but arguably more readable.\<close>
+declare [[argo_timeout = 20]]
+
method dist_refl_sym = simp only: simp_thms dist_commute dist_self
method lin_real_arith uses thms = argo thms
--- a/src/HOL/SMT.thy Tue Nov 09 16:17:13 2021 +0100
+++ b/src/HOL/SMT.thy Tue Nov 09 19:47:24 2021 +0100
@@ -736,7 +736,7 @@
text \<open>
The option \<open>smt_read_only_certificates\<close> controls whether only
-stored certificates are should be used or invocation of an SMT solver
+stored certificates should be used or invocation of an SMT solver
is allowed. When set to \<open>true\<close>, no SMT solver will ever be
invoked and only the existing certificates found in the configured
cache are used; when set to \<open>false\<close> and there is no cached
--- a/src/HOL/ex/Argo_Examples.thy Tue Nov 09 16:17:13 2021 +0100
+++ b/src/HOL/ex/Argo_Examples.thy Tue Nov 09 19:47:24 2021 +0100
@@ -531,6 +531,7 @@
notepad
begin
fix a b :: real
+ fix f :: "real \<Rightarrow> 'a"
have "f (a + b) = f (b + a)" by argo
next
have
--- a/src/Pure/Admin/build_minisat.scala Tue Nov 09 16:17:13 2021 +0100
+++ b/src/Pure/Admin/build_minisat.scala Tue Nov 09 19:47:24 2021 +0100
@@ -85,6 +85,10 @@
Isabelle_System.copy_file(
build_dir + Path.explode("build/release/bin/minisat").platform_exe, platform_dir)
+ if (Platform.is_windows) {
+ Isabelle_System.copy_file(Path.explode("/bin/cygwin1.dll"), platform_dir)
+ }
+
/* settings */
--- a/src/Pure/PIDE/session.scala Tue Nov 09 16:17:13 2021 +0100
+++ b/src/Pure/PIDE/session.scala Tue Nov 09 19:47:24 2021 +0100
@@ -127,7 +127,7 @@
{
session =>
- val cache: XML.Cache = XML.Cache.make()
+ val cache: Term.Cache = Term.Cache.make()
def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info =
Command.Blobs_Info.none
--- a/src/Pure/PIDE/xml.scala Tue Nov 09 16:17:13 2021 +0100
+++ b/src/Pure/PIDE/xml.scala Tue Nov 09 19:47:24 2021 +0100
@@ -199,15 +199,15 @@
object Cache
{
def make(
- xz: XZ.Cache = XZ.Cache.make(),
- max_string: Int = isabelle.Cache.default_max_string,
+ xz: XZ.Cache = XZ.Cache.make(),
+ max_string: Int = isabelle.Cache.default_max_string,
initial_size: Int = isabelle.Cache.default_initial_size): Cache =
new Cache(xz, max_string, initial_size)
val none: Cache = make(XZ.Cache.none, max_string = 0)
}
- class Cache private[XML](val xz: XZ.Cache, max_string: Int, initial_size: Int)
+ class Cache(val xz: XZ.Cache, max_string: Int, initial_size: Int)
extends isabelle.Cache(max_string, initial_size)
{
protected def cache_props(x: Properties.T): Properties.T =
--- a/src/Pure/Thy/document_build.scala Tue Nov 09 16:17:13 2021 +0100
+++ b/src/Pure/Thy/document_build.scala Tue Nov 09 19:47:24 2021 +0100
@@ -185,9 +185,6 @@
def document_bibliography: Boolean = options.bool("document_bibliography")
- def document_preprocessor: Option[String] =
- proper_string(options.string("document_preprocessor"))
-
def document_logo: Option[String] =
options.string("document_logo") match {
case "" => None
@@ -275,16 +272,6 @@
val root_name1 = "root_" + doc.name
val root_name = if ((doc_dir + Path.explode(root_name1).tex).is_file) root_name1 else "root"
- for (name <- document_preprocessor) {
- def message(s: String): String = s + " for document_preprocessor=" + quote(name)
- val path = doc_dir + Path.explode(name)
- if (path.is_file) {
- try { Isabelle_System.bash(File.bash_path(path), cwd = doc_dir.file).check }
- catch { case ERROR(msg) => cat_error(msg, message("The error(s) above occurred")) }
- }
- else error(message("Missing executable"))
- }
-
val digests1 = List(doc.print, document_logo.toString, document_build).map(SHA1.digest)
val digests2 = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest)
val sources = SHA1.digest_set(digests1 ::: digests2)
--- a/src/Pure/Thy/presentation.scala Tue Nov 09 16:17:13 2021 +0100
+++ b/src/Pure/Thy/presentation.scala Tue Nov 09 19:47:24 2021 +0100
@@ -20,12 +20,11 @@
sealed case class HTML_Document(title: String, content: String)
- def html_context(): HTML_Context = new HTML_Context
+ def html_context(cache: Term.Cache = Term.Cache.make()): HTML_Context =
+ new HTML_Context(cache)
- final class HTML_Context private[Presentation]
+ final class HTML_Context private[Presentation](val cache: Term.Cache)
{
- val term_cache: Term.Cache = Term.Cache.make()
-
private val already_presented = Synchronized(Set.empty[String])
def register_presented(nodes: List[Document.Node.Name]): List[Document.Node.Name] =
already_presented.change_result(presented =>
@@ -407,8 +406,10 @@
doc <- info.document_variants
document <- db_context.input_database(session)(Document_Build.read_document(_, _, doc.name))
} yield {
+ val doc_path = (session_dir + doc.path.pdf).expand
if (verbose) progress.echo("Presenting document " + session + "/" + doc.name)
- Bytes.write(session_dir + doc.path.pdf, document.pdf)
+ if (options.bool("document_echo")) progress.echo("Document at " + doc_path)
+ Bytes.write(doc_path, document.pdf)
doc
}
@@ -446,7 +447,7 @@
val provider = Export.Provider.database_context(db_context, hierarchy, thy_name)
if (Export_Theory.read_theory_parents(provider, thy_name).isDefined) {
Export_Theory.read_theory(
- provider, session, thy_name, cache = html_context.term_cache)
+ provider, session, thy_name, cache = html_context.cache)
}
else Export_Theory.no_theory
})
--- a/src/Pure/Thy/sessions.scala Tue Nov 09 16:17:13 2021 +0100
+++ b/src/Pure/Thy/sessions.scala Tue Nov 09 19:47:24 2021 +0100
@@ -1212,7 +1212,7 @@
val store: Sessions.Store,
database_server: Option[SQL.Database]) extends AutoCloseable
{
- def cache: XML.Cache = store.cache
+ def cache: Term.Cache = store.cache
def close(): Unit = database_server.foreach(_.close())
@@ -1267,10 +1267,10 @@
}
}
- def store(options: Options, cache: XML.Cache = XML.Cache.make()): Store =
+ def store(options: Options, cache: Term.Cache = Term.Cache.make()): Store =
new Store(options, cache)
- class Store private[Sessions](val options: Options, val cache: XML.Cache)
+ class Store private[Sessions](val options: Options, val cache: Term.Cache)
{
store =>
--- a/src/Pure/Tools/build.scala Tue Nov 09 16:17:13 2021 +0100
+++ b/src/Pure/Tools/build.scala Tue Nov 09 19:47:24 2021 +0100
@@ -507,7 +507,7 @@
}
val resources = Resources.empty
- val html_context = Presentation.html_context()
+ val html_context = Presentation.html_context(cache = store.cache)
using(store.open_database_context())(db_context =>
for (info <- presentation_sessions) {
--- a/src/Pure/Tools/build_job.scala Tue Nov 09 16:17:13 2021 +0100
+++ b/src/Pure/Tools/build_job.scala Tue Nov 09 19:47:24 2021 +0100
@@ -241,7 +241,7 @@
new Resources(sessions_structure, base, log = log, command_timings = command_timings0)
val session =
new Session(options, resources) {
- override val cache: XML.Cache = store.cache
+ override val cache: Term.Cache = store.cache
override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info =
{
--- a/src/Pure/Tools/scala_project.scala Tue Nov 09 16:17:13 2021 +0100
+++ b/src/Pure/Tools/scala_project.scala Tue Nov 09 19:47:24 2021 +0100
@@ -12,7 +12,7 @@
{
/* Maven project */
- def java_version: String = "11"
+ def java_version: String = "15"
def scala_version: String = scala.util.Properties.versionNumberString
def maven_project(jars: List[Path]): String =
--- a/src/Pure/term.scala Tue Nov 09 16:17:13 2021 +0100
+++ b/src/Pure/term.scala Tue Nov 09 19:47:24 2021 +0100
@@ -200,15 +200,16 @@
object Cache
{
def make(
+ xz: XZ.Cache = XZ.Cache.make(),
max_string: Int = isabelle.Cache.default_max_string,
initial_size: Int = isabelle.Cache.default_initial_size): Cache =
- new Cache(initial_size, max_string)
+ new Cache(xz, initial_size, max_string)
val none: Cache = make(max_string = 0)
}
- class Cache private[Term](max_string: Int, initial_size: Int)
- extends isabelle.Cache(max_string, initial_size)
+ class Cache(xz: XZ.Cache, max_string: Int, initial_size: Int)
+ extends XML.Cache(xz, max_string, initial_size)
{
protected def cache_indexname(x: Indexname): Indexname =
lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index))
--- a/src/Tools/Setup/src/Build.java Tue Nov 09 16:17:13 2021 +0100
+++ b/src/Tools/Setup/src/Build.java Tue Nov 09 19:47:24 2021 +0100
@@ -69,7 +69,7 @@
for (String p : Environment.getenv("ISABELLE_COMPONENTS").split(":", -1)) {
if (!p.isEmpty()) {
Path dir = Path.of(Environment.platform_path(p));
- if (Files.exists(dir.resolve(COMPONENT_BUILD_PROPS))) {
+ if (Files.isRegularFile(dir.resolve(COMPONENT_BUILD_PROPS))) {
result.add(component_context(dir));
}
}
@@ -151,11 +151,6 @@
{
return _dir.resolve(Environment.expand_platform_path(file));
}
- public boolean exists(String file)
- throws IOException, InterruptedException
- {
- return Files.exists(path(file));
- }
public List<Path> requirement_paths(String s)
throws IOException, InterruptedException
@@ -190,12 +185,12 @@
{
MessageDigest sha = MessageDigest.getInstance("SHA");
for (Path file : paths) {
- if (Files.exists(file)) {
+ if (Files.isRegularFile(file)) {
sha.update(Files.readAllBytes(file));
}
else {
throw new RuntimeException(
- error_message("Missing input file " + Library.quote(file.toString())));
+ error_message("Bad input file " + Library.quote(file.toString())));
}
}
return sha_digest(sha, name);
@@ -338,7 +333,7 @@
public static List<String> get_services(Path jar_path)
throws IOException
{
- if (Files.exists(jar_path)) {
+ if (Files.isRegularFile(jar_path)) {
try (JarFile jar_file = new JarFile(jar_path.toFile()))
{
JarEntry entry = jar_file.getJarEntry(SERVICES);