# HG changeset patch
# User wenzelm
# Date 1746648472 -7200
# Node ID b7148ee355f602ca94cf8d6b646027e9698ea850
# Parent  76262e8b53f7063ae9ff58e83ccf8818f42504c4# Parent  c1871d01355610071485c8e11f001a7470cf0035
merged

diff -r 76262e8b53f7 -r b7148ee355f6 etc/build.props
--- a/etc/build.props	Wed May 07 16:08:56 2025 +0200
+++ b/etc/build.props	Wed May 07 22:07:52 2025 +0200
@@ -218,6 +218,7 @@
   src/Pure/Thy/thy_element.scala \
   src/Pure/Thy/thy_header.scala \
   src/Pure/Thy/thy_syntax.scala \
+  src/Pure/Tools/caddy_setup.scala \
   src/Pure/Tools/check_keywords.scala \
   src/Pure/Tools/debugger.scala \
   src/Pure/Tools/doc.scala \
@@ -351,6 +352,7 @@
   isabelle.Bibtex$File_Format \
   isabelle.Build$Engine$Default \
   isabelle.Build_Schedule$Build_Engine \
+  isabelle.Caddy_Setup \
   isabelle.CI_Jobs \
   isabelle.Document_Build$Build_Engine \
   isabelle.Document_Build$LIPIcs_LuaLaTeX_Engine \
diff -r 76262e8b53f7 -r b7148ee355f6 etc/settings
--- a/etc/settings	Wed May 07 16:08:56 2025 +0200
+++ b/etc/settings	Wed May 07 22:07:52 2025 +0200
@@ -183,14 +183,17 @@
 ### .Net / Fsharp
 ###
 
-ISABELLE_DOTNET_VERSION="8.0.203"
+ISABELLE_DOTNET_SETUP_VERSION="8.0.203"
 
 
 ###
-### Go
+### Go and Caddy
 ###
 
-ISABELLE_GO_VERSION="1.22.1"
+ISABELLE_GO_SETUP_VERSION="1.24.1"
+
+ISABELLE_CADDY_SETUP_VERSION="2.10.0"
+ISABELLE_CADDY_SETUP_MODULES="github.com/jasonlovesdoggo/caddy-defender github.com/mholt/caddy-ratelimit"
 
 
 ###
diff -r 76262e8b53f7 -r b7148ee355f6 lib/Tools/caddy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/caddy	Wed May 07 22:07:52 2025 +0200
@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: invoke caddy within the Isabelle environment
+
+if [ -z "$ISABELLE_CADDY" ]; then
+  echo "Missing Caddy installation: need to run \"isabelle caddy_setup\" first" >&2
+  exit 2
+else
+  exec "$ISABELLE_CADDY" "$@"
+fi
diff -r 76262e8b53f7 -r b7148ee355f6 src/Pure/Admin/component_bash_process.scala
--- a/src/Pure/Admin/component_bash_process.scala	Wed May 07 16:08:56 2025 +0200
+++ b/src/Pure/Admin/component_bash_process.scala	Wed May 07 22:07:52 2025 +0200
@@ -39,7 +39,7 @@
 
     /* platform */
 
-    val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM(apple = true)
+    val platform_name = Isabelle_Platform.local.ISABELLE_PLATFORM(apple = true)
     val platform_dir =
       Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
 
diff -r 76262e8b53f7 -r b7148ee355f6 src/Pure/Admin/component_csdp.scala
--- a/src/Pure/Admin/component_csdp.scala	Wed May 07 16:08:56 2025 +0200
+++ b/src/Pure/Admin/component_csdp.scala	Wed May 07 22:07:52 2025 +0200
@@ -80,7 +80,7 @@
 
       /* platform */
 
-      val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM(windows = true)
+      val platform_name = Isabelle_Platform.local.ISABELLE_PLATFORM(windows = true)
       val platform_dir =
         Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
 
diff -r 76262e8b53f7 -r b7148ee355f6 src/Pure/Admin/component_e.scala
--- a/src/Pure/Admin/component_e.scala	Wed May 07 16:08:56 2025 +0200
+++ b/src/Pure/Admin/component_e.scala	Wed May 07 22:07:52 2025 +0200
@@ -26,7 +26,7 @@
       val component_dir =
         Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
 
-      val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM(apple = true)
+      val platform_name = Isabelle_Platform.local.ISABELLE_PLATFORM(apple = true)
       val platform_dir =
         Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
 
diff -r 76262e8b53f7 -r b7148ee355f6 src/Pure/Admin/component_hol_light.scala
--- a/src/Pure/Admin/component_hol_light.scala	Wed May 07 16:08:56 2025 +0200
+++ b/src/Pure/Admin/component_hol_light.scala	Wed May 07 22:07:52 2025 +0200
@@ -48,7 +48,7 @@
     val component_dir =
       Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
 
-    val platform = Isabelle_Platform.self.ISABELLE_PLATFORM(windows = true, apple = true)
+    val platform = Isabelle_Platform.local.ISABELLE_PLATFORM(windows = true, apple = true)
     val platform_dir = Isabelle_System.make_directory(component_dir.path + Path.basic(platform))
 
 
diff -r 76262e8b53f7 -r b7148ee355f6 src/Pure/Admin/component_minisat.scala
--- a/src/Pure/Admin/component_minisat.scala	Wed May 07 16:08:56 2025 +0200
+++ b/src/Pure/Admin/component_minisat.scala	Wed May 07 22:07:52 2025 +0200
@@ -46,7 +46,7 @@
 
       /* platform */
 
-      val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM()
+      val platform_name = Isabelle_Platform.local.ISABELLE_PLATFORM()
       val platform_dir =
         Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
 
diff -r 76262e8b53f7 -r b7148ee355f6 src/Pure/Admin/component_polyml.scala
--- a/src/Pure/Admin/component_polyml.scala	Wed May 07 16:08:56 2025 +0200
+++ b/src/Pure/Admin/component_polyml.scala	Wed May 07 22:07:52 2025 +0200
@@ -12,67 +12,52 @@
 object Component_PolyML {
   /** platform information **/
 
-  sealed case class Platform_Info(
-    options: List[String] = Nil,
-    setup: String = "",
-    libs: Set[String] = Set.empty)
-
-  sealed case class Platform_Context(
-    platform: Isabelle_Platform = Isabelle_Platform.self,
-    mingw: MinGW = MinGW.none,
-    progress: Progress = new Progress
-  ) {
-    def info: Platform_Info =
+  object Platform_Info {
+    def apply(platform: Isabelle_Platform): Platform_Info =
       if (platform.is_linux) {
         Platform_Info(
+          platform = platform,
           options = List("LDFLAGS=-Wl,-rpath,_DUMMY_"),
           libs = Set("libgmp"))
       }
       else if (platform.is_macos) {
         Platform_Info(
+          platform = platform,
           options = List("CFLAGS=-O3", "CXXFLAGS=-O3", "LDFLAGS=-segprot POLY rwx rwx"),
           setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin",
           libs = Set("libpolyml", "libgmp"))
       }
       else if (platform.is_windows) {
         Platform_Info(
+          platform = platform,
           options =
             List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"),
           setup = MinGW.env_prefix,
           libs = Set("libgcc_s_seh", "libgmp", "libstdc++", "libwinpthread"))
       }
       else error("Bad platform: " + quote(platform.toString))
+  }
 
-    def standard_path(path: Path): String =
-      mingw.standard_path(File.standard_path(path))
-
+  sealed case class Platform_Info(
+    platform: Isabelle_Platform = Isabelle_Platform.local,
+    options: List[String] = Nil,
+    setup: String = "",
+    libs: Set[String] = Set.empty
+  ) {
     def polyml(arch_64: Boolean): String =
       (if (arch_64) platform.arch_64 else platform.arch_64_32) + "-" + platform.os_name
-
-    def sha1: String = platform.arch_64 + "-" + platform.os_name
-
-    def execute(cwd: Path, script_lines: String*): Process_Result = {
-      val script = cat_lines("set -e" :: script_lines.toList)
-      val script1 =
-        if (platform.is_arm && platform.is_macos) {
-          "arch -arch arm64 bash -c " + Bash.string(script)
-        }
-        else mingw.bash_script(script)
-      progress.bash(script1, cwd = cwd, echo = progress.verbose).check
-    }
   }
 
 
-
   /** build stages **/
 
   def make_polyml_gmp(
-    platform_context: Platform_Context,
+    platform_context: Isabelle_Platform.Context,
     dir: Path,
     options: List[String] = Nil
   ): Path = {
     val progress = platform_context.progress
-    val platform = platform_context.platform
+    val platform = platform_context.isabelle_platform
 
     val platform_arch = if (platform.is_arm) "aarch64" else "x86_64"
     val platform_os =
@@ -105,7 +90,7 @@
   }
 
   def make_polyml(
-    platform_context: Platform_Context,
+    platform_context: Isabelle_Platform.Context,
     root: Path,
     gmp_root: Option[Path] = None,
     sha1_root: Option[Path] = None,
@@ -116,9 +101,8 @@
     if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir))
       error("Bad Poly/ML root directory: " + root)
 
-    val platform = platform_context.platform
-
-    val info = platform_context.info
+    val platform = platform_context.isabelle_platform
+    val platform_info = Platform_Info(platform)
 
 
     /* configure and make */
@@ -130,8 +114,8 @@
       def detect_CFLAGS(s: String): Boolean = s.startsWith("CFLAGS=")
 
       val info_options =
-        if (info.options.exists(detect_CFLAGS)) info.options
-        else "CFLAGS=" :: info.options
+        if (platform_info.options.exists(detect_CFLAGS)) platform_info.options
+        else "CFLAGS=" :: platform_info.options
 
       val options2 =
         for (opt <- info_options) yield {
@@ -160,7 +144,7 @@
       }
 
     platform_context.execute(root,
-      info.setup,
+      platform_info.setup,
       gmp_setup,
       "[ -f Makefile ] && make distclean",
       """./configure --prefix="$PWD/target" """ + Bash.strings(configure_options),
@@ -174,7 +158,7 @@
     val sha1_files =
       sha1_root match {
         case Some(dir) =>
-          val platform_path = Path.explode(platform_context.sha1)
+          val platform_path = Path.explode(platform.ISABELLE_PLATFORM(windows = true, apple = true))
           val platform_dir = dir + platform_path
           platform_context.execute(dir, "./build " + File.bash_path(platform_path))
           File.read_dir(platform_dir).map(entry => platform_dir + Path.basic(entry))
@@ -184,7 +168,7 @@
 
     /* install */
 
-    val platform_path = Path.explode(platform_context.polyml(arch_64))
+    val platform_path = Path.explode(platform_info.polyml(arch_64))
     val platform_dir = target_dir + platform_path
 
     Isabelle_System.rm_tree(platform_dir)
@@ -200,7 +184,7 @@
       platform_dir + Path.basic("poly").platform_exe,
       env_prefix = gmp_setup + "\n",
       mingw = platform_context.mingw,
-      filter = info.libs)
+      filter = platform_info.libs)
 
 
     /* polyc: directory prefix */
@@ -252,7 +236,7 @@
 
 
   def build_polyml(
-    platform_context: Platform_Context,
+    platform_context: Isabelle_Platform.Context,
     options: List[String] = Nil,
     component_name: String = "",
     gmp_url: String = "",
@@ -264,7 +248,9 @@
     sha1_version: String = default_sha1_version,
     target_dir: Path = Path.current
   ): Unit = {
-    val platform = platform_context.platform
+    val platform = platform_context.isabelle_platform
+    val platform_info = Platform_Info(platform)
+
     val progress = platform_context.progress
 
 
@@ -315,7 +301,7 @@
       init_src_root(component_dir.src, "RootX86.ML", "ROOT.ML")
 
       for (arch_64 <- List(false, true)) {
-        progress.echo("Building Poly/ML " + platform_context.polyml(arch_64))
+        progress.echo("Building Poly/ML " + platform_info.polyml(arch_64))
         make_polyml(
           platform_context,
           root = polyml_download,
@@ -430,9 +416,8 @@
 
         val progress = new Console_Progress(verbose = verbose)
 
-        val target_dir =
-          make_polyml_gmp(Platform_Context(mingw = mingw, progress = progress),
-            root, options = options)
+        val platform_context = Isabelle_Platform.Context(mingw = mingw, progress = progress)
+        val target_dir = make_polyml_gmp(platform_context, root, options = options)
 
         progress.echo("GMP installation directory: " + target_dir)
       })
@@ -478,8 +463,9 @@
           }
 
         val progress = new Console_Progress(verbose = verbose)
-        make_polyml(Platform_Context(mingw = mingw, progress = progress),
-          root, gmp_root = gmp_root, sha1_root = sha1_root, arch_64 = arch_64, options = options)
+        val platform_context = Isabelle_Platform.Context(mingw = mingw, progress = progress)
+        make_polyml(platform_context, root,
+          gmp_root = gmp_root, sha1_root = sha1_root, arch_64 = arch_64, options = options)
       })
 
   val isabelle_tool3 =
@@ -535,7 +521,7 @@
         val options = getopts(args)
 
         val progress = new Console_Progress(verbose = verbose)
-        val platform_context = Platform_Context(mingw = mingw, progress = progress)
+        val platform_context = Isabelle_Platform.Context(mingw = mingw, progress = progress)
 
         build_polyml(platform_context, options = options, component_name = component_name,
           gmp_url = gmp_url, gmp_root = gmp_root, polyml_url = polyml_url,
diff -r 76262e8b53f7 -r b7148ee355f6 src/Pure/Admin/component_rsync.scala
--- a/src/Pure/Admin/component_rsync.scala	Wed May 07 16:08:56 2025 +0200
+++ b/src/Pure/Admin/component_rsync.scala	Wed May 07 22:07:52 2025 +0200
@@ -50,7 +50,7 @@
           .create(progress = progress)
           .write_platforms()
 
-      val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM(apple = true)
+      val platform_name = Isabelle_Platform.local.ISABELLE_PLATFORM(apple = true)
       val platform_dir =
         Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
 
diff -r 76262e8b53f7 -r b7148ee355f6 src/Pure/Admin/component_spass.scala
--- a/src/Pure/Admin/component_spass.scala	Wed May 07 16:08:56 2025 +0200
+++ b/src/Pure/Admin/component_spass.scala	Wed May 07 22:07:52 2025 +0200
@@ -54,7 +54,7 @@
       val component_dir =
         Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
 
-      val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM()
+      val platform_name = Isabelle_Platform.local.ISABELLE_PLATFORM()
       val platform_dir =
         Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
 
diff -r 76262e8b53f7 -r b7148ee355f6 src/Pure/Admin/component_vampire.scala
--- a/src/Pure/Admin/component_vampire.scala	Wed May 07 16:08:56 2025 +0200
+++ b/src/Pure/Admin/component_vampire.scala	Wed May 07 22:07:52 2025 +0200
@@ -48,7 +48,7 @@
 
       /* platform */
 
-      val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM()
+      val platform_name = Isabelle_Platform.local.ISABELLE_PLATFORM()
       val platform_dir =
         Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
 
diff -r 76262e8b53f7 -r b7148ee355f6 src/Pure/Admin/component_verit.scala
--- a/src/Pure/Admin/component_verit.scala	Wed May 07 16:08:56 2025 +0200
+++ b/src/Pure/Admin/component_verit.scala	Wed May 07 22:07:52 2025 +0200
@@ -46,7 +46,7 @@
 
       /* platform */
 
-      val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM(windows = true)
+      val platform_name = Isabelle_Platform.local.ISABELLE_PLATFORM(windows = true)
       val platform_dir =
         Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
 
diff -r 76262e8b53f7 -r b7148ee355f6 src/Pure/Admin/component_windows_app.scala
--- a/src/Pure/Admin/component_windows_app.scala	Wed May 07 16:08:56 2025 +0200
+++ b/src/Pure/Admin/component_windows_app.scala	Wed May 07 22:07:52 2025 +0200
@@ -12,7 +12,7 @@
 
   def tool_platform(): String = {
     require(Platform.is_unix, "Linux or macOS platform required")
-    Isabelle_Platform.self.ISABELLE_PLATFORM64
+    Isabelle_Platform.local.ISABELLE_PLATFORM64
   }
 
   def tool_platform_path(): Path = Path.basic(tool_platform())
diff -r 76262e8b53f7 -r b7148ee355f6 src/Pure/Admin/component_zipperposition.scala
--- a/src/Pure/Admin/component_zipperposition.scala	Wed May 07 16:08:56 2025 +0200
+++ b/src/Pure/Admin/component_zipperposition.scala	Wed May 07 22:07:52 2025 +0200
@@ -31,7 +31,7 @@
 
       /* platform */
 
-      val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM()
+      val platform_name = Isabelle_Platform.local.ISABELLE_PLATFORM()
       val platform_dir =
         Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
 
diff -r 76262e8b53f7 -r b7148ee355f6 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Wed May 07 16:08:56 2025 +0200
+++ b/src/Pure/General/ssh.scala	Wed May 07 22:07:52 2025 +0200
@@ -255,7 +255,8 @@
         progress_stderr = progress.echo(_)).check
     }
 
-    override lazy val isabelle_platform: Isabelle_Platform = Isabelle_Platform(ssh = Some(ssh))
+    override lazy val isabelle_platform: Isabelle_Platform =
+      Isabelle_Platform.remote(ssh)
 
 
     /* remote file-system */
@@ -595,7 +596,7 @@
     def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit =
       Isabelle_System.download_file(url_name, file, progress = progress)
 
-    def isabelle_platform: Isabelle_Platform = Isabelle_Platform()
+    def isabelle_platform: Isabelle_Platform = Isabelle_Platform.local
 
     def isabelle_platform_family: Platform.Family =
       Platform.Family.parse(isabelle_platform.ISABELLE_PLATFORM_FAMILY)
diff -r 76262e8b53f7 -r b7148ee355f6 src/Pure/System/isabelle_platform.scala
--- a/src/Pure/System/isabelle_platform.scala	Wed May 07 16:08:56 2025 +0200
+++ b/src/Pure/System/isabelle_platform.scala	Wed May 07 22:07:52 2025 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Pure/System/isabelle_platform.scala
     Author:     Makarius
 
-General hardware and operating system type for Isabelle system tools.
+Isabelle/Scala platform information, based on settings environment.
 */
 
 package isabelle
@@ -16,22 +16,57 @@
       "ISABELLE_WINDOWS_PLATFORM64",
       "ISABELLE_APPLE_PLATFORM64")
 
-  def apply(ssh: Option[SSH.Session] = None): Isabelle_Platform = {
-    ssh match {
-      case None =>
-        new Isabelle_Platform(settings.map(a => (a, Isabelle_System.getenv(a))))
-      case Some(ssh) =>
-        val script =
-          File.read(Path.explode("~~/lib/scripts/isabelle-platform")) + "\n" +
-            settings.map(a => "echo \"" + Bash.string(a) + "=$" + Bash.string(a) + "\"").mkString("\n")
-        val result = ssh.execute("bash -c " + Bash.string(script)).check
-        new Isabelle_Platform(
-          result.out_lines.map(line =>
-            Properties.Eq.unapply(line) getOrElse error("Bad output: " + quote(result.out))))
+  lazy val local: Isabelle_Platform =
+    new Isabelle_Platform(settings.map(a => (a, Isabelle_System.getenv(a))))
+
+  def remote(ssh: SSH.Session): Isabelle_Platform = {
+    val script =
+      File.read(Path.explode("~~/lib/scripts/isabelle-platform")) + "\n" +
+        settings.map(a => "echo \"" + Bash.string(a) + "=$" + Bash.string(a) + "\"").mkString("\n")
+    val result = ssh.execute("bash -c " + Bash.string(script)).check
+    new Isabelle_Platform(
+      result.out_lines.map(line =>
+        Properties.Eq.unapply(line) getOrElse error("Bad output: " + quote(result.out))))
+  }
+
+
+  /* system context for progress/process */
+
+  object Context {
+    def apply(
+      isabelle_platform: Isabelle_Platform = local,
+      mingw: MinGW = MinGW.none,
+      progress: Progress = new Progress
+    ): Context = {
+      val context_platform = isabelle_platform
+      val context_mingw = mingw
+      val context_progress = progress
+      new Context {
+        override def isabelle_platform: Isabelle_Platform = context_platform
+        override def mingw: MinGW = context_mingw
+        override def progress: Progress = context_progress
+      }
     }
   }
 
-  lazy val self: Isabelle_Platform = apply()
+  trait Context {
+    def isabelle_platform: Isabelle_Platform
+    def mingw: MinGW
+    def progress: Progress
+
+    def standard_path(path: Path): String =
+      mingw.standard_path(File.standard_path(path))
+
+    def execute(cwd: Path, script_lines: String*): Process_Result = {
+      val script = cat_lines("set -e" :: script_lines.toList)
+      val script1 =
+        if (isabelle_platform.is_arm && isabelle_platform.is_macos) {
+          "arch -arch arm64 bash -c " + Bash.string(script)
+        }
+        else mingw.bash_script(script)
+      progress.bash(script1, cwd = cwd, echo = progress.verbose).check
+    }
+  }
 }
 
 class Isabelle_Platform private(val settings: List[(String, String)]) {
diff -r 76262e8b53f7 -r b7148ee355f6 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Wed May 07 16:08:56 2025 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Wed May 07 22:07:52 2025 +0200
@@ -132,6 +132,7 @@
   Build_Manager.isabelle_tool2,
   Build_Schedule.isabelle_tool,
   Build_CI.isabelle_tool,
+  Caddy_Setup.isabelle_tool,
   Doc.isabelle_tool,
   Docker_Build.isabelle_tool,
   Document_Build.isabelle_tool,
diff -r 76262e8b53f7 -r b7148ee355f6 src/Pure/System/platform.scala
--- a/src/Pure/System/platform.scala	Wed May 07 16:08:56 2025 +0200
+++ b/src/Pure/System/platform.scala	Wed May 07 22:07:52 2025 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Pure/System/platform.scala
     Author:     Makarius
 
-System platform identification.
+Java platform information, based on system properties.
 */
 
 package isabelle
diff -r 76262e8b53f7 -r b7148ee355f6 src/Pure/Tools/caddy_setup.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/caddy_setup.scala	Wed May 07 22:07:52 2025 +0200
@@ -0,0 +1,188 @@
+/*  Title:      Pure/Tools/caddy_setup.scala
+    Author:     Makarius
+
+Dynamic setup of Caddy component.
+*/
+
+package isabelle
+
+
+object Caddy_Setup {
+  /* platform information */
+
+  sealed case class Platform_Info(platform: String, xcaddy_template: String)
+  extends Platform.Info {
+    def xcaddy_download(url: String, version: String): String =
+      Url.append_path(url, xcaddy_template.replace("{V}", version))
+  }
+
+  val all_platforms: List[Platform_Info] =
+    List(
+      Platform_Info("arm64-darwin", "v{V}/xcaddy_{V}_mac_arm64.tar.gz"),
+      Platform_Info("arm64-linux", "v{V}/xcaddy_{V}_linux_arm64.tar.gz"),
+      Platform_Info("x86_64-darwin", "v{V}/xcaddy_{V}_mac_amd64.tar.gz"),
+      Platform_Info("x86_64-linux", "v{V}/xcaddy_{V}_linux_amd64.tar.gz"),
+      Platform_Info("x86_64-windows", "v{V}/xcaddy_{V}_windows_amd64.zip"))
+
+
+  /* download and setup */
+
+  def default_target_dir: Path = Components.default_components_base
+  def default_caddy_version: String = Isabelle_System.getenv_strict("ISABELLE_CADDY_SETUP_VERSION")
+  def default_caddy_modules: String = Isabelle_System.getenv_strict("ISABELLE_CADDY_SETUP_MODULES")
+  def default_xcaddy_url: String = "https://github.com/caddyserver/xcaddy/releases/download"
+  def default_xcaddy_version: String = "0.4.4"
+
+  def show_settings(): List[String] =
+    for (a <- List("ISABELLE_CADDY_SETUP_VERSION", "ISABELLE_CADDY_SETUP_MODULES"))
+      yield {
+        val b = Isabelle_System.getenv(a)
+        a + "=" + quote(b)
+      }
+
+  def caddy_setup(
+    caddy_version: String = default_caddy_version,
+    caddy_modules: String = default_caddy_modules,
+    xcaddy_url: String = default_xcaddy_url,
+    xcaddy_version: String = default_xcaddy_version,
+    target_dir: Path = default_target_dir,
+    progress: Progress = new Progress,
+    force: Boolean = false
+  ): Unit = {
+    val platform = Isabelle_Platform.local.ISABELLE_PLATFORM(windows = true, apple = true)
+
+
+    /* component directory */
+
+    val component_dir =
+      Components.Directory(target_dir + Path.basic("caddy-" + caddy_version))
+        .create(permissive = true)
+
+    progress.echo("Component directory " + component_dir)
+
+    component_dir.write_settings("""
+ISABELLE_CADDY_HOME="$COMPONENT"
+
+if [ -n "$ISABELLE_WINDOWS_PLATFORM64" -a -d "$ISABELLE_CADDY_HOME/$ISABELLE_WINDOWS_PLATFORM64" ]; then
+  ISABELLE_CADDY="$ISABELLE_CADDY_HOME/$ISABELLE_WINDOWS_PLATFORM64/caddy.exe"
+elif [ -n "$ISABELLE_APPLE_PLATFORM64" -a -d "$ISABELLE_CADDY_HOME/$ISABELLE_APPLE_PLATFORM64" ]; then
+  ISABELLE_CADDY="$ISABELLE_CADDY_HOME/$ISABELLE_APPLE_PLATFORM64/caddy"
+elif [ -d "$ISABELLE_CADDY_HOME/$ISABELLE_PLATFORM64" ]; then
+  ISABELLE_CADDY="$ISABELLE_CADDY_HOME/$ISABELLE_PLATFORM64/caddy"
+fi
+""")
+
+    for (old <- proper_string(Isabelle_System.getenv("ISABELLE_CADDY_HOME"))) {
+      Components.update_components(false, Path.explode(old))
+    }
+
+    Components.update_components(true, component_dir.path)
+
+
+    /* download and setup */
+
+    Isabelle_System.with_tmp_dir("tmp") { tmp_dir =>
+      val platform_info: Platform_Info =
+        all_platforms.find(_.platform == platform)
+          .getOrElse(error("Bad platform " + quote(platform)))
+
+      val platform_dir = component_dir.path + platform_info.path
+      if (platform_dir.is_dir && !force) {
+        progress.echo_warning("Platform " + platform + " already installed")
+      }
+      else {
+        progress.echo("Platform " + platform + " ...")
+        progress.expose_interrupt()
+
+        Isabelle_System.make_directory(platform_dir)
+
+        val xcaddy_dir = Isabelle_System.make_directory(tmp_dir + Path.explode("xcaddy"))
+        val xcaddy_download = platform_info.xcaddy_download(xcaddy_url, xcaddy_version)
+
+        val xcaddy_archive_name =
+          Url.get_base_name(xcaddy_download) getOrElse
+            error("Malformed download URL " + quote(xcaddy_download))
+        val xcaddy_archive_path = tmp_dir + Path.basic(xcaddy_archive_name)
+
+        Isabelle_System.download_file(xcaddy_download, xcaddy_archive_path)
+        Isabelle_System.extract(xcaddy_archive_path, xcaddy_dir)
+
+        progress.echo("Building caddy " + caddy_version)
+        progress.bash(
+          Library.make_lines(
+            "set -e",
+            "xcaddy/xcaddy build v" + Bash.string(caddy_version) +
+              Word.explode(caddy_modules).map(s => " --with " + Bash.string(s)).mkString,
+            "./caddy list-modules"),
+          cwd = tmp_dir, echo = progress.verbose).check
+
+        Isabelle_System.copy_file(tmp_dir + Path.explode("caddy").platform_exe, platform_dir)
+      }
+    }
+
+    File.find_files(component_dir.path.file, pred = file => File.is_exe(file.getName)).
+      foreach(file => File.set_executable(File.path(file)))
+
+
+    /* README */
+
+    File.write(component_dir.README,
+      """This installation of Caddy has been produced via "isabelle caddy_setup".
+
+
+        Makarius
+        """ + Date.Format.date(Date.now()) + "\n")
+  }
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool =
+    Isabelle_Tool("caddy_setup", "dynamic setup of Caddy component", Scala_Project.here,
+      { args =>
+        var target_dir = default_target_dir
+        var xcaddy_url = default_xcaddy_url
+        var xcaddy_version = default_xcaddy_version
+        var caddy_modules = default_caddy_modules
+        var caddy_version = default_caddy_version
+        var force = false
+        var verbose = false
+
+        val getopts = Getopts("""
+Usage: isabelle caddy_setup [OPTIONS]
+
+  Options are:
+    -D DIR       target directory (default ".")
+    -N MODULES   non-standard modules for caddy
+                 (default: ISABELLE_CADDY_SETUP_MODULES="""" + default_caddy_modules + """")
+    -U URL       download URL for xcaddy (default: """" + default_xcaddy_url + """")
+    -V VERSION   version for caddy
+                 (default: ISABELLE_CADDY_SETUP_VERSION="""" + default_caddy_version + """")
+    -W VERSION   version for xcaddy (default: """" + default_xcaddy_version + """")
+    -f           force fresh installation of specified platforms
+    -v           verbose
+
+  Build the Caddy webserver via xcaddy and configure it as Isabelle
+  component. See also https://github.com/caddyserver/xcaddy""",
+          "D:" -> (arg => target_dir = Path.explode(arg)),
+          "N:" -> (arg => caddy_modules = arg),
+          "U:" -> (arg => xcaddy_url = arg),
+          "V:" -> (arg => caddy_version = arg),
+          "W:" -> (arg => xcaddy_version = arg),
+          "f" -> (_ => force = true),
+          "v" -> (_ => verbose = true))
+
+        val more_args = getopts(args)
+        if (more_args.nonEmpty) getopts.usage()
+
+        val progress = new Console_Progress(verbose = verbose)
+
+        caddy_setup(caddy_version = caddy_version, caddy_modules = caddy_modules,
+          xcaddy_url = xcaddy_url, xcaddy_version = xcaddy_version, target_dir = target_dir,
+          progress = progress, force = force)
+      })
+}
+
+class Caddy_Setup extends Setup_Tool("caddy_setup", "ISABELLE_CADDY_SETUP") {
+  override val test_file: Path = Path.explode("lib/Tools/caddy")
+}
diff -r 76262e8b53f7 -r b7148ee355f6 src/Pure/Tools/dotnet_setup.scala
--- a/src/Pure/Tools/dotnet_setup.scala	Wed May 07 16:08:56 2025 +0200
+++ b/src/Pure/Tools/dotnet_setup.scala	Wed May 07 22:07:52 2025 +0200
@@ -36,10 +36,10 @@
   /* dotnet download and setup */
 
   def default_platform: String =
-    Isabelle_Platform.self.ISABELLE_PLATFORM(windows = true, apple = true)
+    Isabelle_Platform.local.ISABELLE_PLATFORM(windows = true, apple = true)
   def default_target_dir: Path = Components.default_components_base
   def default_install_url: String = "https://dot.net/v1/dotnet-install"
-  def default_version: String = Isabelle_System.getenv_strict("ISABELLE_DOTNET_VERSION")
+  def default_version: String = Isabelle_System.getenv_strict("ISABELLE_DOTNET_SETUP_VERSION")
 
   def dotnet_setup(
     platforms: List[String] = List(default_platform),
@@ -151,7 +151,7 @@
     -I URL       URL for install script without extension
                  (default: """ + quote(default_install_url) + """)
     -V VERSION   version: empty means "latest"
-                 (default: ISABELLE_DOTNET_VERSION=""" + quote(default_version) + """)
+                 (default: ISABELLE_DOTNET_SETUP_VERSION=""" + quote(default_version) + """)
     -f           force fresh installation of specified platforms
     -n           dry run: try download without installation
     -p PLATFORMS comma-separated list of platform specifications: "all" or
diff -r 76262e8b53f7 -r b7148ee355f6 src/Pure/Tools/go_setup.scala
--- a/src/Pure/Tools/go_setup.scala	Wed May 07 16:08:56 2025 +0200
+++ b/src/Pure/Tools/go_setup.scala	Wed May 07 22:07:52 2025 +0200
@@ -34,10 +34,10 @@
   /* Go download and setup */
 
   def default_platform: String =
-    Isabelle_Platform.self.ISABELLE_PLATFORM(windows = true, apple = true)
+    Isabelle_Platform.local.ISABELLE_PLATFORM(windows = true, apple = true)
   def default_target_dir: Path = Components.default_components_base
   val default_url = "https://go.dev/dl"
-  def default_version: String = Isabelle_System.getenv_strict("ISABELLE_GO_VERSION")
+  def default_version: String = Isabelle_System.getenv_strict("ISABELLE_GO_SETUP_VERSION")
 
   def go_setup(
     platforms: List[String] = List(default_platform),
@@ -146,7 +146,7 @@
   Options are:
     -D DIR       target directory (default ".")
     -U URL       download URL (default: """" + default_url + """")
-    -V VERSION   version (default: """" + default_version + """")
+    -V VERSION   version (default: ISABELLE_GO_SETUP_VERSION=""" + quote(default_version) + """)
     -f           force fresh installation of specified platforms
     -p PLATFORMS comma-separated list of platform specifications: "all" or
                  as family or formal name (default: """ + quote(default_platform) + """)