clarified name;
authorwenzelm
Sat Feb 13 17:27:23 2016 +0100 (2016-02-13)
changeset 6229372f6d6fd5853
parent 62292 486236dcd4d7
child 62294 30e9ff9be90a
clarified name;
Admin/bash_process/bash_process.c
Admin/bash_process/build
Admin/bash_process/etc/settings
Admin/exec_process/build
Admin/exec_process/etc/settings
Admin/exec_process/exec_process.c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/Admin/bash_process/bash_process.c	Sat Feb 13 17:27:23 2016 +0100
     1.3 @@ -0,0 +1,72 @@
     1.4 +/*  Author:     Makarius
     1.5 +
     1.6 +Bash process with separate process group id.
     1.7 +*/
     1.8 +
     1.9 +#include <stdlib.h>
    1.10 +#include <stdio.h>
    1.11 +#include <string.h>
    1.12 +#include <sys/types.h>
    1.13 +#include <unistd.h>
    1.14 +
    1.15 +
    1.16 +static void fail(const char *msg)
    1.17 +{
    1.18 +  fprintf(stderr, "%s\n", msg);
    1.19 +  fflush(stderr);
    1.20 +  exit(2);
    1.21 +}
    1.22 +
    1.23 +
    1.24 +int main(int argc, char *argv[])
    1.25 +{
    1.26 +  /* args */
    1.27 +
    1.28 +  if (argc < 2) {
    1.29 +    fprintf(stderr, "Bad arguments: missing pid file\n");
    1.30 +    fflush(stderr);
    1.31 +    exit(1);
    1.32 +  }
    1.33 +  char *pid_name = argv[1];
    1.34 +
    1.35 +
    1.36 +  /* setsid */
    1.37 +
    1.38 +  if (setsid() == -1) {
    1.39 +    pid_t pid = fork();
    1.40 +    if (pid == -1) fail("Cannot set session id (failed to fork)");
    1.41 +    else if (pid != 0) exit(0);
    1.42 +    else if (setsid() == -1) fail("Cannot set session id (after fork)");
    1.43 +  }
    1.44 +
    1.45 +
    1.46 +  /* report pid */
    1.47 +
    1.48 +  if (strcmp(pid_name, "-") == 0) {
    1.49 +    fprintf(stdout, "%d\n", getpid());
    1.50 +    fflush(stdout);
    1.51 +  }
    1.52 +  else if (strlen(pid_name) > 0) {
    1.53 +    FILE *pid_file;
    1.54 +    pid_file = fopen(pid_name, "w");
    1.55 +    if (pid_file == NULL) fail("Cannot open pid file");
    1.56 +    fprintf(pid_file, "%d", getpid());
    1.57 +    fclose(pid_file);
    1.58 +  }
    1.59 +
    1.60 +
    1.61 +  /* shift command line */
    1.62 +
    1.63 +  int i;
    1.64 +  for (i = 2; i < argc; i++) {
    1.65 +    argv[i - 2] = argv[i];
    1.66 +  }
    1.67 +  argv[argc - 2] = NULL;
    1.68 +  argv[argc - 1] = NULL;
    1.69 +
    1.70 +
    1.71 +  /* exec */
    1.72 +
    1.73 +  execvp("bash", argv);
    1.74 +  fail("Cannot exec process");
    1.75 +}
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/Admin/bash_process/build	Sat Feb 13 17:27:23 2016 +0100
     2.3 @@ -0,0 +1,51 @@
     2.4 +#!/usr/bin/env bash
     2.5 +#
     2.6 +# Multi-platform build script
     2.7 +
     2.8 +THIS="$(cd "$(dirname "$0")"; pwd)"
     2.9 +PRG="$(basename "$0")"
    2.10 +
    2.11 +
    2.12 +# diagnostics
    2.13 +
    2.14 +function usage()
    2.15 +{
    2.16 +  echo
    2.17 +  echo "Usage: $PRG TARGET"
    2.18 +  echo
    2.19 +  exit 1
    2.20 +}
    2.21 +
    2.22 +function fail()
    2.23 +{
    2.24 +  echo "$1" >&2
    2.25 +  exit 2
    2.26 +}
    2.27 +
    2.28 +
    2.29 +# command line args
    2.30 +
    2.31 +[ "$#" -eq 0 ] && usage
    2.32 +TARGET="$1"; shift
    2.33 +
    2.34 +[ "$#" -eq 0 ] || usage
    2.35 +
    2.36 +
    2.37 +# main
    2.38 +
    2.39 +mkdir -p "$TARGET"
    2.40 +
    2.41 +case "$TARGET" in
    2.42 +  x86_64-linux | x86_64-darwin)
    2.43 +    cc -m64 bash_process.c -o "$TARGET/bash_process"
    2.44 +    ;;
    2.45 +  x86-linux | x86-darwin)
    2.46 +    cc -m32 bash_process.c -o "$TARGET/bash_process"
    2.47 +    ;;
    2.48 +  x86-cygwin)
    2.49 +    cc bash_process.c -o "$TARGET/bash_process.exe"
    2.50 +    ;;
    2.51 +  *)
    2.52 +    cc bash_process.c -o "$TARGET/bash_process"
    2.53 +    ;;
    2.54 +esac
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/Admin/bash_process/etc/settings	Sat Feb 13 17:27:23 2016 +0100
     3.3 @@ -0,0 +1,3 @@
     3.4 +# -*- shell-script -*- :mode=shellscript:
     3.5 +
     3.6 +ISABELLE_BASH_PROCESS="$COMPONENT/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/bash_process"
     4.1 --- a/Admin/exec_process/build	Sat Feb 13 17:24:00 2016 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,53 +0,0 @@
     4.4 -#!/usr/bin/env bash
     4.5 -#
     4.6 -# Multi-platform build script
     4.7 -
     4.8 -THIS="$(cd "$(dirname "$0")"; pwd)"
     4.9 -PRG="$(basename "$0")"
    4.10 -
    4.11 -
    4.12 -# diagnostics
    4.13 -
    4.14 -function usage()
    4.15 -{
    4.16 -  echo
    4.17 -  echo "Usage: $PRG TARGET"
    4.18 -  echo
    4.19 -  exit 1
    4.20 -}
    4.21 -
    4.22 -function fail()
    4.23 -{
    4.24 -  echo "$1" >&2
    4.25 -  exit 2
    4.26 -}
    4.27 -
    4.28 -
    4.29 -# command line args
    4.30 -
    4.31 -[ "$#" -eq 0 ] && usage
    4.32 -TARGET="$1"; shift
    4.33 -
    4.34 -[ "$#" -eq 0 ] || usage
    4.35 -
    4.36 -
    4.37 -# main
    4.38 -
    4.39 -mkdir -p "$TARGET"
    4.40 -
    4.41 -case "$TARGET" in
    4.42 -  x86_64-linux | x86_64-darwin)
    4.43 -    cc -m64 exec_process.c -o "$TARGET/exec_process"
    4.44 -    ;;
    4.45 -  x86-linux | x86-darwin)
    4.46 -    cc -m32 exec_process.c -o "$TARGET/exec_process"
    4.47 -    ;;
    4.48 -  x86-cygwin)
    4.49 -    cc exec_process.c -o "$TARGET/exec_process.exe"
    4.50 -    ;;
    4.51 -  *)
    4.52 -    cc exec_process.c -o "$TARGET/exec_process"
    4.53 -    ;;
    4.54 -esac
    4.55 -
    4.56 -
     5.1 --- a/Admin/exec_process/etc/settings	Sat Feb 13 17:24:00 2016 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,3 +0,0 @@
     5.4 -# -*- shell-script -*- :mode=shellscript:
     5.5 -
     5.6 -EXEC_PROCESS="$COMPONENT/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/exec_process"
     6.1 --- a/Admin/exec_process/exec_process.c	Sat Feb 13 17:24:00 2016 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,72 +0,0 @@
     6.4 -/*  Author:     Makarius
     6.5 -
     6.6 -Bash process with separate process group id.
     6.7 -*/
     6.8 -
     6.9 -#include <stdlib.h>
    6.10 -#include <stdio.h>
    6.11 -#include <string.h>
    6.12 -#include <sys/types.h>
    6.13 -#include <unistd.h>
    6.14 -
    6.15 -
    6.16 -static void fail(const char *msg)
    6.17 -{
    6.18 -  fprintf(stderr, "%s\n", msg);
    6.19 -  fflush(stderr);
    6.20 -  exit(2);
    6.21 -}
    6.22 -
    6.23 -
    6.24 -int main(int argc, char *argv[])
    6.25 -{
    6.26 -  /* args */
    6.27 -
    6.28 -  if (argc < 2) {
    6.29 -    fprintf(stderr, "Bad arguments: missing pid file\n");
    6.30 -    fflush(stderr);
    6.31 -    exit(1);
    6.32 -  }
    6.33 -  char *pid_name = argv[1];
    6.34 -
    6.35 -
    6.36 -  /* setsid */
    6.37 -
    6.38 -  if (setsid() == -1) {
    6.39 -    pid_t pid = fork();
    6.40 -    if (pid == -1) fail("Cannot set session id (failed to fork)");
    6.41 -    else if (pid != 0) exit(0);
    6.42 -    else if (setsid() == -1) fail("Cannot set session id (after fork)");
    6.43 -  }
    6.44 -
    6.45 -
    6.46 -  /* report pid */
    6.47 -
    6.48 -  if (strcmp(pid_name, "-") == 0) {
    6.49 -    fprintf(stdout, "%d\n", getpid());
    6.50 -    fflush(stdout);
    6.51 -  }
    6.52 -  else if (strlen(pid_name) > 0) {
    6.53 -    FILE *pid_file;
    6.54 -    pid_file = fopen(pid_name, "w");
    6.55 -    if (pid_file == NULL) fail("Cannot open pid file");
    6.56 -    fprintf(pid_file, "%d", getpid());
    6.57 -    fclose(pid_file);
    6.58 -  }
    6.59 -
    6.60 -
    6.61 -  /* shift command line */
    6.62 -
    6.63 -  int i;
    6.64 -  for (i = 2; i < argc; i++) {
    6.65 -    argv[i - 2] = argv[i];
    6.66 -  }
    6.67 -  argv[argc - 2] = NULL;
    6.68 -  argv[argc - 1] = NULL;
    6.69 -
    6.70 -
    6.71 -  /* exec */
    6.72 -
    6.73 -  execvp("bash", argv);
    6.74 -  fail("Cannot exec process");
    6.75 -}