# HG changeset patch # User wenzelm # Date 1711375908 -3600 # Node ID ee45e96eb7c5c1c551dbb4237eaf6ef4f9481aaf # Parent 7bbb0d65ce72d7bba6f170c8d25524afb2fcaba8# Parent 013558fd6fed2fd317b515cb0144d3d134885b02 merged diff -r 7bbb0d65ce72 -r ee45e96eb7c5 etc/build.props --- a/etc/build.props Mon Mar 25 14:08:25 2024 +0100 +++ b/etc/build.props Mon Mar 25 15:11:48 2024 +0100 @@ -26,6 +26,7 @@ src/Pure/Admin/component_eptcs.scala \ src/Pure/Admin/component_foiltex.scala \ src/Pure/Admin/component_fonts.scala \ + src/Pure/Admin/component_go.scala \ src/Pure/Admin/component_hugo.scala \ src/Pure/Admin/component_javamail.scala \ src/Pure/Admin/component_jdk.scala \ diff -r 7bbb0d65ce72 -r ee45e96eb7c5 src/Pure/Admin/component_go.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Admin/component_go.scala Mon Mar 25 15:11:48 2024 +0100 @@ -0,0 +1,155 @@ +/* Title: Pure/Admin/component_go.scala + Author: Makarius + +Build Isabelle component for Go: https://go.dev +*/ + +package isabelle + + +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) + + def download(base_url: String, version: String): String = { + val ext = if (platform_family == Platform.Family.windows) ".zip" else ".tar.gz" + Url.append_path(base_url, "go" + version + "." + go_platform.replace("_", "-") + ext) + } + } + + val platforms: List[Download_Platform] = + 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")) + + + /* build go */ + + val default_url = "https://go.dev/dl" + val default_version = "1.22.1" + + def build_go( + base_url: String = default_url, + version: String = default_version, + target_dir: Path = Path.current, + progress: Progress = new Progress + ): Unit = { + val component_dir = + Components.Directory(target_dir + Path.basic("go-" + version)).create(progress = progress) + + + /* download */ + + Isabelle_System.with_tmp_dir("download") { download_dir => + for (platform <- platforms.reverse) { + val download = platform.download(base_url, version) + + val archive_name = + Url.get_base_name(download) getOrElse + error("Malformed download URL " + quote(download)) + val archive_path = download_dir + Path.basic(archive_name) + + 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) + Isabelle_System.move_file(component_dir.bin, platform_dir) + } + } + + File.find_files(component_dir.path.file, pred = file => File.is_exe(file.getName)). + foreach(file => File.set_executable(File.path(file))) + + + /* isabelle tool */ + + val isabelle_tool_dir = component_dir.path + Path.explode("isabelle_tool") + Isabelle_System.make_directory(isabelle_tool_dir) + + for (tool <- List("go", "gofmt")) { + val isabelle_tool = isabelle_tool_dir + Path.basic(tool) + File.write(isabelle_tool, +"""#!/usr/bin/env bash +# +# Author: Makarius +# +# DESCRIPTION: invoke """ + tool + """ within the Isabelle environment + +export GOROOT="$ISABELLE_GOROOT" +exec "$ISABELLE_GOEXE/""" + tool + """" "$@" +""") + File.set_executable(isabelle_tool) + } + + + /* settings */ + + component_dir.write_settings(""" +ISABELLE_GOROOT="$COMPONENT" +ISABELLE_GOEXE="$ISABELLE_GOROOT/${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}}" + +ISABELLE_TOOLS="$ISABELLE_TOOLS:$ISABELLE_GOROOT/isabelle_tool" +""") + + + /* platform.props */ + + File.write(component_dir.platform_props, + (for ((a, b) <- platforms.groupBy(_.platform_family).iterator) + yield a.toString + " = " + b.flatMap(_.platform_paths).mkString(" ") + ).mkString("", "\n", "\n")) + + + /* README */ + + File.write(component_dir.README, + """This distribution of Go has been assembled from official downloads from +""" + base_url + """ + + + Makarius + """ + Date.Format.date(Date.now()) + "\n") + } + + + /* Isabelle tool wrapper */ + + val isabelle_tool = + Isabelle_Tool("component_go", "build component for Go", Scala_Project.here, + { args => + var target_dir = Path.current + var base_url = default_url + var version = default_version + + val getopts = Getopts(""" +Usage: isabelle component_go [OPTIONS] + + Options are: + -D DIR target directory (default ".") + -U URL download URL (default: """" + default_url + """") + -V VERSION version (default: """" + default_version + """") + + Build component for Go development environment. +""", + "D:" -> (arg => target_dir = Path.explode(arg)), + "U:" -> (arg => base_url = arg), + "V:" -> (arg => version = arg)) + + val more_args = getopts(args) + if (more_args.nonEmpty) getopts.usage() + + val progress = new Console_Progress() + + build_go(base_url = base_url, version = version, target_dir = target_dir, + progress = progress) + }) +} diff -r 7bbb0d65ce72 -r ee45e96eb7c5 src/Pure/Admin/component_hugo.scala --- a/src/Pure/Admin/component_hugo.scala Mon Mar 25 14:08:25 2024 +0100 +++ b/src/Pure/Admin/component_hugo.scala Mon Mar 25 15:11:48 2024 +0100 @@ -17,13 +17,13 @@ override def toString: String = platform_name def is_windows: Boolean = url_template.contains("windows") - def url(base_url: String, version: String): String = + + def download(base_url: String, version: String): String = base_url + "/v" + version + "/" + url_template.replace("{V}", version) } val platforms: List[Download_Platform] = List( - Download_Platform("arm64-darwin", "hugo_extended_{V}_darwin-universal.tar.gz"), Download_Platform("arm64-linux", "hugo_extended_{V}_linux-arm64.tar.gz"), Download_Platform("x86_64-darwin", "hugo_extended_{V}_darwin-universal.tar.gz"), Download_Platform("x86_64-linux", "hugo_extended_{V}_linux-amd64.tar.gz"), @@ -54,8 +54,10 @@ val platform_dir = Isabelle_System.make_directory(component_dir.path + Path.basic(platform.platform_name)) - val url = platform.url(base_url, version) - val name = Library.take_suffix(_ != '/', url.toList)._2.mkString + val download = platform.download(base_url, version) + val name = + Url.get_base_name(download) getOrElse + error("Malformed download name " + quote(download)) val exe = Path.basic("hugo").exe_if(platform.is_windows) @@ -63,7 +65,7 @@ Isabelle_System.with_tmp_dir("tmp", component_dir.path.file) { tmp_dir => val archive_file = download_dir + Path.basic(name) - Isabelle_System.download_file(url, archive_file, progress = progress) + Isabelle_System.download_file(download, archive_file, progress = progress) Isabelle_System.extract(archive_file, tmp_dir) Isabelle_System.move_file(tmp_dir + exe, platform_dir) Isabelle_System.move_file(tmp_dir + Path.basic("LICENSE"), component_dir.LICENSE) @@ -76,18 +78,18 @@ /* settings */ component_dir.write_settings(""" -ISABELLE_HUGO="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}}" +ISABELLE_HUGO="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}" """) /* README */ File.write(component_dir.README, - """This Isabelle components provides a hugo extended """ + version + """. + """This Isabelle components provides hugo extended """ + version + """. See also https://gohugo.io and executables from """ + base_url + """ - Fabian + Fabian Huch """ + Date.Format.date(Date.now()) + "\n") } diff -r 7bbb0d65ce72 -r ee45e96eb7c5 src/Pure/General/file.scala --- a/src/Pure/General/file.scala Mon Mar 25 14:08:25 2024 +0100 +++ b/src/Pure/General/file.scala Mon Mar 25 15:11:48 2024 +0100 @@ -7,6 +7,7 @@ package isabelle +import java.util.{Properties => JProperties} import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream, OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader, InputStreamReader, File => JFile, IOException} @@ -253,6 +254,15 @@ } + /* read properties */ + + def read_props(path: Path): JProperties = { + val props = new JProperties + props.load(Files.newBufferedReader(path.java_path)) + props + } + + /* write */ def writer(file: JFile): BufferedWriter = diff -r 7bbb0d65ce72 -r ee45e96eb7c5 src/Pure/General/mail.scala --- a/src/Pure/General/mail.scala Mon Mar 25 14:08:25 2024 +0100 +++ b/src/Pure/General/mail.scala Mon Mar 25 15:11:48 2024 +0100 @@ -47,7 +47,7 @@ def use_auth: Boolean = user.nonEmpty && password.nonEmpty private def mail_session: JSession = { - val props = new JProperties() + val props = new JProperties props.setProperty("mail.smtp.from", sender.toString) props.setProperty("mail.smtp.host", smtp_host) props.setProperty("mail.smtp.port", smtp_port.toString) @@ -56,7 +56,7 @@ transport match { case Transport.SSL(protocol) => props.setProperty("mail.smtp.ssl.enable", "true") - props.setProperty("mail.smtp.ssl.protocols", protocol) + props.setProperty("mail.smtp.ssl.protocols", protocol) case Transport.STARTTLS => props.setProperty("mail.smtp.starttls.enable", "true") case Transport.Plaintext => diff -r 7bbb0d65ce72 -r ee45e96eb7c5 src/Pure/System/components.scala --- a/src/Pure/System/components.scala Mon Mar 25 14:08:25 2024 +0100 +++ b/src/Pure/System/components.scala Mon Mar 25 15:11:48 2024 +0100 @@ -9,6 +9,8 @@ import java.io.{File => JFile} +import scala.jdk.CollectionConverters._ + object Components { /* archive name */ @@ -35,25 +37,26 @@ /* platforms */ - private val family_platforms: Map[Platform.Family, List[String]] = - Map( - Platform.Family.linux_arm -> List("arm64-linux", "arm64_32-linux"), - Platform.Family.linux -> List("x86_64-linux", "x86_64_32-linux"), - Platform.Family.macos -> - List("arm64-darwin", "arm64_32-darwin", "x86_64-darwin", "x86_64_32-darwin"), - Platform.Family.windows -> - List("x86_64-cygwin", "x86_64-windows", "x86_64_32-windows", "x86-windows")) + sealed case class Platforms(family_platforms: Map[String, List[Path]]) { + def defined(family: String): Boolean = family_platforms.isDefinedAt(family) + def apply(family: String): List[Path] = family_platforms.getOrElse(family, Nil) + def path_iterator: Iterator[Path] = family_platforms.valuesIterator.flatten + } - private val platform_names: Set[String] = - Set("x86-linux", "x86-cygwin") ++ family_platforms.iterator.flatMap(_._2) - - def platform_purge(platforms: List[Platform.Family]): String => Boolean = { - val preserve = - (for { - family <- platforms.iterator - platform <- family_platforms(family) - } yield platform).toSet - (name: String) => platform_names(name) && !preserve(name) + val default_platforms: Platforms = { + def paths(args: String*): List[Path] = args.toList.map(Path.explode) + Platforms( + Map( + Platform.Family.linux_arm.toString -> + paths("arm64-linux", "arm64_32-linux"), + Platform.Family.linux.toString -> + paths("x86_64-linux", "x86_64_32-linux"), + Platform.Family.macos.toString -> + paths("arm64-darwin", "arm64_32-darwin", "x86_64-darwin", "x86_64_32-darwin"), + Platform.Family.windows.toString -> + paths("x86_64-cygwin", "x86_64-windows", "x86_64_32-windows", "x86-windows"), + "obsolete" -> paths("x86-linux", "x86-cygwin") + )) } @@ -89,23 +92,6 @@ name } - def clean( - component_dir: Path, - platforms: List[Platform.Family] = Platform.Family.list, - ssh: SSH.System = SSH.Local, - progress: Progress = new Progress - ): Unit = { - val purge = platform_purge(platforms) - for { - name <- ssh.read_dir(component_dir) - path = Path.basic(name) - if purge(name) && ssh.is_dir(component_dir + path) - } { - progress.echo("Removing " + (component_dir.base + path)) - ssh.rm_tree(component_dir + path) - } - } - def clean_base( base_dir: Path, platforms: List[Platform.Family] = Platform.Family.list, @@ -116,7 +102,7 @@ name <- ssh.read_dir(base_dir) dir = base_dir + Path.basic(name) if is_component_dir(dir) - } clean(dir, platforms = platforms, ssh = ssh, progress = progress) + } Directory(dir, ssh = ssh).clean(preserve = platforms, progress = progress) } def resolve( @@ -148,8 +134,8 @@ unpack(unpack_dir, archive, ssh = ssh, progress = progress) if (clean_platforms.isDefined) { - clean(unpack_dir + Path.basic(name), - platforms = clean_platforms.get, ssh = ssh, progress = progress) + Directory(unpack_dir + Path.basic(name), ssh = ssh). + clean(preserve = clean_platforms.get, progress = progress) } if (clean_archives) { @@ -206,10 +192,12 @@ def etc: Path = path + Path.basic("etc") def src: Path = path + Path.basic("src") + def bin: Path = path + Path.basic("bin") def lib: Path = path + Path.basic("lib") def settings: Path = etc + Path.basic("settings") def components: Path = etc + Path.basic("components") def build_props: Path = etc + Path.basic("build.props") + def platform_props: Path = etc + Path.basic("platform.props") def README: Path = path + Path.basic("README") def LICENSE: Path = path + Path.basic("LICENSE") @@ -220,6 +208,40 @@ this } + def get_platforms(): Platforms = { + val props_path = platform_props.expand + if (props_path.is_file) { + val family_platforms = + try { + Map.from( + for (case (a, b) <- File.read_props(props_path).asScala.iterator) + yield { + if (!default_platforms.defined(a)) error("Bad platform family " + quote(a)) + val ps = List.from(b.split("\\s+").iterator.filter(_.nonEmpty)).map(Path.explode) + for (p <- ps if !p.all_basic) error("Bad path outside component " + p) + a -> ps + }) + } + catch { + case ERROR(msg) => error(msg + Position.here(Position.File(props_path.implode))) + } + Platforms(family_platforms) + } + else default_platforms + } + + def clean( + preserve: List[Platform.Family] = Platform.Family.list, + progress: Progress = new Progress + ): Unit = { + val platforms = get_platforms() + val preserve_path = Set.from(for (a <- preserve; p <- platforms(a.toString)) yield p) + for (dir <- platforms.path_iterator if !preserve_path(dir) && ssh.is_dir(path + dir)) { + progress.echo("Removing " + (path.base + dir)) + ssh.rm_tree(path + dir) + } + } + def ok: Boolean = ssh.is_file(settings) || ssh.is_file(components) || Sessions.is_session_dir(path, ssh = ssh) diff -r 7bbb0d65ce72 -r ee45e96eb7c5 src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Mon Mar 25 14:08:25 2024 +0100 +++ b/src/Pure/System/isabelle_tool.scala Mon Mar 25 15:11:48 2024 +0100 @@ -174,6 +174,7 @@ Component_Easychair.isabelle_tool, Component_Foiltex.isabelle_tool, Component_Fonts.isabelle_tool, + Component_Go.isabelle_tool, Component_Hugo.isabelle_tool, Component_Javamail.isabelle_tool, Component_JDK.isabelle_tool, diff -r 7bbb0d65ce72 -r ee45e96eb7c5 src/Pure/System/platform.scala --- a/src/Pure/System/platform.scala Mon Mar 25 14:08:25 2024 +0100 +++ b/src/Pure/System/platform.scala Mon Mar 25 15:11:48 2024 +0100 @@ -48,6 +48,10 @@ case Family.windows => "x86_64-windows" case platform => standard(platform) } + + def from_platform(platform: String): Family = + list.find(family => platform == standard(family) || platform == native(family)) + .getOrElse(error("Bad platform " + quote(platform))) } enum Family { case linux_arm, linux, macos, windows } diff -r 7bbb0d65ce72 -r ee45e96eb7c5 src/Pure/Tools/scala_build.scala --- a/src/Pure/Tools/scala_build.scala Mon Mar 25 14:08:25 2024 +0100 +++ b/src/Pure/Tools/scala_build.scala Mon Mar 25 15:11:48 2024 +0100 @@ -7,7 +7,6 @@ package isabelle -import java.util.{Properties => JProperties} import java.io.{ByteArrayOutputStream, PrintStream} import java.nio.file.Files import java.nio.file.{Path => JPath} @@ -73,8 +72,7 @@ else isabelle.setup.Build.BUILD_PROPS val props_path = dir + Path.explode(props_name) - val props = new JProperties - props.load(Files.newBufferedReader(props_path.java_path)) + val props = File.read_props(props_path) if (no_title) props.remove(isabelle.setup.Build.TITLE) if (do_build) props.remove(isabelle.setup.Build.NO_BUILD) if (module.isDefined) props.put(isabelle.setup.Build.MODULE, File.standard_path(module.get))