--- a/Admin/components/bundled-windows Sun Mar 16 12:03:39 2025 +0000
+++ b/Admin/components/bundled-windows Sun Mar 16 12:03:47 2025 +0000
@@ -1,3 +1,3 @@
#additional components to be bundled for release
cygwin-20250109
-windows_app-20240205
+windows_app-20250315
--- a/Admin/components/components.sha1 Sun Mar 16 12:03:39 2025 +0000
+++ b/Admin/components/components.sha1 Sun Mar 16 12:03:47 2025 +0000
@@ -607,6 +607,7 @@
4883f93efb27ae51fb2cc0e1f52309728f2dc407 windows_app-20240202.tar.gz
5269b9e38fe58be10272d6817dbfd08b67b312e7 windows_app-20240204.tar.gz
94fecdab25ddc52b5afde4ab3f017a3c14c656c8 windows_app-20240205.tar.gz
+e30e8a802bcae22b6bf0e5ca79677cbef0c1fa6b windows_app-20250315.tar.gz
76ff3ea91d3c781507e6998d9e819ae3564cf495 xz-java-1.10.tar.gz
1c36a840320dfa9bac8af25fc289a4df5ea3eccb xz-java-1.2-1.tar.gz
2ae13aa17d0dc95ce254a52f1dba10929763a10d xz-java-1.2.tar.gz
--- a/NEWS Sun Mar 16 12:03:39 2025 +0000
+++ b/NEWS Sun Mar 16 12:03:47 2025 +0000
@@ -16,18 +16,25 @@
monotone_on_inf_fun
monotone_on_sup_fun
-* Theory "HOL.Relations":
+* Theory "HOL.Relation":
- Changed definition of predicate refl_on to not constrain the domain
and range of the relation. To get the old semantics, explicitely use
the formula "r \<subset> A \<times> A \<and> refl_on A r". INCOMPATIBILITY.
+ - Removed predicate single_valuedp. Use predicate right_unique instead.
+ INCOMPATIBILITY.
- Strengthened lemmas. Minor INCOMPATIBILITY.
refl_on_empty[simp]
- Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
antisymp_equality[simp] ~> antisymp_on_equality[simp]
transp_equality[simp] ~> transp_on_equality[simp]
- Added lemmas.
+ left_unique_iff_Uniq
reflp_on_refl_on_eq[pred_set_conv]
symp_on_equality[simp]
+ totalp_on_mono[mono]
+ totalp_on_mono_strong
+ totalp_on_mono_stronger
+ totalp_on_mono_stronger_alt
* Theory "HOL.Wellfounded":
- Added lemmas.
@@ -52,6 +59,15 @@
- Added lemmas.
quotient_disj_strong
+* Theory "HOL.Transfer":
+ - Moved predicates left_unique and right_unique from HOL.Transfer to
+ HOL.Relation. Minor INCOMPATIBILITY.
+ - Removed lemmas. Minor INCOMPATIBILITY.
+ left_unique_iff (use left_unique_iff_Uniq instead)
+ right_unique_iff (use right_unique_iff_Uniq instead)
+ - Added lemmas.
+ single_valuedp_eq_right_unique
+
* Theory "HOL-Library.Multiset":
- Renamed lemmas. Minor INCOMPATIBILITY.
filter_image_mset ~> filter_mset_image_mset
--- a/src/HOL/Relation.thy Sun Mar 16 12:03:39 2025 +0000
+++ b/src/HOL/Relation.thy Sun Mar 16 12:03:47 2025 +0000
@@ -788,11 +788,59 @@
lemma totalpD: "totalp R \<Longrightarrow> x \<noteq> y \<Longrightarrow> R x y \<or> R y x"
by (simp add: totalp_onD)
+lemma totalp_on_mono_stronger:
+ fixes
+ A :: "'a set" and R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and
+ B :: "'b set" and Q :: "'b \<Rightarrow> 'b \<Rightarrow> bool" and
+ f :: "'a \<Rightarrow> 'b"
+ assumes "totalp_on B Q" and "f ` A \<subseteq> B" and
+ Q_imp_R: "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> Q (f x) (f y) \<Longrightarrow> R x y" and
+ inj_f: "inj_on f A"
+ shows "totalp_on A R"
+proof (rule totalp_onI)
+ fix x y :: 'a
+ assume "x \<in> A" and "y \<in> A" and "x \<noteq> y"
+ hence "f x \<in> B" and "f y \<in> B" and "f x \<noteq> f y"
+ using \<open>f ` A \<subseteq> B\<close> inj_f by (auto dest: inj_onD)
+ hence "Q (f x) (f y) \<or> Q (f y) (f x)"
+ using \<open>totalp_on B Q\<close> by (iprover dest: totalp_onD)
+ thus "R x y \<or> R y x"
+ using Q_imp_R \<open>x \<in> A\<close> \<open>y \<in> A\<close> by iprover
+qed
+
+lemma totalp_on_mono_stronger_alt:
+ fixes
+ A :: "'a set" and R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and
+ B :: "'b set" and Q :: "'b \<Rightarrow> 'b \<Rightarrow> bool" and
+ f :: "'b \<Rightarrow> 'a"
+ assumes "totalp_on B Q" and "A \<subseteq> f ` B" and
+ Q_imp_R: "\<And>x y. x \<in> B \<Longrightarrow> y \<in> B \<Longrightarrow> Q x y \<Longrightarrow> R (f x) (f y)"
+ shows "totalp_on A R"
+proof (rule totalp_onI)
+ fix x y :: 'a
+ assume "x \<in> A" and "y \<in> A" and "x \<noteq> y"
+ then obtain x' y' where "x' \<in> B" and "x = f x'" and "y' \<in> B" and "y = f y'" and "x' \<noteq> y'"
+ using \<open>A \<subseteq> f ` B\<close> by blast
+ hence "Q x' y' \<or> Q y' x'"
+ using \<open>totalp_on B Q\<close>[THEN totalp_onD] by blast
+ hence "R (f x') (f y') \<or> R (f y') (f x')"
+ using Q_imp_R \<open>x' \<in> B\<close> \<open>y' \<in> B\<close> by blast
+ thus "R x y \<or> R y x"
+ using \<open>x = f x'\<close> \<open>y = f y'\<close> by blast
+qed
+
+lemma totalp_on_mono_strong:
+ "totalp_on B Q \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> Q x y \<Longrightarrow> R x y) \<Longrightarrow> totalp_on A R"
+ using totalp_on_mono_stronger[of B Q "\<lambda>x. x" A R, simplified] .
+
+lemma totalp_on_mono[mono]: "A \<subseteq> B \<Longrightarrow> Q \<le> R \<Longrightarrow> totalp_on B Q \<le> totalp_on A R"
+ by (auto intro: totalp_on_mono_strong)
+
lemma total_on_subset: "total_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> total_on B r"
by (auto simp: total_on_def)
lemma totalp_on_subset: "totalp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> totalp_on B R"
- by (auto intro: totalp_onI dest: totalp_onD)
+ using totalp_on_mono_strong .
lemma totalp_on_image:
assumes "inj_on f A"
@@ -824,52 +872,63 @@
by (rule totalp_onI, rule linear)
-subsubsection \<open>Single valued relations\<close>
+subsubsection \<open>Left uniqueness\<close>
+
+definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
+ "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
+
+lemma left_uniqueI: "(\<And>x y z. A x z \<Longrightarrow> A y z \<Longrightarrow> x = y) \<Longrightarrow> left_unique A"
+ unfolding left_unique_def by blast
+
+lemma left_uniqueD: "left_unique A \<Longrightarrow> A x z \<Longrightarrow> A y z \<Longrightarrow> x = y"
+ unfolding left_unique_def by blast
+
+lemma left_unique_iff_Uniq: "left_unique r \<longleftrightarrow> (\<forall>y. \<exists>\<^sub>\<le>\<^sub>1x. r x y)"
+ unfolding Uniq_def left_unique_def by blast
+
+
+subsubsection \<open>Right uniqueness\<close>
definition single_valued :: "('a \<times> 'b) set \<Rightarrow> bool"
where "single_valued r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z))"
-definition single_valuedp :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
- where "single_valuedp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> (\<forall>z. r x z \<longrightarrow> y = z))"
+definition right_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
+ "right_unique R \<longleftrightarrow> (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z)"
-lemma single_valuedp_single_valued_eq [pred_set_conv]:
- "single_valuedp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> single_valued r"
- by (simp add: single_valued_def single_valuedp_def)
+lemma right_unique_single_valued_eq [pred_set_conv]:
+ "right_unique (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> single_valued r"
+ by (simp add: single_valued_def right_unique_def)
-lemma single_valuedp_iff_Uniq:
- "single_valuedp r \<longleftrightarrow> (\<forall>x. \<exists>\<^sub>\<le>\<^sub>1y. r x y)"
- unfolding Uniq_def single_valuedp_def by auto
+lemma right_unique_iff_Uniq:
+ "right_unique r \<longleftrightarrow> (\<forall>x. \<exists>\<^sub>\<le>\<^sub>1y. r x y)"
+ unfolding Uniq_def right_unique_def by auto
lemma single_valuedI:
"(\<And>x y. (x, y) \<in> r \<Longrightarrow> (\<And>z. (x, z) \<in> r \<Longrightarrow> y = z)) \<Longrightarrow> single_valued r"
unfolding single_valued_def by blast
-lemma single_valuedpI:
- "(\<And>x y. r x y \<Longrightarrow> (\<And>z. r x z \<Longrightarrow> y = z)) \<Longrightarrow> single_valuedp r"
- by (fact single_valuedI [to_pred])
+lemma right_uniqueI: "(\<And>x y z. R x y \<Longrightarrow> R x z \<Longrightarrow> y = z) \<Longrightarrow> right_unique R"
+ unfolding right_unique_def by fast
lemma single_valuedD:
"single_valued r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (x, z) \<in> r \<Longrightarrow> y = z"
by (simp add: single_valued_def)
-lemma single_valuedpD:
- "single_valuedp r \<Longrightarrow> r x y \<Longrightarrow> r x z \<Longrightarrow> y = z"
- by (fact single_valuedD [to_pred])
+lemma right_uniqueD: "right_unique R \<Longrightarrow> R x y \<Longrightarrow> R x z \<Longrightarrow> y = z"
+ unfolding right_unique_def by fast
lemma single_valued_empty [simp]:
"single_valued {}"
by (simp add: single_valued_def)
-lemma single_valuedp_bot [simp]:
- "single_valuedp \<bottom>"
- by (fact single_valued_empty [to_pred])
+lemma right_unique_bot[simp]: "right_unique \<bottom>"
+ by (fact single_valued_empty[to_pred])
lemma single_valued_subset:
"r \<subseteq> s \<Longrightarrow> single_valued s \<Longrightarrow> single_valued r"
unfolding single_valued_def by blast
-lemma single_valuedp_less_eq:
- "r \<le> s \<Longrightarrow> single_valuedp s \<Longrightarrow> single_valuedp r"
+lemma right_unique_less_eq: "r \<le> s \<Longrightarrow> right_unique s \<Longrightarrow> right_unique r"
by (fact single_valued_subset [to_pred])
@@ -1224,6 +1283,12 @@
lemma totalp_on_converse [simp]: "totalp_on A R\<inverse>\<inverse> = totalp_on A R"
by (rule total_on_converse[to_pred])
+lemma left_unique_conversep[simp]: "left_unique A\<inverse>\<inverse> \<longleftrightarrow> right_unique A"
+ by (auto simp add: left_unique_def right_unique_def)
+
+lemma right_unique_conversep[simp]: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A"
+ by (auto simp add: left_unique_def right_unique_def)
+
lemma conversep_noteq [simp]: "(\<noteq>)\<inverse>\<inverse> = (\<noteq>)"
by (auto simp add: fun_eq_iff)
--- a/src/HOL/Transfer.thy Sun Mar 16 12:03:39 2025 +0000
+++ b/src/HOL/Transfer.thy Sun Mar 16 12:03:47 2025 +0000
@@ -106,18 +106,14 @@
subsection \<open>Predicates on relations, i.e. ``class constraints''\<close>
+text \<open>See also \<^const>\<open>Relation.left_unique\<close> and \<^const>\<open>Relation.right_unique\<close>.\<close>
+
definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)"
-definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
- where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
-
definition right_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
where "right_total R \<longleftrightarrow> (\<forall>y. \<exists>x. R x y)"
-definition right_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
- where "right_unique R \<longleftrightarrow> (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z)"
-
definition bi_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
where "bi_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y) \<and> (\<forall>y. \<exists>x. R x y)"
@@ -126,15 +122,6 @@
(\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and>
(\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
-lemma left_unique_iff: "left_unique R \<longleftrightarrow> (\<forall>z. \<exists>\<^sub>\<le>\<^sub>1x. R x z)"
- unfolding Uniq_def left_unique_def by force
-
-lemma left_uniqueI: "(\<And>x y z. \<lbrakk> A x z; A y z \<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> left_unique A"
-unfolding left_unique_def by blast
-
-lemma left_uniqueD: "\<lbrakk> left_unique A; A x z; A y z \<rbrakk> \<Longrightarrow> x = y"
-unfolding left_unique_def by blast
-
lemma left_totalI:
"(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R"
unfolding left_total_def by blast
@@ -153,15 +140,6 @@
lemma bi_unique_iff: "bi_unique R \<longleftrightarrow> (\<forall>z. \<exists>\<^sub>\<le>\<^sub>1x. R x z) \<and> (\<forall>z. \<exists>\<^sub>\<le>\<^sub>1x. R z x)"
unfolding Uniq_def bi_unique_def by force
-lemma right_unique_iff: "right_unique R \<longleftrightarrow> (\<forall>z. \<exists>\<^sub>\<le>\<^sub>1x. R z x)"
- unfolding Uniq_def right_unique_def by force
-
-lemma right_uniqueI: "(\<And>x y z. \<lbrakk> A x y; A x z \<rbrakk> \<Longrightarrow> y = z) \<Longrightarrow> right_unique A"
-unfolding right_unique_def by fast
-
-lemma right_uniqueD: "\<lbrakk> right_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
-unfolding right_unique_def by fast
-
lemma right_totalI: "(\<And>y. \<exists>x. A x y) \<Longrightarrow> right_total A"
by(simp add: right_total_def)
@@ -204,11 +182,6 @@
unfolding bi_unique_def rel_fun_def by auto
lemma [simp]:
- shows left_unique_conversep: "left_unique A\<inverse>\<inverse> \<longleftrightarrow> right_unique A"
- and right_unique_conversep: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A"
- by(auto simp add: left_unique_def right_unique_def)
-
-lemma [simp]:
shows left_total_conversep: "left_total A\<inverse>\<inverse> \<longleftrightarrow> right_total A"
and right_total_conversep: "right_total A\<inverse>\<inverse> \<longleftrightarrow> left_total A"
by(simp_all add: left_total_def right_total_def)
--- a/src/Pure/Admin/build_release.scala Sun Mar 16 12:03:39 2025 +0000
+++ b/src/Pure/Admin/build_release.scala Sun Mar 16 12:03:47 2025 +0000
@@ -828,7 +828,9 @@
progress.echo("Packaging " + archive_name + " ...")
execute(tmp_dir,
- "7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name))
+ File.bash_path(Component_Windows_App.seven_zip(exe = true)) +
+ " -myv=1602 -y -bd a " + File.bash_path(exe_archive) + " " +
+ Bash.string(isabelle_name))
if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive)
val sfx_exe = tmp_dir + Component_Windows_App.sfx_path
@@ -950,9 +952,6 @@
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
- if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
- error("Building for windows requires 7z")
-
val progress = new Console_Progress()
def make_context(name: String): Release_Context =
Release_Context(target_dir, release_name = name, progress = progress)
--- a/src/Pure/Admin/component_windows_app.scala Sun Mar 16 12:03:39 2025 +0000
+++ b/src/Pure/Admin/component_windows_app.scala Sun Mar 16 12:03:47 2025 +0000
@@ -15,11 +15,19 @@
Isabelle_Platform.self.ISABELLE_PLATFORM64
}
- def launch4j_jar(): Path =
- Path.explode("windows_app/" + tool_platform() + "/launch4j.jar")
+ def tool_platform_path(): Path = Path.basic(tool_platform())
+
+ val base_path: Path = Path.basic("windows_app")
+
+ def launch4j_jar(base: Path = base_path): Path =
+ base + tool_platform_path() + Path.basic("launch4j.jar")
+
+ def seven_zip(base: Path = base_path, exe: Boolean = false): Path =
+ base + tool_platform_path() + Path.basic("7zip") +
+ (if (exe) Path.basic("7zz") else Path.current)
val sfx_name = "7zsd_All_x64.sfx"
- val sfx_path: Path = Path.basic("windows_app") + Path.basic(sfx_name)
+ val sfx_path: Path = base_path + Path.basic(sfx_name)
val sfx_txt =
""";!@Install@!UTF-8!
@@ -35,6 +43,19 @@
"""
+ /* 7zip platform downloads */
+
+ sealed case class Seven_Zip_Platform(name: String, url_template: String) {
+ def url(version: String): String = url_template.replace("{V}", version)
+ }
+
+ private val seven_zip_platforms: List[Seven_Zip_Platform] =
+ List(
+ Seven_Zip_Platform("arm64-linux", "https://www.7-zip.org/a/7z{V}-linux-arm64.tar.xz"),
+ Seven_Zip_Platform("x86_64-darwin", "https://www.7-zip.org/a/7z{V}-mac.tar.xz"),
+ Seven_Zip_Platform("x86_64-linux", "https://www.7-zip.org/a/7z{V}-linux-x64.tar.xz"))
+
+
/* build windows_app */
val default_launch4j_url =
@@ -46,15 +67,16 @@
val default_sfx_url =
"https://github.com/chrislake/7zsfxmm/releases/download/1.7.1.3901/7zsd_extra_171_3901.7z"
+ val default_seven_zip_version = "2409"
+
def build_windows_app(
launch4j_url: String = default_launch4j_url,
binutils_url: String = default_binutils_url,
sfx_url: String = default_sfx_url,
+ seven_zip_version: String = default_seven_zip_version,
progress: Progress = new Progress,
target_dir: Path = Path.current
): Unit = {
- Isabelle_System.require_command("7z", test = "")
-
val platform_name = tool_platform()
Isabelle_System.with_tmp_dir("build") { tmp_dir =>
@@ -97,13 +119,29 @@
}
+ /* 7zip tool */
+
+ seven_zip_platforms.find(platform => platform.name == platform_name) match {
+ case Some(platform) =>
+ val url = platform.url(seven_zip_version)
+ val name = Url.get_base_name(url).getOrElse(error("No base name in " + quote(url)))
+ val download = tmp_dir + Path.basic(name)
+ Isabelle_System.download_file(url, download, progress = progress)
+ Isabelle_System.extract(download,
+ Isabelle_System.make_directory(seven_zip(base = component_dir.path)))
+ case None => error("No 7zip for platform " + quote(platform_name))
+ }
+
+
/* 7zip sfx module */
val sfx_archive_name = Url.get_base_name(sfx_url).get
Isabelle_System.download_file(sfx_url,
tmp_dir + Path.basic(sfx_archive_name), progress = progress)
- Isabelle_System.bash("7z x " + Bash.string(sfx_archive_name), cwd = tmp_dir).check
+ Isabelle_System.bash(
+ File.bash_path(seven_zip(base = component_dir.path, exe = true)) + " x " +
+ Bash.string(sfx_archive_name), cwd = tmp_dir).check
Isabelle_System.copy_file(tmp_dir + Path.basic(sfx_name), component_dir.path)
@@ -153,6 +191,7 @@
var launch4j_url = default_launch4j_url
var binutils_url = default_binutils_url
var sfx_url = default_sfx_url
+ var seven_zip_version = default_seven_zip_version
var verbose = false
val getopts = Getopts("""
@@ -167,6 +206,7 @@
""" + default_binutils_url + """
-W URL download URL for 7zip sfx module, default:
""" + default_sfx_url + """
+ -X VERSION version for 7zip download (default: """ + default_seven_zip_version + """)
-v verbose
Build Isabelle windows_app component from GNU binutils and launch4j.
@@ -175,6 +215,7 @@
"U:" -> (arg => launch4j_url = arg),
"V:" -> (arg => binutils_url = arg),
"W:" -> (arg => sfx_url = arg),
+ "X:" -> (arg => seven_zip_version = arg),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
@@ -183,6 +224,7 @@
val progress = new Console_Progress(verbose = verbose)
build_windows_app(launch4j_url = launch4j_url, binutils_url = binutils_url,
- sfx_url = sfx_url, progress = progress, target_dir = target_dir)
+ sfx_url = sfx_url, seven_zip_version = seven_zip_version,
+ progress = progress, target_dir = target_dir)
})
}
--- a/src/Pure/General/file.scala Sun Mar 16 12:03:39 2025 +0000
+++ b/src/Pure/General/file.scala Sun Mar 16 12:03:47 2025 +0000
@@ -104,6 +104,7 @@
def is_scala(s: String): Boolean = s.endsWith(".scala")
def is_tar_bz2(s: String): Boolean = s.endsWith(".tar.bz2")
def is_tar_gz(s: String): Boolean = s.endsWith(".tar.gz")
+ def is_tar_xz(s: String): Boolean = s.endsWith(".tar.xz")
def is_tgz(s: String): Boolean = s.endsWith(".tgz")
def is_thy(s: String): Boolean = s.endsWith(".thy")
def is_xz(s: String): Boolean = s.endsWith(".xz")
--- a/src/Pure/System/isabelle_system.scala Sun Mar 16 12:03:39 2025 +0000
+++ b/src/Pure/System/isabelle_system.scala Sun Mar 16 12:03:47 2025 +0000
@@ -487,11 +487,17 @@
} Files.setLastModifiedTime(res, t)
}
}
- else if (File.is_tar_bz2(name) || File.is_tgz(name) || File.is_tar_gz(name)) {
- val flags = if (File.is_tar_bz2(name)) "-xjf " else "-xzf "
- Isabelle_System.gnutar(flags + File.bash_path(archive), dir = dir, strip = strip).check
+ else {
+ val extr =
+ if (File.is_tar_bz2(name)) "-xjf"
+ else if (File.is_tgz(name) || File.is_tar_gz(name)) "-xzf"
+ else if (File.is_tar_xz(name)) "--xz -xf"
+ else ""
+ if (extr.nonEmpty) {
+ Isabelle_System.gnutar(extr + " " + File.bash_path(archive), dir = dir, strip = strip).check
+ }
+ else error("Cannot extract " + archive)
}
- else error("Cannot extract " + archive)
}
def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = {