diff --git a/etc/build.props b/etc/build.props
--- a/etc/build.props
+++ b/etc/build.props
@@ -1,353 +1,355 @@
 title = Isabelle/Scala
 module = $ISABELLE_HOME/lib/classes/isabelle.jar
 main = isabelle.jedit.JEdit_Main
 resources = \
   lib/services/java.nio.charset.spi.CharsetProvider:META-INF/services/ \
   lib/logo/isabelle_transparent-32.gif:isabelle/ \
   lib/logo/isabelle_transparent.gif:isabelle/
 sources = \
   src/HOL/SPARK/Tools/spark.scala \
   src/HOL/Tools/ATP/system_on_tptp.scala \
   src/HOL/Tools/Mirabelle/mirabelle.scala \
   src/HOL/Tools/Nitpick/kodkod.scala \
   src/Pure/Admin/afp.scala \
   src/Pure/Admin/build_doc.scala \
   src/Pure/Admin/build_history.scala \
   src/Pure/Admin/build_log.scala \
   src/Pure/Admin/build_release.scala \
   src/Pure/Admin/build_status.scala \
   src/Pure/Admin/check_sources.scala \
   src/Pure/Admin/ci_build.scala \
   src/Pure/Admin/component_bash_process.scala \
   src/Pure/Admin/component_csdp.scala \
   src/Pure/Admin/component_cvc5.scala \
   src/Pure/Admin/component_cygwin.scala \
   src/Pure/Admin/component_e.scala \
   src/Pure/Admin/component_easychair.scala \
   src/Pure/Admin/component_eptcs.scala \
   src/Pure/Admin/component_foiltex.scala \
   src/Pure/Admin/component_fonts.scala \
   src/Pure/Admin/component_hugo.scala \
   src/Pure/Admin/component_javamail.scala \
   src/Pure/Admin/component_jdk.scala \
   src/Pure/Admin/component_jedit.scala \
   src/Pure/Admin/component_jsoup.scala \
   src/Pure/Admin/component_lipics.scala \
   src/Pure/Admin/component_llncs.scala \
   src/Pure/Admin/component_minisat.scala \
   src/Pure/Admin/component_mlton.scala \
   src/Pure/Admin/component_pdfjs.scala \
   src/Pure/Admin/component_polyml.scala \
   src/Pure/Admin/component_postgresql.scala \
   src/Pure/Admin/component_prismjs.scala \
   src/Pure/Admin/component_rsync.scala \
   src/Pure/Admin/component_scala.scala \
   src/Pure/Admin/component_spass.scala \
   src/Pure/Admin/component_sqlite.scala \
   src/Pure/Admin/component_stack.scala \
   src/Pure/Admin/component_windows_app.scala \
   src/Pure/Admin/component_vampire.scala \
   src/Pure/Admin/component_verit.scala \
   src/Pure/Admin/component_zipperposition.scala \
   src/Pure/Admin/component_zstd.scala \
   src/Pure/Admin/isabelle_cronjob.scala \
   src/Pure/Build/browser_info.scala \
   src/Pure/Build/build.scala \
   src/Pure/Build/build_benchmark.scala \
   src/Pure/Build/build_cluster.scala \
   src/Pure/Build/build_job.scala \
   src/Pure/Build/build_process.scala \
   src/Pure/Build/build_schedule.scala \
   src/Pure/Build/database_progress.scala \
   src/Pure/Build/export.scala \
   src/Pure/Build/export_theory.scala \
   src/Pure/Build/file_format.scala \
   src/Pure/Build/resources.scala \
   src/Pure/Build/sessions.scala \
   src/Pure/Build/store.scala \
   src/Pure/Concurrent/consumer_thread.scala \
   src/Pure/Concurrent/counter.scala \
   src/Pure/Concurrent/delay.scala \
   src/Pure/Concurrent/event_timer.scala \
   src/Pure/Concurrent/future.scala \
   src/Pure/Concurrent/isabelle_thread.scala \
   src/Pure/Concurrent/mailbox.scala \
   src/Pure/Concurrent/multithreading.scala \
   src/Pure/Concurrent/par_list.scala \
   src/Pure/Concurrent/synchronized.scala \
   src/Pure/GUI/color_value.scala \
   src/Pure/GUI/desktop_app.scala \
   src/Pure/GUI/gui.scala \
   src/Pure/GUI/gui_thread.scala \
   src/Pure/GUI/popup.scala \
   src/Pure/GUI/wrap_panel.scala \
   src/Pure/General/antiquote.scala \
   src/Pure/General/base64.scala \
   src/Pure/General/bibtex.scala \
   src/Pure/General/bytes.scala \
   src/Pure/General/cache.scala \
   src/Pure/General/codepoint.scala \
   src/Pure/General/comment.scala \
   src/Pure/General/completion.scala \
   src/Pure/General/compress.scala \
   src/Pure/General/csv.scala \
   src/Pure/General/date.scala \
   src/Pure/General/exn.scala \
   src/Pure/General/file.scala \
   src/Pure/General/file_watcher.scala \
   src/Pure/General/graph.scala \
   src/Pure/General/graph_display.scala \
   src/Pure/General/graphics_file.scala \
   src/Pure/General/html.scala \
   src/Pure/General/http.scala \
   src/Pure/General/js.scala \
   src/Pure/General/json.scala \
   src/Pure/General/json_api.scala \
   src/Pure/General/latex.scala \
   src/Pure/General/linear_set.scala \
   src/Pure/General/logger.scala \
   src/Pure/General/long_name.scala \
   src/Pure/General/mail.scala \
   src/Pure/General/mailman.scala \
   src/Pure/General/mercurial.scala \
   src/Pure/General/multi_map.scala \
   src/Pure/General/output.scala \
   src/Pure/General/path.scala \
   src/Pure/General/position.scala \
   src/Pure/General/pretty.scala \
   src/Pure/General/properties.scala \
   src/Pure/General/rdf.scala \
   src/Pure/General/rsync.scala \
   src/Pure/General/scan.scala \
   src/Pure/General/sha1.scala \
   src/Pure/General/space.scala \
   src/Pure/General/sql.scala \
   src/Pure/General/ssh.scala \
   src/Pure/General/symbol.scala \
   src/Pure/General/time.scala \
   src/Pure/General/timing.scala \
   src/Pure/General/toml.scala \
   src/Pure/General/untyped.scala \
   src/Pure/General/url.scala \
   src/Pure/General/utf8.scala \
   src/Pure/General/uuid.scala \
   src/Pure/General/value.scala \
   src/Pure/General/word.scala \
   src/Pure/General/zstd.scala \
   src/Pure/Isar/document_structure.scala \
   src/Pure/Isar/keyword.scala \
   src/Pure/Isar/line_structure.scala \
   src/Pure/Isar/outer_syntax.scala \
   src/Pure/Isar/parse.scala \
   src/Pure/Isar/token.scala \
   src/Pure/ML/ml_console.scala \
   src/Pure/ML/ml_heap.scala \
   src/Pure/ML/ml_lex.scala \
   src/Pure/ML/ml_process.scala \
   src/Pure/ML/ml_profiling.scala \
   src/Pure/ML/ml_statistics.scala \
   src/Pure/ML/ml_syntax.scala \
   src/Pure/PIDE/byte_message.scala \
   src/Pure/PIDE/command.scala \
   src/Pure/PIDE/command_span.scala \
   src/Pure/PIDE/document.scala \
   src/Pure/PIDE/document_editor.scala \
   src/Pure/PIDE/document_id.scala \
   src/Pure/PIDE/document_info.scala \
   src/Pure/PIDE/document_status.scala \
   src/Pure/PIDE/editor.scala \
   src/Pure/PIDE/headless.scala \
   src/Pure/PIDE/line.scala \
   src/Pure/PIDE/markup.scala \
   src/Pure/PIDE/markup_tree.scala \
   src/Pure/PIDE/protocol.scala \
   src/Pure/PIDE/protocol_handlers.scala \
   src/Pure/PIDE/protocol_message.scala \
   src/Pure/PIDE/prover.scala \
   src/Pure/PIDE/query_operation.scala \
   src/Pure/PIDE/rendering.scala \
   src/Pure/PIDE/session.scala \
   src/Pure/PIDE/text.scala \
   src/Pure/PIDE/xml.scala \
   src/Pure/PIDE/yxml.scala \
   src/Pure/ROOT.scala \
   src/Pure/System/bash.scala \
   src/Pure/System/classpath.scala \
   src/Pure/System/command_line.scala \
   src/Pure/System/components.scala \
   src/Pure/System/executable.scala \
   src/Pure/System/getopts.scala \
   src/Pure/System/host.scala \
   src/Pure/System/isabelle_charset.scala \
   src/Pure/System/isabelle_fonts.scala \
   src/Pure/System/isabelle_platform.scala \
   src/Pure/System/isabelle_process.scala \
   src/Pure/System/isabelle_system.scala \
   src/Pure/System/isabelle_tool.scala \
   src/Pure/System/java_statistics.scala \
   src/Pure/System/linux.scala \
   src/Pure/System/mingw.scala \
   src/Pure/System/nodejs.scala \
   src/Pure/System/options.scala \
   src/Pure/System/other_isabelle.scala \
   src/Pure/System/platform.scala \
   src/Pure/System/posix_interrupt.scala \
   src/Pure/System/process_result.scala \
   src/Pure/System/program_progress.scala \
   src/Pure/System/progress.scala \
   src/Pure/System/registry.scala \
   src/Pure/System/scala.scala \
   src/Pure/System/setup_tool.scala \
   src/Pure/System/system_channel.scala \
   src/Pure/System/tty_loop.scala \
   src/Pure/Thy/document_build.scala \
   src/Pure/Thy/thy_element.scala \
   src/Pure/Thy/thy_header.scala \
   src/Pure/Thy/thy_syntax.scala \
   src/Pure/Tools/check_keywords.scala \
   src/Pure/Tools/debugger.scala \
   src/Pure/Tools/doc.scala \
   src/Pure/Tools/docker_build.scala \
   src/Pure/Tools/dotnet_setup.scala \
   src/Pure/Tools/dump.scala \
   src/Pure/Tools/flarum.scala \
   src/Pure/Tools/fontforge.scala \
   src/Pure/Tools/go_setup.scala \
   src/Pure/Tools/java_monitor.scala \
   src/Pure/Tools/logo.scala \
   src/Pure/Tools/mkroot.scala \
   src/Pure/Tools/phabricator.scala \
   src/Pure/Tools/print_operation.scala \
   src/Pure/Tools/prismjs.scala \
   src/Pure/Tools/profiling.scala \
   src/Pure/Tools/profiling_report.scala \
   src/Pure/Tools/scala_build.scala \
   src/Pure/Tools/scala_project.scala \
   src/Pure/Tools/server.scala \
   src/Pure/Tools/server_commands.scala \
   src/Pure/Tools/simplifier_trace.scala \
   src/Pure/Tools/spell_checker.scala \
   src/Pure/Tools/sync.scala \
   src/Pure/Tools/task_statistics.scala \
   src/Pure/Tools/update.scala \
   src/Pure/Tools/update_cartouches.scala \
   src/Pure/Tools/update_comments.scala \
   src/Pure/Tools/update_header.scala \
   src/Pure/Tools/update_then.scala \
   src/Pure/Tools/update_theorems.scala \
   src/Pure/library.scala \
   src/Pure/pure_thy.scala \
   src/Pure/term.scala \
   src/Pure/term_xml.scala \
   src/Pure/thm_name.scala \
   src/Tools/Graphview/graph_file.scala \
   src/Tools/Graphview/graph_panel.scala \
   src/Tools/Graphview/graphview.scala \
   src/Tools/Graphview/layout.scala \
   src/Tools/Graphview/main_panel.scala \
   src/Tools/Graphview/metrics.scala \
   src/Tools/Graphview/model.scala \
   src/Tools/Graphview/mutator.scala \
   src/Tools/Graphview/mutator_dialog.scala \
   src/Tools/Graphview/mutator_event.scala \
   src/Tools/Graphview/popups.scala \
   src/Tools/Graphview/shapes.scala \
   src/Tools/Graphview/tree_panel.scala \
   src/Tools/VSCode/src/channel.scala \
   src/Tools/VSCode/src/component_vscode_extension.scala \
   src/Tools/VSCode/src/component_vscodium.scala \
   src/Tools/VSCode/src/dynamic_output.scala \
   src/Tools/VSCode/src/language_server.scala \
   src/Tools/VSCode/src/lsp.scala \
   src/Tools/VSCode/src/preview_panel.scala \
   src/Tools/VSCode/src/state_panel.scala \
   src/Tools/VSCode/src/vscode_main.scala \
   src/Tools/VSCode/src/vscode_model.scala \
   src/Tools/VSCode/src/vscode_rendering.scala \
   src/Tools/VSCode/src/vscode_resources.scala \
   src/Tools/VSCode/src/vscode_spell_checker.scala \
   src/Tools/jEdit/src/active.scala \
   src/Tools/jEdit/src/base_plugin.scala \
   src/Tools/jEdit/src/completion_popup.scala \
   src/Tools/jEdit/src/context_menu.scala \
   src/Tools/jEdit/src/debugger_dockable.scala \
   src/Tools/jEdit/src/dockable.scala \
   src/Tools/jEdit/src/document_dockable.scala \
   src/Tools/jEdit/src/document_model.scala \
   src/Tools/jEdit/src/document_view.scala \
   src/Tools/jEdit/src/documentation_dockable.scala \
   src/Tools/jEdit/src/fold_handling.scala \
   src/Tools/jEdit/src/font_info.scala \
   src/Tools/jEdit/src/graphview_dockable.scala \
   src/Tools/jEdit/src/info_dockable.scala \
   src/Tools/jEdit/src/isabelle.scala \
   src/Tools/jEdit/src/isabelle_encoding.scala \
   src/Tools/jEdit/src/isabelle_export.scala \
   src/Tools/jEdit/src/isabelle_session.scala \
   src/Tools/jEdit/src/isabelle_vfs.scala \
   src/Tools/jEdit/src/jedit_bibtex.scala \
   src/Tools/jEdit/src/jedit_editor.scala \
   src/Tools/jEdit/src/jedit_jar.scala \
   src/Tools/jEdit/src/jedit_lib.scala \
   src/Tools/jEdit/src/jedit_main.scala \
   src/Tools/jEdit/src/jedit_options.scala \
   src/Tools/jEdit/src/jedit_plugins.scala \
   src/Tools/jEdit/src/jedit_rendering.scala \
   src/Tools/jEdit/src/jedit_resources.scala \
   src/Tools/jEdit/src/jedit_sessions.scala \
   src/Tools/jEdit/src/jedit_spell_checker.scala \
   src/Tools/jEdit/src/keymap_merge.scala \
   src/Tools/jEdit/src/main_plugin.scala \
   src/Tools/jEdit/src/monitor_dockable.scala \
   src/Tools/jEdit/src/output_dockable.scala \
   src/Tools/jEdit/src/pide_docking_framework.scala \
   src/Tools/jEdit/src/pretty_text_area.scala \
   src/Tools/jEdit/src/pretty_tooltip.scala \
   src/Tools/jEdit/src/process_indicator.scala \
   src/Tools/jEdit/src/protocol_dockable.scala \
   src/Tools/jEdit/src/query_dockable.scala \
   src/Tools/jEdit/src/raw_output_dockable.scala \
   src/Tools/jEdit/src/rich_text_area.scala \
   src/Tools/jEdit/src/session_build.scala \
   src/Tools/jEdit/src/simplifier_trace_dockable.scala \
   src/Tools/jEdit/src/simplifier_trace_window.scala \
   src/Tools/jEdit/src/sledgehammer_dockable.scala \
   src/Tools/jEdit/src/state_dockable.scala \
   src/Tools/jEdit/src/status_widget.scala \
   src/Tools/jEdit/src/symbols_dockable.scala \
   src/Tools/jEdit/src/syntax_style.scala \
   src/Tools/jEdit/src/syslog_dockable.scala \
   src/Tools/jEdit/src/text_overview.scala \
   src/Tools/jEdit/src/text_structure.scala \
   src/Tools/jEdit/src/theories_dockable.scala \
   src/Tools/jEdit/src/theories_status.scala \
   src/Tools/jEdit/src/timing_dockable.scala \
   src/Tools/jEdit/src/token_markup.scala
 services = \
   isabelle.Bash$Handler \
   isabelle.Bibtex$File_Format \
   isabelle.Build$Engine$Default \
   isabelle.Build_Schedule$Build_Engine \
   isabelle.Document_Build$Build_Engine \
   isabelle.Document_Build$LIPIcs_LuaLaTeX_Engine \
   isabelle.Document_Build$LIPIcs_PDFLaTeX_Engine \
   isabelle.Document_Build$LuaLaTeX_Engine \
   isabelle.Document_Build$PDFLaTeX_Engine \
+  isabelle.Dotnet_Setup \
   isabelle.CI_Builds \
+  isabelle.Go_Setup \
   isabelle.GHC_Setup \
   isabelle.ML_Statistics$Handler \
   isabelle.OCaml_Setup \
   isabelle.Print_Operation$Handler \
   isabelle.Scala$Handler \
   isabelle.Scala_Functions \
   isabelle.Server_Commands \
   isabelle.Sessions$ROOTS_File_Format \
   isabelle.Simplifier_Trace$Handler \
   isabelle.Tools \
   isabelle.jedit.JEdit_Plugin0 \
   isabelle.jedit.JEdit_Plugin1 \
   isabelle.jedit.JEdit_JAR$Scala_Functions \
   isabelle.nitpick.Kodkod$Handler \
   isabelle.nitpick.Scala_Functions \
   isabelle.spark.SPARK$Load_Command1 \
   isabelle.spark.SPARK$Load_Command2
diff --git a/src/Pure/Tools/dotnet_setup.scala b/src/Pure/Tools/dotnet_setup.scala
--- a/src/Pure/Tools/dotnet_setup.scala
+++ b/src/Pure/Tools/dotnet_setup.scala
@@ -1,185 +1,189 @@
 /*  Title:      Pure/Tools/dotnet_setup.scala
     Author:     Makarius
 
 Dynamic setup of Dotnet component.
 */
 
 package isabelle
 
 
 object Dotnet_Setup {
   /* platforms */
 
   sealed case class Platform_Info(
     platform: String,
     os: String = "",
     arch: String = "x64",
     ext: String = "sh",
     exec: String = "bash",
     check: () => Unit = () => ()
   ) extends Platform.Info
 
   val all_platforms: List[Platform_Info] =
     List(
       Platform_Info("arm64-linux", os = "linux", arch = "arm64"),
       Platform_Info("x86_64-linux", os = "linux"),
       Platform_Info("arm64-darwin", os = "osx", arch = "arm64"),
       Platform_Info("x86_64-darwin", os = "osx"),
       Platform_Info("x86_64-windows",
         ext = "ps1",
         exec = "powershell -ExecutionPolicy ByPass",
         check = () => Isabelle_System.require_command("powershell", "-NoProfile -Command Out-Null")))
 
   def check_platform_spec(spec: String): String =
     Platform.check_spec(all_platforms, spec)
 
 
   /* dotnet download and setup */
 
   def default_platform: String =
     Isabelle_Platform.self.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 dotnet_setup(
     platforms: List[String] = List(default_platform),
     target_dir: Path = default_target_dir,
     install_url: String = default_install_url,
     version: String = default_version,
     force: Boolean = false,
     dry_run: Boolean = false,
     progress: Progress = new Progress
   ): Unit = {
     platforms.foreach(check_platform_spec)
 
 
     /* component directory */
 
     val component_dir =
       Components.Directory(
         target_dir + Path.explode(if (version.isEmpty) "dotnet-latest" else "dotnet-" + version))
 
     if (!dry_run) {
       progress.echo("Component directory " + component_dir)
       component_dir.create(permissive = true)
 
       component_dir.write_settings("""
 ISABELLE_DOTNET_ROOT="$COMPONENT"
 
 if [ -n "$ISABELLE_WINDOWS_PLATFORM64" -a -d "$ISABELLE_DOTNET_ROOT/$ISABELLE_WINDOWS_PLATFORM64" ]; then
   ISABELLE_DOTNET="$ISABELLE_DOTNET_ROOT/$ISABELLE_WINDOWS_PLATFORM64/dotnet.exe"
 elif [ -n "$ISABELLE_APPLE_PLATFORM64" -a -d "$ISABELLE_DOTNET_ROOT/$ISABELLE_APPLE_PLATFORM64" ]; then
   ISABELLE_DOTNET="$ISABELLE_DOTNET_ROOT/$ISABELLE_APPLE_PLATFORM64/dotnet"
 elif [ -d "$ISABELLE_DOTNET_ROOT/$ISABELLE_PLATFORM64" ]; then
   ISABELLE_DOTNET="$ISABELLE_DOTNET_ROOT/$ISABELLE_PLATFORM64/dotnet"
 fi
 
 DOTNET_CLI_TELEMETRY_OPTOUT="true"
 DOTNET_CLI_HOME="$(platform_path "$ISABELLE_HOME_USER/dotnet")"
 """)
 
       File.write(component_dir.README,
         """This installation of Dotnet has been produced via "isabelle dotnet_setup".
 
 
       Makarius
       """ + Date.Format.date(Date.now()) + "\n")
 
       for (old <- proper_string(Isabelle_System.getenv("ISABELLE_DOTNET_ROOT"))) {
         Components.update_components(false, Path.explode(old))
       }
 
       Components.update_components(true, component_dir.path)
     }
 
 
     /* platform directories */
 
     for (platform <- all_platforms if platforms.exists(platform.is)) {
       progress.expose_interrupt()
 
       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 + platform.path
         if (platform_dir.is_dir && !force) {
           progress.echo_warning("Platform " + platform + " already installed")
         }
         else {
           progress.echo("Platform " + platform + " ...")
           platform.check()
           if (platform_dir.is_dir && force) Isabelle_System.rm_tree(platform_dir)
           val script =
             platform.exec + " " + File.bash_platform_path(install) +
               if_proper(version, " -Version " + Bash.string(version)) +
               " -Architecture " + Bash.string(platform.arch) +
               if_proper(platform.os, " -OS " + Bash.string(platform.os)) +
               " -InstallDir " + File.bash_path(platform.path) +
               (if (dry_run) " -DryRun" else "") +
               " -NoPath"
           progress.bash(script, echo = progress.verbose,
             cwd = if (dry_run) null else component_dir.path.file).check
           for (exe <- File.find_files(platform_dir.file, pred = _.getName.endsWith(".exe"))) {
             File.set_executable(File.path(exe))
           }
         }
       }
     }
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
     Isabelle_Tool("dotnet_setup", "dynamic setup of Dotnet component (for Fsharp)",
       Scala_Project.here,
       { args =>
 
         var target_dir = default_target_dir
         var install_url = default_install_url
         var version = default_version
         var force = false
         var dry_run = false
         var platforms = List(default_platform)
         var verbose = false
 
         val getopts = Getopts("""
 Usage: isabelle dotnet_setup [OPTIONS]
 
   Options are:
     -D DIR       target directory (default: """ + default_target_dir.expand + """)
     -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) + """)
     -f           force fresh installation of specified platforms
     -n           dry run: try download without installation
     -p PLATFORMS comma-separated list of platform specifications,
                  as family or formal name (default: """ + quote(default_platform) + """)
     -v           verbose
 
   Download the Dotnet / Fsharp platform and configure it as Isabelle component.
 
   See also:
     https://fsharp.org
     https://learn.microsoft.com/en-us/dotnet/core/tools/dotnet-install-script
     https://learn.microsoft.com/en-us/dotnet/core/tools/telemetry
 """,
           "D:" -> (arg => target_dir = Path.explode(arg)),
           "I:" -> (arg => install_url = arg),
           "V:" -> (arg => version = arg),
           "f" -> (_ => force = true),
           "n" -> (_ => dry_run = true),
           "p:" -> (arg => platforms = space_explode(',', arg).map(check_platform_spec)),
           "v" -> (_ => verbose = true))
 
         val more_args = getopts(args)
         if (more_args.nonEmpty) getopts.usage()
 
         val progress = new Console_Progress(verbose = verbose)
 
         dotnet_setup(platforms = platforms, target_dir = target_dir, install_url = install_url,
           version = version, force = force, dry_run = dry_run, progress = progress)
       })
 }
+
+class Dotnet_Setup extends Setup_Tool("dotnet_setup", "ISABELLE_DOTNET_SETUP") {
+  override val test_file: Path = Path.explode("lib/Tools/dotnet")
+}
diff --git a/src/Pure/Tools/go_setup.scala b/src/Pure/Tools/go_setup.scala
--- a/src/Pure/Tools/go_setup.scala
+++ b/src/Pure/Tools/go_setup.scala
@@ -1,172 +1,176 @@
 /*  Title:      Pure/Tools/go_setup.scala
     Author:     Makarius
 
 Dynamic setup of Go component.
 */
 
 package isabelle
 
 
 object Go_Setup {
   /* platform information */
 
   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 (is_windows) ".zip" else ".tar.gz"
       Url.append_path(base_url, "go" + version + "." + go_platform.replace("_", "-") + ext)
     }
   }
 
   val all_platforms: List[Platform_Info] =
     List(
       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"))
 
   def check_platform_spec(spec: String): String =
     Platform.check_spec(all_platforms, spec)
 
 
   /* Go download and setup */
 
   def default_platform: String =
     Isabelle_Platform.self.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 go_setup(
     platforms: List[String] = List(default_platform),
     base_url: String = default_url,
     version: String = default_version,
     target_dir: Path = default_target_dir,
     progress: Progress = new Progress,
     force: Boolean = false
   ): Unit = {
     platforms.foreach(check_platform_spec)
 
 
     /* component directory */
 
     val component_dir =
       Components.Directory(target_dir + Path.basic("go-" + version)).create(permissive = true)
 
     progress.echo("Component directory " + component_dir)
 
     component_dir.write_settings("""
 ISABELLE_GOROOT="$COMPONENT"
 
 if [ -n "$ISABELLE_WINDOWS_PLATFORM64" -a -d "$ISABELLE_GOROOT/$ISABELLE_WINDOWS_PLATFORM64" ]; then
   ISABELLE_GOEXE="$ISABELLE_GOROOT/$ISABELLE_WINDOWS_PLATFORM64"
 elif [ -n "$ISABELLE_APPLE_PLATFORM64" -a -d "$ISABELLE_GOROOT/$ISABELLE_APPLE_PLATFORM64" ]; then
   ISABELLE_GOEXE="$ISABELLE_GOROOT/$ISABELLE_APPLE_PLATFORM64"
 elif [ -d "$ISABELLE_GOROOT/$ISABELLE_PLATFORM64" ]; then
   ISABELLE_GOEXE="$ISABELLE_GOROOT/$ISABELLE_PLATFORM64"
 fi
 """)
 
     File.write(component_dir.platform_props,
       (for ((a, b) <- all_platforms.groupBy(_.family_name).iterator)
         yield a + " = " + b.flatMap(_.paths).mkString(" ")
       ).mkString("", "\n", "\n"))
 
     for (old <- proper_string(Isabelle_System.getenv("ISABELLE_GOROOT"))) {
       Components.update_components(false, Path.explode(old))
     }
 
     Components.update_components(true, component_dir.path)
 
 
     /* download and setup */
 
     Isabelle_System.with_tmp_dir("download") { download_dir =>
       for (platform <- all_platforms if platforms.exists(platform.is)) {
         val platform_dir = component_dir.path + platform.path
         if (platform_dir.is_dir && !force) {
           progress.echo_warning("Platform " + platform + " already installed")
         }
         else {
           progress.echo("Platform " + platform + " ...")
           progress.expose_interrupt()
 
           if (force) {
             for (name <- platform.paths) {
               val dir = component_dir.path + Path.explode(name)
               if (dir.is_dir) Isabelle_System.rm_tree(dir)
             }
           }
 
           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)
           Isabelle_System.extract(archive_path, component_dir.path, strip = true)
           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)))
 
 
     /* README */
 
     File.write(component_dir.README,
       """This installation of Go has been produced via "isabelle go_setup".
 
 
         Makarius
         """ + Date.Format.date(Date.now()) + "\n")
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
     Isabelle_Tool("go_setup", "dynamic setup of Go component", Scala_Project.here,
       { args =>
         var target_dir = default_target_dir
         var base_url = default_url
         var version = default_version
         var force = false
         var platforms = List(default_platform)
 
         val getopts = Getopts("""
 Usage: isabelle go_setup [OPTIONS]
 
   Options are:
     -D DIR       target directory (default ".")
     -U URL       download URL (default: """" + default_url + """")
     -V VERSION   version (default: """" + default_version + """")
     -f           force fresh installation of specified platforms
     -p PLATFORMS comma-separated list of platform specifications,
                  as family or formal name (default: """ + quote(default_platform) + """)
 
   Download the Go development environment and configure it as Isabelle
   component. See also https://go.dev
 """,
           "D:" -> (arg => target_dir = Path.explode(arg)),
           "U:" -> (arg => base_url = arg),
           "V:" -> (arg => version = arg),
           "f" -> (_ => force = true),
           "p:" -> (arg => platforms = space_explode(',', arg).map(check_platform_spec)))
 
         val more_args = getopts(args)
         if (more_args.nonEmpty) getopts.usage()
 
         val progress = new Console_Progress()
 
         go_setup(platforms = platforms, base_url = base_url, version = version,
           target_dir = target_dir, progress = progress, force = force)
       })
 }
+
+class Go_Setup extends Setup_Tool("go_setup", "ISABELLE_GO_SETUP") {
+  override val test_file: Path = Path.explode("lib/Tools/go")
+}