--- 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 \
--- /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)
+ })
+}
--- 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")
}
--- 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 =
--- 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 =>
--- 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)
--- 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,
--- 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 }
--- 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))