--- a/Admin/components/bundled-windows Sat Mar 15 10:39:45 2025 +0100
+++ b/Admin/components/bundled-windows Sat Mar 15 14:39:45 2025 +0100
@@ -1,3 +1,3 @@
#additional components to be bundled for release
cygwin-20250109
-windows_app-20240205
+windows_app-20250315
--- a/Admin/components/components.sha1 Sat Mar 15 10:39:45 2025 +0100
+++ b/Admin/components/components.sha1 Sat Mar 15 14:39:45 2025 +0100
@@ -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/src/Pure/Admin/build_release.scala Sat Mar 15 10:39:45 2025 +0100
+++ b/src/Pure/Admin/build_release.scala Sat Mar 15 14:39:45 2025 +0100
@@ -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 Sat Mar 15 10:39:45 2025 +0100
+++ b/src/Pure/Admin/component_windows_app.scala Sat Mar 15 14:39:45 2025 +0100
@@ -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 Sat Mar 15 10:39:45 2025 +0100
+++ b/src/Pure/General/file.scala Sat Mar 15 14:39:45 2025 +0100
@@ -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 Sat Mar 15 10:39:45 2025 +0100
+++ b/src/Pure/System/isabelle_system.scala Sat Mar 15 14:39:45 2025 +0100
@@ -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 = {