--- /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)
+ })
+}