--- a/src/Pure/Admin/build_csdp.scala Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/Admin/build_csdp.scala Fri Nov 25 13:38:15 2022 +0100
@@ -96,10 +96,10 @@
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_name = File.get_dir(tmp_dir)
+ val source_dir = File.get_dir(tmp_dir, title = archive_name)
Isabelle_System.bash(
- "tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src",
+ "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src",
cwd = component_dir.path.file).check
@@ -107,21 +107,20 @@
progress.echo("Building CSDP for " + platform_name + " ...")
- val build_dir = tmp_dir + Path.basic(source_name)
build_flags.find(flags => flags.platform == platform_name) match {
case None => error("No build flags for platform " + quote(platform_name))
case Some(flags) =>
- File.find_files(build_dir.file, pred = file => file.getName == "Makefile").
+ File.find_files(source_dir.file, pred = file => file.getName == "Makefile").
foreach(file => flags.change(File.path(file)))
}
- progress.bash(mingw.bash_script("make"), cwd = build_dir.file, echo = verbose).check
+ progress.bash(mingw.bash_script("make"), cwd = source_dir.file, echo = verbose).check
/* install */
- Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path)
- Isabelle_System.copy_file(build_dir + Path.explode("solver/csdp").platform_exe, platform_dir)
+ Isabelle_System.copy_file(source_dir + Path.explode("LICENSE"), component_dir.path)
+ Isabelle_System.copy_file(source_dir + Path.explode("solver/csdp").platform_exe, platform_dir)
if (Platform.is_windows) {
Executable.libraries_closure(platform_dir + Path.explode("csdp.exe"), mingw = mingw,
--- a/src/Pure/Admin/build_easychair.scala Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/Admin/build_easychair.scala Fri Nov 25 13:38:15 2022 +0100
@@ -30,13 +30,7 @@
Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
cwd = download_dir.file).check
- val easychair_dir =
- File.read_dir(download_dir) match {
- case List(name) => download_dir + Path.explode(name)
- case bad =>
- error("Expected exactly one directory entry in " + download_file +
- bad.mkString("\n", "\n ", ""))
- }
+ val easychair_dir = File.get_dir(download_dir, title = download_url)
/* component */
--- a/src/Pure/Admin/build_foiltex.scala Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/Admin/build_foiltex.scala Fri Nov 25 13:38:15 2022 +0100
@@ -30,13 +30,7 @@
Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
cwd = download_dir.file).check
- val foiltex_dir =
- File.read_dir(download_dir) match {
- case List(name) => download_dir + Path.explode(name)
- case bad =>
- error("Expected exactly one directory entry in " + download_file +
- bad.mkString("\n", "\n ", ""))
- }
+ val foiltex_dir = File.get_dir(download_dir, title = download_url)
val README = Path.explode("README")
val README_flt = Path.explode("README.flt")
--- a/src/Pure/Admin/build_jdk.scala Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/Admin/build_jdk.scala Fri Nov 25 13:38:15 2022 +0100
@@ -121,13 +121,8 @@
Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
}
- val dir_entry =
- File.read_dir(tmp_dir) match {
- case List(s) => s
- case _ => error("Archive contains multiple directories")
- }
+ val jdk_dir = File.get_dir(tmp_dir, title = archive.file_name)
- val jdk_dir = tmp_dir + Path.explode(dir_entry)
val platform =
templates.view.flatMap(_.detect(jdk_dir))
.headOption.getOrElse(error("Failed to detect JDK platform"))
--- a/src/Pure/Admin/build_llncs.scala Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/Admin/build_llncs.scala Fri Nov 25 13:38:15 2022 +0100
@@ -33,13 +33,7 @@
Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
cwd = download_dir.file).check
- val llncs_dir =
- File.read_dir(download_dir) match {
- case List(name) => download_dir + Path.explode(name)
- case bad =>
- error("Expected exactly one directory entry in " + download_file +
- bad.mkString("\n", "\n ", ""))
- }
+ val llncs_dir = File.get_dir(download_dir, title = download_url)
val readme = Path.explode("README.md")
File.change(llncs_dir + readme)(_.replace(" ", "\u00a0"))
--- a/src/Pure/Admin/build_minisat.scala Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/Admin/build_minisat.scala Fri Nov 25 13:38:15 2022 +0100
@@ -61,10 +61,10 @@
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_name = File.get_dir(tmp_dir)
+ val source_dir = File.get_dir(tmp_dir, title = download_url)
Isabelle_System.bash(
- "tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src",
+ "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src",
cwd = component_dir.path.file).check
@@ -72,18 +72,17 @@
progress.echo("Building Minisat for " + platform_name + " ...")
- val build_dir = tmp_dir + Path.basic(source_name)
- Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path)
+ Isabelle_System.copy_file(source_dir + Path.explode("LICENSE"), component_dir.path)
if (Platform.is_macos) {
- File.change(build_dir + Path.explode("Makefile")) {
+ File.change(source_dir + Path.explode("Makefile")) {
_.replaceAll("--static", "").replaceAll("-Wl,-soname\\S+", "")
}
}
- progress.bash("make r", build_dir.file, echo = verbose).check
+ progress.bash("make r", source_dir.file, echo = verbose).check
Isabelle_System.copy_file(
- build_dir + Path.explode("build/release/bin/minisat").platform_exe, platform_dir)
+ source_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)
--- a/src/Pure/Admin/build_vampire.scala Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/Admin/build_vampire.scala Fri Nov 25 13:38:15 2022 +0100
@@ -66,10 +66,10 @@
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_name = File.get_dir(tmp_dir)
+ val source_dir = File.get_dir(tmp_dir, title = download_url)
Isabelle_System.bash(
- "tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src",
+ "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src",
cwd = component_dir.path.file).check
@@ -77,22 +77,21 @@
progress.echo("Building Vampire for " + platform_name + " ...")
- val build_dir = tmp_dir + Path.basic(source_name)
- Isabelle_System.copy_file(build_dir + Path.explode("LICENCE"), component_dir.path)
+ Isabelle_System.copy_file(source_dir + Path.explode("LICENCE"), component_dir.path)
val cmake_opts = if (Platform.is_linux) "-DBUILD_SHARED_LIBS=0 " else ""
val cmake_out =
progress.bash("cmake " + cmake_opts + """-G "Unix Makefiles" .""",
- cwd = build_dir.file, echo = verbose).check.out
+ cwd = source_dir.file, echo = verbose).check.out
val Pattern = """-- Setting binary name to '?([^\s']*)'?""".r
val binary =
split_lines(cmake_out).collectFirst({ case Pattern(name) => name })
.getOrElse(error("Failed to determine binary name from cmake output:\n" + cmake_out))
- progress.bash("make -j" + jobs, cwd = build_dir.file, echo = verbose).check
+ progress.bash("make -j" + jobs, cwd = source_dir.file, echo = verbose).check
- Isabelle_System.copy_file(build_dir + Path.basic("bin") + Path.basic(binary).platform_exe,
+ Isabelle_System.copy_file(source_dir + Path.basic("bin") + Path.basic(binary).platform_exe,
platform_dir + Path.basic("vampire").platform_exe)
--- a/src/Pure/Admin/build_verit.scala Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/Admin/build_verit.scala Fri Nov 25 13:38:15 2022 +0100
@@ -62,10 +62,10 @@
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_name = File.get_dir(tmp_dir)
+ val source_dir = File.get_dir(tmp_dir, title = download_url)
Isabelle_System.bash(
- "tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src",
+ "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src",
cwd = component_dir.path.file).check
@@ -76,17 +76,16 @@
val configure_options =
if (Platform.is_linux) "LDFLAGS=-Wl,-rpath,_DUMMY_" else ""
- val build_dir = tmp_dir + Path.basic(source_name)
progress.bash(mingw.bash_script("set -e\n./configure " + configure_options + "\nmake"),
- cwd = build_dir.file, echo = verbose).check
+ cwd = source_dir.file, echo = verbose).check
/* install */
- Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path)
+ Isabelle_System.copy_file(source_dir + Path.explode("LICENSE"), component_dir.path)
val exe_path = Path.basic("veriT").platform_exe
- Isabelle_System.copy_file(build_dir + exe_path, platform_dir)
+ Isabelle_System.copy_file(source_dir + exe_path, platform_dir)
Executable.libraries_closure(platform_dir + exe_path, filter = Set("libgmp"), mingw = mingw)
--- a/src/Pure/General/file.scala Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/General/file.scala Fri Nov 25 13:38:15 2022 +0100
@@ -128,13 +128,26 @@
else files.toList.map(_.getName).sorted
}
- def get_dir(dir: Path): String =
- read_dir(dir).filter(name => (dir + Path.basic(name)).is_dir) match {
- case List(entry) => entry
- case dirs =>
- error("Exactly one directory entry expected: " + commas_quote(dirs.sorted))
+ def get_entry(
+ dir: Path,
+ pred: Path => Boolean = _ => true,
+ title: String = ""
+ ): Path =
+ read_dir(dir).filter(name => pred(dir + Path.basic(name))) match {
+ case List(entry) => dir + Path.basic(entry)
+ case bad =>
+ error("Bad directory content in " + (if (title.nonEmpty) title else dir.toString) +
+ "\nexpected a single entry, but found" +
+ (if (bad.isEmpty) " nothing"
+ else bad.sorted.map(quote).mkString(":\n ", "\n ", "")))
}
+ def get_file(dir: Path, title: String = ""): Path =
+ get_entry(dir, pred = _.is_file, title = title)
+
+ def get_dir(dir: Path, title: String = ""): Path =
+ get_entry(dir, pred = _.is_dir, title = title)
+
def find_files(
start: JFile,
pred: JFile => Boolean = _ => true,
--- a/src/Pure/General/sql.scala Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/General/sql.scala Fri Nov 25 13:38:15 2022 +0100
@@ -367,11 +367,8 @@
lazy val init_jdbc: Unit = {
val lib_path = Path.explode("$ISABELLE_SQLITE_HOME/" + Platform.jvm_platform)
- val lib_name =
- File.find_files(lib_path.file) match {
- case List(file) => file.getName
- case _ => error("Exactly one file expected in directory " + lib_path.expand)
- }
+ val lib_name = File.get_file(lib_path).file_name
+
System.setProperty("org.sqlite.lib.path", File.platform_path(lib_path))
System.setProperty("org.sqlite.lib.name", lib_name)
--- a/src/Pure/General/zstd.scala Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/General/zstd.scala Fri Nov 25 13:38:15 2022 +0100
@@ -18,12 +18,9 @@
"Zstd library already initialized by other means than isabelle.Zstd.init()")
val lib_dir = Path.explode("$ISABELLE_ZSTD_HOME/" + Platform.jvm_platform)
- val lib_file =
- File.find_files(lib_dir.file) match {
- case List(file) => file
- case _ => error("Exactly one file expected in directory " + lib_dir.expand)
- }
- System.load(File.platform_path(lib_file.getAbsolutePath))
+ val lib_file = File.get_file(lib_dir)
+
+ System.load(lib_file.absolute_file.getPath)
zstd.util.Native.assumeLoaded()
assert(zstd.util.Native.isLoaded())
--- a/src/Pure/Tools/phabricator.scala Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/Tools/phabricator.scala Fri Nov 25 13:38:15 2022 +0100
@@ -205,7 +205,7 @@
else Path.explode(mercurial_source)
Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
- val build_dir = tmp_dir + Path.basic(File.get_dir(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
}