--- a/src/Pure/Admin/build_csdp.scala Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/Admin/build_csdp.scala Wed Nov 30 15:03:31 2022 +0100
@@ -95,12 +95,11 @@
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download_file(download_url, archive_path, progress = progress)
- Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
- val source_dir = File.get_dir(tmp_dir, title = archive_name)
+ Isabelle_System.extract(archive_path, tmp_dir)
+ val source_dir = File.get_dir(tmp_dir, title = download_url)
- Isabelle_System.bash(
- "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src",
- cwd = component_dir.path.file).check
+ Isabelle_System.extract(archive_path, component_dir.path)
+ Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src)
/* build */
--- a/src/Pure/Admin/build_e.scala Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/Admin/build_e.scala Wed Nov 30 15:03:31 2022 +0100
@@ -41,35 +41,35 @@
val archive_path = tmp_dir + Path.explode("E.tgz")
Isabelle_System.download_file(archive_url, archive_path, progress = progress)
- Isabelle_System.bash("tar xzf " + archive_path, cwd = tmp_dir.file).check
- Isabelle_System.bash("tar xzf " + archive_path + " && mv E src",
- cwd = component_dir.path.file).check
+ Isabelle_System.extract(archive_path, tmp_dir)
+ val source_dir = File.get_dir(tmp_dir, title = archive_url)
+
+ Isabelle_System.extract(archive_path, component_dir.path)
+ Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src)
/* build */
progress.echo("Building E prover for " + platform_name + " ...")
- val build_dir = tmp_dir + Path.basic("E")
val build_options = {
- val result = Isabelle_System.bash("./configure --help", cwd = build_dir.file)
+ val result = Isabelle_System.bash("./configure --help", cwd = source_dir.file)
if (result.check.out.containsSlice("--enable-ho")) " --enable-ho" else ""
}
val build_script = "./configure" + build_options + " && make"
- Isabelle_System.bash(build_script,
- cwd = build_dir.file,
+ Isabelle_System.bash(build_script, cwd = source_dir.file,
progress_stdout = progress.echo_if(verbose, _),
progress_stderr = progress.echo_if(verbose, _)).check
/* install */
- Isabelle_System.copy_file(build_dir + Path.basic("COPYING"), component_dir.LICENSE)
+ Isabelle_System.copy_file(source_dir + Path.basic("COPYING"), component_dir.LICENSE)
val install_files = List("epclextract", "eprover", "eprover-ho")
for (name <- install_files ::: install_files.map(_ + ".exe")) {
- val path = build_dir + Path.basic("PROVER") + Path.basic(name)
+ val path = source_dir + Path.basic("PROVER") + Path.basic(name)
if (path.is_file) Isabelle_System.copy_file(path, platform_dir)
}
Isabelle_System.bash("if [ -f eprover-ho ]; then mv eprover-ho eprover; fi",
--- a/src/Pure/Admin/build_jedit.scala Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/Admin/build_jedit.scala Wed Nov 30 15:03:31 2022 +0100
@@ -143,7 +143,7 @@
File.bash_platform_path(jedit_dir) + " unix-script=off unix-man=off").check
val source_path = download_jedit(tmp_dir, "source.tar.bz2")
- Isabelle_System.gnutar("-xjf " + File.bash_path(source_path), dir = jedit_dir).check
+ Isabelle_System.extract(source_path, jedit_dir)
/* patched version */
--- a/src/Pure/Admin/build_lipics.scala Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/Admin/build_lipics.scala Wed Nov 30 15:03:31 2022 +0100
@@ -36,8 +36,7 @@
/* download */
Isabelle_System.download_file(download_url, download_file, progress = progress)
- Isabelle_System.gnutar("-xzf " + File.bash_path(download_file),
- dir = download_dir, strip = 1).check
+ Isabelle_System.extract(download_file, download_dir, strip = true)
val lipics_dir = download_dir + Path.explode("LIPIcs/authors")
--- a/src/Pure/Admin/build_minisat.scala Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/Admin/build_minisat.scala Wed Nov 30 15:03:31 2022 +0100
@@ -60,12 +60,11 @@
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download_file(download_url, archive_path, progress = progress)
- Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
+ Isabelle_System.extract(archive_path, tmp_dir)
val source_dir = File.get_dir(tmp_dir, title = download_url)
- Isabelle_System.bash(
- "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src",
- cwd = component_dir.path.file).check
+ Isabelle_System.extract(archive_path, component_dir.path)
+ Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src)
/* build */
--- a/src/Pure/Admin/build_release.scala Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/Admin/build_release.scala Wed Nov 30 15:03:31 2022 +0100
@@ -13,7 +13,7 @@
private def execute(dir: Path, script: String): Unit =
Isabelle_System.bash(script, cwd = dir.file).check
- private def execute_tar(dir: Path, args: String, strip: Int = 0): Process_Result =
+ private def execute_tar(dir: Path, args: String, strip: Boolean = false): Process_Result =
Isabelle_System.gnutar(args, dir = dir, strip = strip).check
private def bash_java_opens(args: String*): String =
@@ -107,7 +107,7 @@
val isabelle_dir = Isabelle_System.make_directory(dir + ISABELLE)
Bytes.write(archive_path, bytes)
- execute_tar(isabelle_dir, "-xzf " + File.bash_path(archive_path), strip = 1)
+ execute_tar(isabelle_dir, "-xzf " + File.bash_path(archive_path), strip = true)
val id = File.read(isabelle_dir + ISABELLE_ID)
val tags = File.read(isabelle_dir + ISABELLE_TAGS)
--- a/src/Pure/Admin/build_scala.scala Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/Admin/build_scala.scala Wed Nov 30 15:03:31 2022 +0100
@@ -28,12 +28,11 @@
def get(path: Path, progress: Progress = new Progress): Unit =
Isabelle_System.download_file(proper_url, path, progress = progress)
- def get_unpacked(dir: Path, strip: Int = 0, progress: Progress = new Progress): Unit =
- Isabelle_System.with_tmp_file("archive"){ archive_path =>
+ def get_unpacked(dir: Path, strip: Boolean = false, progress: Progress = new Progress): Unit =
+ Isabelle_System.with_tmp_file("archive", ext = "tar.gz"){ archive_path =>
get(archive_path, progress = progress)
progress.echo("Unpacking " + artifact)
- Isabelle_System.gnutar(
- "-xzf " + File.bash_path(archive_path), dir = dir, strip = strip).check
+ Isabelle_System.extract(archive_path, dir, strip = strip)
}
def print: String =
@@ -77,7 +76,7 @@
/* download */
- main_download.get_unpacked(component_dir.path, strip = 1, progress = progress)
+ main_download.get_unpacked(component_dir.path, strip = true, progress = progress)
lib_downloads.foreach(download =>
download.get(component_dir.lib + Path.basic(download.artifact), progress = progress))
--- a/src/Pure/Admin/build_spass.scala Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/Admin/build_spass.scala Wed Nov 30 15:03:31 2022 +0100
@@ -29,9 +29,9 @@
val Component_Name = """^(.+)-src\.tar.gz$""".r
val Version = """^[^-]+-([^-]+)$""".r
- val (archive_name, archive_base_name) =
+ val archive_name =
download_url match {
- case Archive_Name(name) => (name, Library.perhaps_unsuffix(".tar.gz", name))
+ case Archive_Name(name) => name
case _ => error("Failed to determine source archive name from " + quote(download_url))
}
@@ -67,38 +67,36 @@
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download_file(download_url, archive_path, progress = progress)
- Isabelle_System.bash("tar xzf " + archive_path, cwd = tmp_dir.file).check
- Isabelle_System.bash(
- "tar xzf " + archive_path + " && mv " + Bash.string(archive_base_name) + " src",
- cwd = component_dir.path.file).check
+ Isabelle_System.extract(archive_path, tmp_dir)
+ val source_dir = File.get_dir(tmp_dir, title = download_url)
+
+ Isabelle_System.extract(archive_path, component_dir.path)
+ Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src)
/* build */
progress.echo("Building SPASS for " + platform_name + " ...")
- val build_dir = tmp_dir + Path.basic(archive_base_name)
-
if (Platform.is_windows) {
- File.change(build_dir + Path.basic("misc.c")) {
+ File.change(source_dir + Path.basic("misc.c")) {
_.replace("""#include "execinfo.h" """, "")
.replaceAll("""void misc_DumpCore\(void\)[^}]+}""", "void misc_DumpCore(void) { abort(); }")
}
}
- Isabelle_System.bash("make",
- cwd = build_dir.file,
+ Isabelle_System.bash("make", cwd = source_dir.file,
progress_stdout = progress.echo_if(verbose, _),
progress_stderr = progress.echo_if(verbose, _)).check
/* install */
- Isabelle_System.copy_file(build_dir + Path.basic("LICENCE"), component_dir.LICENSE)
+ Isabelle_System.copy_file(source_dir + Path.basic("LICENCE"), component_dir.LICENSE)
val install_files = List("SPASS")
for (name <- install_files ::: install_files.map(_ + ".exe")) {
- val path = build_dir + Path.basic(name)
+ val path = source_dir + Path.basic(name)
if (path.is_file) Isabelle_System.copy_file(path, platform_dir)
}
--- a/src/Pure/Admin/build_vampire.scala Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/Admin/build_vampire.scala Wed Nov 30 15:03:31 2022 +0100
@@ -65,12 +65,11 @@
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download_file(download_url, archive_path, progress = progress)
- Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
+ Isabelle_System.extract(archive_path, tmp_dir)
val source_dir = File.get_dir(tmp_dir, title = download_url)
- Isabelle_System.bash(
- "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src",
- cwd = component_dir.path.file).check
+ Isabelle_System.extract(archive_path, component_dir.path)
+ Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src)
/* build */
--- a/src/Pure/Admin/build_verit.scala Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/Admin/build_verit.scala Wed Nov 30 15:03:31 2022 +0100
@@ -61,12 +61,11 @@
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download_file(download_url, archive_path, progress = progress)
- Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
+ Isabelle_System.extract(archive_path, tmp_dir)
val source_dir = File.get_dir(tmp_dir, title = download_url)
- Isabelle_System.bash(
- "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src",
- cwd = component_dir.path.file).check
+ Isabelle_System.extract(archive_path, component_dir.path)
+ Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src)
/* build */
--- a/src/Pure/General/file.scala Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/General/file.scala Wed Nov 30 15:03:31 2022 +0100
@@ -83,7 +83,9 @@
def is_node(s: String): Boolean = s.endsWith(".node")
def is_pdf(s: String): Boolean = s.endsWith(".pdf")
def is_png(s: String): Boolean = s.endsWith(".png")
+ def is_tar_bz2(s: String): Boolean = s.endsWith(".tar.bz2")
def is_tar_gz(s: String): Boolean = s.endsWith(".tar.gz")
+ 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")
def is_zip(s: String): Boolean = s.endsWith(".zip")
--- a/src/Pure/General/mercurial.scala Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/General/mercurial.scala Wed Nov 30 15:03:31 2022 +0100
@@ -74,7 +74,7 @@
Bytes.write(archive_path, content.bytes)
progress.echo("Unpacking " + rev + ".tar.gz")
Isabelle_System.gnutar("-xzf " + File.bash_path(archive_path),
- dir = dir, original_owner = true, strip = 1).check
+ dir = dir, original_owner = true, strip = true).check
}
}
}
--- a/src/Pure/System/components.scala Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/System/components.scala Wed Nov 30 15:03:31 2022 +0100
@@ -48,7 +48,7 @@
def unpack(dir: Path, archive: Path, progress: Progress = new Progress): String = {
val name = Archive.get_name(archive.file_name)
progress.echo("Unpacking " + name)
- Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check
+ Isabelle_System.extract(archive, dir)
name
}
@@ -271,7 +271,7 @@
// contrib directory
val is_standard_component =
Isabelle_System.with_tmp_dir("component") { tmp_dir =>
- Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
+ Isabelle_System.extract(archive, tmp_dir)
Directory(tmp_dir + Path.explode(name)).check
}
if (is_standard_component) {
--- a/src/Pure/System/isabelle_system.scala Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/System/isabelle_system.scala Wed Nov 30 15:03:31 2022 +0100
@@ -421,25 +421,27 @@
args: String,
dir: Path = Path.current,
original_owner: Boolean = false,
- strip: Int = 0,
+ strip: Boolean = false,
redirect: Boolean = false
): Process_Result = {
val options =
(if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") +
(if (original_owner) "" else "--owner=root --group=staff ") +
- (if (strip <= 0) "" else "--strip-components=" + strip + " ")
+ (if (!strip) "" else "--strip-components=1 ")
if (gnutar_check) bash("tar " + options + args, redirect = redirect)
else error("Expected to find GNU tar executable")
}
- def extract(archive: Path, dir: Path): Unit = {
+ def extract(archive: Path, dir: Path, strip: Boolean = false): Unit = {
val name = archive.file_name
if (File.is_zip(name)) {
+ require(!strip, "Cannot use unzip with strip")
Isabelle_System.bash("unzip -x " + File.bash_path(archive.absolute), cwd = dir.file).check
}
- else if (File.is_tar_gz(name)) {
- Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check
+ 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 error("Cannot extract " + archive)
}
--- a/src/Pure/Tools/phabricator.scala Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/Tools/phabricator.scala Wed Nov 30 15:03:31 2022 +0100
@@ -204,7 +204,7 @@
}
else Path.explode(mercurial_source)
- Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
+ Isabelle_System.extract(archive, tmp_dir)
val build_dir = File.get_dir(tmp_dir, title = mercurial_source)
progress.bash("make all && make install", cwd = build_dir.file, echo = true).check