universal component exec_process -- avoids special Admin/components/windows and might actually improve stability of forked processes (without using perl);
authorwenzelm
Wed, 19 Sep 2012 18:01:48 +0200
changeset 49447 bec1add86e79
parent 49446 b8d8f738bf63
child 49448 8a232a4e3fd8
universal component exec_process -- avoids special Admin/components/windows and might actually improve stability of forked processes (without using perl);
Admin/Windows/exec_process/build
Admin/Windows/exec_process/etc/settings
Admin/Windows/exec_process/exec_process.c
Admin/component_repository/components.sha1
Admin/components/main
Admin/components/windows
Admin/exec_process/build
Admin/exec_process/etc/settings
Admin/exec_process/exec_process.c
--- a/Admin/Windows/exec_process/build	Wed Sep 19 17:27:37 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-#!/usr/bin/env bash
-#
-# Multi-platform build script
-
-THIS="$(cd "$(dirname "$0")"; pwd)"
-PRG="$(basename "$0")"
-
-
-# diagnostics
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG TARGET"
-  echo
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-# command line args
-
-[ "$#" -eq 0 ] && usage
-TARGET="$1"; shift
-
-[ "$#" -eq 0 ] || usage
-
-
-# main
-
-mkdir -p "$TARGET"
-
-case "$TARGET" in
-  x86_64-linux | x86_64-darwin)
-    cc -m64 exec_process.c -o "$TARGET/exec_process"
-    ;;
-  x86-linux | x86-darwin)
-    cc -m32 exec_process.c -o "$TARGET/exec_process"
-    ;;
-  x86-cygwin)
-    cc exec_process.c -o "$TARGET/exec_process.exe"
-    ;;
-  *)
-    cc exec_process.c -o "$TARGET/exec_process"
-    ;;
-esac
-
-
--- a/Admin/Windows/exec_process/etc/settings	Wed Sep 19 17:27:37 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-EXEC_PROCESS="$COMPONENT/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}/exec_process"
--- a/Admin/Windows/exec_process/exec_process.c	Wed Sep 19 17:27:37 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,57 +0,0 @@
-/*  Author:     Makarius
-
-Bash process group invocation.
-*/
-
-#include <stdlib.h>
-#include <stdio.h>
-#include <sys/types.h>
-#include <unistd.h>
-
-
-static void fail(const char *msg)
-{
-  fprintf(stderr, "%s\n", msg);
-  exit(2);
-}
-
-
-int main(int argc, char *argv[])
-{
-  /* args */
-
-  if (argc != 3) {
-    fprintf(stderr, "Bad arguments\n");
-    exit(1);
-  }
-  char *pid_name = argv[1];
-  char *script = argv[2];
-
-
-  /* report pid */
-
-  FILE *pid_file;
-  pid_file = fopen(pid_name, "w");
-  if (pid_file == NULL) fail("Cannot open pid file");
-  fprintf(pid_file, "%d", getpid());
-  fclose(pid_file);
-
-
-  /* setsid */
-
-  if (getgid() == getpid()) fail("Cannot set session id");
-  setsid();
-
-
-  /* exec */
-
-  char *cmd_line[4];
-  cmd_line[0] = "/bin/bash";
-  cmd_line[1] = "-c";
-  cmd_line[2] = script;
-  cmd_line[3] = NULL;
-
-  execv("/bin/bash", cmd_line);
-  fail("Cannot exec process");
-}
-
--- a/Admin/component_repository/components.sha1	Wed Sep 19 17:27:37 2012 +0200
+++ b/Admin/component_repository/components.sha1	Wed Sep 19 18:01:48 2012 +0200
@@ -1,5 +1,6 @@
 2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7  cvc3-2.4.1.tar.gz
 0fe549949a025d65d52d6deca30554de8fca3b6e  e-1.5.tar.gz
+6d34b18ca0aa1e10bab6413045d079188c0e2dfb  exec_process-1.0.1.tar.gz
 ae7ee5becb26512f18c609e83b34612918bae5f0  exec_process-1.0.tar.gz
 683acd94761ef460cca1a628f650355370de5afb  hol-light-bundle-0.5-126.tar.gz
 8d83e433c1419e0c0cc5fd1762903d11b4a5752c  jdk-6u31.tar.gz
--- a/Admin/components/main	Wed Sep 19 17:27:37 2012 +0200
+++ b/Admin/components/main	Wed Sep 19 18:01:48 2012 +0200
@@ -1,6 +1,7 @@
 #main components for everyday use, without big impact on overall build time
 cvc3-2.4.1
 e-1.5
+exec_process-1.0.1
 jdk-7u6
 jedit_build-20120903
 kodkodi-1.2.16
--- a/Admin/components/windows	Wed Sep 19 17:27:37 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-#specific components for Windows/Cygwin only
-exec_process-1.0
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/exec_process/build	Wed Sep 19 18:01:48 2012 +0200
@@ -0,0 +1,53 @@
+#!/usr/bin/env bash
+#
+# Multi-platform build script
+
+THIS="$(cd "$(dirname "$0")"; pwd)"
+PRG="$(basename "$0")"
+
+
+# diagnostics
+
+function usage()
+{
+  echo
+  echo "Usage: $PRG TARGET"
+  echo
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+# command line args
+
+[ "$#" -eq 0 ] && usage
+TARGET="$1"; shift
+
+[ "$#" -eq 0 ] || usage
+
+
+# main
+
+mkdir -p "$TARGET"
+
+case "$TARGET" in
+  x86_64-linux | x86_64-darwin)
+    cc -m64 exec_process.c -o "$TARGET/exec_process"
+    ;;
+  x86-linux | x86-darwin)
+    cc -m32 exec_process.c -o "$TARGET/exec_process"
+    ;;
+  x86-cygwin)
+    cc exec_process.c -o "$TARGET/exec_process.exe"
+    ;;
+  *)
+    cc exec_process.c -o "$TARGET/exec_process"
+    ;;
+esac
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/exec_process/etc/settings	Wed Sep 19 18:01:48 2012 +0200
@@ -0,0 +1,3 @@
+# -*- shell-script -*- :mode=shellscript:
+
+EXEC_PROCESS="$COMPONENT/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/exec_process"
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/exec_process/exec_process.c	Wed Sep 19 18:01:48 2012 +0200
@@ -0,0 +1,57 @@
+/*  Author:     Makarius
+
+Bash process group invocation.
+*/
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <sys/types.h>
+#include <unistd.h>
+
+
+static void fail(const char *msg)
+{
+  fprintf(stderr, "%s\n", msg);
+  exit(2);
+}
+
+
+int main(int argc, char *argv[])
+{
+  /* args */
+
+  if (argc != 3) {
+    fprintf(stderr, "Bad arguments\n");
+    exit(1);
+  }
+  char *pid_name = argv[1];
+  char *script = argv[2];
+
+
+  /* report pid */
+
+  FILE *pid_file;
+  pid_file = fopen(pid_name, "w");
+  if (pid_file == NULL) fail("Cannot open pid file");
+  fprintf(pid_file, "%d", getpid());
+  fclose(pid_file);
+
+
+  /* setsid */
+
+  if (getgid() == getpid()) fail("Cannot set session id");
+  setsid();
+
+
+  /* exec */
+
+  char *cmd_line[4];
+  cmd_line[0] = "/bin/bash";
+  cmd_line[1] = "-c";
+  cmd_line[2] = script;
+  cmd_line[3] = NULL;
+
+  execv("/bin/bash", cmd_line);
+  fail("Cannot exec process");
+}
+