# HG changeset patch # User wenzelm # Date 1711469183 -3600 # Node ID 914c4a81027d8e6b326231a6a09adce990b1c397 # Parent a4d94dd5c210e8ee48f4659988f04f62cae4805a clarified signature: explicit type Platform.Info with derived operations; diff -r a4d94dd5c210 -r 914c4a81027d src/Pure/Admin/component_go.scala --- 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")) diff -r a4d94dd5c210 -r 914c4a81027d src/Pure/System/platform.scala --- 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 diff -r a4d94dd5c210 -r 914c4a81027d src/Pure/Tools/dotnet_setup.scala --- 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,