--- a/src/Pure/Admin/component_go.scala Tue Mar 26 16:04:06 2024 +0100
+++ b/src/Pure/Admin/component_go.scala Tue Mar 26 17:06:23 2024 +0100
@@ -10,26 +10,23 @@
object Component_Go {
/* platform information */
- sealed case class Download_Platform(platform_name: String, go_platform: String) {
- val platform_family: Platform.Family =
- Platform.Family.from_platform(platform_name)
-
- def platform_paths: List[String] =
- List(platform_name, "pkg/tool/" + go_platform)
+ sealed case class Platform_Info(platform: String, go_platform: String)
+ extends Platform.Info {
+ def paths: List[String] = List(platform, "pkg/tool/" + go_platform)
def download(base_url: String, version: String): String = {
- val ext = if (platform_family == Platform.Family.windows) ".zip" else ".tar.gz"
+ val ext = if (is_windows) ".zip" else ".tar.gz"
Url.append_path(base_url, "go" + version + "." + go_platform.replace("_", "-") + ext)
}
}
- val platforms: List[Download_Platform] =
+ val all_platforms: List[Platform_Info] =
List(
- Download_Platform("arm64-darwin", "darwin_arm64"),
- Download_Platform("arm64-linux", "linux_arm64"),
- Download_Platform("x86_64-darwin", "darwin_amd64"),
- Download_Platform("x86_64-linux", "linux_amd64"),
- Download_Platform("x86_64-windows", "windows_amd64"))
+ Platform_Info("arm64-darwin", "darwin_arm64"),
+ Platform_Info("arm64-linux", "linux_arm64"),
+ Platform_Info("x86_64-darwin", "darwin_amd64"),
+ Platform_Info("x86_64-linux", "linux_amd64"),
+ Platform_Info("x86_64-windows", "windows_amd64"))
/* build go */
@@ -50,7 +47,7 @@
/* download */
Isabelle_System.with_tmp_dir("download") { download_dir =>
- for (platform <- platforms.reverse) {
+ for (platform <- all_platforms.reverse) {
val download = platform.download(base_url, version)
val archive_name =
@@ -61,7 +58,7 @@
Isabelle_System.download_file(download, archive_path, progress = progress)
Isabelle_System.extract(archive_path, component_dir.path, strip = true)
- val platform_dir = component_dir.path + Path.explode(platform.platform_name)
+ val platform_dir = component_dir.path + platform.path
Isabelle_System.move_file(component_dir.bin, platform_dir)
}
}
@@ -104,8 +101,8 @@
/* platform.props */
File.write(component_dir.platform_props,
- (for ((a, b) <- platforms.groupBy(_.platform_family).iterator)
- yield a.toString + " = " + b.flatMap(_.platform_paths).mkString(" ")
+ (for ((a, b) <- all_platforms.groupBy(_.family_name).iterator)
+ yield a + " = " + b.flatMap(_.paths).mkString(" ")
).mkString("", "\n", "\n"))
--- a/src/Pure/System/platform.scala Tue Mar 26 16:04:06 2024 +0100
+++ b/src/Pure/System/platform.scala Tue Mar 26 17:06:23 2024 +0100
@@ -79,6 +79,34 @@
lazy val jvm_platform: String = cpu_arch + "-" + os_name
+ /* platform info */
+
+ trait Info {
+ def platform: String
+ override def toString: String = platform
+ def path: Path = Path.explode(platform)
+
+ val family: Family = Family.from_platform(platform)
+ def family_name: String = family.toString
+
+ def is_linux_arm: Boolean = family == Family.linux_arm
+ def is_linux: Boolean = family == Family.linux
+ def is_macos: Boolean = family == Family.macos
+ def is_windows: Boolean = family == Family.windows
+
+ def is(spec: String): Boolean = platform == spec || family_name == spec
+ }
+
+ def check_spec(infos: List[Info], spec: String): String = {
+ val specs = Library.distinct(infos.map(_.family_name) ::: infos.map(_.platform))
+ if (specs.contains(spec)) spec
+ else {
+ error("Bad platform specification " + quote(spec) +
+ "\n expected " + commas_quote(specs))
+ }
+ }
+
+
/* JVM version */
private val Version = """1\.(\d+)\.0_(\d+)""".r
--- a/src/Pure/Tools/dotnet_setup.scala Tue Mar 26 16:04:06 2024 +0100
+++ b/src/Pure/Tools/dotnet_setup.scala Tue Mar 26 17:06:23 2024 +0100
@@ -11,17 +11,15 @@
/* platforms */
sealed case class Platform_Info(
- name: String,
+ platform: String,
os: String = "",
arch: String = "x64",
ext: String = "sh",
exec: String = "bash",
check: () => Unit = () => ()
- ) {
- val family: Platform.Family = Platform.Family.from_platform(name)
- }
+ ) extends Platform.Info
- private val all_platforms =
+ val all_platforms: List[Platform_Info] =
List(
Platform_Info("arm64-linux", os = "linux", arch = "arm64"),
Platform_Info("x86_64-linux", os = "linux"),
@@ -32,15 +30,8 @@
exec = "powershell -ExecutionPolicy ByPass",
check = () => Isabelle_System.require_command("powershell", "-NoProfile -Command Out-Null")))
- def check_platform_spec(spec: String): String = {
- val all_specs =
- Library.distinct(all_platforms.map(_.family.toString) ::: all_platforms.map(_.name))
- if (all_specs.contains(spec)) spec
- else {
- error("Bad platform specification " + quote(spec) +
- "\n expected " + commas_quote(all_specs))
- }
- }
+ def check_platform_spec(spec: String): String =
+ Platform.check_spec(all_platforms, spec)
/* dotnet download and setup */
@@ -67,10 +58,7 @@
): Unit = {
check_platform_spec(platform_spec)
- for {
- platform <- all_platforms
- if platform.family.toString == platform_spec || platform.name == platform_spec
- } {
+ for (platform <- all_platforms if platform.is(platform_spec)) {
progress.expose_interrupt()
@@ -119,12 +107,12 @@
Isabelle_System.with_tmp_file("install", ext = platform.ext) { install =>
Isabelle_System.download_file(install_url + "." + platform.ext, install)
- val platform_dir = component_dir.path + Path.explode(platform.name)
+ val platform_dir = component_dir.path + platform.path
if (platform_dir.is_dir && !force) {
- progress.echo_warning("Platform " + platform.name + " already installed")
+ progress.echo_warning("Platform " + platform + " already installed")
}
else {
- progress.echo("Platform " + platform.name + " ...")
+ progress.echo("Platform " + platform + " ...")
platform.check()
if (platform_dir.is_dir && force) Isabelle_System.rm_tree(platform_dir)
val script =
@@ -132,7 +120,7 @@
if_proper(version, " -Version " + Bash.string(version)) +
" -Architecture " + Bash.string(platform.arch) +
if_proper(platform.os, " -OS " + Bash.string(platform.os)) +
- " -InstallDir " + Bash.string(platform.name) +
+ " -InstallDir " + File.bash_path(platform.path) +
(if (dry_run) " -DryRun" else "") +
" -NoPath"
progress.bash(script, echo = progress.verbose,