# HG changeset patch # User wenzelm # Date 1742045985 -3600 # Node ID 295a36401d88155514a4f1eef4be34cdb5dd14fb # Parent c17902fcf5e7996aa46e3ca855a8c02d751baabe# Parent 1a8aa332548b7f55e83d1da48572926525cf1cc5 merged diff -r c17902fcf5e7 -r 295a36401d88 Admin/components/bundled-windows --- 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 diff -r c17902fcf5e7 -r 295a36401d88 Admin/components/components.sha1 --- 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 diff -r c17902fcf5e7 -r 295a36401d88 src/Pure/Admin/build_release.scala --- 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) diff -r c17902fcf5e7 -r 295a36401d88 src/Pure/Admin/component_windows_app.scala --- 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) }) } diff -r c17902fcf5e7 -r 295a36401d88 src/Pure/General/file.scala --- 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") diff -r c17902fcf5e7 -r 295a36401d88 src/Pure/System/isabelle_system.scala --- 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 = {