build bash_process in Isabelle/Scala, with etc/platforms.prop to preserve all platform directories (e.g. for SSH upload);

--- a/Admin/bash_process/bash_process.c	Tue Mar 26 10:30:41 2024 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,121 +0,0 @@
-/*  Author:     Makarius
-
-Bash process with separate process group id.
-*/
-
-#include <signal.h>
-#include <stdio.h>
-#include <stdlib.h>
-#include <string.h>
-#include <sys/resource.h>
-#include <sys/time.h>
-#include <sys/types.h>
-#include <sys/wait.h>
-#include <time.h>
-#include <unistd.h>
-
-static void fail(const char *msg)
-{
-  fprintf(stderr, "%s\n", msg);
-  fflush(stderr);
-  exit(2);
-}
-
-static time_t now()
-{
-  struct timeval tv;
-  if (gettimeofday(&tv, NULL) == 0) {
-    return tv.tv_sec * 1000 + tv.tv_usec / 1000;
-  }
-  else {
-    return time(NULL) * 1000;
-  }
-}
-
-
-int main(int argc, char *argv[])
-{
-  /* args */
-
-  if (argc < 2) {
-    fprintf(stderr, "Bad arguments: missing TIMING_FILE\n");
-    fflush(stderr);
-    exit(1);
-  }
-  char *timing_name = argv[1];
-
-
-  /* potential fork */
-
-  time_t time_start = now();
-
-  if (strlen(timing_name) > 0 || setsid() == -1) {
-    pid_t pid = fork();
-
-    if (pid == -1) fail("Cannot set session id (failed to fork)");
-    else if (pid != 0) {
-      int status;
-
-      // ingore SIGINT
-      struct sigaction sa;
-      memset(&sa, 0, sizeof(sa));
-      sa.sa_handler = SIG_IGN;
-      sigaction(SIGINT, &sa, 0);
-
-      if (waitpid(pid, &status, 0) == -1) {
-        fail("Cannot join forked process");
-      }
-
-      /* report timing */
-
-      if (strlen(timing_name) > 0) {
-        long long timing_elapsed = now() - time_start;
-
-        struct rusage ru;
-        getrusage(RUSAGE_CHILDREN, &ru);
-
-        long long timing_cpu =
-          ru.ru_utime.tv_sec * 1000 + ru.ru_utime.tv_usec / 1000 +
-          ru.ru_stime.tv_sec * 1000 + ru.ru_stime.tv_usec / 1000;
-
-        FILE *timing_file = fopen(timing_name, "w");
-        if (timing_file == NULL) fail("Cannot open timing file");
-        fprintf(timing_file, "%lld %lld", timing_elapsed, timing_cpu);
-        fclose(timing_file);
-      }
-
-      if (WIFEXITED(status)) {
-        exit(WEXITSTATUS(status));
-      }
-      else if (WIFSIGNALED(status)) {
-        exit(128 + WTERMSIG(status));
-      }
-      else {
-        fail("Unknown status of forked process");
-      }
-    }
-    else if (setsid() == -1) fail("Cannot set session id (after fork)");
-  }
-
-
-  /* report pid */
-
-  fprintf(stdout, "%d\n", getpid());
-  fflush(stdout);
-
-
-  /* shift command line */
-
-  int i;
-  for (i = 2; i < argc; i++) {
-    argv[i - 2] = argv[i];
-  }
-  argv[argc - 2] = NULL;
-  argv[argc - 1] = NULL;
-
-
-  /* exec */
-
-  execvp("bash", argv);
-  fail("Cannot exec process");
-}

--- a/Admin/bash_process/build	Tue Mar 26 10:30:41 2024 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,55 +0,0 @@
-#!/usr/bin/env bash
-#
-# Multi-platform build script
-
-unset CDPATH
-THIS="$(cd "$(dirname "$0")"; pwd)"
-PRG="$(basename "$0")"
-
-
-# diagnostics
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG PLATFORM"
-  echo
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-# command line args
-
-[ "$#" -eq 0 ] && usage
-PLATFORM="$1"; shift
-
-[ "$#" -eq 0 ] || usage
-
-
-# main
-
-PLATFORM_DIR="platform_${PLATFORM}"
-
-case "$PLATFORM" in
-  arm64-linux | arm64-darwin)
-    mkdir -p "$PLATFORM_DIR"
-    cc -Wall bash_process.c -o "$PLATFORM_DIR/bash_process"
-    ;;
-  x86_64-linux | x86_64-darwin)
-    mkdir -p "$PLATFORM_DIR"
-    cc -Wall -m64 bash_process.c -o "$PLATFORM_DIR/bash_process"
-    ;;
-  x86_64-cygwin)
-    mkdir -p "$PLATFORM_DIR"
-    cc -Wall bash_process.c -o "$PLATFORM_DIR/bash_process.exe"
-    ;;
-  *)
-    fail "Bad target platform: \"$PLATFORM\""
-    ;;
-esac

--- a/Admin/bash_process/etc/settings	Tue Mar 26 10:30:41 2024 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-ISABELLE_BASH_PROCESS_HOME="$COMPONENT"
-ISABELLE_BASH_PROCESS="$ISABELLE_BASH_PROCESS_HOME/platform_${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}/bash_process"

--- a/etc/build.props	Tue Mar 26 10:30:41 2024 +0100
+++ b/etc/build.props	Tue Mar 26 11:15:48 2024 +0100
@@ -18,6 +18,7 @@
   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 \

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/component_bash_process.scala	Tue Mar 26 11:15:48 2024 +0100
@@ -0,0 +1,226 @@
+/*  Title:      Pure/Admin/component_bash_process.scala
+    Author:     Makarius
+
+Build bash_process component from C source.
+*/
+
+package isabelle
+
+
+object Component_Bash_Process {
+  /* build bash_process */
+
+  def build_bash_process(
+    progress: Progress = new Progress,
+    target_dir: Path = Path.current,
+  ): Unit = {
+    Isabelle_System.require_command("cc")
+
+
+    /* component */
+
+    val component_date = Date.Format.alt_date(Date.now())
+    val component_name = "bash_process-" + component_date
+    val component_dir =
+      Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
+
+
+    /* platform */
+
+    val platform_name =
+      proper_string(Isabelle_System.getenv("ISABELLE_APPLE_PLATFORM64")) orElse
+      proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse
+      error("Missing ISABELLE_PLATFORM64")
+
+    val platform_dir =
+      Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
+
+
+    /* source */
+
+    val source_file = Path.explode("bash_process.c")
+    File.write(component_dir.path + source_file,
+"""/*  Author:     Makarius
+    License:    Isabelle BSD-3
+
+Bash process with separate process group id.
+*/
+
+#include <signal.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <sys/resource.h>
+#include <sys/time.h>
+#include <sys/types.h>
+#include <sys/wait.h>
+#include <time.h>
+#include <unistd.h>
+
+static void fail(const char *msg)
+{
+  fprintf(stderr, "%s\n", msg);
+  fflush(stderr);
+  exit(2);
+}
+
+static time_t now()
+{
+  struct timeval tv;
+  if (gettimeofday(&tv, NULL) == 0) {
+    return tv.tv_sec * 1000 + tv.tv_usec / 1000;
+  }
+  else {
+    return time(NULL) * 1000;
+  }
+}
+
+
+int main(int argc, char *argv[])
+{
+  /* args */
+
+  if (argc < 2) {
+    fprintf(stderr, "Bad arguments: missing TIMING_FILE\n");
+    fflush(stderr);
+    exit(1);
+  }
+  char *timing_name = argv[1];
+
+
+  /* potential fork */
+
+  time_t time_start = now();
+
+  if (strlen(timing_name) > 0 || setsid() == -1) {
+    pid_t pid = fork();
+
+    if (pid == -1) fail("Cannot set session id (failed to fork)");
+    else if (pid != 0) {
+      int status;
+
+      // ingore SIGINT
+      struct sigaction sa;
+      memset(&sa, 0, sizeof(sa));
+      sa.sa_handler = SIG_IGN;
+      sigaction(SIGINT, &sa, 0);
+
+      if (waitpid(pid, &status, 0) == -1) {
+        fail("Cannot join forked process");
+      }
+
+      /* report timing */
+
+      if (strlen(timing_name) > 0) {
+        long long timing_elapsed = now() - time_start;
+
+        struct rusage ru;
+        getrusage(RUSAGE_CHILDREN, &ru);
+
+        long long timing_cpu =
+          ru.ru_utime.tv_sec * 1000 + ru.ru_utime.tv_usec / 1000 +
+          ru.ru_stime.tv_sec * 1000 + ru.ru_stime.tv_usec / 1000;
+
+        FILE *timing_file = fopen(timing_name, "w");
+        if (timing_file == NULL) fail("Cannot open timing file");
+        fprintf(timing_file, "%lld %lld", timing_elapsed, timing_cpu);
+        fclose(timing_file);
+      }
+
+      if (WIFEXITED(status)) {
+        exit(WEXITSTATUS(status));
+      }
+      else if (WIFSIGNALED(status)) {
+        exit(128 + WTERMSIG(status));
+      }
+      else {
+        fail("Unknown status of forked process");
+      }
+    }
+    else if (setsid() == -1) fail("Cannot set session id (after fork)");
+  }
+
+
+  /* report pid */
+
+  fprintf(stdout, "%d\n", getpid());
+  fflush(stdout);
+
+
+  /* shift command line */
+
+  int i;
+  for (i = 2; i < argc; i++) {
+    argv[i - 2] = argv[i];
+  }
+  argv[argc - 2] = NULL;
+  argv[argc - 1] = NULL;
+
+
+  /* exec */
+
+  execvp("bash", argv);
+  fail("Cannot exec process");
+}
+""")
+
+
+    /* build */
+
+    progress.echo("Building bash_process for " + platform_name + " ...")
+    progress.bash("cc ../bash_process.c -o bash_process", cwd = platform_dir.file).check
+
+
+    /* settings */
+
+    component_dir.write_settings("""
+ISABELLE_BASH_PROCESS_HOME="$COMPONENT"
+ISABELLE_BASH_PROCESS="$ISABELLE_BASH_PROCESS_HOME/${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}/bash_process"
+""")
+
+
+    /* platform.props */
+
+    File.write(component_dir.platform_props,
+      Platform.Family.list.map(family => family.toString + " = ").mkString("", "\n", "\n"))
+
+
+    /* README */
+
+    File.write(component_dir.README,
+"""The bash_process executable has been built like this:
+
+  cc -Wall bash_process.c -o bash_process
+
+
+        Makarius
+        """ + Date.Format.date(Date.now()) + "\n")
+}
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool =
+    Isabelle_Tool("component_bash_process", "build bash_process component from C source",
+      Scala_Project.here,
+      { args =>
+        var target_dir = Path.current
+
+        val getopts = Getopts("""
+Usage: isabelle component_bash_process [OPTIONS]
+
+  Options are:
+    -D DIR       target directory (default ".")
+
+  Build prover component from official download.
+""",
+          "D:" -> (arg => target_dir = Path.explode(arg)))
+
+        val more_args = getopts(args)
+        if (more_args.nonEmpty) getopts.usage()
+
+        val progress = new Console_Progress()
+
+        build_bash_process(progress = progress, target_dir = target_dir)
+      })
+}

--- a/src/Pure/System/isabelle_tool.scala	Tue Mar 26 10:30:41 2024 +0100
+++ b/src/Pure/System/isabelle_tool.scala	Tue Mar 26 11:15:48 2024 +0100
@@ -166,6 +166,7 @@
   Build_Log.isabelle_tool,
   Build_Status.isabelle_tool,
   Check_Sources.isabelle_tool,
+  Component_Bash_Process.isabelle_tool,
   Component_CSDP.isabelle_tool,
   Component_CVC5.isabelle_tool,
   Component_Cygwin.isabelle_tool,